PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p6000.opb
MD5SUM	9658c3320439c0e9ede5a5b3bf39501b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-301287
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.17
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 18962

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        625280 kB
Buffers:         31628 kB
Cached:         349920 kB
SwapCached:         68 kB
Active:          70508 kB
Inactive:       313956 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        625028 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6876 kB
Slab:            19384 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:41:35 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 17183 7 1200.27 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.79 0.92 0.89 2/54 2755
Raw data (stat): 2755 (runsolver) R 2754 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546845020 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 15110 0 0 0 958 40 0 0 25 0 1 0 546845020 62812160 14321 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15335 14321 603 41 0 15294 0
vsize: 61340
[startup+20.0012 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 15453 0 0 0 1958 41 0 0 25 0 1 0 546845020 64319488 14664 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15703 14664 603 41 0 15662 0
vsize: 62812
[startup+30.0004 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 15584 0 0 0 2956 41 0 0 25 0 1 0 546845020 64860160 14795 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15835 14795 603 41 0 15794 0
vsize: 63340
[startup+40.0003 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 15664 0 0 0 3955 42 0 0 25 0 1 0 546845020 65130496 14875 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15901 14875 603 41 0 15860 0
vsize: 63604
[startup+50.001 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 15820 0 0 0 4955 42 0 0 25 0 1 0 546845020 65806336 15031 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16066 15031 603 41 0 16025 0
vsize: 64264
[startup+60.0013 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 16284 0 0 0 5954 43 0 0 25 0 1 0 546845020 67678208 15495 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16523 15495 603 41 0 16482 0
vsize: 66092
[startup+70.0013 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 16759 0 0 0 6953 45 0 0 25 0 1 0 546845020 69681152 15970 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17012 15970 603 41 0 16971 0
vsize: 68048
[startup+80.001 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 17430 0 0 0 7951 46 0 0 25 0 1 0 546845020 72380416 16641 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17671 16641 603 41 0 17630 0
vsize: 70684
[startup+90.0004 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 17874 0 0 0 8950 47 0 0 25 0 1 0 546845020 74276864 17085 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18134 17085 603 41 0 18093 0
vsize: 72536
[startup+100 s]
Raw data (loadavg): 0.96 0.94 0.90 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 18264 0 0 0 9949 48 0 0 25 0 1 0 546845020 75890688 17475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18528 17475 603 41 0 18487 0
vsize: 74112
[startup+110.001 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 18645 0 0 0 10949 49 0 0 25 0 1 0 546845020 77635584 17856 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18954 17856 603 41 0 18913 0
vsize: 75816
[startup+120.001 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 19083 0 0 0 11948 51 0 0 25 0 1 0 546845020 79384576 18294 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19381 18294 603 41 0 19340 0
vsize: 77524
[startup+130.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 19609 0 0 0 12946 52 0 0 25 0 1 0 546845020 81539072 18820 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19907 18820 603 41 0 19866 0
vsize: 79628
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 20131 0 0 0 13944 54 0 0 25 0 1 0 546845020 83685376 19342 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20431 19342 603 41 0 20390 0
vsize: 81724
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 20604 0 0 0 14943 55 0 0 25 0 1 0 546845020 85561344 19815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20889 19815 603 41 0 20848 0
vsize: 83556
[startup+160.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 21001 0 0 0 15942 57 0 0 25 0 1 0 546845020 87175168 20212 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21283 20212 603 41 0 21242 0
vsize: 85132
[startup+170.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 21394 0 0 0 16941 58 0 0 25 0 1 0 546845020 88784896 20605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21676 20605 603 41 0 21635 0
vsize: 86704
[startup+180.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 21816 0 0 0 17940 59 0 0 25 0 1 0 546845020 90542080 21027 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22105 21027 603 41 0 22064 0
vsize: 88420
[startup+190.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 22187 0 0 0 18939 60 0 0 25 0 1 0 546845020 92016640 21398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22465 21398 603 41 0 22424 0
vsize: 89860
[startup+200.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 22523 0 0 0 19938 61 0 0 25 0 1 0 546845020 93495296 21734 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22826 21734 603 41 0 22785 0
vsize: 91304
[startup+210.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 22838 0 0 0 20938 62 0 0 25 0 1 0 546845020 94703616 22049 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23121 22049 603 41 0 23080 0
vsize: 92484
[startup+220.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 23151 0 0 0 21937 62 0 0 25 0 1 0 546845020 96051200 22362 4294967295 134512640 134672761 3221224544 3221223728 134558645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23450 22362 603 41 0 23409 0
vsize: 93800
[startup+230.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 23444 0 0 0 22937 63 0 0 25 0 1 0 546845020 97173504 22655 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23724 22655 603 41 0 23683 0
vsize: 94896
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 23734 0 0 0 23936 65 0 0 25 0 1 0 546845020 98385920 22945 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24020 22945 603 41 0 23979 0
vsize: 96080
[startup+250.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 24043 0 0 0 24935 65 0 0 25 0 1 0 546845020 99635200 23254 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24325 23254 603 41 0 24284 0
vsize: 97300
[startup+260.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 24305 0 0 0 25935 66 0 0 25 0 1 0 546845020 101236736 23516 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24716 23516 603 41 0 24675 0
vsize: 98864
[startup+270.002 s]
Raw data (loadavg): 1.15 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 24659 0 0 0 26933 68 0 0 25 0 1 0 546845020 102715392 23870 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25077 23870 603 41 0 25036 0
vsize: 100308
[startup+280.002 s]
Raw data (loadavg): 1.12 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 25142 0 0 0 27932 69 0 0 25 0 1 0 546845020 104603648 24353 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25538 24353 603 41 0 25497 0
vsize: 102152
[startup+290.002 s]
Raw data (loadavg): 1.10 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 25605 0 0 0 28932 69 0 0 25 0 1 0 546845020 106496000 24816 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26000 24816 603 41 0 25959 0
vsize: 104000
[startup+300.002 s]
Raw data (loadavg): 1.09 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 25890 0 0 0 29931 70 0 0 25 0 1 0 546845020 107708416 25101 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26296 25101 603 41 0 26255 0
vsize: 105184
[startup+310.002 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 26158 0 0 0 30930 71 0 0 25 0 1 0 546845020 108789760 25369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26560 25369 603 41 0 26519 0
vsize: 106240
[startup+320.002 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 26438 0 0 0 31930 72 0 0 25 0 1 0 546845020 110014464 25649 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26859 25649 603 41 0 26818 0
vsize: 107436
[startup+330.002 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 26681 0 0 0 32929 72 0 0 25 0 1 0 546845020 110956544 25892 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27089 25892 603 41 0 27048 0
vsize: 108356
[startup+340.002 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 26924 0 0 0 33929 73 0 0 25 0 1 0 546845020 111902720 26135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27320 26135 603 41 0 27279 0
vsize: 109280
[startup+350.002 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 27142 0 0 0 34928 74 0 0 25 0 1 0 546845020 112701440 26353 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27515 26353 603 41 0 27474 0
vsize: 110060
[startup+360.002 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 27381 0 0 0 35928 74 0 0 25 0 1 0 546845020 113790976 26592 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27781 26592 603 41 0 27740 0
vsize: 111124
[startup+370.002 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 27613 0 0 0 36928 75 0 0 25 0 1 0 546845020 114659328 26824 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27993 26824 603 41 0 27952 0
vsize: 111972
[startup+380.002 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 27827 0 0 0 37928 75 0 0 25 0 1 0 546845020 115642368 27038 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28233 27038 603 41 0 28192 0
vsize: 112932
[startup+390.002 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 28070 0 0 0 38927 76 0 0 25 0 1 0 546845020 116609024 27281 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28469 27281 603 41 0 28428 0
vsize: 113876
[startup+400.002 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 28314 0 0 0 39926 77 0 0 25 0 1 0 546845020 117547008 27525 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28698 27525 603 41 0 28657 0
vsize: 114792
[startup+410.003 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 28537 0 0 0 40925 77 0 0 25 0 1 0 546845020 118513664 27748 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28934 27748 603 41 0 28893 0
vsize: 115736
[startup+420.002 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 28793 0 0 0 41925 78 0 0 25 0 1 0 546845020 119595008 28004 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29198 28004 603 41 0 29157 0
vsize: 116792
[startup+430.002 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 29102 0 0 0 42925 79 0 0 25 0 1 0 546845020 120795136 28313 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29491 28313 603 41 0 29450 0
vsize: 117964
[startup+440.003 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 29404 0 0 0 43924 80 0 0 25 0 1 0 546845020 121991168 28615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29783 28615 603 41 0 29742 0
vsize: 119132
[startup+450.002 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 29681 0 0 0 44923 80 0 0 25 0 1 0 546845020 123248640 28892 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30090 28892 603 41 0 30049 0
vsize: 120360
[startup+460.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 29934 0 0 0 45923 81 0 0 25 0 1 0 546845020 124325888 29145 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30353 29145 603 41 0 30312 0
vsize: 121412
[startup+470.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 30209 0 0 0 46922 82 0 0 25 0 1 0 546845020 125394944 29420 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30614 29420 603 41 0 30573 0
vsize: 122456
[startup+480.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 30415 0 0 0 47921 83 0 0 25 0 1 0 546845020 126193664 29626 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30809 29627 603 41 0 30768 0
vsize: 123236
[startup+490.003 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 30603 0 0 0 48921 84 0 0 25 0 1 0 546845020 126996480 29814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31005 29814 603 41 0 30964 0
vsize: 124020
[startup+500.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 30797 0 0 0 49920 84 0 0 25 0 1 0 546845020 127799296 30008 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31201 30008 603 41 0 31160 0
vsize: 124804
[startup+510.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 30962 0 0 0 50920 85 0 0 25 0 1 0 546845020 128479232 30173 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31367 30173 603 41 0 31326 0
vsize: 125468
[startup+520.004 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 31114 0 0 0 51920 85 0 0 25 0 1 0 546845020 129155072 30325 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31532 30325 603 41 0 31491 0
vsize: 126128
[startup+530.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 31288 0 0 0 52919 86 0 0 25 0 1 0 546845020 129826816 30499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31696 30499 603 41 0 31655 0
vsize: 126784
[startup+540.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 31443 0 0 0 53919 86 0 0 25 0 1 0 546845020 130494464 30654 4294967295 134512640 134672761 3221224544 3221223712 134561136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31859 30654 603 41 0 31818 0
vsize: 127436
[startup+550.005 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 31582 0 0 0 54919 87 0 0 25 0 1 0 546845020 131031040 30793 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31990 30793 603 41 0 31949 0
vsize: 127960
[startup+560.006 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 31743 0 0 0 55919 87 0 0 25 0 1 0 546845020 131702784 30954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32154 30954 603 41 0 32113 0
vsize: 128616
[startup+570.006 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 31894 0 0 0 56919 87 0 0 25 0 1 0 546845020 133353472 31105 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32557 31105 603 41 0 32516 0
vsize: 130228
[startup+580.007 s]
Raw data (loadavg): 1.00 0.99 0.92 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 32017 0 0 0 57919 87 0 0 25 0 1 0 546845020 133894144 31228 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32689 31228 603 41 0 32648 0
vsize: 130756
[startup+590.007 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 32202 0 0 0 58919 88 0 0 25 0 1 0 546845020 134664192 31413 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32877 31413 603 41 0 32836 0
vsize: 131508
[startup+600.007 s]
Raw data (loadavg): 1.14 1.02 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 32351 0 0 0 59919 88 0 0 25 0 1 0 546845020 135331840 31562 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33040 31562 603 41 0 32999 0
vsize: 132160
[startup+610.007 s]
Raw data (loadavg): 1.12 1.02 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 32496 0 0 0 60918 89 0 0 25 0 1 0 546845020 135868416 31707 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33171 31707 603 41 0 33130 0
vsize: 132684
[startup+620.007 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 32640 0 0 0 61918 89 0 0 25 0 1 0 546845020 136413184 31851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33304 31851 603 41 0 33263 0
vsize: 133216
[startup+630.007 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 32765 0 0 0 62917 90 0 0 25 0 1 0 546845020 137080832 31976 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33467 31976 603 41 0 33426 0
vsize: 133868
[startup+640.008 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 32886 0 0 0 63917 90 0 0 25 0 1 0 546845020 137486336 32097 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33566 32097 603 41 0 33525 0
vsize: 134264
[startup+650.007 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 33048 0 0 0 64917 91 0 0 25 0 1 0 546845020 138285056 32259 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33761 32259 603 41 0 33720 0
vsize: 135044
[startup+660.007 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 33196 0 0 0 65916 92 0 0 25 0 1 0 546845020 138821632 32407 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33892 32407 603 41 0 33851 0
vsize: 135568
[startup+670.007 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 33370 0 0 0 66916 92 0 0 25 0 1 0 546845020 139489280 32581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34055 32581 603 41 0 34014 0
vsize: 136220
[startup+680.007 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 33533 0 0 0 67916 93 0 0 25 0 1 0 546845020 140247040 32744 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34240 32744 603 41 0 34199 0
vsize: 136960
[startup+690.007 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 33673 0 0 0 68915 93 0 0 25 0 1 0 546845020 140881920 32884 4294967295 134512640 134672761 3221224544 3221223680 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34395 32884 603 41 0 34354 0
vsize: 137580
[startup+700.008 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 33805 0 0 0 69915 93 0 0 25 0 1 0 546845020 141414400 33016 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34525 33016 603 41 0 34484 0
vsize: 138100
[startup+710.008 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 33938 0 0 0 70915 94 0 0 25 0 1 0 546845020 141950976 33149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34656 33149 603 41 0 34615 0
vsize: 138624
[startup+720.008 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 34068 0 0 0 71915 94 0 0 25 0 1 0 546845020 142483456 33279 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34786 33279 603 41 0 34745 0
vsize: 139144
[startup+730.008 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 34397 0 0 0 72914 95 0 0 25 0 1 0 546845020 143835136 33608 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35116 33608 603 41 0 35075 0
vsize: 140464
[startup+740.008 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 34650 0 0 0 73913 96 0 0 25 0 1 0 546845020 144781312 33861 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35347 33861 603 41 0 35306 0
vsize: 141388
[startup+750.008 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 34785 0 0 0 74913 96 0 0 25 0 1 0 546845020 145502208 33996 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35523 33996 603 41 0 35482 0
vsize: 142092
[startup+760.009 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 34867 0 0 0 75913 96 0 0 25 0 1 0 546845020 145772544 34078 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35589 34078 603 41 0 35548 0
vsize: 142356
[startup+770.009 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 34971 0 0 0 76913 96 0 0 25 0 1 0 546845020 146206720 34182 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35695 34182 603 41 0 35654 0
vsize: 142780
[startup+780.009 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 35065 0 0 0 77913 97 0 0 25 0 1 0 546845020 146608128 34276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35793 34276 603 41 0 35752 0
vsize: 143172
[startup+790.01 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 35145 0 0 0 78913 97 0 0 25 0 1 0 546845020 147042304 34356 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35899 34356 603 41 0 35858 0
vsize: 143596
[startup+800.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 35246 0 0 0 79913 97 0 0 25 0 1 0 546845020 147308544 34457 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35964 34457 603 41 0 35923 0
vsize: 143856
[startup+810.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 35353 0 0 0 80913 97 0 0 25 0 1 0 546845020 147709952 34564 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36062 34564 603 41 0 36021 0
vsize: 144248
[startup+820.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 35480 0 0 0 81913 98 0 0 25 0 1 0 546845020 148291584 34691 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36204 34691 603 41 0 36163 0
vsize: 144816
[startup+830.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 36155 0 0 0 82911 100 0 0 25 0 1 0 546845020 151117824 35366 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36894 35366 603 41 0 36853 0
vsize: 147576
[startup+840.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 36804 0 0 0 83910 101 0 0 25 0 1 0 546845020 153681920 36015 4294967295 134512640 134672761 3221224544 3221223648 134560198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37520 36015 603 41 0 37479 0
vsize: 150080
[startup+850.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 37426 0 0 0 84908 103 0 0 25 0 1 0 546845020 156229632 36637 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38142 36637 603 41 0 38101 0
vsize: 152568
[startup+860.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 38007 0 0 0 85907 104 0 0 25 0 1 0 546845020 158650368 37218 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38733 37218 603 41 0 38692 0
vsize: 154932
[startup+870.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 38649 0 0 0 86906 106 0 0 25 0 1 0 546845020 161206272 37860 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39357 37860 603 41 0 39316 0
vsize: 157428
[startup+880.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 39244 0 0 0 87905 107 0 0 25 0 1 0 546845020 163631104 38455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39949 38455 603 41 0 39908 0
vsize: 159796
[startup+890.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 39828 0 0 0 88903 109 0 0 25 0 1 0 546845020 166064128 39039 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40543 39039 603 41 0 40502 0
vsize: 162172
[startup+900.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 40382 0 0 0 89902 111 0 0 25 0 1 0 546845020 168378368 39593 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41108 39593 603 41 0 41067 0
vsize: 164432
[startup+910.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 40894 0 0 0 90900 112 0 0 25 0 1 0 546845020 170393600 40105 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41600 40105 603 41 0 41559 0
vsize: 166400
[startup+920.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 41420 0 0 0 91899 114 0 0 25 0 1 0 546845020 172544000 40631 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42125 40631 603 41 0 42084 0
vsize: 168500
[startup+930.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 42032 0 0 0 92896 116 0 0 25 0 1 0 546845020 175095808 41243 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42748 41243 603 41 0 42707 0
vsize: 170992
[startup+940.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 42148 0 0 0 93897 116 0 0 25 0 1 0 546845020 175501312 41359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42847 41359 603 41 0 42806 0
vsize: 171388
[startup+950.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 42275 0 0 0 94896 117 0 0 25 0 1 0 546845020 176037888 41486 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42978 41486 603 41 0 42937 0
vsize: 171912
[startup+960.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 42415 0 0 0 95896 117 0 0 25 0 1 0 546845020 176570368 41626 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43108 41626 603 41 0 43067 0
vsize: 172432
[startup+970.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 42538 0 0 0 96896 117 0 0 25 0 1 0 546845020 177106944 41749 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43239 41749 603 41 0 43198 0
vsize: 172956
[startup+980.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 42665 0 0 0 97896 118 0 0 25 0 1 0 546845020 177672192 41876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43377 41876 603 41 0 43336 0
vsize: 173508
[startup+990.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 42790 0 0 0 98896 118 0 0 25 0 1 0 546845020 178212864 42001 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43509 42001 603 41 0 43468 0
vsize: 174036
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 42966 0 0 0 99895 119 0 0 25 0 1 0 546845020 178900992 42177 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43677 42177 603 41 0 43636 0
vsize: 174708
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 43101 0 0 0 100895 119 0 0 25 0 1 0 546845020 179470336 42312 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43816 42312 603 41 0 43775 0
vsize: 175264
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 43260 0 0 0 101895 120 0 0 25 0 1 0 546845020 180146176 42471 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43981 42471 603 41 0 43940 0
vsize: 175924
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 43442 0 0 0 102894 120 0 0 25 0 1 0 546845020 180813824 42653 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44144 42653 603 41 0 44103 0
vsize: 176576
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 43616 0 0 0 103894 121 0 0 25 0 1 0 546845020 181473280 42827 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44305 42827 603 41 0 44264 0
vsize: 177220
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 43779 0 0 0 104893 122 0 0 25 0 1 0 546845020 182145024 42990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44469 42990 603 41 0 44428 0
vsize: 177876
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 43951 0 0 0 105893 123 0 0 25 0 1 0 546845020 182820864 43162 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44634 43162 603 41 0 44593 0
vsize: 178536
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 44106 0 0 0 106892 123 0 0 25 0 1 0 546845020 183492608 43317 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44798 43317 603 41 0 44757 0
vsize: 179192
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 44283 0 0 0 107892 124 0 0 25 0 1 0 546845020 184295424 43494 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44994 43494 603 41 0 44953 0
vsize: 179976
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 44397 0 0 0 108891 125 0 0 25 0 1 0 546845020 184700928 43608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45093 43608 603 41 0 45052 0
vsize: 180372
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 44565 0 0 0 109891 125 0 0 25 0 1 0 546845020 185524224 43776 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45294 43776 603 41 0 45253 0
vsize: 181176
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 44693 0 0 0 110891 125 0 0 25 0 1 0 546845020 186060800 43904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45425 43904 603 41 0 45384 0
vsize: 181700
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 44838 0 0 0 111890 126 0 0 25 0 1 0 546845020 186626048 44049 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45563 44049 603 41 0 45522 0
vsize: 182252
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 44968 0 0 0 112890 127 0 0 25 0 1 0 546845020 187174912 44179 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45697 44179 603 41 0 45656 0
vsize: 182788
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 45108 0 0 0 113889 127 0 0 25 0 1 0 546845020 187809792 44319 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45852 44319 603 41 0 45811 0
vsize: 183408
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 45231 0 0 0 114889 128 0 0 25 0 1 0 546845020 188211200 44442 4294967295 134512640 134672761 3221224544 3221223648 134560335 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45950 44442 603 41 0 45909 0
vsize: 183800
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 45356 0 0 0 115889 128 0 0 25 0 1 0 546845020 188747776 44567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46081 44567 603 41 0 46040 0
vsize: 184324
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 45480 0 0 0 116889 128 0 0 25 0 1 0 546845020 189198336 44691 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46191 44691 603 41 0 46150 0
vsize: 184764
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 45606 0 0 0 117889 128 0 0 25 0 1 0 546845020 189767680 44817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46330 44817 603 41 0 46289 0
vsize: 185320
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 45724 0 0 0 118889 129 0 0 25 0 1 0 546845020 190300160 44935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46460 44935 603 41 0 46419 0
vsize: 185840
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2755
Raw data (stat): 2755 (minisat+) R 2754 22612 22611 0 -1 0 45856 0 0 0 119889 129 0 0 25 0 1 0 546845020 190836736 45067 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46591 45067 603 41 0 46550 0
vsize: 186364
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 2755
Raw data (stat): 2755 (minisat+) Z 2754 22612 22611 0 -1 12 45858 0 0 0 119889 137 0 0 25 0 1 0 546845020 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.1
CPU time (s): 1200.27
CPU user time (s): 1198.89
CPU system time (s): 1.37979
CPU usage (%): 100.014
Max. virtual memory (Kb): 186364
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####