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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-cap6000.opb
MD5SUM	b4da9562dcd40afcc9afd9f695cf339d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-258414
Optimality of the best value was proved	NO
Number of terms in the objective function	5995
Biggest coefficient in the objective function	91110
Number of bits for the biggest coefficient in the objective function	17
Sum of the numbers in the objective function	12969603
Number of bits of the sum of numbers in the objective function	24
Biggest number in a constraint	800000
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	28761906
Number of bits of the biggest sum of numbers	25
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.18
Number of variables	6000
Total number of constraints	8176
Number of constraints which are clauses	222
Number of constraints which are cardinality constraints (but not clauses)	7919
Number of constraints which are nor clauses,nor cardinality constraints	35
Minimum length of a constraint	1
Maximum length of a constraint	6000
Trace number 16467

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-21 07:28:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13257 boxname=wulflinc19 idbench=1020 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b4da9562dcd40afcc9afd9f695cf339d  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-cap6000.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-cap6000.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-20-10-cap6000.opb
IDLAUNCH: 13257
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        702684 kB
Buffers:          9308 kB
Cached:         296532 kB
SwapCached:        568 kB
Active:         108688 kB
Inactive:       199216 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        702432 kB
SwapTotal:     2097892 kB
SwapFree:      2096412 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5188 kB
Slab:            18272 kB
Committed_AS:    63772 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 07:48:40 (client local time) WITH STATUS 0 IN 1200.37 SECONDS
stats: 13257 7 1200.37 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2294 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###########################################################################################################################
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................
c ---[2293]---> Adder-cost: 61016   maxlim: 27161905   bits: 25/25
c ---[2292]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2291]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2290]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2289]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2288]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2287]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2286]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2285]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2284]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2283]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2282]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2281]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2280]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2279]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2278]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2277]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2276]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2275]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2274]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2273]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2272]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2271]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2270]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2269]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2268]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2267]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2266]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2265]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2264]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2263]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2262]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2261]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2260]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2259]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2258]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2257]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2256]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2255]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2254]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2253]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2252]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2251]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2250]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2249]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2248]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2247]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2246]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2245]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2244]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2243]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2242]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2241]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2240]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2239]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2238]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2237]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2236]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2235]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2234]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2233]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2232]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2231]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2230]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2229]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2228]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2227]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2226]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2225]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2224]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2223]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2222]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2221]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2220]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2219]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2218]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2217]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2216]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2215]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2214]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2213]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2212]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2211]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2210]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2209]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2208]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2207]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2206]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2205]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2204]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2203]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2202]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2201]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2200]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2199]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2198]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2197]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2196]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2195]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2194]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2193]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2192]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2191]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2190]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2189]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2188]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2187]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2186]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2185]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2184]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2183]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2182]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2181]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2180]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2179]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2178]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2177]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2176]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2175]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2174]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2173]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2172]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2171]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2170]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2169]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2168]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2167]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2165]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2164]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2163]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2162]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2161]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2160]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2159]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2158]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2157]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2156]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2155]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2154]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2153]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2152]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2151]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2150]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2149]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2148]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2147]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2146]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2145]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2144]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2143]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2142]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2141]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2140]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2139]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2138]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2137]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2136]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2135]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2134]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2133]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2132]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2131]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2130]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2129]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2128]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2127]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2126]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2125]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2124]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2123]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2122]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2121]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2120]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2119]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2118]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2117]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2116]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2115]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2114]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2113]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2112]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2111]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2110]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2109]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2108]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2107]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2106]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2105]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2104]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2103]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2102]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2101]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2100]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2099]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2098]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2097]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2096]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2095]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2094]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2093]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2092]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2091]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2090]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2089]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2088]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2087]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2086]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2085]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2084]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2083]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2082]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2081]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2080]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2079]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2078]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2077]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2076]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2075]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2074]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2073]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2072]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2071]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2070]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2069]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2068]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2067]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2066]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2065]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2064]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2063]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2062]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2061]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2060]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2059]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2058]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2057]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2056]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2055]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2054]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2053]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2052]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2051]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2050]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2049]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2048]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2047]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2046]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2045]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2044]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2043]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2042]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2041]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2040]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2039]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2038]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2037]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2036]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2035]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2034]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2033]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2032]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2031]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2030]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2029]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2028]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2027]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2026]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2025]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2024]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2023]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2022]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2021]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2020]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2019]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2018]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2017]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2016]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2015]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2014]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2013]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2012]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2011]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2010]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2009]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2008]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2007]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2006]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[2004]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2002]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[2001]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1999]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1997]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1995]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1993]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1991]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1989]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1987]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1985]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1983]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1981]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1980]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1978]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1976]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1974]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1972]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1970]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1968]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1966]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1964]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1962]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1960]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1959]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1957]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1955]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1953]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1951]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1949]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1947]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1945]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1943]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1941]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1939]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1938]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1936]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1934]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1932]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1930]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1928]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1926]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1924]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1922]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1919]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1918]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1907]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1896]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1885]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1874]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1863]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1852]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1841]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1830]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1829]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1827]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1825]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1823]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1821]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1819]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1817]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1815]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1813]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1811]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1809]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1808]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1806]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1804]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1802]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1800]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1798]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1796]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1794]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1792]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1790]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1788]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1787]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1786]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1784]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1782]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1780]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1778]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1776]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1774]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1772]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1770]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1768]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1766]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1765]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1763]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1761]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1759]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1757]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1755]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1753]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1751]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1749]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1747]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1745]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1744]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1742]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1741]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1740]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1739]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1738]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1737]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1736]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1735]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1734]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1733]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1732]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1731]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1730]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1729]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1728]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1727]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1726]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1725]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1724]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1723]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1722]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1721]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1720]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1719]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1718]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1717]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1716]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1715]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1714]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1713]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1712]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1711]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1710]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1709]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1708]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1707]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1706]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1705]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1704]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1703]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1702]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1700]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1698]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1697]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1695]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1694]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1693]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1692]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1691]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1690]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1689]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1688]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1687]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1686]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1685]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1684]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1683]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1682]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1681]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1680]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1679]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1678]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1677]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1676]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1675]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1674]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1673]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1672]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1671]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1670]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1669]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1668]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1667]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1666]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1665]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1664]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1663]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1662]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1661]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1660]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1659]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1658]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1657]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1656]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1655]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1654]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1653]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1652]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1651]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1650]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1649]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1648]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1647]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1646]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1645]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1644]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1643]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1642]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1641]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1640]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1639]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1638]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1637]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1636]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1635]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1634]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1633]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1632]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1631]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1630]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1629]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1628]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1627]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1626]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1625]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1624]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1623]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1622]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1621]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1620]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1619]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1618]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1617]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1616]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1615]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1614]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1613]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1612]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1611]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1610]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1609]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1608]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1607]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1606]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1605]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1604]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1603]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1602]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1601]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1600]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1599]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1598]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1597]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1596]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1595]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1594]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1593]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1592]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1591]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1590]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1589]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1588]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1587]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1586]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1585]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1584]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1583]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1582]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1581]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1580]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1579]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1578]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1577]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1576]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1575]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1574]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1573]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1572]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1571]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1570]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1569]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1568]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1567]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1566]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1565]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1564]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1563]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1562]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1561]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1560]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1559]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1558]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1557]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1556]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1555]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1554]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1553]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1552]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1551]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1550]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1549]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1548]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1547]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1546]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1545]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1544]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1543]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1542]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1541]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1540]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1539]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1538]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1537]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1536]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1535]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1534]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1533]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1532]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1531]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1530]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1529]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1528]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1527]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1526]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1525]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1524]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1523]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1522]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1521]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1520]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1518]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1517]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1515]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1513]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1511]---> Adder-cost: 2   maxlim: 2   bits: 2/2
c ---[1509]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1508]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1507]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1506]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1505]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1504]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1503]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1502]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1501]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1500]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1499]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1498]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1497]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1496]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1495]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1494]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1493]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1492]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1491]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1490]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1489]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1488]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1487]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1486]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1485]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1484]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1483]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1482]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1481]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1480]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1479]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1478]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1477]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1476]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1475]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1474]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1473]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1472]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1471]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1470]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1469]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1468]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1467]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1466]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1465]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1464]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1463]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1462]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1461]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1460]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1459]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1458]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1457]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1456]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1455]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1454]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1453]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1452]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1451]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1450]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1449]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1448]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1447]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1446]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1445]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1444]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1443]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1442]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1441]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1440]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1439]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1438]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1437]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1436]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1435]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1434]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1433]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1432]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1431]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1430]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1429]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1428]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1427]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1426]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1425]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1424]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1423]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1422]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1421]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1420]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1419]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1418]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1417]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1416]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1415]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1414]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1413]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1412]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1411]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1410]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1409]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1408]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1407]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1406]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1405]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1404]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1403]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1402]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1401]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1400]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1399]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1398]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1397]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1396]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1395]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1394]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1393]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1392]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1391]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1390]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1389]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1388]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1387]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1386]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1385]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1384]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1383]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1382]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1381]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1380]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1379]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1378]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1377]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1376]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1375]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1374]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1373]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1372]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1371]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1370]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1369]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1368]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1367]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1366]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1365]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1364]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1363]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1362]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1361]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1360]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1359]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1358]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1357]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1356]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1355]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1354]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1353]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1352]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1351]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1350]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1349]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1348]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1347]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1346]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1345]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1344]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1343]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1342]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1341]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1340]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1339]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1338]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1337]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1336]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1335]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1334]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1333]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1332]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1331]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1330]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1329]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1328]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1327]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1326]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1325]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1324]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1323]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1322]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1321]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1320]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1319]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1318]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1317]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1316]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1315]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1314]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1313]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1312]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1311]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1310]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1309]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1308]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1307]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1306]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1305]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1304]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1303]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1302]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1301]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1300]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1299]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1298]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1297]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1296]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1295]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1294]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1293]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1292]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1291]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1290]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1289]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1288]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1287]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1286]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1285]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1284]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1283]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1282]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1281]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1280]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1279]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1278]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1277]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1276]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1275]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1274]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1273]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1272]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1271]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1270]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1269]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1268]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1267]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1266]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1265]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1264]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1263]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1262]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1261]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1260]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1259]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1258]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1257]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1256]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1255]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1254]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1253]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1252]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1251]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1250]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1249]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1248]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1247]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1246]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1245]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1244]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1243]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1242]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1241]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1240]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1239]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1238]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1237]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1236]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1235]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1234]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1233]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1232]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1231]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1230]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1229]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1228]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1227]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1226]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1225]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1224]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1223]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1222]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1221]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1220]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1219]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1218]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1217]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1216]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1215]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1214]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1213]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1212]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1211]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1210]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1209]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1208]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1207]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1206]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1205]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1204]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1203]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1202]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1201]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1200]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1199]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1198]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1197]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1196]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1195]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1194]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1193]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1192]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1191]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1190]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1189]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1188]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1187]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1186]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1185]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1184]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1183]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1182]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1181]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1180]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1179]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1178]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1177]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1176]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1175]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1174]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1173]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1172]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1171]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1170]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1169]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1168]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1167]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1165]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1164]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1163]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1162]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1161]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1160]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1159]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1158]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1157]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1156]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1155]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1154]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1153]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1152]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1151]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1150]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1149]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1148]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1147]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1146]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1145]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1144]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1143]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1142]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1141]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1140]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1139]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1138]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1137]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1136]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1135]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1134]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1133]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1132]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1131]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1130]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1129]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1128]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1127]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1126]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1125]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1124]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1123]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1122]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1121]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1120]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1119]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1118]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1117]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1116]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1115]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1114]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1113]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1112]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1111]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1110]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1109]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1108]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1107]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1106]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1105]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1104]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1103]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1102]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1101]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1100]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1099]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1098]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1097]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1096]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1095]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1094]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1093]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1092]---> Adder-cost: 59486   maxlim: 14773890   bits: 24/24
c ---[1091]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1090]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1089]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1088]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1087]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1085]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1083]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1081]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1079]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1077]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1075]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1073]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1072]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1070]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1068]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1066]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1064]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1062]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1060]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1058]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1056]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1054]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1052]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1051]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1049]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1047]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1045]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1037]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1026]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1015]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1004]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 993]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 982]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 971]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 960]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 959]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 948]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 937]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 926]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 915]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 904]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 902]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 900]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 898]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 896]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 894]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 892]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 890]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 888]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 886]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 884]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 883]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 881]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 879]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 877]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 869]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 861]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 860]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 859]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 858]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 857]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 856]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 855]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 854]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 853]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 852]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 851]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 850]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 849]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 848]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 847]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 846]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 845]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 844]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 843]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 842]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 841]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 840]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 839]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 838]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 837]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 836]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 835]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 834]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 833]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 832]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 831]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 830]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 829]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 828]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 827]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 826]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 825]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 824]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 823]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 822]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 821]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 820]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 819]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 818]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 817]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 816]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 815]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 814]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 813]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 812]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 811]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 810]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 809]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 808]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 807]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 806]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 805]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 804]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 803]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 802]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 801]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 800]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 799]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 798]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 797]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 796]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 795]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 794]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 793]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 792]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 791]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 790]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 789]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 788]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 787]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 786]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 785]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 784]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 783]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 782]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 781]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 780]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 779]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 778]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 777]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 776]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 775]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 774]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 773]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 772]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 771]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 770]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 769]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 768]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 767]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 766]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 765]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 764]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 763]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 762]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 761]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 760]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 759]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 758]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 757]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 756]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 755]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 754]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 753]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 752]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 751]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 750]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 749]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 748]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 747]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 746]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 745]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 744]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 743]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 742]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 741]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 740]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 739]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 738]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 737]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 736]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 735]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 734]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 733]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 732]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 731]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 730]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 729]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 728]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 727]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 726]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 725]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 724]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 723]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 722]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 721]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 720]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 719]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 718]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 717]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 716]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 715]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 714]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 713]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 712]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 711]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 710]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 709]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 708]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 707]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 706]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 705]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 704]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 703]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 702]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 701]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 700]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 699]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 698]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 697]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 696]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 695]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 694]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 693]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 692]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 691]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 690]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 689]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 688]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 687]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 686]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 685]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 684]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 683]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 682]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 681]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 680]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 679]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 678]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 677]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 676]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 675]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 674]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 673]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 672]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 671]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 670]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 669]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 668]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 667]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 666]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 665]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 664]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 663]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 662]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 661]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 660]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 659]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 658]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 657]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 656]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 655]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 654]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 653]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 652]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 651]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 650]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 649]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 648]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 647]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 646]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 645]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 644]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 643]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 642]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 641]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 640]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 639]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 638]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 637]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 636]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 635]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 634]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 633]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 632]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 631]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 630]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 629]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 628]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 627]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 626]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 625]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 624]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 623]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 622]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 621]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 620]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 619]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 618]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 617]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 616]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 615]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 614]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 613]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 612]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 611]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 610]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 609]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 608]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 607]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 606]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 605]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 604]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 603]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 602]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 601]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 600]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 599]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 598]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 597]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 596]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 595]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 594]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 593]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 592]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 591]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 590]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 589]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 588]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 587]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 586]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 585]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 584]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 583]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 582]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 581]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 580]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 579]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 578]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 577]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 576]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 575]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 574]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 573]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 572]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 571]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 570]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 569]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 568]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 567]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 566]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 565]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 564]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 563]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 562]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 561]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 560]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 559]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 558]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 557]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 556]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 555]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 554]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 553]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 552]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 551]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 550]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 549]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 548]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 547]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 546]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 545]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 544]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 543]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 542]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 541]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 540]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 539]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 538]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 537]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 536]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 535]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 534]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 533]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 532]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 531]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 530]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 529]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 528]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 527]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 526]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 525]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 524]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 523]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 522]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 521]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 520]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 519]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 518]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 517]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 516]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 515]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 514]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 513]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 512]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 511]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 510]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 509]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 508]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 507]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 506]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 505]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 504]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 503]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 502]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 501]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 500]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 499]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 498]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 497]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 496]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 495]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 494]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 493]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 492]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 491]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 490]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 489]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 488]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 487]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 486]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 485]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 484]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 483]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 482]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 481]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 480]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 479]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 478]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 477]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 476]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 475]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 474]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 473]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 472]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 471]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 470]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 469]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 468]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 467]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 466]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 465]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 464]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 463]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 462]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 461]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 460]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 459]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 458]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 457]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 456]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 455]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 454]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 453]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 452]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 451]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 450]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 449]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 448]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 447]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 446]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 445]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 444]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 443]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 442]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 441]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 440]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 439]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 438]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 437]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 436]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 435]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 434]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 433]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 432]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 431]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 430]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 429]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 428]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 427]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 426]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 425]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 424]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 423]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 422]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 421]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 420]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 419]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 418]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 417]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 416]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 415]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 414]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 413]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 412]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 411]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 410]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 409]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 408]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 407]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 406]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 405]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 404]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 403]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 402]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 401]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 400]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 399]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 398]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 397]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 396]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 395]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 394]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 393]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 392]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 391]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 390]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 389]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 388]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 387]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 386]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 385]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 384]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 383]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 382]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 381]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 380]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 379]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 378]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 377]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 376]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 375]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 374]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 373]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 372]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 371]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 370]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 369]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 368]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 367]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 366]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 365]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 364]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 363]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 362]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 361]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 360]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 359]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 358]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 357]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 356]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 355]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 354]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 353]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 352]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 351]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 350]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 349]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 348]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 347]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 346]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 345]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 344]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 343]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 342]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 341]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 340]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 339]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 338]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 337]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 336]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 335]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 334]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 333]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 332]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 331]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 330]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 329]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 328]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 327]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 326]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 325]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 324]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 323]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 322]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 321]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 320]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 319]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 318]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 317]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 316]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 315]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 314]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 313]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 312]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 311]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 310]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 309]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 308]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 307]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 306]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 305]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 304]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 303]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 302]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 301]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 300]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 299]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 298]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 297]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 296]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 295]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 294]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 293]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 292]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 291]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 290]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 289]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 288]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 287]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 286]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 285]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 284]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 283]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 282]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 281]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 280]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 279]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 278]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 277]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 276]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 275]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 274]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 273]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 272]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 271]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 270]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 269]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 268]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 267]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 266]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 265]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 264]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 263]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 262]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 261]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 260]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 259]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 258]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 257]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 256]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 255]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 254]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 253]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 252]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 251]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 250]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 249]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 248]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 247]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 246]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 245]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 244]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 243]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 242]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 241]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 240]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 239]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 238]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 237]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 236]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 235]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 234]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 233]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 232]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 231]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 230]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 229]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 228]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 227]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 226]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 225]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 224]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 223]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 222]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 221]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 220]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 219]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 218]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 217]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 216]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 215]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 214]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 213]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 212]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 211]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 210]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 209]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 208]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 207]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 206]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 205]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 204]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 203]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 202]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 201]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 200]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 199]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 198]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 197]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 196]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 195]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 194]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 193]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 192]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 191]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 190]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 189]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 188]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 187]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 186]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 185]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 184]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 183]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 182]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 181]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 180]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 179]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 178]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 177]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 176]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 175]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 174]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 173]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 172]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 171]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 170]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 169]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 168]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 167]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 166]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 165]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 164]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 163]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 162]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 161]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 160]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 159]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 158]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 157]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 156]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 155]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 154]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 153]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 152]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 151]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 150]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 149]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 148]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 147]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 146]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 145]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 144]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 143]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 142]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 141]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 140]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 139]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 138]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 137]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 136]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 135]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 134]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 133]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 132]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 131]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 130]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 129]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 128]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 127]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 126]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 125]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 124]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 123]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 122]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 121]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 120]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 119]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 118]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 117]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 116]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 115]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 114]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 113]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 112]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 111]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 110]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 109]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 108]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 107]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 106]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 105]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 104]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 103]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 102]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 101]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 100]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  99]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  98]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  97]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  96]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  95]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  94]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  93]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  92]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  91]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  90]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  89]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  88]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  87]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  86]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  85]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  84]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  83]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  82]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  81]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  80]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  79]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  78]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  77]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  76]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  75]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  74]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  73]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  72]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  71]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  70]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  69]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  68]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  67]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  66]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  65]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  64]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  63]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  62]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  61]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  60]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  59]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  58]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  57]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  56]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  55]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  54]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  53]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  52]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  51]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  50]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  49]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  48]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  47]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  46]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  45]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  44]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  43]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  42]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  41]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  40]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  39]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  38]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  37]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  36]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  35]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  34]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  33]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  32]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  31]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  30]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  29]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  28]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  27]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  26]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  25]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  22]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  21]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  20]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  19]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  18]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  17]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  16]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  15]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  14]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  13]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  12]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  11]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[  10]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   9]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   8]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   7]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   6]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   5]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   4]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   3]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   2]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   1]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[   0]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  850461  3033508 |  283487       0        0     nan |  0.000 % |
c |       100 |  850437  3033426 |  311835      97      305     3.1 |  1.760 % |
c |       250 |  850244  3032759 |  343019     228      737     3.2 |  1.781 % |
c |       475 |  850244  3032759 |  377321     453     1619     3.6 |  1.781 % |
c |       812 |  850127  3032344 |  415053     787     4020     5.1 |  1.784 % |
c |      1318 |  850127  3032344 |  456558    1293     5683     4.4 |  1.784 % |
c |      2077 |  850087  3032204 |  502214    2051     8446     4.1 |  1.785 % |
c |      3216 |  849857  3031384 |  552435    3186    13433     4.2 |  1.788 % |
c |      4924 |  849622  3030544 |  607679    4890    21025     4.3 |  1.791 % |
c |      7486 |  849193  3029006 |  668447    7445    35403     4.8 |  1.796 % |
c |     11330 |  849025  3028424 |  735292   11281    55386     4.9 |  1.806 % |
c |     17096 |  849007  3028373 |  808821   17044   213124    12.5 |  1.809 % |
c |     25745 |  848989  3028322 |  889703   25690   416698    16.2 |  1.811 % |
c |     38720 |  848828  3027742 |  978674   38663   771121    19.9 |  1.813 % |
c |     58181 |  848822  3027725 | 1076541   58123  1637386    28.2 |  1.814 % |
c |     87374 |  848654  3027119 | 1184195   87314  2925288    33.5 |  1.816 % |
c |    131163 |  848654  3027119 | 1302615  131103  7390462    56.4 |  1.816 % |
c |    196848 |  848602  3026935 | 1432876  196787 10342882    52.6 |  1.816 % |
c |    295375 |  848527  3026665 | 1576164  295313 15628516    52.9 |  1.817 % |
#### 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.76 0.85 0.87 2/55 28993
Raw data (stat): 28993 (runsolver) R 28992 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 543276830 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.80 0.85 0.87 2/55 28993
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 15110 0 0 0 963 35 0 0 25 0 1 0 543276830 62812160 14321 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15335 14321 603 41 0 15294 0
vsize: 61340
[startup+20.0018 s]
Raw data (loadavg): 0.83 0.85 0.87 2/55 28993
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 15453 0 0 0 1962 36 0 0 25 0 1 0 543276830 64319488 14664 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15703 14664 603 41 0 15662 0
vsize: 62812
[startup+30.0022 s]
Raw data (loadavg): 0.85 0.86 0.87 2/55 28993
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 15585 0 0 0 2961 36 0 0 25 0 1 0 543276830 64860160 14796 4294967295 134512640 134672761 3221224544 3221223696 134565070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15835 14796 603 41 0 15794 0
vsize: 63340
[startup+40.0019 s]
Raw data (loadavg): 0.88 0.86 0.87 2/55 28993
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 15665 0 0 0 3961 37 0 0 25 0 1 0 543276830 65130496 14876 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15901 14876 603 41 0 15860 0
vsize: 63604
[startup+50.003 s]
Raw data (loadavg): 0.89 0.87 0.87 2/55 28993
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 15823 0 0 0 4960 38 0 0 25 0 1 0 543276830 65806336 15034 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16066 15034 603 41 0 16025 0
vsize: 64264
[startup+60.0025 s]
Raw data (loadavg): 0.91 0.87 0.87 2/55 28993
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 16298 0 0 0 5959 39 0 0 25 0 1 0 543276830 67813376 15509 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16556 15509 603 41 0 16515 0
vsize: 66224
[startup+70.0034 s]
Raw data (loadavg): 0.92 0.87 0.87 2/55 28993
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 16764 0 0 0 6958 40 0 0 25 0 1 0 543276830 69816320 15975 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17045 15975 603 41 0 17004 0
vsize: 68180
[startup+80.0045 s]
Raw data (loadavg): 0.93 0.88 0.87 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 17461 0 0 0 7956 42 0 0 25 0 1 0 543276830 72515584 16672 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17704 16672 603 41 0 17663 0
vsize: 70816
[startup+90.004 s]
Raw data (loadavg): 0.94 0.88 0.87 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 17876 0 0 0 8955 44 0 0 25 0 1 0 543276830 74276864 17087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18134 17087 603 41 0 18093 0
vsize: 72536
[startup+100.004 s]
Raw data (loadavg): 0.95 0.89 0.87 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 18293 0 0 0 9954 45 0 0 25 0 1 0 543276830 76025856 17504 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18561 17504 603 41 0 18520 0
vsize: 74244
[startup+110.004 s]
Raw data (loadavg): 0.96 0.89 0.88 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 18665 0 0 0 10952 47 0 0 25 0 1 0 543276830 77770752 17876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18987 17876 603 41 0 18946 0
vsize: 75948
[startup+120.004 s]
Raw data (loadavg): 0.97 0.89 0.88 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 19103 0 0 0 11951 48 0 0 25 0 1 0 543276830 79519744 18314 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19414 18314 603 41 0 19373 0
vsize: 77656
[startup+130.004 s]
Raw data (loadavg): 0.97 0.89 0.88 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 19629 0 0 0 12949 50 0 0 25 0 1 0 543276830 81674240 18840 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19940 18840 603 41 0 19899 0
vsize: 79760
[startup+140.004 s]
Raw data (loadavg): 0.97 0.90 0.88 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 20147 0 0 0 13948 51 0 0 25 0 1 0 543276830 83685376 19358 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20431 19358 603 41 0 20390 0
vsize: 81724
[startup+150.005 s]
Raw data (loadavg): 0.98 0.90 0.88 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 20623 0 0 0 14947 52 0 0 25 0 1 0 543276830 85696512 19834 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20922 19834 603 41 0 20881 0
vsize: 83688
[startup+160.005 s]
Raw data (loadavg): 0.98 0.90 0.88 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 21015 0 0 0 15945 54 0 0 25 0 1 0 543276830 87310336 20226 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21316 20226 603 41 0 21275 0
vsize: 85264
[startup+170.006 s]
Raw data (loadavg): 0.98 0.91 0.88 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 21408 0 0 0 16944 56 0 0 25 0 1 0 543276830 88920064 20619 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21709 20619 603 41 0 21668 0
vsize: 86836
[startup+180.006 s]
Raw data (loadavg): 0.98 0.91 0.88 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 21830 0 0 0 17942 57 0 0 25 0 1 0 543276830 90542080 21041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22105 21041 603 41 0 22064 0
vsize: 88420
[startup+190.006 s]
Raw data (loadavg): 0.99 0.91 0.88 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 22200 0 0 0 18942 58 0 0 25 0 1 0 543276830 92151808 21411 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22498 21411 603 41 0 22457 0
vsize: 89992
[startup+200.006 s]
Raw data (loadavg): 0.99 0.91 0.88 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 22536 0 0 0 19941 59 0 0 25 0 1 0 543276830 93495296 21747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22826 21747 603 41 0 22785 0
vsize: 91304
[startup+210.007 s]
Raw data (loadavg): 0.99 0.92 0.89 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 22847 0 0 0 20940 60 0 0 25 0 1 0 543276830 94838784 22058 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 22058 603 41 0 23113 0
vsize: 92616
[startup+220.007 s]
Raw data (loadavg): 0.99 0.92 0.89 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 23161 0 0 0 21940 61 0 0 25 0 1 0 543276830 96051200 22372 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23450 22372 603 41 0 23409 0
vsize: 93800
[startup+230.008 s]
Raw data (loadavg): 0.99 0.92 0.89 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 23453 0 0 0 22939 62 0 0 25 0 1 0 543276830 97308672 22664 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23757 22664 603 41 0 23716 0
vsize: 95028
[startup+240.007 s]
Raw data (loadavg): 0.99 0.92 0.89 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 23743 0 0 0 23938 63 0 0 25 0 1 0 543276830 98385920 22954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24020 22954 603 41 0 23979 0
vsize: 96080
[startup+250.008 s]
Raw data (loadavg): 0.99 0.92 0.89 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 24051 0 0 0 24937 64 0 0 25 0 1 0 543276830 99770368 23262 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24358 23262 603 41 0 24317 0
vsize: 97432
[startup+260.008 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 24328 0 0 0 25936 65 0 0 25 0 1 0 543276830 101371904 23539 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24749 23539 603 41 0 24708 0
vsize: 98996
[startup+270.009 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 24664 0 0 0 26934 66 0 0 25 0 1 0 543276830 102715392 23875 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25077 23875 603 41 0 25036 0
vsize: 100308
[startup+280.009 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 25150 0 0 0 27933 67 0 0 25 0 1 0 543276830 104738816 24361 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25571 24361 603 41 0 25530 0
vsize: 102284
[startup+290.009 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 25611 0 0 0 28932 68 0 0 25 0 1 0 543276830 106631168 24822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26033 24822 603 41 0 25992 0
vsize: 104132
[startup+300.01 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 25894 0 0 0 29932 69 0 0 25 0 1 0 543276830 107708416 25105 4294967295 134512640 134672761 3221224544 3221223680 134565146 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26296 25105 603 41 0 26255 0
vsize: 105184
[startup+310.01 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 26162 0 0 0 30931 70 0 0 25 0 1 0 543276830 108789760 25373 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26560 25373 603 41 0 26519 0
vsize: 106240
[startup+320.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 26439 0 0 0 31931 70 0 0 25 0 1 0 543276830 110014464 25650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26859 25650 603 41 0 26818 0
vsize: 107436
[startup+330.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 26683 0 0 0 32930 71 0 0 25 0 1 0 543276830 110956544 25894 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27089 25894 603 41 0 27048 0
vsize: 108356
[startup+340.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 26925 0 0 0 33930 71 0 0 25 0 1 0 543276830 111902720 26136 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27320 26136 603 41 0 27279 0
vsize: 109280
[startup+350.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 27142 0 0 0 34930 72 0 0 25 0 1 0 543276830 112701440 26353 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27515 26353 603 41 0 27474 0
vsize: 110060
[startup+360.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 27381 0 0 0 35930 72 0 0 25 0 1 0 543276830 113790976 26592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27781 26592 603 41 0 27740 0
vsize: 111124
[startup+370.013 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 28995
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 27611 0 0 0 36929 73 0 0 25 0 1 0 543276830 114659328 26822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27993 26822 603 41 0 27952 0
vsize: 111972
[startup+380.013 s]
Raw data (loadavg): 0.99 0.95 0.90 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 27825 0 0 0 37928 74 0 0 25 0 1 0 543276830 115507200 27036 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28200 27036 603 41 0 28159 0
vsize: 112800
[startup+390.013 s]
Raw data (loadavg): 0.99 0.95 0.90 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 28067 0 0 0 38927 75 0 0 25 0 1 0 543276830 116609024 27278 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28469 27278 603 41 0 28428 0
vsize: 113876
[startup+400.013 s]
Raw data (loadavg): 0.99 0.95 0.90 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 28310 0 0 0 39927 75 0 0 25 0 1 0 543276830 117547008 27521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28698 27521 603 41 0 28657 0
vsize: 114792
[startup+410.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 28532 0 0 0 40926 76 0 0 25 0 1 0 543276830 118513664 27743 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28934 27743 603 41 0 28893 0
vsize: 115736
[startup+420.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 28784 0 0 0 41926 77 0 0 25 0 1 0 543276830 119459840 27995 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29165 27995 603 41 0 29124 0
vsize: 116660
[startup+430.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 29090 0 0 0 42925 78 0 0 25 0 1 0 543276830 120795136 28301 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29491 28301 603 41 0 29450 0
vsize: 117964
[startup+440.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 29395 0 0 0 43924 79 0 0 25 0 1 0 543276830 121991168 28606 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29783 28606 603 41 0 29742 0
vsize: 119132
[startup+450.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 29667 0 0 0 44924 79 0 0 25 0 1 0 543276830 123248640 28878 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30090 28878 603 41 0 30049 0
vsize: 120360
[startup+460.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 29921 0 0 0 45923 80 0 0 25 0 1 0 543276830 124194816 29132 4294967295 134512640 134672761 3221224544 3221223648 134555093 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30321 29132 603 41 0 30280 0
vsize: 121284
[startup+470.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 30193 0 0 0 46923 81 0 0 25 0 1 0 543276830 125394944 29404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30614 29404 603 41 0 30573 0
vsize: 122456
[startup+480.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 30400 0 0 0 47923 81 0 0 25 0 1 0 543276830 126193664 29611 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30809 29611 603 41 0 30768 0
vsize: 123236
[startup+490.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 30589 0 0 0 48923 81 0 0 25 0 1 0 543276830 126865408 29800 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30973 29800 603 41 0 30932 0
vsize: 123892
[startup+500.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 30785 0 0 0 49922 82 0 0 25 0 1 0 543276830 127799296 29996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31201 29996 603 41 0 31160 0
vsize: 124804
[startup+510.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 30947 0 0 0 50922 82 0 0 25 0 1 0 543276830 128479232 30158 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31367 30158 603 41 0 31326 0
vsize: 125468
[startup+520.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 31100 0 0 0 51922 83 0 0 25 0 1 0 543276830 129019904 30311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31499 30311 603 41 0 31458 0
vsize: 125996
[startup+530.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 31272 0 0 0 52922 83 0 0 25 0 1 0 543276830 129826816 30483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31696 30483 603 41 0 31655 0
vsize: 126784
[startup+540.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 31424 0 0 0 53921 83 0 0 25 0 1 0 543276830 130359296 30635 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31826 30635 603 41 0 31785 0
vsize: 127304
[startup+550.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 31569 0 0 0 54921 84 0 0 25 0 1 0 543276830 130895872 30780 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31957 30780 603 41 0 31916 0
vsize: 127828
[startup+560.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 31730 0 0 0 55921 84 0 0 25 0 1 0 543276830 131567616 30941 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32121 30941 603 41 0 32080 0
vsize: 128484
[startup+570.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 31877 0 0 0 56921 84 0 0 25 0 1 0 543276830 133353472 31088 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32557 31088 603 41 0 32516 0
vsize: 130228
[startup+580.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 32002 0 0 0 57921 85 0 0 25 0 1 0 543276830 133758976 31213 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32656 31213 603 41 0 32615 0
vsize: 130624
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 32178 0 0 0 58920 86 0 0 25 0 1 0 543276830 134533120 31389 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32845 31389 603 41 0 32804 0
vsize: 131380
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 32335 0 0 0 59920 86 0 0 25 0 1 0 543276830 135196672 31546 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33007 31546 603 41 0 32966 0
vsize: 132028
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 32473 0 0 0 60920 86 0 0 25 0 1 0 543276830 135737344 31684 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33139 31684 603 41 0 33098 0
vsize: 132556
[startup+620.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 32617 0 0 0 61920 87 0 0 25 0 1 0 543276830 136282112 31828 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33272 31828 603 41 0 33231 0
vsize: 133088
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 32750 0 0 0 62919 87 0 0 25 0 1 0 543276830 136945664 31961 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33434 31961 603 41 0 33393 0
vsize: 133736
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 32867 0 0 0 63919 88 0 0 25 0 1 0 543276830 137486336 32078 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33566 32078 603 41 0 33525 0
vsize: 134264
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 33025 0 0 0 64919 88 0 0 25 0 1 0 543276830 138149888 32236 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33728 32236 603 41 0 33687 0
vsize: 134912
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 33167 0 0 0 65918 89 0 0 25 0 1 0 543276830 138686464 32378 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33859 32378 603 41 0 33818 0
vsize: 135436
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28997
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 33343 0 0 0 66918 89 0 0 25 0 1 0 543276830 139358208 32554 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34023 32554 603 41 0 33982 0
vsize: 136092
[startup+680.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 33503 0 0 0 67918 90 0 0 25 0 1 0 543276830 140021760 32714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34185 32714 603 41 0 34144 0
vsize: 136740
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 33646 0 0 0 68918 90 0 0 25 0 1 0 543276830 140746752 32857 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34362 32857 603 41 0 34321 0
vsize: 137448
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 33781 0 0 0 69917 90 0 0 25 0 1 0 543276830 141279232 32992 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34492 32992 603 41 0 34451 0
vsize: 137968
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 33916 0 0 0 70917 90 0 0 25 0 1 0 543276830 141815808 33127 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34623 33127 603 41 0 34582 0
vsize: 138492
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 34041 0 0 0 71917 91 0 0 25 0 1 0 543276830 142352384 33252 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34754 33252 603 41 0 34713 0
vsize: 139016
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 34321 0 0 0 72916 92 0 0 25 0 1 0 543276830 143429632 33532 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35017 33532 603 41 0 34976 0
vsize: 140068
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 34600 0 0 0 73915 93 0 0 25 0 1 0 543276830 144646144 33811 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35314 33811 603 41 0 35273 0
vsize: 141256
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 34771 0 0 0 74915 93 0 0 25 0 1 0 543276830 145371136 33982 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35491 33982 603 41 0 35450 0
vsize: 141964
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 34848 0 0 0 75915 94 0 0 25 0 1 0 543276830 145772544 34059 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35589 34059 603 41 0 35548 0
vsize: 142356
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 34946 0 0 0 76915 94 0 0 25 0 1 0 543276830 146042880 34157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35655 34157 603 41 0 35614 0
vsize: 142620
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 35045 0 0 0 77914 94 0 0 25 0 1 0 543276830 146472960 34256 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35760 34256 603 41 0 35719 0
vsize: 143040
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 35125 0 0 0 78914 95 0 0 25 0 1 0 543276830 146890752 34336 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35862 34336 603 41 0 35821 0
vsize: 143448
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 35217 0 0 0 79914 95 0 0 25 0 1 0 543276830 147308544 34428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35964 34428 603 41 0 35923 0
vsize: 143856
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 35332 0 0 0 80913 96 0 0 25 0 1 0 543276830 147709952 34543 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36062 34543 603 41 0 36021 0
vsize: 144248
[startup+820.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 35423 0 0 0 81913 96 0 0 25 0 1 0 543276830 148115456 34634 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36161 34634 603 41 0 36120 0
vsize: 144644
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 35977 0 0 0 82911 99 0 0 25 0 1 0 543276830 150306816 35188 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36696 35188 603 41 0 36655 0
vsize: 146784
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 36653 0 0 0 83909 100 0 0 25 0 1 0 543276830 153141248 35864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37388 35864 603 41 0 37347 0
vsize: 149552
[startup+850.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 37273 0 0 0 84908 102 0 0 25 0 1 0 543276830 155566080 36484 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37980 36484 603 41 0 37939 0
vsize: 151920
[startup+860.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 37858 0 0 0 85907 103 0 0 25 0 1 0 543276830 157978624 37069 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38569 37069 603 41 0 38528 0
vsize: 154276
[startup+870.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 38448 0 0 0 86906 104 0 0 25 0 1 0 543276830 160399360 37659 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39160 37659 603 41 0 39119 0
vsize: 156640
[startup+880.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 39090 0 0 0 87905 106 0 0 25 0 1 0 543276830 163090432 38301 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39817 38301 603 41 0 39776 0
vsize: 159268
[startup+890.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 39677 0 0 0 88903 107 0 0 25 0 1 0 543276830 165392384 38888 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40379 38888 603 41 0 40338 0
vsize: 161516
[startup+900.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 40243 0 0 0 89901 109 0 0 25 0 1 0 543276830 167710720 39454 4294967295 134512640 134672761 3221224544 3221223712 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40945 39454 603 41 0 40904 0
vsize: 163780
[startup+910.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 40771 0 0 0 90901 110 0 0 25 0 1 0 543276830 169865216 39982 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41471 39982 603 41 0 41430 0
vsize: 165884
[startup+920.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 41281 0 0 0 91899 112 0 0 25 0 1 0 543276830 172003328 40492 4294967295 134512640 134672761 3221224544 3221223712 134560828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41993 40492 603 41 0 41952 0
vsize: 167972
[startup+930.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 41888 0 0 0 92898 113 0 0 25 0 1 0 543276830 174555136 41099 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42616 41099 603 41 0 42575 0
vsize: 170464
[startup+940.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 42119 0 0 0 93898 114 0 0 25 0 1 0 543276830 175501312 41330 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42847 41330 603 41 0 42806 0
vsize: 171388
[startup+950.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 42241 0 0 0 94898 114 0 0 25 0 1 0 543276830 175906816 41452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42946 41452 603 41 0 42905 0
vsize: 171784
[startup+960.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 42381 0 0 0 95898 114 0 0 25 0 1 0 543276830 176439296 41592 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43076 41592 603 41 0 43035 0
vsize: 172304
[startup+970.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 28999
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 42508 0 0 0 96898 114 0 0 25 0 1 0 543276830 176971776 41719 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43206 41719 603 41 0 43165 0
vsize: 172824
[startup+980.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 42627 0 0 0 97898 114 0 0 25 0 1 0 543276830 177512448 41838 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43338 41838 603 41 0 43297 0
vsize: 173352
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 42757 0 0 0 98898 114 0 0 25 0 1 0 543276830 178081792 41968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43477 41968 603 41 0 43436 0
vsize: 173908
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 42873 0 0 0 99898 115 0 0 25 0 1 0 543276830 178618368 42084 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43608 42084 603 41 0 43567 0
vsize: 174432
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 43056 0 0 0 100898 115 0 0 25 0 1 0 543276830 179335168 42267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43783 42267 603 41 0 43742 0
vsize: 175132
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 43213 0 0 0 101897 115 0 0 25 0 1 0 543276830 180011008 42424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43948 42424 603 41 0 43907 0
vsize: 175792
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 43382 0 0 0 102897 116 0 0 25 0 1 0 543276830 180547584 42593 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44079 42593 603 41 0 44038 0
vsize: 176316
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 43557 0 0 0 103897 116 0 0 25 0 1 0 543276830 181342208 42768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44273 42768 603 41 0 44232 0
vsize: 177092
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 43725 0 0 0 104896 117 0 0 25 0 1 0 543276830 182009856 42936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44436 42936 603 41 0 44395 0
vsize: 177744
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 43894 0 0 0 105896 117 0 0 25 0 1 0 543276830 182685696 43105 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44601 43105 603 41 0 44560 0
vsize: 178404
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 44058 0 0 0 106896 118 0 0 25 0 1 0 543276830 183226368 43269 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44733 43269 603 41 0 44692 0
vsize: 178932
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 44203 0 0 0 107896 118 0 0 25 0 1 0 543276830 183898112 43414 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44897 43414 603 41 0 44856 0
vsize: 179588
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 44350 0 0 0 108895 119 0 0 25 0 1 0 543276830 184565760 43561 4294967295 134512640 134672761 3221224544 3221223728 134559254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45060 43561 603 41 0 45019 0
vsize: 180240
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 44494 0 0 0 109895 119 0 0 25 0 1 0 543276830 185126912 43705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45197 43705 603 41 0 45156 0
vsize: 180788
[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 44647 0 0 0 110905 119 0 0 25 0 1 0 543276830 185794560 43858 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45360 43858 603 41 0 45319 0
vsize: 181440
[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 44791 0 0 0 111905 119 0 0 25 0 1 0 543276830 186494976 44002 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45531 44002 603 41 0 45490 0
vsize: 182124
[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 44924 0 0 0 112905 119 0 0 25 0 1 0 543276830 187031552 44135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45662 44135 603 41 0 45621 0
vsize: 182648
[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 45059 0 0 0 113905 120 0 0 25 0 1 0 543276830 187531264 44270 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45784 44270 603 41 0 45743 0
vsize: 183136
[startup+1150.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 45187 0 0 0 114906 120 0 0 25 0 1 0 543276830 188076032 44398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45917 44398 603 41 0 45876 0
vsize: 183668
[startup+1160.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 45309 0 0 0 115906 121 0 0 25 0 1 0 543276830 188477440 44520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46015 44520 603 41 0 45974 0
vsize: 184060
[startup+1170.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 45433 0 0 0 116906 121 0 0 25 0 1 0 543276830 189009920 44644 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46145 44644 603 41 0 46104 0
vsize: 184580
[startup+1180.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 45558 0 0 0 117905 121 0 0 25 0 1 0 543276830 189632512 44769 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46297 44769 603 41 0 46256 0
vsize: 185188
[startup+1190.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 45681 0 0 0 118905 122 0 0 25 0 1 0 543276830 190038016 44892 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46396 44892 603 41 0 46355 0
vsize: 185584
[startup+1200.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29001
Raw data (stat): 28993 (minisat+) R 28992 22929 22928 0 -1 0 45799 0 0 0 119905 122 0 0 25 0 1 0 543276830 190566400 45010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46525 45010 603 41 0 46484 0
vsize: 186100
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.24 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 29001
Raw data (stat): 28993 (minisat+) Z 28992 22929 22928 0 -1 12 45801 0 0 0 119905 130 0 0 23 0 1 0 543276830 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.24
CPU time (s): 1200.37
CPU user time (s): 1199.06
CPU system time (s): 1.3088
CPU usage (%): 100.011
Max. virtual memory (Kb): 186100
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####