PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-mitre.opb
MD5SUM	cb52c3dd346b4d656b5e715b686fba39
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	8401
Optimality of the best value was proved	NO
Number of terms in the objective function	9324
Biggest coefficient in the objective function	213
Number of bits for the biggest coefficient in the objective function	8
Sum of the numbers in the objective function	909647
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	1069
Number of bits of the biggest number in a constraint	11
Biggest sum of numbers in a constraint	909647
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.29
Number of variables	10724
Total number of constraints	12778
Number of constraints which are clauses	140
Number of constraints which are cardinality constraints (but not clauses)	12255
Number of constraints which are nor clauses,nor cardinality constraints	383
Minimum length of a constraint	1
Maximum length of a constraint	98
Trace number 18084

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 13:30:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18600 boxname=wulflinc20 idbench=1431 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  cb52c3dd346b4d656b5e715b686fba39  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-mitre.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-mitre.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-mitre.opb
IDLAUNCH: 18600
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        306436 kB
Buffers:         31276 kB
Cached:         672416 kB
SwapCached:        516 kB
Active:         175876 kB
Inactive:       529868 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        306184 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            16872 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:50:33 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 18600 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2045 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): .................................................................sssssssssssssssssssssss.ss.sss.s.sssssssssssssssssssssssssssssssssssssssssss.ssssss.sss.sssss.sssssssssss.ssss.ss...........................................................................
c ---[2147]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[2146]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[2145]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2134]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2123]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2112]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2104]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2103]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2102]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2101]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2100]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2099]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2098]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2097]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2096]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2095]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2094]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2093]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2092]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2091]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2090]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2089]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2088]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2087]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2086]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2085]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2084]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2083]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2082]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2081]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2080]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2079]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2078]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2077]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2076]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2075]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2074]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2073]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2072]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2071]---> Adder-cost: 36   maxlim: 16   bits: 5/5
c ---[2070]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[2069]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2068]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2067]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[2066]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2065]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2064]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2063]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2062]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2061]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2060]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2059]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2058]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2057]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2056]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2055]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2054]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2053]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2052]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2051]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2050]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2049]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2048]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2047]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2046]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2045]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2044]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2043]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2042]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2041]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2040]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2039]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[2038]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2037]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2036]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2035]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2034]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2033]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2032]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2031]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2030]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2029]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2028]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2027]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2026]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2025]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2024]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2023]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2022]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2021]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2020]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2019]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2018]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2017]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2016]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2015]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[2014]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2013]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2012]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2011]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[2010]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[1981]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1980]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1979]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1978]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1977]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1976]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1975]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1974]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1973]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1972]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1971]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1970]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1969]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1968]---> Adder-cost: 544   maxlim: 24180   bits: 16/15
c ---[1967]---> Adder-cost: 544   maxlim: 24195   bits: 16/15
c ---[1966]---> Adder-cost: 552   maxlim: 24196   bits: 16/15
c ---[1965]---> Adder-cost: 552   maxlim: 24211   bits: 16/15
c ---[1964]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1963]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1962]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1961]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1960]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1959]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1958]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1957]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1956]---> Adder-cost: 368   maxlim: 1615   bits: 12/11
c ---[1955]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1954]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1953]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1952]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1951]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1950]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1949]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1948]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1947]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1946]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1945]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1944]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1943]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1942]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1941]---> Adder-cost: 448   maxlim: 8068   bits: 14/13
c ---[1940]---> Adder-cost: 448   maxlim: 8073   bits: 14/13
c ---[1939]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1938]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1937]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1936]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1935]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1934]---> Adder-cost: 546   maxlim: 24195   bits: 16/15
c ---[1933]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1932]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1931]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1930]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1929]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1928]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1927]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1926]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1925]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1924]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1923]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1922]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1921]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1920]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1919]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1918]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1917]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[1916]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1915]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1914]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1913]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1912]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1911]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1910]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1909]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[1908]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1907]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[1906]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1905]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1904]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1903]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1902]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1901]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1900]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1899]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1898]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1897]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1896]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1895]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1894]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1893]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1892]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1891]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1890]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1889]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1888]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1887]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1886]---> Adder-cost: 368   maxlim: 1616   bits: 12/11
c ---[1885]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1884]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1883]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1882]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1881]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1880]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1879]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1878]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1877]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1876]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1875]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1874]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1873]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1872]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1871]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1870]---> Adder-cost: 462   maxlim: 8078   bits: 14/13
c ---[1869]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1868]---> Adder-cost: 462   maxlim: 8083   bits: 14/13
c ---[1867]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1866]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1865]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1864]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1863]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1862]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1861]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1860]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1859]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1858]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1857]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1856]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1855]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1854]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1853]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1852]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1851]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1850]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1849]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1848]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1847]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1846]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1845]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1844]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1843]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1842]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1841]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1840]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1839]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1838]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1837]---> Adder-cost: 536   maxlim: 24232   bits: 16/15
c ---[1836]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1835]---> Adder-cost: 536   maxlim: 24247   bits: 16/15
c ---[1834]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1833]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1832]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1831]---> Adder-cost: 424   maxlim: 4849   bits: 14/13
c ---[1830]---> Adder-cost: 424   maxlim: 4852   bits: 14/13
c ---[1829]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[1828]---> Adder-cost: 552   maxlim: 24205   bits: 16/15
c ---[1827]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[1826]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1825]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1824]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1823]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1822]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1821]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1820]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1819]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1818]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1817]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1816]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1815]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1814]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1813]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1812]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1811]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1810]---> Adder-cost: 448   maxlim: 8063   bits: 14/13
c ---[1809]---> Adder-cost: 448   maxlim: 8068   bits: 14/13
c ---[1808]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1807]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1806]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1805]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1804]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1803]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1802]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1801]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1800]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1799]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1798]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1797]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1796]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1795]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1794]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1793]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1792]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1791]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1790]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1789]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1788]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1787]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1786]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1785]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1784]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1783]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1782]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1781]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1780]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1779]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1778]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1777]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[1776]---> Adder-cost: 552   maxlim: 24205   bits: 16/15
c ---[1775]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[1774]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1773]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1772]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1771]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[1770]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1769]---> Adder-cost: 552   maxlim: 24205   bits: 16/15
c ---[1768]---> Adder-cost: 552   maxlim: 24190   bits: 16/15
c ---[1767]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1766]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1765]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1764]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1763]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1762]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1761]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1760]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1759]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1758]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1757]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1756]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1755]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1754]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1753]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1752]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1751]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1750]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1749]---> Adder-cost: 368   maxlim: 1615   bits: 12/11
c ---[1748]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1747]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1746]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1745]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1744]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1743]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1742]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1741]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1740]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1739]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1738]---> Adder-cost: 552   maxlim: 24211   bits: 16/15
c ---[1737]---> Adder-cost: 552   maxlim: 24196   bits: 16/15
c ---[1736]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1735]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1734]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1733]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1732]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1731]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1730]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1729]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1728]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1727]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1726]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1725]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1724]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1723]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1722]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1721]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1720]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1719]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1718]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1717]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1716]---> Adder-cost: 368   maxlim: 1613   bits: 12/11
c ---[1715]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1714]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1713]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1712]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1711]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1710]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1709]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1708]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1707]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1706]---> Adder-cost: 368   maxlim: 1614   bits: 12/11
c ---[1705]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1704]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1703]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1702]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1701]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1700]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1699]---> Adder-cost: 368   maxlim: 1612   bits: 12/11
c ---[1698]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1697]---> Adder-cost: 546   maxlim: 24195   bits: 16/15
c ---[1696]---> Adder-cost: 546   maxlim: 24195   bits: 16/15
c ---[1695]---> Adder-cost: 368   maxlim: 1610   bits: 12/11
c ---[1694]---> Adder-cost: 368   maxlim: 1611   bits: 12/11
c ---[1692]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1691]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1689]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1687]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1685]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1683]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1681]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1679]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1677]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1675]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1673]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1671]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1670]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1668]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1666]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1664]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1662]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1660]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1658]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1656]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1654]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1652]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1650]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1649]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1647]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1645]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1643]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1641]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1639]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1637]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1635]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1633]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1631]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1629]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1628]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1626]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1624]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1622]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1620]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1618]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1616]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1614]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1612]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1610]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1608]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1607]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1606]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1604]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1602]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1600]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1598]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1596]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1594]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1592]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1590]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1588]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1586]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1585]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1583]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1581]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1579]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1577]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1575]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1573]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1571]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1569]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1567]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1565]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1564]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1562]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1560]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1558]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1556]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1554]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1552]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1550]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1548]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1546]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1544]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1543]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1541]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1539]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1537]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1535]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1533]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1531]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1529]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1527]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1525]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1523]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1522]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1520]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1518]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1516]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1514]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1512]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1510]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1508]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1506]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1504]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1502]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1501]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1499]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1497]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1495]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1493]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1491]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1489]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1487]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1485]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1483]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1481]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1480]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1478]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1476]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1474]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1472]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1470]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1468]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1466]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1464]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1462]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1460]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1459]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1457]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1455]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1453]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1451]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1449]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1447]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1445]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1443]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1441]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1439]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1438]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1436]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1434]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1432]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1430]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1428]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1426]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1424]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1422]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1420]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1418]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1417]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1415]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1413]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1411]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1409]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1407]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1405]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1403]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1401]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1399]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1397]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1396]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1395]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1393]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1391]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1389]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1387]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1385]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1383]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1381]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1379]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1377]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1375]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1374]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1372]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1370]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1368]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1366]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1364]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1362]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1360]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1358]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1356]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1354]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1353]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1351]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1349]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1347]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1345]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1343]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1341]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1339]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1337]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1335]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1333]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1332]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1330]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1328]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1326]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1324]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1322]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1320]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1318]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1316]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1314]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1312]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1311]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1309]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1307]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1305]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1303]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1301]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1299]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1297]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1295]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1293]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1291]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1290]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1288]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1286]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1284]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1282]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1280]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1278]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1276]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1274]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1272]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1270]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1269]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1267]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1265]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1263]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1261]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1259]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1257]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1255]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1253]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1251]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1249]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1248]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1246]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1244]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1242]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1240]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1238]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1236]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1234]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1232]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1230]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1228]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1227]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1225]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1223]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1221]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1219]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1217]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1215]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1213]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1211]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1209]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1207]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1206]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1204]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1202]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1200]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1198]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1196]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1194]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1192]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1190]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1188]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1186]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1185]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[1184]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1182]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1180]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1178]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1176]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1174]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1172]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1170]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1168]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1166]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1164]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1163]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1161]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1159]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1157]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1155]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1153]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1151]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1149]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1147]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1145]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1143]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1142]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1140]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1138]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1136]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1134]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1132]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1130]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1128]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1126]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1124]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1122]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1121]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1119]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1117]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1115]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1113]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1111]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1109]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1107]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1105]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1103]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1101]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1100]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1098]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1096]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1094]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1092]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1090]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1088]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1086]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1084]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1082]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1080]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1079]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1077]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1075]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1073]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1071]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1069]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1067]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1065]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1063]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1061]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1059]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1058]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1056]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1054]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1052]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1050]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1048]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1046]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1044]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1042]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1040]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1038]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1037]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1035]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1033]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1031]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1029]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1027]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1025]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1023]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1021]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1019]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1017]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1016]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[1014]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1012]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1010]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1008]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1006]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1004]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1002]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[1000]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 998]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 996]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 995]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 993]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 991]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 989]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 987]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 985]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 983]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 981]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 979]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 977]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 975]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 974]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 973]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 971]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 969]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 967]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 965]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 963]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 961]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 959]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 957]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 955]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 953]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 952]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 950]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 948]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 946]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 944]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 942]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 940]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 938]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 936]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 934]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 932]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 931]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 929]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 927]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 925]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 923]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 921]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 919]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 917]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 915]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 913]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 911]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 910]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 908]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 906]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 904]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 902]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 900]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 898]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 896]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 894]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 892]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 890]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 889]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 887]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 885]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 876]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 865]---> Adder-cost: 16   maxlim: 7   bits: 4/3
c ---[ 854]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 843]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 832]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 821]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 820]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 819]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 808]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 797]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 786]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 775]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 764]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 758]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 757]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 756]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 755]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 754]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 753]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 752]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 751]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 750]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 749]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 748]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 747]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 746]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 745]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 744]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 743]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 742]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 741]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 740]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 739]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 738]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 737]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 736]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 735]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 734]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 733]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 732]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 731]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 730]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 729]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 728]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 727]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 726]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 725]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 724]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 723]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 722]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 721]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 720]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 719]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 718]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 717]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 716]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 715]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 714]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 713]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 712]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 711]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 710]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 709]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 708]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 707]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 706]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 705]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 704]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 703]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 702]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 701]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 700]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 699]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 698]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 697]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 696]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 695]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 694]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 693]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 692]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 691]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 690]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 689]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 688]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 687]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 686]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 685]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 684]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 683]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 682]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 681]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 680]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 679]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 678]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 677]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 676]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 675]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 674]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 673]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 672]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 671]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 670]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 669]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 668]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 667]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 666]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 665]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 664]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 663]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 662]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 661]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 660]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 659]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 658]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 657]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 656]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 655]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 654]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 653]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 652]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 651]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 650]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 649]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 648]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 647]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 646]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 645]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 644]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 643]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 642]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 641]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 640]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 639]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 638]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 637]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 636]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 635]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 634]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 633]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 632]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 631]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 630]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 629]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 628]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 627]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 626]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 625]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 624]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 623]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 622]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 621]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 620]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 619]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 618]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 617]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 616]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 615]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 614]---> Adder-cost: 15   maxlim: 3   bits: 3/2
c ---[ 613]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 612]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 611]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 605]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 594]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 583]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 579]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 578]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 577]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 576]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 575]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 574]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 573]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 572]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 571]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 570]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 569]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 568]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 567]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 566]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 565]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 564]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 563]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 562]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 561]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 560]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 559]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 558]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 557]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 556]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 555]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 554]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 553]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 552]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 551]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 550]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 549]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 548]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 547]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 546]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 545]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 544]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 543]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 542]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 541]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 540]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 539]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 538]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 537]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 536]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 535]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 534]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 533]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 532]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 531]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 530]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 529]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 528]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 527]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 526]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 525]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 524]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 523]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 522]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 521]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 520]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 519]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 518]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 517]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 516]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 515]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 514]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 513]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 512]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 511]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 510]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 509]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 508]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 507]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 506]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 505]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 504]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 503]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 502]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 501]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 500]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 499]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 498]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 497]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 496]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 495]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 494]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 493]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 492]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 491]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 490]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 489]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 488]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 487]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 486]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 485]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 484]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 483]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 482]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 481]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 480]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 479]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 478]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 477]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 476]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 475]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 474]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 473]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 472]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 471]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 470]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 469]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 468]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 467]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 466]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 465]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 464]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 463]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 462]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 461]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 460]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 459]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 458]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 457]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 456]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 455]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 454]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 453]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 452]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 451]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 450]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 449]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 448]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 447]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 446]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 445]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 444]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 443]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 442]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 441]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 440]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 439]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 438]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 437]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 436]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 435]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 434]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 433]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 432]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 431]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 430]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 429]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 428]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 427]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 426]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 425]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 424]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 423]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 422]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 421]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 420]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 419]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 418]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 417]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 416]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 415]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 414]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 413]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 412]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 411]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 410]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 409]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 408]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 407]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 406]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 405]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 404]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 403]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 402]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 401]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 400]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 399]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 398]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 397]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 396]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 395]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 394]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 393]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 392]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 391]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 390]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 389]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 388]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 387]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 386]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 385]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 384]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 383]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 382]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 381]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 380]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 379]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 378]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 377]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 376]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 375]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 374]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 373]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 372]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 371]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 370]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 369]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 368]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 367]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 366]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 365]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 364]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 363]---> Adder-cost: 14   maxlim: 5   bits: 4/3
c ---[ 362]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 361]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 360]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 359]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 358]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 357]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 356]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 355]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 354]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 353]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 352]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 351]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 350]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 349]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 348]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 347]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 346]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 345]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 344]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 343]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 342]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 341]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 340]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 339]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 338]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 337]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 336]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 335]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 334]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 333]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 332]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 331]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 330]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 329]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 328]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 327]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 326]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 325]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 324]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 323]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 322]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 321]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 320]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 319]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 318]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 317]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 316]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 315]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 314]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 313]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 312]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 311]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 310]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 309]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 308]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 307]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 306]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 305]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 304]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 303]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 302]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 301]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 300]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 299]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 298]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 297]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 296]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 295]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 294]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 293]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 292]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 291]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 290]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 289]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 288]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 287]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 286]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 285]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 284]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 283]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 282]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 281]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 280]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 279]---> Adder-cost: 20   maxlim: 8   bits: 4/4
c ---[ 278]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 277]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 276]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 275]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 274]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 273]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 272]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 271]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 270]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 269]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 268]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 267]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 266]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 265]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 264]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 263]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 262]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 261]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 260]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 259]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 258]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 257]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 256]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 255]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 254]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 253]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 252]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 251]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 250]---> Adder-cost: 5   maxlim: 1   bits: 2/1
c ---[ 221]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 220]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 219]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 218]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 217]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 216]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 215]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 214]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 213]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 212]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 211]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 210]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 209]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 208]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 207]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 206]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 205]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 204]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 203]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 202]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 201]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 200]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 199]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 198]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 197]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 196]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 195]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 194]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 193]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 192]---> Adder-cost: 22   maxlim: 11   bits: 4/4
c ---[ 191]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 190]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 189]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 188]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 187]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 186]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 185]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 184]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 183]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 182]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 181]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 180]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 179]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 178]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 177]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 176]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 175]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 174]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 173]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 172]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 171]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 170]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 169]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 168]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 167]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 166]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 165]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 164]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 163]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 162]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 161]---> Adder-cost: 8   maxlim: 3   bits: 3/2
c ---[ 160]---> Adder-cost: 190   maxlim: 87   bits: 7/7
c ---[ 159]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 158]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 157]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 156]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 155]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 154]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 153]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 152]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 151]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 150]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 149]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 148]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 147]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 146]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 145]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 144]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 143]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 142]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 141]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 140]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 139]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 138]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 137]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 136]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 135]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 134]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 133]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 132]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 131]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 130]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 129]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 128]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 127]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 126]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 125]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 124]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 123]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 113]---> Adder-cost: 30   maxlim: 13   bits: 5/4
c ---[ 102]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[ 101]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[ 100]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  99]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  98]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  97]---> Adder-cost: 23   maxlim: 48   bits: 7/6
c ---[  96]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  95]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  94]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  93]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  92]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[  91]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  90]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  89]---> Adder-cost: 117   maxlim: 62   bits: 7/6
c ---[  88]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  87]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  86]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  85]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[  84]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  83]---> Adder-cost: 23   maxlim: 48   bits: 7/6
c ---[  82]---> Adder-cost: 51   maxlim: 53   bits: 7/6
c ---[  81]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  80]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  79]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  78]---> Adder-cost: 76   maxlim: 57   bits: 7/6
c ---[  77]---> Adder-cost: 76   maxlim: 57   bits: 7/6
c ---[  76]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  75]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  74]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  73]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  72]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  71]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  70]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  69]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  68]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  67]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  66]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  65]---> Adder-cost: 94   maxlim: 59   bits: 7/6
c ---[  64]---> Adder-cost: 51   maxlim: 53   bits: 7/6
c ---[  63]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  62]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  61]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  60]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  59]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  58]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  57]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  56]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  55]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[  54]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  53]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  52]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  51]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  50]---> Adder-cost: 85   maxlim: 58   bits: 7/6
c ---[  49]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  48]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  47]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  46]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  45]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  44]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  43]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[  42]---> Adder-cost: 23   maxlim: 48   bits: 7/6
c ---[  41]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  40]---> Adder-cost: 118   maxlim: 63   bits: 7/6
c ---[  39]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[  38]---> Adder-cost: 117   maxlim: 62   bits: 7/6
c ---[  37]---> Adder-cost: 23   maxlim: 48   bits: 7/6
c ---[  36]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  35]---> Adder-cost: 94   maxlim: 59   bits: 7/6
c ---[  34]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  33]---> Adder-cost: 118   maxlim: 63   bits: 7/6
c ---[  32]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  31]---> Adder-cost: 30   maxlim: 49   bits: 7/6
c ---[  30]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  29]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  28]---> Adder-cost: 104   maxlim: 61   bits: 7/6
c ---[  27]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  26]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[  25]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  24]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[  23]---> Adder-cost: 76   maxlim: 57   bits: 7/6
c ---[  22]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  21]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  20]---> Adder-cost: 67   maxlim: 55   bits: 7/6
c ---[  19]---> Adder-cost: 46   maxlim: 52   bits: 7/6
c ---[  18]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  17]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  16]---> Adder-cost: 51   maxlim: 53   bits: 7/6
c ---[  15]---> Adder-cost: 20   maxlim: 47   bits: 7/6
c ---[  14]---> Adder-cost: 43   maxlim: 51   bits: 7/6
c ---[  13]---> Adder-cost: 9   maxlim: 45   bits: 7/6
c ---[  12]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[  11]---> Adder-cost: 15   maxlim: 46   bits: 7/6
c ---[  10]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[   9]---> Adder-cost: 85   maxlim: 58   bits: 7/6
c ---[   8]---> Adder-cost: 76   maxlim: 57   bits: 7/6
c ---[   7]---> Adder-cost: 51   maxlim: 53   bits: 7/6
c ---[   6]---> Adder-cost: 85   maxlim: 58   bits: 7/6
c ---[   5]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ---[   4]---> Adder-cost: 34   maxlim: 50   bits: 7/6
c ---[   3]---> Adder-cost: 74   maxlim: 56   bits: 7/6
c ---[   2]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[   1]---> Adder-cost: 103   maxlim: 60   bits: 7/6
c ---[   0]---> Adder-cost: 64   maxlim: 54   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  939742  3345077 |  313247       0        0     nan |  0.000 % |
c |       100 |  939742  3345077 |  344571     100      882     8.8 |  4.490 % |
c |       251 |  939735  3345054 |  379028     250     2114     8.5 |  4.491 % |
c |       477 |  939564  3344469 |  416931     457     3749     8.2 |  4.510 % |
c |       814 |  939551  3344428 |  458624     792     5681     7.2 |  4.511 % |
c |      1320 |  939189  3343198 |  504487    1260     9076     7.2 |  4.552 % |
c |      2081 |  939070  3342801 |  554936    2007    14144     7.0 |  4.566 % |
c |      3220 |  938211  3339804 |  610429    2996    24660     8.2 |  4.638 % |
c |      4928 |  936896  3335280 |  671472    4507    48790    10.8 |  4.756 % |
c |      7490 |  936688  3334554 |  738620    7035   112389    16.0 |  4.776 % |
c |     11334 |  936688  3334554 |  812482   10879   200195    18.4 |  4.776 % |
c |     17100 |  936672  3334502 |  893730   16641   348821    21.0 |  4.778 % |
c |     25749 |  934574  3327162 |  983103   24588   553369    22.5 |  4.937 % |
c |     38723 |  932159  3318732 | 1081413   37057   909252    24.5 |  5.143 % |
c |     58185 |  932153  3318714 | 1189554   56519  1430263    25.3 |  5.143 % |
c |     87378 |  928623  3306355 | 1308510   67968  1567214    23.1 |  5.411 % |
c |    131167 |  926017  3297165 | 1439361  100852  2250634    22.3 |  5.564 % |
c |    196851 |  920628  3278301 | 1583297  157978  3742273    23.7 |  6.017 % |
c |    295377 |  898646  3200703 | 1741627  234569  5493166    23.4 |  7.604 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.91 1/54 8079
Raw data (stat): 8079 (runsolver) R 8078 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545452848 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 17493 0 0 0 952 46 0 0 25 0 1 0 545452848 79278080 16760 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19355 16760 603 41 0 19314 0
vsize: 77420
[startup+20.0006 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 17586 0 0 0 1951 47 0 0 25 0 1 0 545452848 79683584 16853 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19454 16853 603 41 0 19413 0
vsize: 77816
[startup+30.0011 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 17627 0 0 0 2950 47 0 0 25 0 1 0 545452848 79831040 16894 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19490 16894 603 41 0 19449 0
vsize: 77960
[startup+40.0005 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 17664 0 0 0 3950 47 0 0 25 0 1 0 545452848 79966208 16931 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19523 16931 603 41 0 19482 0
vsize: 78092
[startup+50.0005 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 17704 0 0 0 4950 48 0 0 25 0 1 0 545452848 80232448 16971 4294967295 134512640 134672761 3221224544 3221223712 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19588 16971 603 41 0 19547 0
vsize: 78352
[startup+60.0005 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 17754 0 0 0 5950 48 0 0 25 0 1 0 545452848 80367616 17021 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19621 17021 603 41 0 19580 0
vsize: 78484
[startup+70.0007 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 18258 0 0 0 6948 50 0 0 25 0 1 0 545452848 82497536 17525 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20141 17525 603 41 0 20100 0
vsize: 80564
[startup+80.0017 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 18403 0 0 0 7947 50 0 0 25 0 1 0 545452848 83038208 17670 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20273 17670 603 41 0 20232 0
vsize: 81092
[startup+90.0014 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 18466 0 0 0 8947 50 0 0 25 0 1 0 545452848 83308544 17733 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20339 17733 603 41 0 20298 0
vsize: 81356
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 18519 0 0 0 9947 51 0 0 25 0 1 0 545452848 83578880 17786 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20405 17786 603 41 0 20364 0
vsize: 81620
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 18554 0 0 0 10947 51 0 0 25 0 1 0 545452848 83714048 17821 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20438 17821 603 41 0 20397 0
vsize: 81752
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 18608 0 0 0 11947 51 0 0 25 0 1 0 545452848 83849216 17875 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20471 17875 603 41 0 20430 0
vsize: 81884
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 18637 0 0 0 12947 51 0 0 25 0 1 0 545452848 83984384 17904 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20504 17904 603 41 0 20463 0
vsize: 82016
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 18647 0 0 0 13947 51 0 0 25 0 1 0 545452848 84119552 17914 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20537 17914 603 41 0 20496 0
vsize: 82148
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 19184 0 0 0 14946 53 0 0 25 0 1 0 545452848 86392832 18451 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21092 18451 603 41 0 21051 0
vsize: 84368
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 19628 0 0 0 15945 54 0 0 25 0 1 0 545452848 88227840 18895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21540 18895 603 41 0 21499 0
vsize: 86160
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 19900 0 0 0 16944 55 0 0 25 0 1 0 545452848 89354240 19167 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21815 19167 603 41 0 21774 0
vsize: 87260
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 19938 0 0 0 17944 55 0 0 25 0 1 0 545452848 89501696 19205 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21851 19205 603 41 0 21810 0
vsize: 87404
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 19938 0 0 0 18944 55 0 0 25 0 1 0 545452848 89501696 19205 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21851 19205 603 41 0 21810 0
vsize: 87404
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 19938 0 0 0 19944 55 0 0 25 0 1 0 545452848 89501696 19205 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21851 19205 603 41 0 21810 0
vsize: 87404
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 19938 0 0 0 20945 55 0 0 25 0 1 0 545452848 89501696 19205 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21851 19205 603 41 0 21810 0
vsize: 87404
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 19938 0 0 0 21945 55 0 0 25 0 1 0 545452848 89501696 19205 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21851 19205 603 41 0 21810 0
vsize: 87404
[startup+230.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 19938 0 0 0 22945 56 0 0 25 0 1 0 545452848 89501696 19205 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21851 19205 603 41 0 21810 0
vsize: 87404
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 19970 0 0 0 23945 56 0 0 25 0 1 0 545452848 89636864 19237 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21884 19237 603 41 0 21843 0
vsize: 87536
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 20382 0 0 0 24943 57 0 0 25 0 1 0 545452848 91512832 19649 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22342 19649 603 41 0 22301 0
vsize: 89368
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 20610 0 0 0 25942 58 0 0 25 0 1 0 545452848 92487680 19877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22580 19877 603 41 0 22539 0
vsize: 90320
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 20663 0 0 0 26942 58 0 0 25 0 1 0 545452848 92753920 19930 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22645 19930 603 41 0 22604 0
vsize: 90580
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 20724 0 0 0 27942 59 0 0 25 0 1 0 545452848 92901376 19991 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22681 19991 603 41 0 22640 0
vsize: 90724
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 20738 0 0 0 28942 59 0 0 25 0 1 0 545452848 93036544 20005 4294967295 134512640 134672761 3221224544 3221223680 134542710 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22714 20005 603 41 0 22673 0
vsize: 90856
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 20791 0 0 0 29942 60 0 0 25 0 1 0 545452848 93306880 20058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22780 20058 603 41 0 22739 0
vsize: 91120
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 20813 0 0 0 30942 60 0 0 25 0 1 0 545452848 93306880 20080 4294967295 134512640 134672761 3221224544 3221223728 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22780 20080 603 41 0 22739 0
vsize: 91120
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 21205 0 0 0 31941 61 0 0 25 0 1 0 545452848 94928896 20472 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23176 20472 603 41 0 23135 0
vsize: 92704
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 21511 0 0 0 32941 61 0 0 25 0 1 0 545452848 96133120 20778 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23470 20778 603 41 0 23429 0
vsize: 93880
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 21772 0 0 0 33940 62 0 0 25 0 1 0 545452848 97259520 21039 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23745 21039 603 41 0 23704 0
vsize: 94980
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 21882 0 0 0 34940 62 0 0 25 0 1 0 545452848 97673216 21149 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23846 21149 603 41 0 23805 0
vsize: 95384
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 21931 0 0 0 35940 62 0 0 25 0 1 0 545452848 97955840 21198 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23915 21198 603 41 0 23874 0
vsize: 95660
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 21949 0 0 0 36940 62 0 0 25 0 1 0 545452848 97955840 21216 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23915 21216 603 41 0 23874 0
vsize: 95660
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 22003 0 0 0 37940 62 0 0 25 0 1 0 545452848 98246656 21270 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23986 21270 603 41 0 23945 0
vsize: 95944
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 22013 0 0 0 38940 62 0 0 25 0 1 0 545452848 98246656 21280 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23986 21280 603 41 0 23945 0
vsize: 95944
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 22017 0 0 0 39940 63 0 0 25 0 1 0 545452848 98246656 21284 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23986 21284 603 41 0 23945 0
vsize: 95944
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 22073 0 0 0 40940 63 0 0 25 0 1 0 545452848 98512896 21340 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24051 21340 603 41 0 24010 0
vsize: 96204
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 22115 0 0 0 41940 63 0 0 25 0 1 0 545452848 98648064 21382 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24084 21382 603 41 0 24043 0
vsize: 96336
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 22644 0 0 0 42939 65 0 0 25 0 1 0 545452848 100806656 21911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24611 21911 603 41 0 24570 0
vsize: 98444
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 23045 0 0 0 43938 66 0 0 25 0 1 0 545452848 102961152 22312 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25137 22312 603 41 0 25096 0
vsize: 100548
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 23363 0 0 0 44937 67 0 0 25 0 1 0 545452848 104316928 22630 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25468 22630 603 41 0 25427 0
vsize: 101872
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 23487 0 0 0 45937 68 0 0 25 0 1 0 545452848 104861696 22754 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25601 22754 603 41 0 25560 0
vsize: 102404
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 23690 0 0 0 46936 68 0 0 25 0 1 0 545452848 105689088 22957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25803 22957 603 41 0 25762 0
vsize: 103212
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 23847 0 0 0 47936 69 0 0 25 0 1 0 545452848 106373120 23114 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25970 23114 603 41 0 25929 0
vsize: 103880
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 23878 0 0 0 48936 69 0 0 25 0 1 0 545452848 106520576 23145 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26006 23145 603 41 0 25965 0
vsize: 104024
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 23904 0 0 0 49935 69 0 0 25 0 1 0 545452848 106655744 23171 4294967295 134512640 134672761 3221224544 3221223648 134559824 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26039 23171 603 41 0 25998 0
vsize: 104156
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 23919 0 0 0 50935 69 0 0 25 0 1 0 545452848 106655744 23186 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26039 23186 603 41 0 25998 0
vsize: 104156
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 23930 0 0 0 51936 69 0 0 25 0 1 0 545452848 106655744 23197 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26039 23197 603 41 0 25998 0
vsize: 104156
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 24033 0 0 0 52935 70 0 0 25 0 1 0 545452848 107057152 23300 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26137 23300 603 41 0 26096 0
vsize: 104548
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 24220 0 0 0 53935 71 0 0 25 0 1 0 545452848 107859968 23487 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26333 23487 603 41 0 26292 0
vsize: 105332
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 24241 0 0 0 54935 71 0 0 25 0 1 0 545452848 108019712 23508 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26372 23508 603 41 0 26331 0
vsize: 105488
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 24252 0 0 0 55935 71 0 0 25 0 1 0 545452848 108019712 23519 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26372 23519 603 41 0 26331 0
vsize: 105488
[startup+570.009 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 24282 0 0 0 56935 71 0 0 25 0 1 0 545452848 108150784 23549 4294967295 134512640 134672761 3221224544 3221223716 134556609 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26404 23549 603 41 0 26363 0
vsize: 105616
[startup+580.01 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 24306 0 0 0 57935 71 0 0 25 0 1 0 545452848 108285952 23573 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26437 23573 603 41 0 26396 0
vsize: 105748
[startup+590.01 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 24716 0 0 0 58934 72 0 0 25 0 1 0 545452848 109895680 23983 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26830 23983 603 41 0 26789 0
vsize: 107320
[startup+600.01 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 24760 0 0 0 59934 73 0 0 25 0 1 0 545452848 110030848 24027 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26863 24027 603 41 0 26822 0
vsize: 107452
[startup+610.01 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25355 0 0 0 60932 75 0 0 25 0 1 0 545452848 112451584 24622 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27454 24622 603 41 0 27413 0
vsize: 109816
[startup+620.01 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25553 0 0 0 61931 75 0 0 25 0 1 0 545452848 113266688 24820 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27653 24820 603 41 0 27612 0
vsize: 110612
[startup+630.011 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25575 0 0 0 62931 76 0 0 25 0 1 0 545452848 113401856 24842 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27686 24842 603 41 0 27645 0
vsize: 110744
[startup+640.011 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25646 0 0 0 63931 76 0 0 25 0 1 0 545452848 113672192 24913 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27752 24913 603 41 0 27711 0
vsize: 111008
[startup+650.011 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25665 0 0 0 64931 76 0 0 25 0 1 0 545452848 113672192 24932 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27752 24932 603 41 0 27711 0
vsize: 111008
[startup+660.012 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25704 0 0 0 65931 76 0 0 25 0 1 0 545452848 113942528 24971 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27818 24971 603 41 0 27777 0
vsize: 111272
[startup+670.011 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25708 0 0 0 66932 76 0 0 25 0 1 0 545452848 113942528 24975 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27818 24975 603 41 0 27777 0
vsize: 111272
[startup+680.011 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25751 0 0 0 67931 76 0 0 25 0 1 0 545452848 114077696 25018 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27851 25018 603 41 0 27810 0
vsize: 111404
[startup+690.011 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25774 0 0 0 68931 77 0 0 25 0 1 0 545452848 114212864 25041 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27884 25041 603 41 0 27843 0
vsize: 111536
[startup+700.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25779 0 0 0 69931 77 0 0 25 0 1 0 545452848 114212864 25046 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27884 25046 603 41 0 27843 0
vsize: 111536
[startup+710.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25786 0 0 0 70931 77 0 0 25 0 1 0 545452848 114212864 25053 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27884 25053 603 41 0 27843 0
vsize: 111536
[startup+720.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25830 0 0 0 71931 77 0 0 25 0 1 0 545452848 114348032 25097 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27917 25097 603 41 0 27876 0
vsize: 111668
[startup+730.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25841 0 0 0 72931 77 0 0 25 0 1 0 545452848 114348032 25108 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27917 25108 603 41 0 27876 0
vsize: 111668
[startup+740.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25846 0 0 0 73931 77 0 0 25 0 1 0 545452848 114479104 25113 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27949 25113 603 41 0 27908 0
vsize: 111796
[startup+750.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25884 0 0 0 74931 78 0 0 25 0 1 0 545452848 114614272 25151 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27982 25151 603 41 0 27941 0
vsize: 111928
[startup+760.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25922 0 0 0 75931 78 0 0 25 0 1 0 545452848 114745344 25189 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28014 25189 603 41 0 27973 0
vsize: 112056
[startup+770.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25922 0 0 0 76931 78 0 0 25 0 1 0 545452848 114745344 25189 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28014 25189 603 41 0 27973 0
vsize: 112056
[startup+780.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25922 0 0 0 77931 78 0 0 25 0 1 0 545452848 114745344 25189 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28014 25189 603 41 0 27973 0
vsize: 112056
[startup+790.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25922 0 0 0 78932 78 0 0 25 0 1 0 545452848 114745344 25189 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28014 25189 603 41 0 27973 0
vsize: 112056
[startup+800.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25922 0 0 0 79932 78 0 0 25 0 1 0 545452848 114745344 25189 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28014 25189 603 41 0 27973 0
vsize: 112056
[startup+810.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25922 0 0 0 80932 78 0 0 25 0 1 0 545452848 114745344 25189 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28014 25189 603 41 0 27973 0
vsize: 112056
[startup+820.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25925 0 0 0 81932 79 0 0 25 0 1 0 545452848 114745344 25192 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28014 25192 603 41 0 27973 0
vsize: 112056
[startup+830.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25926 0 0 0 82932 79 0 0 25 0 1 0 545452848 114745344 25193 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28014 25193 603 41 0 27973 0
vsize: 112056
[startup+840.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25928 0 0 0 83932 79 0 0 25 0 1 0 545452848 114745344 25195 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28014 25195 603 41 0 27973 0
vsize: 112056
[startup+850.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25930 0 0 0 84932 79 0 0 25 0 1 0 545452848 114745344 25197 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28014 25197 603 41 0 27973 0
vsize: 112056
[startup+860.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25958 0 0 0 85932 79 0 0 25 0 1 0 545452848 114876416 25225 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28046 25225 603 41 0 28005 0
vsize: 112184
[startup+870.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25959 0 0 0 86932 79 0 0 25 0 1 0 545452848 114876416 25226 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28046 25226 603 41 0 28005 0
vsize: 112184
[startup+880.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25959 0 0 0 87932 79 0 0 25 0 1 0 545452848 114876416 25226 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28046 25226 603 41 0 28005 0
vsize: 112184
[startup+890.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25959 0 0 0 88932 79 0 0 25 0 1 0 545452848 114876416 25226 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28046 25226 603 41 0 28005 0
vsize: 112184
[startup+900.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25961 0 0 0 89932 80 0 0 25 0 1 0 545452848 114876416 25228 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28046 25228 603 41 0 28005 0
vsize: 112184
[startup+910.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 25966 0 0 0 90932 80 0 0 25 0 1 0 545452848 114876416 25233 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28046 25233 603 41 0 28005 0
vsize: 112184
[startup+920.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26334 0 0 0 91931 81 0 0 25 0 1 0 545452848 116346880 25601 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28405 25601 603 41 0 28364 0
vsize: 113620
[startup+930.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26575 0 0 0 92931 82 0 0 25 0 1 0 545452848 117321728 25842 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28643 25842 603 41 0 28602 0
vsize: 114572
[startup+940.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26699 0 0 0 93930 82 0 0 25 0 1 0 545452848 117870592 25966 4294967295 134512640 134672761 3221224544 3221223696 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28777 25966 603 41 0 28736 0
vsize: 115108
[startup+950.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26715 0 0 0 94929 83 0 0 25 0 1 0 545452848 117870592 25982 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28777 25982 603 41 0 28736 0
vsize: 115108
[startup+960.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26788 0 0 0 95929 83 0 0 25 0 1 0 545452848 118272000 26055 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28875 26055 603 41 0 28834 0
vsize: 115500
[startup+970.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26816 0 0 0 96929 84 0 0 25 0 1 0 545452848 118272000 26083 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28875 26083 603 41 0 28834 0
vsize: 115500
[startup+980.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26851 0 0 0 97929 84 0 0 25 0 1 0 545452848 118538240 26118 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28940 26118 603 41 0 28899 0
vsize: 115760
[startup+990.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26879 0 0 0 98929 84 0 0 25 0 1 0 545452848 118538240 26146 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28940 26146 603 41 0 28899 0
vsize: 115760
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26903 0 0 0 99929 84 0 0 25 0 1 0 545452848 118669312 26170 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28972 26170 603 41 0 28931 0
vsize: 115888
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26914 0 0 0 100929 84 0 0 25 0 1 0 545452848 118669312 26181 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28972 26181 603 41 0 28931 0
vsize: 115888
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26917 0 0 0 101929 84 0 0 25 0 1 0 545452848 118669312 26184 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28972 26184 603 41 0 28931 0
vsize: 115888
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26930 0 0 0 102929 84 0 0 25 0 1 0 545452848 118804480 26197 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29005 26197 603 41 0 28964 0
vsize: 116020
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26932 0 0 0 103929 84 0 0 25 0 1 0 545452848 118804480 26199 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29005 26199 603 41 0 28964 0
vsize: 116020
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26932 0 0 0 104930 84 0 0 25 0 1 0 545452848 118804480 26199 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29005 26199 603 41 0 28964 0
vsize: 116020
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26937 0 0 0 105930 84 0 0 25 0 1 0 545452848 118804480 26204 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29005 26204 603 41 0 28964 0
vsize: 116020
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26937 0 0 0 106930 84 0 0 25 0 1 0 545452848 118804480 26204 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29005 26204 603 41 0 28964 0
vsize: 116020
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 26963 0 0 0 107930 84 0 0 25 0 1 0 545452848 118935552 26230 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29037 26230 603 41 0 28996 0
vsize: 116148
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 27002 0 0 0 108930 84 0 0 25 0 1 0 545452848 119070720 26269 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29070 26269 603 41 0 29029 0
vsize: 116280
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 27026 0 0 0 109930 84 0 0 25 0 1 0 545452848 119205888 26293 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29103 26293 603 41 0 29062 0
vsize: 116412
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 27028 0 0 0 110930 84 0 0 25 0 1 0 545452848 119205888 26295 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29103 26295 603 41 0 29062 0
vsize: 116412
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 27037 0 0 0 111931 84 0 0 25 0 1 0 545452848 119205888 26304 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29103 26304 603 41 0 29062 0
vsize: 116412
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 27043 0 0 0 112931 84 0 0 25 0 1 0 545452848 119205888 26310 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29103 26310 603 41 0 29062 0
vsize: 116412
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 27450 0 0 0 113930 86 0 0 25 0 1 0 545452848 120819712 26717 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29497 26717 603 41 0 29456 0
vsize: 117988
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 27607 0 0 0 114929 86 0 0 25 0 1 0 545452848 121491456 26874 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29661 26874 603 41 0 29620 0
vsize: 118644
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 27615 0 0 0 115930 86 0 0 25 0 1 0 545452848 121491456 26882 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29661 26882 603 41 0 29620 0
vsize: 118644
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 27637 0 0 0 116930 86 0 0 25 0 1 0 545452848 121622528 26904 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29693 26904 603 41 0 29652 0
vsize: 118772
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 27683 0 0 0 117930 86 0 0 25 0 1 0 545452848 121757696 26950 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29726 26950 603 41 0 29685 0
vsize: 118904
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 27738 0 0 0 118930 86 0 0 25 0 1 0 545452848 123076608 27005 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30048 27005 603 41 0 30007 0
vsize: 120192
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 8079
Raw data (stat): 8079 (minisat+) R 8078 27565 27564 0 -1 0 27766 0 0 0 119930 87 0 0 25 0 1 0 545452848 123211776 27033 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30081 27033 603 41 0 30040 0
vsize: 120324
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.92 1/54 8079
Raw data (stat): 8079 (minisat+) Z 8078 27565 27564 0 -1 12 27768 0 0 0 119930 92 0 0 25 0 1 0 545452848 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.23
CPU user time (s): 1199.3
CPU system time (s): 0.921859
CPU usage (%): 100.013
Max. virtual memory (Kb): 120324
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####