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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-degen3.opb
MD5SUM	60f638829868e3a2820fb14a59c3225e
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	31460
Biggest coefficient in the objective function	977797120
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	331425197400
Number of bits of the sum of numbers in the objective function	39
Biggest number in a constraint	977797120
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	331425197400
Number of bits of the biggest sum of numbers	39
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.311952
Number of variables	36360
Total number of constraints	1503
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1503
Minimum length of a constraint	40
Maximum length of a constraint	4060
Trace number 16220

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 06:31:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15701 boxname=wulflinc28 idbench=1208 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  60f638829868e3a2820fb14a59c3225e  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-degen3.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-degen3.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-degen3.opb
IDLAUNCH: 15701
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        715132 kB
Buffers:         22808 kB
Cached:         269148 kB
SwapCached:        104 kB
Active:          64976 kB
Inactive:       229400 kB
HighTotal:      131008 kB
HighFree:         1064 kB
LowTotal:       903652 kB
LowFree:        714068 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            19472 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 06:51:37 (client local time) WITH STATUS 0 IN 1200.15 SECONDS
stats: 15701 7 1200.15 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2220 PB-constraints to clauses...
c   -- Unit propagations: ppp
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[2219]---> Adder-cost: 4174   maxlim: 1316290   bits: 21/21
c ---[2218]---> Adder-cost: 3858   maxlim: 621634   bits: 20/20
c ---[2217]---> Adder-cost: 3962   maxlim: 679235   bits: 20/20
c ---[2215]---> Adder-cost: 304   maxlim: 2550   bits: 13/12
c ---[2213]---> Adder-cost: 304   maxlim: 2550   bits: 13/12
c ---[2211]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2209]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2207]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2205]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2203]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2201]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2199]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2197]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2195]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2193]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2191]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2189]---> Adder-cost: 144   maxlim: 1275   bits: 12/11
c ---[2187]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2185]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2183]---> Adder-cost: 64   maxlim: 765   bits: 11/10
c ---[2181]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2179]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2177]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2175]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2173]---> Adder-cost: 16   maxlim: 255   bits: 9/8
c ---[2171]---> Adder-cost: 16   maxlim: 255   bits: 9/8
c ---[2169]---> Adder-cost: 688   maxlim: 5610   bits: 14/13
c ---[2167]---> Adder-cost: 640   maxlim: 5100   bits: 14/13
c ---[2165]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2163]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2161]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2159]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2157]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2155]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2153]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2151]---> Adder-cost: 63   maxlim: 510   bits: 10/9
c ---[2149]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2147]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2145]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[2143]---> Adder-cost: 160   maxlim: 1275   bits: 12/11
c ---[2141]---> Adder-cost: 2720   maxlim: 22185   bits: 16/15
c ---[2139]---> Adder-cost: 1880   maxlim: 11475   bits: 15/14
c ---[2137]---> Adder-cost: 240   maxlim: 2040   bits: 12/11
c ---[2135]---> Adder-cost: 240   maxlim: 2040   bits: 12/11
c ---[2133]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2131]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2129]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2127]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2125]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2123]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2121]---> Adder-cost: 80   maxlim: 1020   bits: 11/10
c ---[2119]---> Adder-cost: 80   maxlim: 1020   bits: 11/10
c ---[2117]---> Adder-cost: 144   maxlim: 1275   bits: 12/11
c ---[2115]---> Adder-cost: 144   maxlim: 1275   bits: 12/11
c ---[2113]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2111]---> Adder-cost: 64   maxlim: 765   bits: 11/10
c ---[2109]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2107]---> Adder-cost: 64   maxlim: 765   bits: 11/10
c ---[2105]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2103]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2101]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2099]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2097]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2095]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2093]---> Adder-cost: 208   maxlim: 1785   bits: 12/11
c ---[2091]---> Adder-cost: 144   maxlim: 1785   bits: 12/11
c ---[2089]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2087]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2085]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2083]---> Adder-cost: 63   maxlim: 510   bits: 10/9
c ---[2081]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2079]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2077]---> Adder-cost: 48   maxlim: 765   bits: 10/10
c ---[2075]---> Adder-cost: 160   maxlim: 1275   bits: 12/11
c ---[2073]---> Adder-cost: 160   maxlim: 1275   bits: 12/11
c ---[2071]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2069]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2067]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2065]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2063]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2061]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2059]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2057]---> Adder-cost: 31   maxlim: 255   bits: 9/8
c ---[2055]---> Adder-cost: 1040   maxlim: 8415   bits: 15/14
c ---[2053]---> Adder-cost: 896   maxlim: 8160   bits: 14/13
c ---[2051]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2049]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2047]---> Adder-cost: 544   maxlim: 4590   bits: 14/13
c ---[2045]---> Adder-cost: 528   maxlim: 4590   bits: 14/13
c ---[2043]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2041]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2039]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2037]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2035]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2033]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2031]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2029]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2027]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[2025]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2023]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2021]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2019]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2017]---> Adder-cost: 64   maxlim: 765   bits: 11/10
c ---[2015]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2013]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2011]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2009]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[2007]---> Adder-cost: 144   maxlim: 1275   bits: 12/11
c ---[2005]---> Adder-cost: 144   maxlim: 1275   bits: 12/11
c ---[2003]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[2001]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[1999]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[1997]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[1995]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[1993]---> Adder-cost: 96   maxlim: 765   bits: 11/10
c ---[1991]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[1989]---> Adder-cost: 64   maxlim: 765   bits: 11/10
c ---[1987]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[1985]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[1983]---> Adder-cost: 112   maxlim: 1275   bits: 11/11
c ---[1981]---> Adder-cost: 2736   maxlim: 22440   bits: 16/15
c ---[1979]---> Adder-cost: 2512   maxlim: 21930   bits: 16/15
c ---[1977]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[1975]---> Adder-cost: 128   maxlim: 1530   bits: 12/11
c ---[1973]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[1971]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[1969]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[1967]---> Adder-cost: 144   maxlim: 1275   bits: 12/11
c ---[1965]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[1963]---> Adder-cost: 16   maxlim: 255   bits: 9/8
c ---[1961]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[1959]---> Adder-cost: 160   maxlim: 1530   bits: 12/11
c ---[1957]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[1955]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[1953]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[1951]---> Adder-cost: 64   maxlim: 765   bits: 11/10
c ---[1949]---> Adder-cost: 144   maxlim: 1275   bits: 12/11
c ---[1947]---> Adder-cost: 144   maxlim: 1275   bits: 12/11
c ---[1945]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[1943]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[1941]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[1939]---> Adder-cost: 63   maxlim: 510   bits: 10/9
c ---[1937]---> Adder-cost: 720   maxlim: 5865   bits: 14/13
c ---[1935]---> Adder-cost: 608   maxlim: 5355   bits: 14/13
c ---[1933]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[1931]---> Adder-cost: 160   maxlim: 1530   bits: 12/11
c ---[1929]---> Adder-cost: 160   maxlim: 1275   bits: 12/11
c ---[1927]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[1925]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[1923]---> Adder-cost: 31   maxlim: 255   bits: 9/8
c ---[1921]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[1919]---> Adder-cost: 32   maxlim: 510   bits: 10/9
c ---[1917]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[1915]---> Adder-cost: 176   maxlim: 1530   bits: 12/11
c ---[1913]---> Adder-cost: 80   maxlim: 765   bits: 11/10
c ---[1911]---> Adder-cost: 31   maxlim: 255   bits: 9/8
c ---[1909]---> Adder-cost: 112   maxlim: 1020   bits: 11/10
c ---[1907]---> Adder-cost: 80   maxlim: 1020   bits: 11/10
c ---[1905]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[1903]---> Adder-cost: 32   maxlim: 510   bits: 10/9
c ---[1901]---> Adder-cost: 48   maxlim: 510   bits: 10/9
c ---[1899]---> Adder-cost: 31   maxlim: 255   bits: 9/8
c ---[1898]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1897]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1896]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1895]---> Adder-cost: 87   maxlim: 764   bits: 11/10
c ---[1894]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[1893]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1892]---> Adder-cost: 97   maxlim: 1019   bits: 11/10
c ---[1891]---> Adder-cost: 96   maxlim: 1019   bits: 11/10
c ---[1890]---> Adder-cost: 96   maxlim: 1019   bits: 11/10
c ---[1889]---> Adder-cost: 148   maxlim: 1529   bits: 12/11
c ---[1888]---> Adder-cost: 147   maxlim: 1529   bits: 12/11
c ---[1887]---> Adder-cost: 147   maxlim: 1529   bits: 12/11
c ---[1886]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1885]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1884]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1883]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1882]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1881]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1880]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1879]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1878]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1877]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1876]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1875]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1874]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1873]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1872]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1871]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1870]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1869]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1868]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1867]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1866]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1865]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1864]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1863]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1862]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1861]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1860]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1859]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1858]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1857]---> Adder-cost: 131   maxlim: 1019   bits: 11/10
c ---[1856]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1855]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[1854]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1853]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1852]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1851]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1850]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1849]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1848]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1847]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1846]---> Adder-cost: 71   maxlim: 509   bits: 10/9
c ---[1845]---> Adder-cost: 70   maxlim: 509   bits: 10/9
c ---[1844]---> Adder-cost: 70   maxlim: 509   bits: 10/9
c ---[1843]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1842]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1841]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1840]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1839]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1838]---> Adder-cost: 53   maxlim: 254   bits: 9/8
c ---[1837]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1836]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1835]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1834]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1833]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1832]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[1831]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1830]---> Adder-cost: 152   maxlim: 1274   bits: 12/11
c ---[1829]---> Adder-cost: 151   maxlim: 1274   bits: 12/11
c ---[1828]---> Adder-cost: 151   maxlim: 1274   bits: 12/11
c ---[1827]---> Adder-cost: 164   maxlim: 1529   bits: 12/11
c ---[1826]---> Adder-cost: 181   maxlim: 1529   bits: 12/11
c ---[1825]---> Adder-cost: 163   maxlim: 1529   bits: 12/11
c ---[1824]---> Adder-cost: 242   maxlim: 2039   bits: 12/11
c ---[1823]---> Adder-cost: 215   maxlim: 1784   bits: 12/11
c ---[1822]---> Adder-cost: 257   maxlim: 2039   bits: 12/11
c ---[1821]---> Adder-cost: 263   maxlim: 2294   bits: 13/12
c ---[1820]---> Adder-cost: 223   maxlim: 2039   bits: 12/11
c ---[1819]---> Adder-cost: 246   maxlim: 2294   bits: 13/12
c ---[1818]---> Adder-cost: 277   maxlim: 2549   bits: 13/12
c ---[1817]---> Adder-cost: 262   maxlim: 2294   bits: 13/12
c ---[1816]---> Adder-cost: 292   maxlim: 2549   bits: 13/12
c ---[1815]---> Adder-cost: 307   maxlim: 3059   bits: 13/12
c ---[1814]---> Adder-cost: 310   maxlim: 2804   bits: 13/12
c ---[1813]---> Adder-cost: 306   maxlim: 3059   bits: 13/12
c ---[1812]---> Adder-cost: 357   maxlim: 3059   bits: 13/12
c ---[1811]---> Adder-cost: 344   maxlim: 2804   bits: 13/12
c ---[1810]---> Adder-cost: 356   maxlim: 3059   bits: 13/12
c ---[1809]---> Adder-cost: 327   maxlim: 3314   bits: 13/12
c ---[1808]---> Adder-cost: 322   maxlim: 3059   bits: 13/12
c ---[1807]---> Adder-cost: 342   maxlim: 3314   bits: 13/12
c ---[1806]---> Adder-cost: 355   maxlim: 3569   bits: 13/12
c ---[1805]---> Adder-cost: 294   maxlim: 3314   bits: 13/12
c ---[1804]---> Adder-cost: 354   maxlim: 3569   bits: 13/12
c ---[1803]---> Adder-cost: 409   maxlim: 3824   bits: 13/12
c ---[1802]---> Adder-cost: 390   maxlim: 3569   bits: 13/12
c ---[1801]---> Adder-cost: 440   maxlim: 3824   bits: 13/12
c ---[1800]---> Adder-cost: 433   maxlim: 4079   bits: 13/12
c ---[1799]---> Adder-cost: 432   maxlim: 4079   bits: 13/12
c ---[1798]---> Adder-cost: 408   maxlim: 4334   bits: 14/13
c ---[1797]---> Adder-cost: 332   maxlim: 3824   bits: 13/12
c ---[1796]---> Adder-cost: 423   maxlim: 4334   bits: 14/13
c ---[1795]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1794]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1793]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1792]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1791]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1790]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1789]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1788]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1787]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1786]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1785]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1784]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1783]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1782]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1781]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1780]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1779]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1778]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1777]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1776]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1775]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1774]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1773]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1772]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1771]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1770]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1769]---> Adder-cost: 114   maxlim: 1019   bits: 11/10
c ---[1768]---> Adder-cost: 131   maxlim: 1019   bits: 11/10
c ---[1767]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1766]---> Adder-cost: 134   maxlim: 1274   bits: 12/11
c ---[1765]---> Adder-cost: 135   maxlim: 1019   bits: 11/10
c ---[1764]---> Adder-cost: 147   maxlim: 1529   bits: 12/11
c ---[1763]---> Adder-cost: 425   maxlim: 4589   bits: 14/13
c ---[1762]---> Adder-cost: 424   maxlim: 4589   bits: 14/13
c ---[1761]---> Adder-cost: 600   maxlim: 6629   bits: 14/13
c ---[1760]---> Adder-cost: 217   maxlim: 1274   bits: 12/11
c ---[1759]---> Adder-cost: 679   maxlim: 6885   bits: 14/13
c ---[1758]---> Adder-cost: 441   maxlim: 2039   bits: 12/11
c ---[1757]---> Adder-cost: 794   maxlim: 9434   bits: 15/14
c ---[1756]---> Adder-cost: 786   maxlim: 9434   bits: 15/14
c ---[1755]---> Adder-cost: 847   maxlim: 10709   bits: 15/14
c ---[1754]---> Adder-cost: 475   maxlim: 3059   bits: 13/12
c ---[1753]---> Adder-cost: 844   maxlim: 10709   bits: 15/14
c ---[1752]---> Adder-cost: 1299   maxlim: 12749   bits: 15/14
c ---[1751]---> Adder-cost: 635   maxlim: 4334   bits: 14/13
c ---[1750]---> Adder-cost: 1358   maxlim: 12877   bits: 15/14
c ---[1749]---> Adder-cost: 973   maxlim: 13004   bits: 15/14
c ---[1748]---> Adder-cost: 1128   maxlim: 13132   bits: 15/14
c ---[1747]---> Adder-cost: 607   maxlim: 4589   bits: 14/13
c ---[1746]---> Adder-cost: 915   maxlim: 14789   bits: 15/14
c ---[1745]---> Adder-cost: 961   maxlim: 14661   bits: 15/14
c ---[1744]---> Adder-cost: 1049   maxlim: 15044   bits: 15/14
c ---[1743]---> Adder-cost: 1213   maxlim: 14916   bits: 15/14
c ---[1742]---> Adder-cost: 1099   maxlim: 15299   bits: 15/14
c ---[1741]---> Adder-cost: 987   maxlim: 15171   bits: 15/14
c ---[1740]---> Adder-cost: 1588   maxlim: 17849   bits: 16/15
c ---[1739]---> Adder-cost: 1096   maxlim: 6629   bits: 14/13
c ---[1738]---> Adder-cost: 1706   maxlim: 17849   bits: 16/15
c ---[1737]---> Adder-cost: 1418   maxlim: 18104   bits: 16/15
c ---[1736]---> Adder-cost: 1404   maxlim: 18104   bits: 16/15
c ---[1735]---> Adder-cost: 1474   maxlim: 20399   bits: 16/15
c ---[1734]---> Adder-cost: 884   maxlim: 8414   bits: 15/14
c ---[1733]---> Adder-cost: 1698   maxlim: 20271   bits: 16/15
c ---[1732]---> Adder-cost: 1374   maxlim: 20654   bits: 16/15
c ---[1731]---> Adder-cost: 1588   maxlim: 20526   bits: 16/15
c ---[1730]---> Adder-cost: 1367   maxlim: 9434   bits: 15/14
c ---[1729]---> Adder-cost: 2168   maxlim: 21674   bits: 16/15
c ---[1728]---> Adder-cost: 2018   maxlim: 21546   bits: 16/15
c ---[1727]---> Adder-cost: 1238   maxlim: 21929   bits: 16/15
c ---[1726]---> Adder-cost: 1728   maxlim: 21801   bits: 16/15
c ---[1725]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1724]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1723]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1722]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1721]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1720]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1719]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1718]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1717]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1716]---> Adder-cost: 131   maxlim: 1019   bits: 11/10
c ---[1715]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[1714]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[1713]---> Adder-cost: 150   maxlim: 1529   bits: 12/11
c ---[1712]---> Adder-cost: 165   maxlim: 1529   bits: 12/11
c ---[1711]---> Adder-cost: 197   maxlim: 1529   bits: 12/11
c ---[1710]---> Adder-cost: 182   maxlim: 1784   bits: 12/11
c ---[1709]---> Adder-cost: 181   maxlim: 1784   bits: 12/11
c ---[1708]---> Adder-cost: 181   maxlim: 1784   bits: 12/11
c ---[1707]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1706]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1705]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1704]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1703]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1702]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1701]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1700]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1699]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1698]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1697]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1696]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1695]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1694]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1693]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1692]---> Adder-cost: 87   maxlim: 764   bits: 11/10
c ---[1691]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[1690]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[1689]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1688]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1687]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1686]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1685]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1684]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1683]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1682]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1681]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1680]---> Adder-cost: 97   maxlim: 1019   bits: 11/10
c ---[1679]---> Adder-cost: 96   maxlim: 1019   bits: 11/10
c ---[1678]---> Adder-cost: 96   maxlim: 1019   bits: 11/10
c ---[1677]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1676]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1675]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1674]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1673]---> Adder-cost: 51   maxlim: 509   bits: 10/9
c ---[1672]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1671]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1670]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1669]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1668]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1667]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1666]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1665]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1664]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1663]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1662]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1661]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1660]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1659]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1658]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1657]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1656]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1655]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1654]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1653]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1652]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1651]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1650]---> Adder-cost: 71   maxlim: 764   bits: 11/10
c ---[1649]---> Adder-cost: 55   maxlim: 509   bits: 10/9
c ---[1648]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[1647]---> Adder-cost: 136   maxlim: 1274   bits: 12/11
c ---[1646]---> Adder-cost: 86   maxlim: 1019   bits: 11/10
c ---[1645]---> Adder-cost: 151   maxlim: 1274   bits: 12/11
c ---[1644]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1643]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1642]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1641]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1640]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1639]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1638]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1637]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1636]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1635]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1634]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1633]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1632]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1631]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1630]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1629]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1628]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1627]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1626]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1625]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1624]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1623]---> Adder-cost: 96   maxlim: 1019   bits: 11/10
c ---[1622]---> Adder-cost: 87   maxlim: 764   bits: 11/10
c ---[1621]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[1620]---> Adder-cost: 133   maxlim: 1274   bits: 12/11
c ---[1619]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1618]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1617]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1616]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1615]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1614]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1613]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1612]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1611]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1610]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1609]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1608]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1607]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1606]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1605]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1604]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1603]---> Adder-cost: 89   maxlim: 764   bits: 11/10
c ---[1602]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1601]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1600]---> Adder-cost: 121   maxlim: 1019   bits: 11/10
c ---[1599]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[1598]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[1597]---> Adder-cost: 138   maxlim: 1274   bits: 12/11
c ---[1596]---> Adder-cost: 151   maxlim: 1274   bits: 12/11
c ---[1595]---> Adder-cost: 151   maxlim: 1274   bits: 12/11
c ---[1594]---> Adder-cost: 182   maxlim: 1529   bits: 12/11
c ---[1593]---> Adder-cost: 181   maxlim: 1529   bits: 12/11
c ---[1592]---> Adder-cost: 181   maxlim: 1529   bits: 12/11
c ---[1591]---> Adder-cost: 199   maxlim: 1784   bits: 12/11
c ---[1590]---> Adder-cost: 199   maxlim: 1784   bits: 12/11
c ---[1589]---> Adder-cost: 186   maxlim: 2039   bits: 12/11
c ---[1588]---> Adder-cost: 207   maxlim: 2039   bits: 12/11
c ---[1587]---> Adder-cost: 207   maxlim: 2039   bits: 12/11
c ---[1586]---> Adder-cost: 293   maxlim: 2549   bits: 13/12
c ---[1585]---> Adder-cost: 264   maxlim: 2549   bits: 13/12
c ---[1584]---> Adder-cost: 292   maxlim: 2549   bits: 13/12
c ---[1583]---> Adder-cost: 323   maxlim: 3059   bits: 13/12
c ---[1582]---> Adder-cost: 338   maxlim: 3059   bits: 13/12
c ---[1581]---> Adder-cost: 359   maxlim: 3314   bits: 13/12
c ---[1580]---> Adder-cost: 374   maxlim: 3314   bits: 13/12
c ---[1579]---> Adder-cost: 293   maxlim: 3569   bits: 13/12
c ---[1578]---> Adder-cost: 310   maxlim: 3569   bits: 13/12
c ---[1577]---> Adder-cost: 421   maxlim: 3824   bits: 13/12
c ---[1576]---> Adder-cost: 374   maxlim: 3824   bits: 13/12
c ---[1575]---> Adder-cost: 404   maxlim: 3824   bits: 13/12
c ---[1574]---> Adder-cost: 394   maxlim: 4334   bits: 14/13
c ---[1573]---> Adder-cost: 368   maxlim: 4334   bits: 14/13
c ---[1572]---> Adder-cost: 393   maxlim: 4334   bits: 14/13
c ---[1571]---> Adder-cost: 420   maxlim: 4589   bits: 14/13
c ---[1570]---> Adder-cost: 457   maxlim: 4844   bits: 14/13
c ---[1569]---> Adder-cost: 517   maxlim: 4844   bits: 14/13
c ---[1568]---> Adder-cost: 434   maxlim: 5099   bits: 14/13
c ---[1567]---> Adder-cost: 483   maxlim: 5099   bits: 14/13
c ---[1566]---> Adder-cost: 543   maxlim: 5099   bits: 14/13
c ---[1565]---> Adder-cost: 508   maxlim: 5354   bits: 14/13
c ---[1564]---> Adder-cost: 453   maxlim: 5354   bits: 14/13
c ---[1563]---> Adder-cost: 495   maxlim: 5354   bits: 14/13
c ---[1562]---> Adder-cost: 457   maxlim: 5864   bits: 14/13
c ---[1561]---> Adder-cost: 563   maxlim: 5864   bits: 14/13
c ---[1560]---> Adder-cost: 572   maxlim: 6374   bits: 14/13
c ---[1559]---> Adder-cost: 535   maxlim: 6374   bits: 14/13
c ---[1558]---> Adder-cost: 615   maxlim: 6374   bits: 14/13
c ---[1557]---> Adder-cost: 654   maxlim: 6629   bits: 14/13
c ---[1556]---> Adder-cost: 541   maxlim: 6629   bits: 14/13
c ---[1555]---> Adder-cost: 763   maxlim: 6629   bits: 14/13
c ---[1554]---> Adder-cost: 740   maxlim: 6884   bits: 14/13
c ---[1553]---> Adder-cost: 579   maxlim: 6884   bits: 14/13
c ---[1552]---> Adder-cost: 669   maxlim: 6884   bits: 14/13
c ---[1551]---> Adder-cost: 684   maxlim: 7139   bits: 14/13
c ---[1550]---> Adder-cost: 549   maxlim: 7139   bits: 14/13
c ---[1549]---> Adder-cost: 633   maxlim: 7139   bits: 14/13
c ---[1548]---> Adder-cost: 644   maxlim: 7394   bits: 14/13
c ---[1547]---> Adder-cost: 483   maxlim: 7394   bits: 14/13
c ---[1546]---> Adder-cost: 599   maxlim: 7394   bits: 14/13
c ---[1545]---> Adder-cost: 794   maxlim: 7649   bits: 14/13
c ---[1544]---> Adder-cost: 799   maxlim: 7649   bits: 14/13
c ---[1543]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1542]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1541]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1540]---> Adder-cost: 52   maxlim: 509   bits: 10/9
c ---[1539]---> Adder-cost: 51   maxlim: 509   bits: 10/9
c ---[1538]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1537]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1536]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1535]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1534]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1533]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1532]---> Adder-cost: 115   maxlim: 1019   bits: 11/10
c ---[1531]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1530]---> Adder-cost: 114   maxlim: 1019   bits: 11/10
c ---[1529]---> Adder-cost: 168   maxlim: 1274   bits: 12/11
c ---[1528]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[1527]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1526]---> Adder-cost: 200   maxlim: 1784   bits: 12/11
c ---[1525]---> Adder-cost: 197   maxlim: 1529   bits: 12/11
c ---[1524]---> Adder-cost: 199   maxlim: 1784   bits: 12/11
c ---[1523]---> Adder-cost: 208   maxlim: 2039   bits: 12/11
c ---[1522]---> Adder-cost: 183   maxlim: 1784   bits: 12/11
c ---[1521]---> Adder-cost: 225   maxlim: 2039   bits: 12/11
c ---[1520]---> Adder-cost: 215   maxlim: 2294   bits: 13/12
c ---[1519]---> Adder-cost: 187   maxlim: 2039   bits: 12/11
c ---[1518]---> Adder-cost: 230   maxlim: 2294   bits: 13/12
c ---[1517]---> Adder-cost: 265   maxlim: 2549   bits: 13/12
c ---[1516]---> Adder-cost: 248   maxlim: 2294   bits: 13/12
c ---[1515]---> Adder-cost: 264   maxlim: 2549   bits: 13/12
c ---[1514]---> Adder-cost: 307   maxlim: 3059   bits: 13/12
c ---[1513]---> Adder-cost: 262   maxlim: 2804   bits: 13/12
c ---[1512]---> Adder-cost: 322   maxlim: 3059   bits: 13/12
c ---[1511]---> Adder-cost: 343   maxlim: 3314   bits: 13/12
c ---[1510]---> Adder-cost: 306   maxlim: 3059   bits: 13/12
c ---[1509]---> Adder-cost: 326   maxlim: 3314   bits: 13/12
c ---[1508]---> Adder-cost: 315   maxlim: 3569   bits: 13/12
c ---[1507]---> Adder-cost: 304   maxlim: 3314   bits: 13/12
c ---[1506]---> Adder-cost: 314   maxlim: 3569   bits: 13/12
c ---[1505]---> Adder-cost: 335   maxlim: 3824   bits: 13/12
c ---[1504]---> Adder-cost: 308   maxlim: 3569   bits: 13/12
c ---[1503]---> Adder-cost: 330   maxlim: 3824   bits: 13/12
c ---[1502]---> Adder-cost: 356   maxlim: 4079   bits: 13/12
c ---[1501]---> Adder-cost: 364   maxlim: 3824   bits: 13/12
c ---[1500]---> Adder-cost: 383   maxlim: 4079   bits: 13/12
c ---[1499]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1498]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1497]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1496]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1495]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1494]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1493]---> Adder-cost: 87   maxlim: 764   bits: 11/10
c ---[1492]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[1491]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1490]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1489]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1488]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1487]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1486]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1485]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1484]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1483]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1482]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1481]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1480]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1479]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1478]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1477]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1476]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1475]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1474]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1473]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1472]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1471]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1470]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1469]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1468]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1467]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1466]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1465]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1464]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1463]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1462]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1461]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1460]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1459]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1458]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1457]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1456]---> Adder-cost: 55   maxlim: 509   bits: 10/9
c ---[1455]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1454]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1453]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1452]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1451]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1450]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1449]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1448]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1447]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1446]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1445]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1444]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1443]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1442]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1441]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1440]---> Adder-cost: 87   maxlim: 764   bits: 11/10
c ---[1439]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[1438]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[1437]---> Adder-cost: 99   maxlim: 1019   bits: 11/10
c ---[1436]---> Adder-cost: 98   maxlim: 1019   bits: 11/10
c ---[1435]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[1434]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1433]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1432]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1431]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1430]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1429]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1428]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1427]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1426]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1425]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1424]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1423]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1422]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1421]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1420]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1419]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1418]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1417]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1416]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1415]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1414]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1413]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1412]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1411]---> Adder-cost: 51   maxlim: 509   bits: 10/9
c ---[1410]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1409]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1408]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1407]---> Adder-cost: 71   maxlim: 764   bits: 11/10
c ---[1406]---> Adder-cost: 67   maxlim: 764   bits: 11/10
c ---[1405]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[1404]---> Adder-cost: 131   maxlim: 1019   bits: 11/10
c ---[1403]---> Adder-cost: 86   maxlim: 1019   bits: 11/10
c ---[1402]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[1401]---> Adder-cost: 168   maxlim: 1274   bits: 12/11
c ---[1400]---> Adder-cost: 167   maxlim: 1274   bits: 12/11
c ---[1399]---> Adder-cost: 186   maxlim: 2294   bits: 13/12
c ---[1398]---> Adder-cost: 197   maxlim: 2549   bits: 13/12
c ---[1397]---> Adder-cost: 202   maxlim: 2549   bits: 13/12
c ---[1396]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1395]---> Adder-cost: 215   maxlim: 2804   bits: 13/12
c ---[1394]---> Adder-cost: 234   maxlim: 2804   bits: 13/12
c ---[1393]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1392]---> Adder-cost: 241   maxlim: 3059   bits: 13/12
c ---[1391]---> Adder-cost: 389   maxlim: 3059   bits: 13/12
c ---[1390]---> Adder-cost: 216   maxlim: 764   bits: 11/10
c ---[1389]---> Adder-cost: 410   maxlim: 3314   bits: 13/12
c ---[1388]---> Adder-cost: 395   maxlim: 3569   bits: 13/12
c ---[1387]---> Adder-cost: 257   maxlim: 1274   bits: 12/11
c ---[1386]---> Adder-cost: 422   maxlim: 3824   bits: 13/12
c ---[1385]---> Adder-cost: 524   maxlim: 4844   bits: 14/13
c ---[1384]---> Adder-cost: 360   maxlim: 2549   bits: 13/12
c ---[1383]---> Adder-cost: 553   maxlim: 5099   bits: 14/13
c ---[1382]---> Adder-cost: 620   maxlim: 6629   bits: 14/13
c ---[1381]---> Adder-cost: 458   maxlim: 4079   bits: 13/12
c ---[1380]---> Adder-cost: 601   maxlim: 6884   bits: 14/13
c ---[1379]---> Adder-cost: 566   maxlim: 6884   bits: 14/13
c ---[1378]---> Adder-cost: 400   maxlim: 4334   bits: 14/13
c ---[1377]---> Adder-cost: 565   maxlim: 7395   bits: 14/13
c ---[1376]---> Adder-cost: 708   maxlim: 7139   bits: 14/13
c ---[1375]---> Adder-cost: 583   maxlim: 4589   bits: 14/13
c ---[1374]---> Adder-cost: 763   maxlim: 7650   bits: 14/13
c ---[1373]---> Adder-cost: 824   maxlim: 8924   bits: 15/14
c ---[1372]---> Adder-cost: 761   maxlim: 6629   bits: 14/13
c ---[1371]---> Adder-cost: 844   maxlim: 9435   bits: 15/14
c ---[1370]---> Adder-cost: 816   maxlim: 9179   bits: 15/14
c ---[1369]---> Adder-cost: 711   maxlim: 6884   bits: 14/13
c ---[1368]---> Adder-cost: 852   maxlim: 9690   bits: 15/14
c ---[1367]---> Adder-cost: 742   maxlim: 9434   bits: 15/14
c ---[1366]---> Adder-cost: 673   maxlim: 7139   bits: 14/13
c ---[1365]---> Adder-cost: 850   maxlim: 9945   bits: 15/14
c ---[1364]---> Adder-cost: 759   maxlim: 9689   bits: 15/14
c ---[1363]---> Adder-cost: 661   maxlim: 7394   bits: 14/13
c ---[1362]---> Adder-cost: 782   maxlim: 10200   bits: 15/14
c ---[1361]---> Adder-cost: 749   maxlim: 9944   bits: 15/14
c ---[1360]---> Adder-cost: 599   maxlim: 7649   bits: 14/13
c ---[1359]---> Adder-cost: 716   maxlim: 10455   bits: 15/14
c ---[1358]---> Adder-cost: 671   maxlim: 9944   bits: 15/14
c ---[1357]---> Adder-cost: 799   maxlim: 7904   bits: 14/13
c ---[1356]---> Adder-cost: 686   maxlim: 10455   bits: 15/14
c ---[1355]---> Adder-cost: 923   maxlim: 10964   bits: 15/14
c ---[1354]---> Adder-cost: 762   maxlim: 8924   bits: 15/14
c ---[1353]---> Adder-cost: 938   maxlim: 11475   bits: 15/14
c ---[1352]---> Adder-cost: 1005   maxlim: 11729   bits: 15/14
c ---[1351]---> Adder-cost: 888   maxlim: 9689   bits: 15/14
c ---[1350]---> Adder-cost: 1024   maxlim: 12112   bits: 15/14
c ---[1349]---> Adder-cost: 933   maxlim: 11984   bits: 15/14
c ---[1348]---> Adder-cost: 854   maxlim: 9944   bits: 15/14
c ---[1347]---> Adder-cost: 922   maxlim: 12367   bits: 15/14
c ---[1346]---> Adder-cost: 1087   maxlim: 12749   bits: 15/14
c ---[1345]---> Adder-cost: 962   maxlim: 10709   bits: 15/14
c ---[1344]---> Adder-cost: 1132   maxlim: 13132   bits: 15/14
c ---[1343]---> Adder-cost: 1027   maxlim: 13004   bits: 15/14
c ---[1342]---> Adder-cost: 928   maxlim: 10964   bits: 15/14
c ---[1341]---> Adder-cost: 1020   maxlim: 13387   bits: 15/14
c ---[1340]---> Adder-cost: 1221   maxlim: 13259   bits: 15/14
c ---[1339]---> Adder-cost: 1084   maxlim: 11219   bits: 15/14
c ---[1338]---> Adder-cost: 1219   maxlim: 13642   bits: 15/14
c ---[1337]---> Adder-cost: 697   maxlim: 13259   bits: 15/14
c ---[1336]---> Adder-cost: 642   maxlim: 11219   bits: 15/14
c ---[1335]---> Adder-cost: 707   maxlim: 13642   bits: 15/14
c ---[1334]---> Adder-cost: 1131   maxlim: 14279   bits: 15/14
c ---[1333]---> Adder-cost: 1058   maxlim: 12239   bits: 15/14
c ---[1332]---> Adder-cost: 1161   maxlim: 14662   bits: 15/14
c ---[1331]---> Adder-cost: 1267   maxlim: 14279   bits: 15/14
c ---[1330]---> Adder-cost: 1323   maxlim: 14662   bits: 15/14
c ---[1329]---> Adder-cost: 1091   maxlim: 14789   bits: 15/14
c ---[1328]---> Adder-cost: 982   maxlim: 12494   bits: 15/14
c ---[1327]---> Adder-cost: 1141   maxlim: 15427   bits: 15/14
c ---[1326]---> Adder-cost: 1163   maxlim: 15044   bits: 15/14
c ---[1325]---> Adder-cost: 1153   maxlim: 12749   bits: 15/14
c ---[1324]---> Adder-cost: 1263   maxlim: 15682   bits: 15/14
c ---[1323]---> Adder-cost: 1267   maxlim: 15044   bits: 15/14
c ---[1322]---> Adder-cost: 1211   maxlim: 12749   bits: 15/14
c ---[1321]---> Adder-cost: 1309   maxlim: 15682   bits: 15/14
c ---[1320]---> Adder-cost: 1237   maxlim: 15809   bits: 15/14
c ---[1319]---> Adder-cost: 1295   maxlim: 13514   bits: 15/14
c ---[1318]---> Adder-cost: 1450   maxlim: 16447   bits: 16/15
c ---[1317]---> Adder-cost: 1316   maxlim: 16957   bits: 16/15
c ---[1316]---> Adder-cost: 1288   maxlim: 16574   bits: 16/15
c ---[1315]---> Adder-cost: 1193   maxlim: 14279   bits: 15/14
c ---[1314]---> Adder-cost: 1196   maxlim: 17340   bits: 16/15
c ---[1313]---> Adder-cost: 1320   maxlim: 17084   bits: 16/15
c ---[1312]---> Adder-cost: 1109   maxlim: 14789   bits: 15/14
c ---[1311]---> Adder-cost: 1220   maxlim: 17594   bits: 16/15
c ---[1310]---> Adder-cost: 1342   maxlim: 17339   bits: 16/15
c ---[1309]---> Adder-cost: 1293   maxlim: 15044   bits: 15/14
c ---[1308]---> Adder-cost: 1504   maxlim: 17849   bits: 16/15
c ---[1307]---> Adder-cost: 1564   maxlim: 18104   bits: 16/15
c ---[1306]---> Adder-cost: 1407   maxlim: 15809   bits: 15/14
c ---[1305]---> Adder-cost: 1628   maxlim: 18614   bits: 16/15
c ---[1304]---> Adder-cost: 1496   maxlim: 18359   bits: 16/15
c ---[1303]---> Adder-cost: 1512   maxlim: 19124   bits: 16/15
c ---[1302]---> Adder-cost: 1464   maxlim: 16829   bits: 16/15
c ---[1301]---> Adder-cost: 1612   maxlim: 19634   bits: 16/15
c ---[1300]---> Adder-cost: 1234   maxlim: 17339   bits: 16/15
c ---[1299]---> Adder-cost: 1626   maxlim: 20144   bits: 16/15
c ---[1298]---> Adder-cost: 1468   maxlim: 19634   bits: 16/15
c ---[1297]---> Adder-cost: 718   maxlim: 17339   bits: 16/15
c ---[1296]---> Adder-cost: 736   maxlim: 20144   bits: 16/15
c ---[1295]---> Adder-cost: 1500   maxlim: 19889   bits: 16/15
c ---[1294]---> Adder-cost: 1454   maxlim: 17594   bits: 16/15
c ---[1293]---> Adder-cost: 1654   maxlim: 20399   bits: 16/15
c ---[1292]---> Adder-cost: 1736   maxlim: 19889   bits: 16/15
c ---[1291]---> Adder-cost: 1664   maxlim: 17594   bits: 16/15
c ---[1290]---> Adder-cost: 1808   maxlim: 20399   bits: 16/15
c ---[1289]---> Adder-cost: 1728   maxlim: 21419   bits: 16/15
c ---[1288]---> Adder-cost: 1598   maxlim: 19124   bits: 16/15
c ---[1287]---> Adder-cost: 1836   maxlim: 21929   bits: 16/15
c ---[1286]---> Adder-cost: 1662   maxlim: 22184   bits: 16/15
c ---[1285]---> Adder-cost: 1560   maxlim: 19634   bits: 16/15
c ---[1284]---> Adder-cost: 2100   maxlim: 22694   bits: 16/15
c ---[1283]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1282]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1281]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1280]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1279]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1278]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1277]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1276]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1275]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1274]---> Adder-cost: 120   maxlim: 1019   bits: 11/10
c ---[1273]---> Adder-cost: 114   maxlim: 1019   bits: 11/10
c ---[1272]---> Adder-cost: 135   maxlim: 1019   bits: 11/10
c ---[1271]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1270]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1269]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1268]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1267]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1266]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1265]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1264]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1263]---> Adder-cost: 53   maxlim: 254   bits: 9/8
c ---[1262]---> Adder-cost: 87   maxlim: 764   bits: 11/10
c ---[1261]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1260]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1259]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1258]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1257]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1256]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1255]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1254]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1253]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1252]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1251]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1250]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1249]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1248]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1247]---> Adder-cost: 115   maxlim: 1019   bits: 11/10
c ---[1246]---> Adder-cost: 114   maxlim: 1019   bits: 11/10
c ---[1245]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[1244]---> Adder-cost: 118   maxlim: 1274   bits: 12/11
c ---[1243]---> Adder-cost: 111   maxlim: 1274   bits: 12/11
c ---[1242]---> Adder-cost: 169   maxlim: 1274   bits: 12/11
c ---[1241]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1240]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1239]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1238]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1237]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1236]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1235]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1234]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1233]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1232]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1231]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1230]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1229]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1228]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1227]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1226]---> Adder-cost: 87   maxlim: 764   bits: 11/10
c ---[1225]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[1224]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1223]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1222]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1221]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1220]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1219]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1218]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1217]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1216]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1215]---> Adder-cost: 56   maxlim: 509   bits: 10/9
c ---[1214]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1213]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1212]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1211]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1210]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1209]---> Adder-cost: 87   maxlim: 764   bits: 11/10
c ---[1208]---> Adder-cost: 66   maxlim: 254   bits: 9/8
c ---[1207]---> Adder-cost: 86   maxlim: 764   bits: 11/10
c ---[1206]---> Adder-cost: 115   maxlim: 1019   bits: 11/10
c ---[1205]---> Adder-cost: 100   maxlim: 509   bits: 10/9
c ---[1204]---> Adder-cost: 114   maxlim: 1019   bits: 11/10
c ---[1203]---> Adder-cost: 136   maxlim: 1274   bits: 12/11
c ---[1202]---> Adder-cost: 130   maxlim: 764   bits: 11/10
c ---[1201]---> Adder-cost: 135   maxlim: 1274   bits: 12/11
c ---[1200]---> Adder-cost: 164   maxlim: 1529   bits: 12/11
c ---[1199]---> Adder-cost: 149   maxlim: 1019   bits: 11/10
c ---[1198]---> Adder-cost: 163   maxlim: 1529   bits: 12/11
c ---[1197]---> Adder-cost: 150   maxlim: 1529   bits: 12/11
c ---[1196]---> Adder-cost: 117   maxlim: 1019   bits: 11/10
c ---[1195]---> Adder-cost: 165   maxlim: 1529   bits: 12/11
c ---[1194]---> Adder-cost: 198   maxlim: 1784   bits: 12/11
c ---[1193]---> Adder-cost: 181   maxlim: 1274   bits: 12/11
c ---[1192]---> Adder-cost: 197   maxlim: 1784   bits: 12/11
c ---[1191]---> Adder-cost: 208   maxlim: 2039   bits: 12/11
c ---[1190]---> Adder-cost: 207   maxlim: 2039   bits: 12/11
c ---[1189]---> Adder-cost: 265   maxlim: 2294   bits: 13/12
c ---[1188]---> Adder-cost: 217   maxlim: 1784   bits: 12/11
c ---[1187]---> Adder-cost: 264   maxlim: 2294   bits: 13/12
c ---[1186]---> Adder-cost: 245   maxlim: 2549   bits: 13/12
c ---[1185]---> Adder-cost: 226   maxlim: 2039   bits: 12/11
c ---[1184]---> Adder-cost: 260   maxlim: 2549   bits: 13/12
c ---[1183]---> Adder-cost: 313   maxlim: 2804   bits: 13/12
c ---[1182]---> Adder-cost: 266   maxlim: 2294   bits: 13/12
c ---[1181]---> Adder-cost: 312   maxlim: 2804   bits: 13/12
c ---[1180]---> Adder-cost: 303   maxlim: 3059   bits: 13/12
c ---[1179]---> Adder-cost: 260   maxlim: 2549   bits: 13/12
c ---[1178]---> Adder-cost: 302   maxlim: 3059   bits: 13/12
c ---[1177]---> Adder-cost: 345   maxlim: 3314   bits: 13/12
c ---[1176]---> Adder-cost: 298   maxlim: 2804   bits: 13/12
c ---[1175]---> Adder-cost: 344   maxlim: 3314   bits: 13/12
c ---[1174]---> Adder-cost: 389   maxlim: 3824   bits: 13/12
c ---[1173]---> Adder-cost: 374   maxlim: 3314   bits: 13/12
c ---[1172]---> Adder-cost: 404   maxlim: 3824   bits: 13/12
c ---[1171]---> Adder-cost: 459   maxlim: 3824   bits: 13/12
c ---[1170]---> Adder-cost: 474   maxlim: 3824   bits: 13/12
c ---[1169]---> Adder-cost: 342   maxlim: 4334   bits: 14/13
c ---[1168]---> Adder-cost: 354   maxlim: 3824   bits: 13/12
c ---[1167]---> Adder-cost: 357   maxlim: 4334   bits: 14/13
c ---[1166]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1165]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1164]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1163]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1162]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1161]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1160]---> Adder-cost: 103   maxlim: 764   bits: 11/10
c ---[1159]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1158]---> Adder-cost: 115   maxlim: 1019   bits: 11/10
c ---[1157]---> Adder-cost: 120   maxlim: 1019   bits: 11/10
c ---[1156]---> Adder-cost: 114   maxlim: 1019   bits: 11/10
c ---[1155]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1154]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1153]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1152]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1151]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1150]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1149]---> Adder-cost: 115   maxlim: 1019   bits: 11/10
c ---[1148]---> Adder-cost: 114   maxlim: 1019   bits: 11/10
c ---[1147]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[1146]---> Adder-cost: 135   maxlim: 1274   bits: 12/11
c ---[1145]---> Adder-cost: 151   maxlim: 1274   bits: 12/11
c ---[1144]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1143]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1142]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1141]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1140]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1139]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1138]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1137]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1136]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1135]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1134]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1133]---> Adder-cost: 131   maxlim: 1019   bits: 11/10
c ---[1132]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[1131]---> Adder-cost: 130   maxlim: 1019   bits: 11/10
c ---[1130]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1129]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1128]---> Adder-cost: 68   maxlim: 509   bits: 10/9
c ---[1127]---> Adder-cost: 67   maxlim: 509   bits: 10/9
c ---[1126]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1125]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1124]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1123]---> Adder-cost: 87   maxlim: 764   bits: 11/10
c ---[1122]---> Adder-cost: 72   maxlim: 764   bits: 11/10
c ---[1121]---> Adder-cost: 102   maxlim: 764   bits: 11/10
c ---[1120]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1119]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1118]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1117]---> Adder-cost: 37   maxlim: 254   bits: 9/8
c ---[1116]---> Adder-cost: 36   maxlim: 254   bits: 9/8
c ---[1114]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[1112]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[1110]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[1108]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[1106]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1104]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1102]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1100]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1098]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1096]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1094]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1092]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1090]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1088]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1086]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1084]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1082]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1080]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1078]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1076]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1074]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1072]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1070]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1068]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1066]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1064]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1062]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1060]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1058]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1056]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1054]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[1052]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1050]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1048]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1046]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1044]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1042]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1040]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1038]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1036]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1034]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1032]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1030]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1028]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1026]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1024]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1022]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1020]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1018]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1016]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1014]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1012]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[1010]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1008]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1006]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1004]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1002]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[1000]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 998]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 996]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 994]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 992]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 990]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 988]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 986]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 984]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 982]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 980]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 978]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 976]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 974]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 972]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 970]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 968]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 966]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 964]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 962]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 960]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 958]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 956]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 954]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 952]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 950]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 948]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 946]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 944]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 942]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 940]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 938]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 936]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 934]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 932]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 930]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 928]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 926]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 924]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 922]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 920]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 918]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 916]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 914]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 912]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 910]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 908]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 906]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 904]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 902]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 900]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 898]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 896]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 894]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 892]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 890]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 888]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 886]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 884]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 882]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 880]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 878]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 876]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 874]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 872]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 870]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 868]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 866]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 864]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 862]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 860]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 858]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 856]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 854]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 852]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 850]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 848]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 846]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 844]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 842]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 840]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 838]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 836]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 834]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 832]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 830]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 828]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 826]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 824]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 822]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 820]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 818]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 816]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 814]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 812]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 810]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 808]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 806]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 804]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 802]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 800]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 798]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 796]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 794]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 792]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 790]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 788]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 786]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 784]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 782]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 780]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 778]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 776]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 774]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 772]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 770]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 768]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 766]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 764]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 762]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 760]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 758]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 756]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 754]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 752]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 750]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 748]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 746]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 744]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 742]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 740]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 738]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 736]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 734]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 732]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 730]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 728]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 726]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 724]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 722]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 720]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 718]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 716]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 714]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 712]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 710]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 708]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 706]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 704]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 702]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 700]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 698]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 696]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 694]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 692]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 690]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 688]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 686]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 684]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 682]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 680]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 678]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 676]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 674]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 672]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 670]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 668]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 666]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 664]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 662]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 660]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 658]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 656]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 654]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 652]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 650]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 648]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 646]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 644]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 642]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 640]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 638]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 636]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 634]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 632]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 630]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 628]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 626]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 624]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 622]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 620]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 618]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 616]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 614]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 612]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 610]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 608]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 606]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 604]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 602]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 600]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 598]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 596]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 594]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 592]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 590]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 588]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 586]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 584]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 582]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 580]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 578]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 576]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 574]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 572]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 570]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 568]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 566]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 564]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 562]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 560]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 558]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 556]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 554]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 552]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 550]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 548]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 546]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 544]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 542]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 540]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 538]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 536]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 534]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 532]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 530]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 528]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 526]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 524]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 522]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 520]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 518]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 516]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 514]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 512]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 510]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 508]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 506]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 504]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 502]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 500]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 498]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 496]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 494]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 492]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 490]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 488]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 486]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 484]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 482]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 480]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 478]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 476]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 474]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 472]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 470]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 468]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 466]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 464]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 462]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 460]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 458]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 456]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 454]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 452]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 450]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 448]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 446]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 444]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 442]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 440]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 438]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 436]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 434]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 432]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 430]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 428]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 426]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 424]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 422]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 420]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 418]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 416]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 414]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 412]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 410]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 408]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 406]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 404]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 402]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 400]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 398]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 396]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 394]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 392]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 390]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 388]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 386]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 384]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 382]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 380]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 378]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 376]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 374]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 372]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 370]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 368]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 366]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 364]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 362]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 360]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 358]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 356]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 354]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 352]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 350]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 348]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 346]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 344]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 342]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 340]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 338]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 336]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 334]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 332]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 330]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 328]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 326]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 324]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 322]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 320]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 318]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 316]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 314]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 312]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 310]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 308]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 306]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 304]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 302]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 300]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 298]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 296]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 294]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 292]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 290]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 288]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 286]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 284]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 282]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 280]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 278]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 276]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 274]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 272]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 270]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 268]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 266]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 264]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 262]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 260]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 258]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 256]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 254]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 252]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 250]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 248]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 246]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 244]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 242]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 240]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 238]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 236]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 234]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 232]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 230]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 228]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 226]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 224]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 222]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 220]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 218]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 216]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 214]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 212]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 210]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 208]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 206]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 204]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 202]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 200]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 198]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 196]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 194]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 192]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 190]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 188]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 186]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 184]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 182]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 180]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 178]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 176]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 174]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 172]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 170]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 168]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 166]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 164]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 162]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 160]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 158]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 156]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 154]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 152]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 150]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 148]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 146]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 144]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 142]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 140]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 138]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 136]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 134]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 132]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 130]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 128]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 126]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 124]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 122]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 120]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 118]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 116]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 114]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 112]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 110]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 108]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 106]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[ 104]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 102]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[ 100]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  98]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  96]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  94]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  92]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  90]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  88]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  86]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  84]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  82]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  80]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  78]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  76]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  74]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  72]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  70]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  68]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  66]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  64]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  62]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  60]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  58]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  56]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  54]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  52]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  50]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  48]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  46]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  44]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  42]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  40]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  38]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  36]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  34]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  32]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  30]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  28]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  26]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  24]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  22]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  20]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  18]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  16]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  14]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[  12]---> Adder-cost: 16   maxlim: 382   bits: 9/9
c ---[  10]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[   8]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[   6]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[   4]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[   2]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ---[   0]---> Adder-cost: 32   maxlim: 637   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1980733  7074171 |  660244       0        0     nan |  0.000 % |
c |       100 | 1980733  7074171 |  726268     100      292     2.9 | 12.179 % |
c |       251 | 1980733  7074171 |  798895     251      716     2.9 | 12.179 % |
c |       476 | 1980733  7074171 |  878784     476     1336     2.8 | 12.179 % |
c |       814 | 1980706  7074076 |  966663     812     2374     2.9 | 12.180 % |
c |      1321 | 1980679  7073981 | 1063329    1317     4054     3.1 | 12.182 % |
c |      2080 | 1980671  7073951 | 1169662    2075     6680     3.2 | 12.182 % |
c |      3219 | 1980587  7073659 | 1286628    3203    11600     3.6 | 12.187 % |
c |      4927 | 1980571  7073607 | 1415291    4909    20550     4.2 | 12.187 % |
c |      7489 | 1980571  7073607 | 1556820    7471    38336     5.1 | 12.187 % |
c |     11333 | 1980571  7073607 | 1712502   11315    62768     5.5 | 12.187 % |
c |     17099 | 1980563  7073581 | 1883753   17080   110014     6.4 | 12.188 % |
c |     25748 | 1980547  7073529 | 2072128   25727   209064     8.1 | 12.188 % |
c |     38722 | 1980513  7073411 | 2279341   38698   312784     8.1 | 12.191 % |
c |     58183 | 1980376  7072972 | 2507275   58130   472886     8.1 | 12.196 % |
c |     87375 | 1980327  7072813 | 2758003   87308   916480    10.5 | 12.198 % |
c |    131164 | 1980084  7072016 | 3033803  131061  1749447    13.3 | 12.209 % |
c |    196849 | 1979668  7070608 | 3337183  196674  2671381    13.6 | 12.228 % |
c |    295375 | 1979581  7070309 | 3670902  295189  4939782    16.7 | 12.232 % |
c |    443166 | 1979494  7070028 | 4037992  442965 12380493    27.9 | 12.236 % |
#### 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.85 0.94 0.91 2/54 20233
Raw data (stat): 20233 (runsolver) R 20232 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542944402 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 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 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 6783 0 0 0 975 23 0 0 25 0 1 0 542944402 30478336 6501 4294967295 134512640 134672761 3221224544 3221223936 134580814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7441 6501 603 41 0 7400 0
vsize: 29764
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 9374 0 0 0 1970 29 0 0 25 0 1 0 542944402 38174720 8384 4294967295 134512640 134672761 3221224544 3221223288 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9320 8384 603 41 0 9279 0
vsize: 37280
[startup+30.0006 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 37020 0 0 0 2905 93 0 0 25 0 1 0 542944402 162095104 35370 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39574 35370 603 41 0 39533 0
vsize: 158296
[startup+40.0002 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 37352 0 0 0 3904 94 0 0 25 0 1 0 542944402 163446784 35702 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39904 35702 603 41 0 39863 0
vsize: 159616
[startup+50.0072 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 37509 0 0 0 4904 94 0 0 25 0 1 0 542944402 163987456 35859 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40036 35859 603 41 0 39995 0
vsize: 160144
[startup+60.0066 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 37627 0 0 0 5903 94 0 0 25 0 1 0 542944402 164569088 35977 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40178 35977 603 41 0 40137 0
vsize: 160712
[startup+70.0063 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 37714 0 0 0 6903 95 0 0 25 0 1 0 542944402 164839424 36064 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40244 36064 603 41 0 40203 0
vsize: 160976
[startup+80.0116 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 37830 0 0 0 7903 95 0 0 25 0 1 0 542944402 165244928 36180 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40343 36180 603 41 0 40302 0
vsize: 161372
[startup+90.0106 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 37971 0 0 0 8902 96 0 0 25 0 1 0 542944402 165974016 36321 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40521 36321 603 41 0 40480 0
vsize: 162084
[startup+100.01 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 38154 0 0 0 9891 97 0 0 25 0 1 0 542944402 166649856 36504 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40686 36504 603 41 0 40645 0
vsize: 162744
[startup+110.015 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 38262 0 0 0 10891 97 0 0 25 0 1 0 542944402 167055360 36612 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40785 36612 603 41 0 40744 0
vsize: 163140
[startup+120.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 38391 0 0 0 11891 97 0 0 25 0 1 0 542944402 167723008 36741 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40948 36741 603 41 0 40907 0
vsize: 163792
[startup+130.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 38524 0 0 0 12891 98 0 0 25 0 1 0 542944402 168263680 36874 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41080 36874 603 41 0 41039 0
vsize: 164320
[startup+140.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 38607 0 0 0 13890 98 0 0 25 0 1 0 542944402 168534016 36957 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41146 36957 603 41 0 41105 0
vsize: 164584
[startup+150.015 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 38705 0 0 0 14890 99 0 0 25 0 1 0 542944402 168939520 37055 4294967295 134512640 134672761 3221224544 3221223680 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41245 37055 603 41 0 41204 0
vsize: 164980
[startup+160.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 38782 0 0 0 15890 99 0 0 25 0 1 0 542944402 169209856 37132 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41311 37132 603 41 0 41270 0
vsize: 165244
[startup+170.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 38874 0 0 0 16890 99 0 0 25 0 1 0 542944402 169615360 37224 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41410 37224 603 41 0 41369 0
vsize: 165640
[startup+180.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 38968 0 0 0 17890 99 0 0 25 0 1 0 542944402 169885696 37318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41476 37318 603 41 0 41435 0
vsize: 165904
[startup+190.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 39059 0 0 0 18889 100 0 0 25 0 1 0 542944402 170291200 37409 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41575 37409 603 41 0 41534 0
vsize: 166300
[startup+200.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 39209 0 0 0 19889 100 0 0 25 0 1 0 542944402 170827776 37559 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41706 37559 603 41 0 41665 0
vsize: 166824
[startup+210.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 39392 0 0 0 20888 101 0 0 25 0 1 0 542944402 171900928 37742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41968 37742 603 41 0 41927 0
vsize: 167872
[startup+220.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 39498 0 0 0 21888 101 0 0 25 0 1 0 542944402 172306432 37848 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42067 37848 603 41 0 42026 0
vsize: 168268
[startup+230.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 39604 0 0 0 22888 102 0 0 25 0 1 0 542944402 172707840 37954 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42165 37954 603 41 0 42124 0
vsize: 168660
[startup+240.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 39689 0 0 0 23888 102 0 0 25 0 1 0 542944402 173113344 38039 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42264 38039 603 41 0 42223 0
vsize: 169056
[startup+250.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 39893 0 0 0 24887 103 0 0 25 0 1 0 542944402 173789184 38243 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42429 38243 603 41 0 42388 0
vsize: 169716
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 40037 0 0 0 25887 103 0 0 25 0 1 0 542944402 174460928 38387 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42593 38387 603 41 0 42552 0
vsize: 170372
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 40153 0 0 0 26886 104 0 0 25 0 1 0 542944402 174866432 38503 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42692 38503 603 41 0 42651 0
vsize: 170768
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 40231 0 0 0 27886 104 0 0 25 0 1 0 542944402 175136768 38581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42758 38581 603 41 0 42717 0
vsize: 171032
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 40301 0 0 0 28886 104 0 0 25 0 1 0 542944402 175407104 38651 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42824 38651 603 41 0 42783 0
vsize: 171296
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 40392 0 0 0 29886 104 0 0 25 0 1 0 542944402 175808512 38742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42922 38742 603 41 0 42881 0
vsize: 171688
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 40468 0 0 0 30886 105 0 0 25 0 1 0 542944402 176078848 38818 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42988 38818 603 41 0 42947 0
vsize: 171952
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 40551 0 0 0 31886 105 0 0 25 0 1 0 542944402 176484352 38901 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43087 38901 603 41 0 43046 0
vsize: 172348
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 40643 0 0 0 32886 105 0 0 25 0 1 0 542944402 176754688 38993 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43153 38993 603 41 0 43112 0
vsize: 172612
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 40726 0 0 0 33886 106 0 0 25 0 1 0 542944402 177156096 39076 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43251 39076 603 41 0 43210 0
vsize: 173004
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 40790 0 0 0 34886 106 0 0 25 0 1 0 542944402 177426432 39140 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43317 39140 603 41 0 43276 0
vsize: 173268
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 40972 0 0 0 35885 107 0 0 25 0 1 0 542944402 178098176 39322 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43481 39322 603 41 0 43440 0
vsize: 173924
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 41231 0 0 0 36884 107 0 0 25 0 1 0 542944402 179167232 39581 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43742 39581 603 41 0 43701 0
vsize: 174968
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 41510 0 0 0 37883 109 0 0 25 0 1 0 542944402 180772864 39860 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44134 39860 603 41 0 44093 0
vsize: 176536
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 41582 0 0 0 38882 109 0 0 25 0 1 0 542944402 181043200 39932 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44200 39932 603 41 0 44159 0
vsize: 176800
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 41676 0 0 0 39882 109 0 0 25 0 1 0 542944402 181456896 40026 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44301 40026 603 41 0 44260 0
vsize: 177204
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 41739 0 0 0 40882 110 0 0 25 0 1 0 542944402 181727232 40089 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44367 40089 603 41 0 44326 0
vsize: 177468
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 41828 0 0 0 41882 110 0 0 25 0 1 0 542944402 181997568 40178 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44433 40178 603 41 0 44392 0
vsize: 177732
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 41900 0 0 0 42882 110 0 0 25 0 1 0 542944402 182403072 40250 4294967295 134512640 134672761 3221224544 3221223680 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44532 40250 603 41 0 44491 0
vsize: 178128
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 41962 0 0 0 43882 110 0 0 25 0 1 0 542944402 182538240 40312 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44565 40312 603 41 0 44524 0
vsize: 178260
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42032 0 0 0 44882 110 0 0 25 0 1 0 542944402 182808576 40382 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44631 40382 603 41 0 44590 0
vsize: 178524
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42080 0 0 0 45882 111 0 0 25 0 1 0 542944402 183078912 40430 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44697 40430 603 41 0 44656 0
vsize: 178788
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42134 0 0 0 46882 111 0 0 25 0 1 0 542944402 183214080 40484 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44730 40484 603 41 0 44689 0
vsize: 178920
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42211 0 0 0 47882 111 0 0 25 0 1 0 542944402 183615488 40561 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44828 40562 603 41 0 44787 0
vsize: 179312
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42392 0 0 0 48881 112 0 0 25 0 1 0 542944402 184295424 40742 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44994 40742 603 41 0 44953 0
vsize: 179976
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42452 0 0 0 49881 112 0 0 25 0 1 0 542944402 184565760 40802 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45060 40802 603 41 0 45019 0
vsize: 180240
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42547 0 0 0 50881 112 0 0 25 0 1 0 542944402 184836096 40897 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45126 40897 603 41 0 45085 0
vsize: 180504
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42621 0 0 0 51881 113 0 0 25 0 1 0 542944402 185241600 40971 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45225 40971 603 41 0 45184 0
vsize: 180900
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42707 0 0 0 52880 113 0 0 25 0 1 0 542944402 185511936 41057 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45291 41057 603 41 0 45250 0
vsize: 181164
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42776 0 0 0 53880 113 0 0 25 0 1 0 542944402 185782272 41126 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45357 41126 603 41 0 45316 0
vsize: 181428
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42845 0 0 0 54880 114 0 0 25 0 1 0 542944402 186052608 41195 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45423 41195 603 41 0 45382 0
vsize: 181692
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42928 0 0 0 55880 114 0 0 25 0 1 0 542944402 186458112 41278 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45522 41278 603 41 0 45481 0
vsize: 182088
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 42974 0 0 0 56880 114 0 0 25 0 1 0 542944402 186589184 41324 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45554 41324 603 41 0 45513 0
vsize: 182216
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 43203 0 0 0 57880 115 0 0 25 0 1 0 542944402 187523072 41553 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45782 41553 603 41 0 45741 0
vsize: 183128
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 43332 0 0 0 58880 115 0 0 25 0 1 0 542944402 188059648 41682 4294967295 134512640 134672761 3221224544 3221223712 134560808 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45913 41682 603 41 0 45872 0
vsize: 183652
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 43396 0 0 0 59879 115 0 0 25 0 1 0 542944402 188194816 41746 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45946 41746 603 41 0 45905 0
vsize: 183784
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 43528 0 0 0 60878 116 0 0 25 0 1 0 542944402 188735488 41878 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46078 41878 603 41 0 46037 0
vsize: 184312
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 43603 0 0 0 61879 116 0 0 25 0 1 0 542944402 189005824 41953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46144 41953 603 41 0 46103 0
vsize: 184576
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 43693 0 0 0 62879 116 0 0 25 0 1 0 542944402 189411328 42043 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46243 42043 603 41 0 46202 0
vsize: 184972
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 43758 0 0 0 63879 117 0 0 25 0 1 0 542944402 189681664 42108 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46309 42108 603 41 0 46268 0
vsize: 185236
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 43855 0 0 0 64878 117 0 0 25 0 1 0 542944402 190087168 42205 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46408 42205 603 41 0 46367 0
vsize: 185632
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 43900 0 0 0 65878 117 0 0 25 0 1 0 542944402 190222336 42250 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46441 42250 603 41 0 46400 0
vsize: 185764
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 44022 0 0 0 66878 118 0 0 25 0 1 0 542944402 190763008 42372 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46573 42372 603 41 0 46532 0
vsize: 186292
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 44386 0 0 0 67877 119 0 0 25 0 1 0 542944402 192233472 42736 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46932 42736 603 41 0 46891 0
vsize: 187728
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 44798 0 0 0 68876 119 0 0 25 0 1 0 542944402 193855488 43148 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47328 43148 603 41 0 47287 0
vsize: 189312
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 45097 0 0 0 69876 120 0 0 25 0 1 0 542944402 195104768 43447 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47633 43447 603 41 0 47592 0
vsize: 190532
[startup+710.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 45331 0 0 0 70875 121 0 0 25 0 1 0 542944402 196063232 43681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47867 43681 603 41 0 47826 0
vsize: 191468
[startup+720.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 45548 0 0 0 71874 122 0 0 25 0 1 0 542944402 196997120 43898 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48095 43898 603 41 0 48054 0
vsize: 192380
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 45768 0 0 0 72874 123 0 0 25 0 1 0 542944402 198897664 44118 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48559 44118 603 41 0 48518 0
vsize: 194236
[startup+740.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 45959 0 0 0 73873 123 0 0 25 0 1 0 542944402 199704576 44309 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48756 44309 603 41 0 48715 0
vsize: 195024
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 46109 0 0 0 74873 124 0 0 25 0 1 0 542944402 200388608 44459 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48923 44459 603 41 0 48882 0
vsize: 195692
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 46251 0 0 0 75872 125 0 0 25 0 1 0 542944402 200929280 44601 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49055 44601 603 41 0 49014 0
vsize: 196220
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 46400 0 0 0 76872 126 0 0 25 0 1 0 542944402 201502720 44750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49195 44750 603 41 0 49154 0
vsize: 196780
[startup+780.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 46534 0 0 0 77871 126 0 0 25 0 1 0 542944402 202067968 44884 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49333 44884 603 41 0 49292 0
vsize: 197332
[startup+790.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 46714 0 0 0 78871 126 0 0 25 0 1 0 542944402 202895360 45064 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49535 45064 603 41 0 49494 0
vsize: 198140
[startup+800.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 46841 0 0 0 79871 127 0 0 25 0 1 0 542944402 203448320 45191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49670 45191 603 41 0 49629 0
vsize: 198680
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 46951 0 0 0 80870 128 0 0 25 0 1 0 542944402 203943936 45301 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49791 45301 603 41 0 49750 0
vsize: 199164
[startup+820.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 47037 0 0 0 81870 128 0 0 25 0 1 0 542944402 204214272 45387 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49857 45387 603 41 0 49816 0
vsize: 199428
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 47131 0 0 0 82870 128 0 0 25 0 1 0 542944402 204619776 45481 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49956 45481 603 41 0 49915 0
vsize: 199824
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 47310 0 0 0 83870 128 0 0 25 0 1 0 542944402 205287424 45660 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50119 45660 603 41 0 50078 0
vsize: 200476
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 47376 0 0 0 84869 129 0 0 25 0 1 0 542944402 205553664 45726 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50184 45726 603 41 0 50143 0
vsize: 200736
[startup+860.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 47469 0 0 0 85869 129 0 0 25 0 1 0 542944402 205959168 45819 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50283 45819 603 41 0 50242 0
vsize: 201132
[startup+870.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 47560 0 0 0 86869 129 0 0 25 0 1 0 542944402 206245888 45910 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50353 45910 603 41 0 50312 0
vsize: 201412
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 47651 0 0 0 87869 129 0 0 25 0 1 0 542944402 206651392 46001 4294967295 134512640 134672761 3221224544 3221223636 134555596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50452 46001 603 41 0 50411 0
vsize: 201808
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 47714 0 0 0 88869 130 0 0 25 0 1 0 542944402 206921728 46064 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50518 46064 603 41 0 50477 0
vsize: 202072
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 47804 0 0 0 89868 130 0 0 25 0 1 0 542944402 207327232 46154 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50617 46154 603 41 0 50576 0
vsize: 202468
[startup+910.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 48327 0 0 0 90867 132 0 0 25 0 1 0 542944402 209342464 46677 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51109 46677 603 41 0 51068 0
vsize: 204436
[startup+920.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 48398 0 0 0 91866 132 0 0 25 0 1 0 542944402 209612800 46748 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51175 46748 603 41 0 51134 0
vsize: 204700
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 48544 0 0 0 92866 133 0 0 25 0 1 0 542944402 210288640 46894 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51340 46894 603 41 0 51299 0
vsize: 205360
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 48643 0 0 0 93866 133 0 0 25 0 1 0 542944402 210694144 46993 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51439 46993 603 41 0 51398 0
vsize: 205756
[startup+950.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 48694 0 0 0 94866 133 0 0 25 0 1 0 542944402 210825216 47044 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51471 47044 603 41 0 51430 0
vsize: 205884
[startup+960.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 49224 0 0 0 95865 135 0 0 25 0 1 0 542944402 212975616 47574 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51996 47574 603 41 0 51955 0
vsize: 207984
[startup+970.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 49987 0 0 0 96863 137 0 0 25 0 1 0 542944402 216092672 48337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52757 48337 603 41 0 52716 0
vsize: 211028
[startup+980.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 50635 0 0 0 97861 139 0 0 25 0 1 0 542944402 218644480 48985 4294967295 134512640 134672761 3221224544 3221223728 134559625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53380 48985 603 41 0 53339 0
vsize: 213520
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 51188 0 0 0 98860 140 0 0 25 0 1 0 542944402 220946432 49538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53942 49538 603 41 0 53901 0
vsize: 215768
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 51637 0 0 0 99859 141 0 0 25 0 1 0 542944402 222814208 49987 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54398 49987 603 41 0 54357 0
vsize: 217592
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 52043 0 0 0 100858 143 0 0 25 0 1 0 542944402 224497664 50393 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54809 50393 603 41 0 54768 0
vsize: 219236
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 52364 0 0 0 101856 144 0 0 25 0 1 0 542944402 225779712 50714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55122 50714 603 41 0 55081 0
vsize: 220488
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 52669 0 0 0 102856 145 0 0 25 0 1 0 542944402 227135488 51019 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55453 51019 603 41 0 55412 0
vsize: 221812
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 52979 0 0 0 103855 146 0 0 25 0 1 0 542944402 228327424 51329 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55744 51329 603 41 0 55703 0
vsize: 222976
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 53267 0 0 0 104854 147 0 0 25 0 1 0 542944402 229539840 51617 4294967295 134512640 134672761 3221224544 3221223728 134559390 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56040 51617 603 41 0 55999 0
vsize: 224160
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 53548 0 0 0 105852 149 0 0 25 0 1 0 542944402 230612992 51898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56302 51898 603 41 0 56261 0
vsize: 225208
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 53803 0 0 0 106851 150 0 0 25 0 1 0 542944402 231817216 52153 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56596 52153 603 41 0 56555 0
vsize: 226384
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 54082 0 0 0 107851 150 0 0 25 0 1 0 542944402 232886272 52432 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56857 52432 603 41 0 56816 0
vsize: 227428
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 54333 0 0 0 108850 151 0 0 25 0 1 0 542944402 233963520 52683 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57120 52683 603 41 0 57079 0
vsize: 228480
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 54589 0 0 0 109850 152 0 0 25 0 1 0 542944402 234954752 52939 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57362 52939 603 41 0 57321 0
vsize: 229448
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 54773 0 0 0 110849 153 0 0 25 0 1 0 542944402 235724800 53123 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57550 53123 603 41 0 57509 0
vsize: 230200
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 54978 0 0 0 111849 153 0 0 25 0 1 0 542944402 236621824 53328 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57769 53328 603 41 0 57728 0
vsize: 231076
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 55163 0 0 0 112848 154 0 0 25 0 1 0 542944402 237490176 53513 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57981 53513 603 41 0 57940 0
vsize: 231924
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 55344 0 0 0 113848 154 0 0 25 0 1 0 542944402 238149632 53694 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58142 53694 603 41 0 58101 0
vsize: 232568
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 55533 0 0 0 114847 155 0 0 25 0 1 0 542944402 238944256 53883 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58336 53883 603 41 0 58295 0
vsize: 233344
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 55700 0 0 0 115847 155 0 0 25 0 1 0 542944402 239616000 54050 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58500 54050 603 41 0 58459 0
vsize: 234000
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 55922 0 0 0 116847 156 0 0 25 0 1 0 542944402 240545792 54272 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58727 54272 603 41 0 58686 0
vsize: 234908
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 56112 0 0 0 117846 157 0 0 25 0 1 0 542944402 241393664 54462 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58934 54462 603 41 0 58893 0
vsize: 235736
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 56296 0 0 0 118845 158 0 0 25 0 1 0 542944402 242077696 54646 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59101 54646 603 41 0 59060 0
vsize: 236404
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20233
Raw data (stat): 20233 (minisat+) R 20232 10614 10613 0 -1 0 56557 0 0 0 119844 159 0 0 25 0 1 0 542944402 243163136 54907 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59366 54907 603 41 0 59325 0
vsize: 237464
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 20233
Raw data (stat): 20233 (minisat+) Z 20232 10614 10613 0 -1 12 56559 0 0 0 119844 169 0 0 25 0 1 0 542944402 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.12
CPU time (s): 1200.15
CPU user time (s): 1198.45
CPU system time (s): 1.69874
CPU usage (%): 100.002
Max. virtual memory (Kb): 237464
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####