PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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	-279330
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.15
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 22034

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        524932 kB
Buffers:         30632 kB
Cached:         455664 kB
SwapCached:        516 kB
Active:         174496 kB
Inactive:       313848 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        524680 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            15552 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:18:04 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 12191 7 1200.28 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.91 0.95 0.98 2/54 17081
Raw data (stat): 17081 (runsolver) R 17080 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549938624 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.93 0.95 0.98 2/54 17081
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 15110 0 0 0 960 38 0 0 25 0 1 0 549938624 62812160 14321 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15335 14321 603 41 0 15294 0
vsize: 61340
[startup+20.0001 s]
Raw data (loadavg): 0.94 0.96 0.98 2/54 17081
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 15453 0 0 0 1958 39 0 0 25 0 1 0 549938624 64319488 14664 4294967295 134512640 134672761 3221224544 3221223712 134560983 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.0011 s]
Raw data (loadavg): 0.95 0.96 0.98 2/54 17081
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 15586 0 0 0 2958 40 0 0 25 0 1 0 549938624 64860160 14797 4294967295 134512640 134672761 3221224544 3221223680 134566155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15835 14797 603 41 0 15794 0
vsize: 63340
[startup+40.0016 s]
Raw data (loadavg): 0.95 0.96 0.98 2/54 17081
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 15666 0 0 0 3957 40 0 0 25 0 1 0 549938624 65130496 14877 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15901 14877 603 41 0 15860 0
vsize: 63604
[startup+50.0012 s]
Raw data (loadavg): 0.96 0.96 0.98 2/54 17081
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 15827 0 0 0 4957 41 0 0 25 0 1 0 549938624 65806336 15038 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16066 15038 603 41 0 16025 0
vsize: 64264
[startup+60.0012 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 17081
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 16302 0 0 0 5956 42 0 0 25 0 1 0 549938624 67813376 15513 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16556 15513 603 41 0 16515 0
vsize: 66224
[startup+70.0023 s]
Raw data (loadavg): 0.97 0.96 0.98 2/54 17081
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 16767 0 0 0 6954 44 0 0 25 0 1 0 549938624 69816320 15978 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17045 15978 603 41 0 17004 0
vsize: 68180
[startup+80.0034 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 17081
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 17465 0 0 0 7953 46 0 0 25 0 1 0 549938624 72646656 16676 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17736 16676 603 41 0 17695 0
vsize: 70944
[startup+90.0034 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 17081
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 17877 0 0 0 8952 47 0 0 25 0 1 0 549938624 74276864 17088 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18134 17088 603 41 0 18093 0
vsize: 72536
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 17081
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 18297 0 0 0 9951 47 0 0 25 0 1 0 549938624 76025856 17508 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18561 17508 603 41 0 18520 0
vsize: 74244
[startup+110.004 s]
Raw data (loadavg): 0.98 0.96 0.98 2/54 17081
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 18667 0 0 0 10951 48 0 0 25 0 1 0 549938624 77770752 17878 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18987 17878 603 41 0 18946 0
vsize: 75948
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 17081
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 19107 0 0 0 11949 49 0 0 25 0 1 0 549938624 79519744 18318 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19414 18318 603 41 0 19373 0
vsize: 77656
[startup+130.004 s]
Raw data (loadavg): 1.13 1.00 0.99 2/54 17134
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 19637 0 0 0 12947 51 0 0 25 0 1 0 549938624 81674240 18848 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19940 18848 603 41 0 19899 0
vsize: 79760
[startup+140.005 s]
Raw data (loadavg): 1.11 1.00 0.99 2/54 17134
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 20161 0 0 0 13945 53 0 0 25 0 1 0 549938624 83820544 19372 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20464 19372 603 41 0 20423 0
vsize: 81856
[startup+150.005 s]
Raw data (loadavg): 1.10 1.00 0.99 2/54 17134
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 20636 0 0 0 14944 55 0 0 25 0 1 0 549938624 85696512 19847 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20922 19847 603 41 0 20881 0
vsize: 83688
[startup+160.005 s]
Raw data (loadavg): 1.08 1.00 0.99 2/54 17134
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 21027 0 0 0 15943 56 0 0 25 0 1 0 549938624 87310336 20238 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21316 20238 603 41 0 21275 0
vsize: 85264
[startup+170.005 s]
Raw data (loadavg): 1.07 1.00 0.99 2/54 17134
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 21422 0 0 0 16941 58 0 0 25 0 1 0 549938624 88920064 20633 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21709 20633 603 41 0 21668 0
vsize: 86836
[startup+180.006 s]
Raw data (loadavg): 1.06 1.00 0.99 2/54 17134
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 21842 0 0 0 17940 59 0 0 25 0 1 0 549938624 90677248 21053 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22138 21053 603 41 0 22097 0
vsize: 88552
[startup+190.007 s]
Raw data (loadavg): 1.05 1.00 0.99 2/54 17134
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 22212 0 0 0 18938 62 0 0 25 0 1 0 549938624 92151808 21423 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22498 21423 603 41 0 22457 0
vsize: 89992
[startup+200.006 s]
Raw data (loadavg): 1.04 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 22552 0 0 0 19936 64 0 0 25 0 1 0 549938624 93630464 21763 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22859 21763 603 41 0 22818 0
vsize: 91436
[startup+210.006 s]
Raw data (loadavg): 1.03 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 22859 0 0 0 20935 65 0 0 25 0 1 0 549938624 94838784 22070 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23154 22070 603 41 0 23113 0
vsize: 92616
[startup+220.006 s]
Raw data (loadavg): 1.03 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 23174 0 0 0 21934 66 0 0 25 0 1 0 549938624 96051200 22385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23450 22385 603 41 0 23409 0
vsize: 93800
[startup+230.007 s]
Raw data (loadavg): 1.02 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 23464 0 0 0 22933 67 0 0 25 0 1 0 549938624 97308672 22675 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23757 22675 603 41 0 23716 0
vsize: 95028
[startup+240.007 s]
Raw data (loadavg): 1.02 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 23757 0 0 0 23932 69 0 0 25 0 1 0 549938624 98521088 22968 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24053 22968 603 41 0 24012 0
vsize: 96212
[startup+250.007 s]
Raw data (loadavg): 1.02 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 24063 0 0 0 24931 70 0 0 25 0 1 0 549938624 99770368 23274 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24358 23274 603 41 0 24317 0
vsize: 97432
[startup+260.007 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 24339 0 0 0 25930 71 0 0 25 0 1 0 549938624 101371904 23550 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24749 23550 603 41 0 24708 0
vsize: 98996
[startup+270.007 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 24695 0 0 0 26929 72 0 0 25 0 1 0 549938624 102846464 23906 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25109 23906 603 41 0 25068 0
vsize: 100436
[startup+280.008 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 25183 0 0 0 27927 74 0 0 25 0 1 0 549938624 104873984 24394 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25604 24394 603 41 0 25563 0
vsize: 102416
[startup+290.009 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 25630 0 0 0 28927 75 0 0 25 0 1 0 549938624 106631168 24841 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26033 24841 603 41 0 25992 0
vsize: 104132
[startup+300.009 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 25912 0 0 0 29925 77 0 0 25 0 1 0 549938624 107708416 25123 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26296 25123 603 41 0 26255 0
vsize: 105184
[startup+310.009 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 26186 0 0 0 30924 78 0 0 25 0 1 0 549938624 108789760 25397 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26560 25397 603 41 0 26519 0
vsize: 106240
[startup+320.01 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 26457 0 0 0 31924 79 0 0 25 0 1 0 549938624 110014464 25668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26859 25668 603 41 0 26818 0
vsize: 107436
[startup+330.011 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 26697 0 0 0 32923 79 0 0 25 0 1 0 549938624 110956544 25908 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27089 25908 603 41 0 27048 0
vsize: 108356
[startup+340.011 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 26944 0 0 0 33922 81 0 0 25 0 1 0 549938624 112037888 26155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27353 26155 603 41 0 27312 0
vsize: 109412
[startup+350.011 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 27168 0 0 0 34921 82 0 0 25 0 1 0 549938624 112844800 26379 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27550 26379 603 41 0 27509 0
vsize: 110200
[startup+360.012 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 27396 0 0 0 35921 82 0 0 25 0 1 0 549938624 113790976 26607 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27781 26607 603 41 0 27740 0
vsize: 111124
[startup+370.012 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 27630 0 0 0 36920 84 0 0 25 0 1 0 549938624 114790400 26841 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28025 26841 603 41 0 27984 0
vsize: 112100
[startup+380.012 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 27844 0 0 0 37919 85 0 0 25 0 1 0 549938624 115642368 27055 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28233 27055 603 41 0 28192 0
vsize: 112932
[startup+390.013 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 28089 0 0 0 38918 86 0 0 25 0 1 0 549938624 116744192 27300 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28502 27300 603 41 0 28461 0
vsize: 114008
[startup+400.013 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 28333 0 0 0 39917 87 0 0 25 0 1 0 549938624 117678080 27544 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28730 27544 603 41 0 28689 0
vsize: 114920
[startup+410.012 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 28558 0 0 0 40916 88 0 0 25 0 1 0 549938624 118648832 27769 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28967 27769 603 41 0 28926 0
vsize: 115868
[startup+420.012 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 28821 0 0 0 41915 90 0 0 25 0 1 0 549938624 119730176 28032 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29231 28032 603 41 0 29190 0
vsize: 116924
[startup+430.013 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 29125 0 0 0 42914 91 0 0 25 0 1 0 549938624 120926208 28336 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29523 28336 603 41 0 29482 0
vsize: 118092
[startup+440.013 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17136
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 29423 0 0 0 43913 92 0 0 25 0 1 0 549938624 122130432 28634 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29817 28634 603 41 0 29776 0
vsize: 119268
[startup+450.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 29705 0 0 0 44911 94 0 0 25 0 1 0 549938624 123383808 28916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30123 28916 603 41 0 30082 0
vsize: 120492
[startup+460.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 29955 0 0 0 45911 94 0 0 25 0 1 0 549938624 124325888 29166 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30353 29166 603 41 0 30312 0
vsize: 121412
[startup+470.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 30222 0 0 0 46910 96 0 0 25 0 1 0 549938624 125530112 29433 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30647 29433 603 41 0 30606 0
vsize: 122588
[startup+480.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 30425 0 0 0 47909 96 0 0 25 0 1 0 549938624 126328832 29636 4294967295 134512640 134672761 3221224544 3221223712 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30842 29636 603 41 0 30801 0
vsize: 123368
[startup+490.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 30618 0 0 0 48909 97 0 0 25 0 1 0 549938624 126996480 29829 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31005 29829 603 41 0 30964 0
vsize: 124020
[startup+500.015 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 30809 0 0 0 49908 98 0 0 25 0 1 0 549938624 127934464 30020 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31234 30020 603 41 0 31193 0
vsize: 124936
[startup+510.015 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 30974 0 0 0 50907 99 0 0 25 0 1 0 549938624 128614400 30185 4294967295 134512640 134672761 3221224544 3221223680 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31400 30185 603 41 0 31359 0
vsize: 125600
[startup+520.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 31124 0 0 0 51907 99 0 0 25 0 1 0 549938624 129155072 30335 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31532 30335 603 41 0 31491 0
vsize: 126128
[startup+530.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 31298 0 0 0 52906 100 0 0 25 0 1 0 549938624 129826816 30509 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31696 30509 603 41 0 31655 0
vsize: 126784
[startup+540.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 31456 0 0 0 53906 101 0 0 25 0 1 0 549938624 130494464 30667 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31859 30667 603 41 0 31818 0
vsize: 127436
[startup+550.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 31592 0 0 0 54905 102 0 0 25 0 1 0 549938624 131031040 30803 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31990 30803 603 41 0 31949 0
vsize: 127960
[startup+560.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 31752 0 0 0 55904 103 0 0 25 0 1 0 549938624 131702784 30963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32154 30963 603 41 0 32113 0
vsize: 128616
[startup+570.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 31902 0 0 0 56903 104 0 0 25 0 1 0 549938624 133353472 31113 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32557 31113 603 41 0 32516 0
vsize: 130228
[startup+580.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 32024 0 0 0 57902 105 0 0 25 0 1 0 549938624 133894144 31235 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32689 31235 603 41 0 32648 0
vsize: 130756
[startup+590.013 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 32212 0 0 0 58902 106 0 0 25 0 1 0 549938624 134664192 31423 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32877 31423 603 41 0 32836 0
vsize: 131508
[startup+600.013 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 32358 0 0 0 59901 106 0 0 25 0 1 0 549938624 135331840 31569 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33040 31569 603 41 0 32999 0
vsize: 132160
[startup+610.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 32503 0 0 0 60900 107 0 0 25 0 1 0 549938624 135868416 31714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33171 31714 603 41 0 33130 0
vsize: 132684
[startup+620.013 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 32649 0 0 0 61900 108 0 0 25 0 1 0 549938624 136413184 31860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33304 31860 603 41 0 33263 0
vsize: 133216
[startup+630.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 32772 0 0 0 62900 108 0 0 25 0 1 0 549938624 137080832 31983 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33467 31983 603 41 0 33426 0
vsize: 133868
[startup+640.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 32891 0 0 0 63899 109 0 0 25 0 1 0 549938624 137486336 32102 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33566 32102 603 41 0 33525 0
vsize: 134264
[startup+650.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 33055 0 0 0 64899 110 0 0 25 0 1 0 549938624 138285056 32266 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33761 32266 603 41 0 33720 0
vsize: 135044
[startup+660.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 33200 0 0 0 65898 110 0 0 25 0 1 0 549938624 138821632 32411 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33892 32411 603 41 0 33851 0
vsize: 135568
[startup+670.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 33378 0 0 0 66898 111 0 0 25 0 1 0 549938624 139489280 32589 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34055 32589 603 41 0 34014 0
vsize: 136220
[startup+680.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 33546 0 0 0 67898 111 0 0 25 0 1 0 549938624 140247040 32757 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34240 32757 603 41 0 34199 0
vsize: 136960
[startup+690.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 33677 0 0 0 68897 112 0 0 25 0 1 0 549938624 140881920 32888 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34395 32888 603 41 0 34354 0
vsize: 137580
[startup+700.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 33814 0 0 0 69896 113 0 0 25 0 1 0 549938624 141414400 33025 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34525 33025 603 41 0 34484 0
vsize: 138100
[startup+710.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 33946 0 0 0 70895 114 0 0 25 0 1 0 549938624 141950976 33157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34656 33157 603 41 0 34615 0
vsize: 138624
[startup+720.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 34072 0 0 0 71894 116 0 0 25 0 1 0 549938624 142483456 33283 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34786 33283 603 41 0 34745 0
vsize: 139144
[startup+730.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 34405 0 0 0 72893 117 0 0 25 0 1 0 549938624 143835136 33616 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35116 33616 603 41 0 35075 0
vsize: 140464
[startup+740.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 34690 0 0 0 73892 118 0 0 25 0 1 0 549938624 145088512 33901 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35422 33901 603 41 0 35381 0
vsize: 141688
[startup+750.014 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 34789 0 0 0 74891 119 0 0 25 0 1 0 549938624 145502208 34000 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35523 34000 603 41 0 35482 0
vsize: 142092
[startup+760.015 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 34871 0 0 0 75891 119 0 0 25 0 1 0 549938624 145772544 34082 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35589 34082 603 41 0 35548 0
vsize: 142356
[startup+770.015 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 34975 0 0 0 76890 120 0 0 25 0 1 0 549938624 146206720 34186 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35695 34186 603 41 0 35654 0
vsize: 142780
[startup+780.015 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 35069 0 0 0 77890 121 0 0 25 0 1 0 549938624 146608128 34280 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35793 34280 603 41 0 35752 0
vsize: 143172
[startup+790.016 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 35145 0 0 0 78889 122 0 0 25 0 1 0 549938624 147042304 34356 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35899 34356 603 41 0 35858 0
vsize: 143596
[startup+800.016 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 35251 0 0 0 79889 123 0 0 25 0 1 0 549938624 147439616 34462 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35996 34462 603 41 0 35955 0
vsize: 143984
[startup+810.016 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 35358 0 0 0 80888 123 0 0 25 0 1 0 549938624 147849216 34569 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36096 34569 603 41 0 36055 0
vsize: 144384
[startup+820.016 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 35493 0 0 0 81887 124 0 0 25 0 1 0 549938624 148422656 34704 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36236 34704 603 41 0 36195 0
vsize: 144944
[startup+830.016 s]
Raw data (loadavg): 1.08 1.02 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 36193 0 0 0 82885 127 0 0 25 0 1 0 549938624 151252992 35404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36927 35404 603 41 0 36886 0
vsize: 147708
[startup+840.017 s]
Raw data (loadavg): 1.07 1.02 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 36833 0 0 0 83883 129 0 0 25 0 1 0 549938624 153817088 36044 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37553 36044 603 41 0 37512 0
vsize: 150212
[startup+850.016 s]
Raw data (loadavg): 1.06 1.01 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 37456 0 0 0 84883 129 0 0 25 0 1 0 549938624 156364800 36667 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38175 36667 603 41 0 38134 0
vsize: 152700
[startup+860.017 s]
Raw data (loadavg): 1.05 1.01 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 38038 0 0 0 85881 132 0 0 25 0 1 0 549938624 158785536 37249 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38766 37249 603 41 0 38725 0
vsize: 155064
[startup+870.017 s]
Raw data (loadavg): 1.04 1.01 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 38678 0 0 0 86879 134 0 0 25 0 1 0 549938624 161337344 37889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39389 37889 603 41 0 39348 0
vsize: 157556
[startup+880.016 s]
Raw data (loadavg): 1.03 1.01 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 39265 0 0 0 87877 135 0 0 25 0 1 0 549938624 163766272 38476 4294967295 134512640 134672761 3221224544 3221223484 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39982 38476 603 41 0 39941 0
vsize: 159928
[startup+890.016 s]
Raw data (loadavg): 1.03 1.01 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 39854 0 0 0 88876 137 0 0 25 0 1 0 549938624 166195200 39065 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40575 39065 603 41 0 40534 0
vsize: 162300
[startup+900.016 s]
Raw data (loadavg): 1.02 1.01 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 40404 0 0 0 89874 139 0 0 25 0 1 0 549938624 168378368 39615 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41108 39615 603 41 0 41067 0
vsize: 164432
[startup+910.017 s]
Raw data (loadavg): 1.02 1.01 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 40916 0 0 0 90872 141 0 0 25 0 1 0 549938624 170528768 40127 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41633 40127 603 41 0 41592 0
vsize: 166532
[startup+920.016 s]
Raw data (loadavg): 1.02 1.01 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 41449 0 0 0 91871 142 0 0 25 0 1 0 549938624 172679168 40660 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42158 40660 603 41 0 42117 0
vsize: 168632
[startup+930.016 s]
Raw data (loadavg): 1.01 1.01 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 42043 0 0 0 92869 144 0 0 25 0 1 0 549938624 175095808 41254 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42748 41254 603 41 0 42707 0
vsize: 170992
[startup+940.017 s]
Raw data (loadavg): 1.01 1.01 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 42153 0 0 0 93869 145 0 0 25 0 1 0 549938624 175636480 41364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42880 41364 603 41 0 42839 0
vsize: 171520
[startup+950.016 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 42281 0 0 0 94868 146 0 0 25 0 1 0 549938624 176168960 41492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43010 41492 603 41 0 42969 0
vsize: 172040
[startup+960.016 s]
Raw data (loadavg): 1.01 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 42421 0 0 0 95867 147 0 0 25 0 1 0 549938624 176705536 41632 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43141 41632 603 41 0 43100 0
vsize: 172564
[startup+970.016 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 42544 0 0 0 96867 147 0 0 25 0 1 0 549938624 177106944 41755 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43239 41755 603 41 0 43198 0
vsize: 172956
[startup+980.015 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 42671 0 0 0 97866 148 0 0 25 0 1 0 549938624 177672192 41882 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43377 41882 603 41 0 43336 0
vsize: 173508
[startup+990.016 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 42796 0 0 0 98866 149 0 0 25 0 1 0 549938624 178212864 42007 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43509 42007 603 41 0 43468 0
vsize: 174036
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.99 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 42966 0 0 0 99865 149 0 0 25 0 1 0 549938624 178900992 42177 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43677 42177 603 41 0 43636 0
vsize: 174708
[startup+1010.02 s]
Raw data (loadavg): 1.07 1.02 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 43108 0 0 0 100865 150 0 0 25 0 1 0 549938624 179470336 42319 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43816 42319 603 41 0 43775 0
vsize: 175264
[startup+1020.02 s]
Raw data (loadavg): 1.06 1.02 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 43271 0 0 0 101864 151 0 0 25 0 1 0 549938624 180146176 42482 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43981 42482 603 41 0 43940 0
vsize: 175924
[startup+1030.02 s]
Raw data (loadavg): 1.05 1.01 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 43451 0 0 0 102863 152 0 0 25 0 1 0 549938624 180813824 42662 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44144 42662 603 41 0 44103 0
vsize: 176576
[startup+1040.02 s]
Raw data (loadavg): 1.04 1.01 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 43625 0 0 0 103862 153 0 0 25 0 1 0 549938624 181608448 42836 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44338 42836 603 41 0 44297 0
vsize: 177352
[startup+1050.02 s]
Raw data (loadavg): 1.04 1.01 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 43786 0 0 0 104862 154 0 0 25 0 1 0 549938624 182145024 42997 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44469 42997 603 41 0 44428 0
vsize: 177876
[startup+1060.02 s]
Raw data (loadavg): 1.03 1.01 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 43960 0 0 0 105861 154 0 0 25 0 1 0 549938624 182820864 43171 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44634 43171 603 41 0 44593 0
vsize: 178536
[startup+1070.02 s]
Raw data (loadavg): 1.03 1.01 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 44112 0 0 0 106860 156 0 0 25 0 1 0 549938624 183492608 43323 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44798 43323 603 41 0 44757 0
vsize: 179192
[startup+1080.02 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 44283 0 0 0 107859 157 0 0 25 0 1 0 549938624 184295424 43494 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44994 43494 603 41 0 44953 0
vsize: 179976
[startup+1090.02 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 44403 0 0 0 108858 158 0 0 25 0 1 0 549938624 184832000 43614 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45125 43614 603 41 0 45084 0
vsize: 180500
[startup+1100.02 s]
Raw data (loadavg): 1.01 1.01 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 44565 0 0 0 109857 159 0 0 25 0 1 0 549938624 185524224 43776 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45294 43776 603 41 0 45253 0
vsize: 181176
[startup+1110.02 s]
Raw data (loadavg): 1.01 1.01 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 44702 0 0 0 110857 159 0 0 25 0 1 0 549938624 186060800 43913 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45425 43913 603 41 0 45384 0
vsize: 181700
[startup+1120.02 s]
Raw data (loadavg): 1.01 1.01 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 44844 0 0 0 111857 160 0 0 25 0 1 0 549938624 186626048 44055 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45563 44055 603 41 0 45522 0
vsize: 182252
[startup+1130.02 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 44973 0 0 0 112856 161 0 0 25 0 1 0 549938624 187174912 44184 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45697 44184 603 41 0 45656 0
vsize: 182788
[startup+1140.02 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 45115 0 0 0 113855 162 0 0 25 0 1 0 549938624 187809792 44326 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45852 44326 603 41 0 45811 0
vsize: 183408
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 45237 0 0 0 114855 162 0 0 25 0 1 0 549938624 188211200 44448 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45950 44448 603 41 0 45909 0
vsize: 183800
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 45362 0 0 0 115854 164 0 0 25 0 1 0 549938624 188747776 44573 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46081 44573 603 41 0 46040 0
vsize: 184324
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 45486 0 0 0 116853 164 0 0 25 0 1 0 549938624 189333504 44697 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46224 44697 603 41 0 46183 0
vsize: 184896
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 45613 0 0 0 117852 165 0 0 25 0 1 0 549938624 189767680 44824 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46330 44824 603 41 0 46289 0
vsize: 185320
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 45730 0 0 0 118851 167 0 0 25 0 1 0 549938624 190300160 44941 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46460 44941 603 41 0 46419 0
vsize: 185840
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 17138
Raw data (stat): 17081 (minisat+) R 17080 27565 27564 0 -1 0 45863 0 0 0 119850 168 0 0 25 0 1 0 549938624 190836736 45074 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46591 45074 603 41 0 46550 0
vsize: 186364
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 1.00 1/54 17138
Raw data (stat): 17081 (minisat+) Z 17080 27565 27564 0 -1 12 45865 0 0 0 119851 176 0 0 25 0 1 0 549938624 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.28
CPU user time (s): 1198.51
CPU system time (s): 1.76573
CPU usage (%): 100.014
Max. virtual memory (Kb): 186364
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####