PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-liu.opb
MD5SUM	216e30ba4678325d93810a111dd11436
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	451651
Optimality of the best value was proved	NO
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	2143744
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	6434814
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	2429
Total number of constraints	3267
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	1089
Number of constraints which are nor clauses,nor cardinality constraints	2178
Minimum length of a constraint	1
Maximum length of a constraint	43
Trace number 18732

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-21 16:16:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17612 boxname=wulflinc31 idbench=1355 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  216e30ba4678325d93810a111dd11436  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-liu.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-liu.opb /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-liu.opb
IDLAUNCH: 17612
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        340456 kB
Buffers:         34484 kB
Cached:         631308 kB
SwapCached:        540 kB
Active:         142868 kB
Inactive:       524856 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        340204 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            20852 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 16:36:20 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 17612 7 1200.26 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2178 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[2177]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2176]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[2175]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[2174]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[2173]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2172]---> Adder-cost: 77   maxlim: 1078014   bits: 22/21
c ---[2171]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2170]---> Adder-cost: 77   maxlim: 1078014   bits: 22/21
c ---[2169]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2168]---> Adder-cost: 98   maxlim: 1070846   bits: 22/21
c ---[2167]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2166]---> Adder-cost: 98   maxlim: 1070846   bits: 22/21
c ---[2165]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2164]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2163]---> Adder-cost: 71   maxlim: 1074430   bits: 22/21
c ---[2162]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2161]---> Adder-cost: 71   maxlim: 1074430   bits: 22/21
c ---[2160]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2159]---> Adder-cost: 85   maxlim: 1095934   bits: 22/21
c ---[2158]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2157]---> Adder-cost: 85   maxlim: 1095934   bits: 22/21
c ---[2156]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2155]---> Adder-cost: 86   maxlim: 1063678   bits: 22/21
c ---[2154]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2153]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[2152]---> Adder-cost: 86   maxlim: 1063678   bits: 22/21
c ---[2151]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2150]---> Adder-cost: 98   maxlim: 1064702   bits: 22/21
c ---[2149]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2148]---> Adder-cost: 98   maxlim: 1064702   bits: 22/21
c ---[2147]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2146]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[2145]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2144]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[2143]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2142]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2141]---> Adder-cost: 79   maxlim: 1082622   bits: 22/21
c ---[2140]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2139]---> Adder-cost: 79   maxlim: 1082622   bits: 22/21
c ---[2138]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2137]---> Adder-cost: 89   maxlim: 1069054   bits: 22/21
c ---[2136]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2135]---> Adder-cost: 89   maxlim: 1069054   bits: 22/21
c ---[2134]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2133]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[2132]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2131]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[2130]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[2129]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2128]---> Adder-cost: 81   maxlim: 1073662   bits: 22/21
c ---[2127]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2126]---> Adder-cost: 81   maxlim: 1073662   bits: 22/21
c ---[2125]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2124]---> Adder-cost: 75   maxlim: 1112062   bits: 22/21
c ---[2123]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2122]---> Adder-cost: 75   maxlim: 1112062   bits: 22/21
c ---[2121]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2120]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2119]---> Adder-cost: 81   maxlim: 1100542   bits: 22/21
c ---[2118]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2117]---> Adder-cost: 81   maxlim: 1100542   bits: 22/21
c ---[2116]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2115]---> Adder-cost: 83   maxlim: 1070846   bits: 22/21
c ---[2114]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2113]---> Adder-cost: 83   maxlim: 1070846   bits: 22/21
c ---[2112]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2111]---> Adder-cost: 100   maxlim: 1063678   bits: 22/21
c ---[2110]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2109]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[2108]---> Adder-cost: 100   maxlim: 1063678   bits: 22/21
c ---[2107]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2106]---> Adder-cost: 77   maxlim: 1071870   bits: 22/21
c ---[2105]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2104]---> Adder-cost: 77   maxlim: 1071870   bits: 22/21
c ---[2103]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2102]---> Adder-cost: 85   maxlim: 1069054   bits: 22/21
c ---[2101]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2100]---> Adder-cost: 85   maxlim: 1069054   bits: 22/21
c ---[2099]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2098]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2097]---> Adder-cost: 73   maxlim: 1096958   bits: 22/21
c ---[2096]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2095]---> Adder-cost: 73   maxlim: 1096958   bits: 22/21
c ---[2094]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2093]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[2092]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2091]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[2090]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2089]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[2088]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2087]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[2086]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[2085]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2084]---> Adder-cost: 60   maxlim: 1075454   bits: 22/21
c ---[2083]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2082]---> Adder-cost: 60   maxlim: 1075454   bits: 22/21
c ---[2081]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2080]---> Adder-cost: 77   maxlim: 1071870   bits: 22/21
c ---[2079]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2078]---> Adder-cost: 77   maxlim: 1071870   bits: 22/21
c ---[2077]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2076]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2075]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[2074]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2073]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[2072]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2071]---> Adder-cost: 64   maxlim: 1078014   bits: 22/21
c ---[2070]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2069]---> Adder-cost: 64   maxlim: 1078014   bits: 22/21
c ---[2068]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2067]---> Adder-cost: 87   maxlim: 1070846   bits: 22/21
c ---[2066]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2065]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2064]---> Adder-cost: 73   maxlim: 1075454   bits: 22/21
c ---[2063]---> Adder-cost: 87   maxlim: 1070846   bits: 22/21
c ---[2062]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2061]---> Adder-cost: 85   maxlim: 1095934   bits: 22/21
c ---[2060]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2059]---> Adder-cost: 85   maxlim: 1095934   bits: 22/21
c ---[2058]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2057]---> Adder-cost: 86   maxlim: 1063678   bits: 22/21
c ---[2056]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2055]---> Adder-cost: 86   maxlim: 1063678   bits: 22/21
c ---[2054]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2053]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2052]---> Adder-cost: 98   maxlim: 1064702   bits: 22/21
c ---[2051]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2050]---> Adder-cost: 98   maxlim: 1064702   bits: 22/21
c ---[2049]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2048]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[2047]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2046]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[2045]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2044]---> Adder-cost: 79   maxlim: 1082622   bits: 22/21
c ---[2043]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2042]---> Adder-cost: 73   maxlim: 1075454   bits: 22/21
c ---[2041]---> Adder-cost: 79   maxlim: 1082622   bits: 22/21
c ---[2040]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2039]---> Adder-cost: 89   maxlim: 1069054   bits: 22/21
c ---[2038]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2037]---> Adder-cost: 89   maxlim: 1069054   bits: 22/21
c ---[2036]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2035]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[2034]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2033]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[2032]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2031]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2030]---> Adder-cost: 81   maxlim: 1073662   bits: 22/21
c ---[2029]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2028]---> Adder-cost: 81   maxlim: 1073662   bits: 22/21
c ---[2027]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2026]---> Adder-cost: 75   maxlim: 1112062   bits: 22/21
c ---[2025]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2024]---> Adder-cost: 75   maxlim: 1112062   bits: 22/21
c ---[2023]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2022]---> Adder-cost: 81   maxlim: 1100542   bits: 22/21
c ---[2021]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2020]---> Adder-cost: 92   maxlim: 1071870   bits: 22/21
c ---[2019]---> Adder-cost: 81   maxlim: 1100542   bits: 22/21
c ---[2018]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2017]---> Adder-cost: 83   maxlim: 1070846   bits: 22/21
c ---[2016]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2015]---> Adder-cost: 83   maxlim: 1070846   bits: 22/21
c ---[2014]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2013]---> Adder-cost: 100   maxlim: 1063678   bits: 22/21
c ---[2012]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2011]---> Adder-cost: 100   maxlim: 1063678   bits: 22/21
c ---[2010]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2009]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[2008]---> Adder-cost: 77   maxlim: 1071870   bits: 22/21
c ---[2007]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2006]---> Adder-cost: 77   maxlim: 1071870   bits: 22/21
c ---[2005]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2004]---> Adder-cost: 85   maxlim: 1069054   bits: 22/21
c ---[2003]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2002]---> Adder-cost: 85   maxlim: 1069054   bits: 22/21
c ---[2001]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[2000]---> Adder-cost: 73   maxlim: 1096958   bits: 22/21
c ---[1999]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1998]---> Adder-cost: 92   maxlim: 1071870   bits: 22/21
c ---[1997]---> Adder-cost: 73   maxlim: 1096958   bits: 22/21
c ---[1996]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1995]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1994]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1993]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1992]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1991]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1990]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1989]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1988]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1987]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[1986]---> Adder-cost: 60   maxlim: 1075454   bits: 22/21
c ---[1985]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1984]---> Adder-cost: 60   maxlim: 1075454   bits: 22/21
c ---[1983]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1982]---> Adder-cost: 77   maxlim: 1071870   bits: 22/21
c ---[1981]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1980]---> Adder-cost: 77   maxlim: 1071870   bits: 22/21
c ---[1979]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1978]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[1977]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1976]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[1975]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[1974]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1973]---> Adder-cost: 64   maxlim: 1078014   bits: 22/21
c ---[1972]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1971]---> Adder-cost: 64   maxlim: 1078014   bits: 22/21
c ---[1970]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1969]---> Adder-cost: 87   maxlim: 1070846   bits: 22/21
c ---[1968]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1967]---> Adder-cost: 87   maxlim: 1070846   bits: 22/21
c ---[1966]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1965]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[1964]---> Adder-cost: 105   maxlim: 1063678   bits: 22/21
c ---[1963]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1962]---> Adder-cost: 105   maxlim: 1063678   bits: 22/21
c ---[1961]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1960]---> Adder-cost: 117   maxlim: 1064702   bits: 22/21
c ---[1959]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1958]---> Adder-cost: 117   maxlim: 1064702   bits: 22/21
c ---[1957]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1956]---> Adder-cost: 86   maxlim: 1091582   bits: 22/21
c ---[1955]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1954]---> Adder-cost: 85   maxlim: 1120254   bits: 22/21
c ---[1953]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[1952]---> Adder-cost: 86   maxlim: 1091582   bits: 22/21
c ---[1951]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1950]---> Adder-cost: 76   maxlim: 1082622   bits: 22/21
c ---[1949]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1948]---> Adder-cost: 76   maxlim: 1082622   bits: 22/21
c ---[1947]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1946]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1945]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1944]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1943]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1942]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[1941]---> Adder-cost: 79   maxlim: 1086206   bits: 22/21
c ---[1940]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1939]---> Adder-cost: 79   maxlim: 1086206   bits: 22/21
c ---[1938]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1937]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1936]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1935]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1934]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1933]---> Adder-cost: 75   maxlim: 1112062   bits: 22/21
c ---[1932]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1931]---> Adder-cost: 77   maxlim: 1078014   bits: 22/21
c ---[1930]---> Adder-cost: 75   maxlim: 1112062   bits: 22/21
c ---[1929]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1928]---> Adder-cost: 82   maxlim: 1100542   bits: 22/21
c ---[1927]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1926]---> Adder-cost: 82   maxlim: 1100542   bits: 22/21
c ---[1925]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1924]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1923]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1922]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1921]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1920]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[1919]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1918]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1917]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1916]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1915]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1914]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1913]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1912]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1911]---> Adder-cost: 114   maxlim: 1069054   bits: 22/21
c ---[1910]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1909]---> Adder-cost: 77   maxlim: 1078014   bits: 22/21
c ---[1908]---> Adder-cost: 114   maxlim: 1069054   bits: 22/21
c ---[1907]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1906]---> Adder-cost: 73   maxlim: 1096958   bits: 22/21
c ---[1905]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1904]---> Adder-cost: 73   maxlim: 1096958   bits: 22/21
c ---[1903]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1902]---> Adder-cost: 81   maxlim: 1091582   bits: 22/21
c ---[1901]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1900]---> Adder-cost: 81   maxlim: 1091582   bits: 22/21
c ---[1899]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1898]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[1897]---> Adder-cost: 85   maxlim: 1096958   bits: 22/21
c ---[1896]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1895]---> Adder-cost: 85   maxlim: 1096958   bits: 22/21
c ---[1894]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1893]---> Adder-cost: 72   maxlim: 1075454   bits: 22/21
c ---[1892]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1891]---> Adder-cost: 72   maxlim: 1075454   bits: 22/21
c ---[1890]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1889]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1888]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1887]---> Adder-cost: 98   maxlim: 1070846   bits: 22/21
c ---[1886]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1885]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1884]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[1883]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1882]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[1881]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1880]---> Adder-cost: 78   maxlim: 1078014   bits: 22/21
c ---[1879]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1878]---> Adder-cost: 78   maxlim: 1078014   bits: 22/21
c ---[1877]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1876]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[1875]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[1874]---> Adder-cost: 87   maxlim: 1095934   bits: 22/21
c ---[1873]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[1872]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1871]---> Adder-cost: 79   maxlim: 1064702   bits: 22/21
c ---[1870]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1869]---> Adder-cost: 79   maxlim: 1064702   bits: 22/21
c ---[1868]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1867]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1866]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1865]---> Adder-cost: 98   maxlim: 1070846   bits: 22/21
c ---[1864]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1863]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1862]---> Adder-cost: 81   maxlim: 1082622   bits: 22/21
c ---[1861]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1860]---> Adder-cost: 81   maxlim: 1082622   bits: 22/21
c ---[1859]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1858]---> Adder-cost: 98   maxlim: 1069054   bits: 22/21
c ---[1857]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1856]---> Adder-cost: 98   maxlim: 1069054   bits: 22/21
c ---[1855]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1854]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1853]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[1852]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1851]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[1850]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1849]---> Adder-cost: 94   maxlim: 1073662   bits: 22/21
c ---[1848]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1847]---> Adder-cost: 94   maxlim: 1073662   bits: 22/21
c ---[1846]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1845]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1844]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1843]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[1842]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[1841]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1840]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1839]---> Adder-cost: 81   maxlim: 1100542   bits: 22/21
c ---[1838]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1837]---> Adder-cost: 81   maxlim: 1100542   bits: 22/21
c ---[1836]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1835]---> Adder-cost: 94   maxlim: 1070846   bits: 22/21
c ---[1834]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1833]---> Adder-cost: 94   maxlim: 1070846   bits: 22/21
c ---[1832]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1831]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1830]---> Adder-cost: 96   maxlim: 1063678   bits: 22/21
c ---[1829]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1828]---> Adder-cost: 96   maxlim: 1063678   bits: 22/21
c ---[1827]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1826]---> Adder-cost: 82   maxlim: 1071870   bits: 22/21
c ---[1825]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1824]---> Adder-cost: 82   maxlim: 1071870   bits: 22/21
c ---[1823]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1822]---> Adder-cost: 100   maxlim: 1069054   bits: 22/21
c ---[1821]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1820]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[1819]---> Adder-cost: 100   maxlim: 1069054   bits: 22/21
c ---[1818]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1817]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[1816]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1815]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[1814]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1813]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1812]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1811]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1810]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1809]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1808]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1807]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1806]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1805]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1804]---> Adder-cost: 73   maxlim: 1075454   bits: 22/21
c ---[1803]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1802]---> Adder-cost: 73   maxlim: 1075454   bits: 22/21
c ---[1801]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1800]---> Adder-cost: 88   maxlim: 1071870   bits: 22/21
c ---[1799]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1798]---> Adder-cost: 86   maxlim: 1120254   bits: 22/21
c ---[1797]---> Adder-cost: 88   maxlim: 1071870   bits: 22/21
c ---[1796]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1795]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[1794]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1793]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[1792]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1791]---> Adder-cost: 77   maxlim: 1078014   bits: 22/21
c ---[1790]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1789]---> Adder-cost: 77   maxlim: 1078014   bits: 22/21
c ---[1788]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1787]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1786]---> Adder-cost: 98   maxlim: 1070846   bits: 22/21
c ---[1785]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1784]---> Adder-cost: 98   maxlim: 1070846   bits: 22/21
c ---[1783]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1782]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[1781]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1780]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[1779]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1778]---> Adder-cost: 81   maxlim: 1082622   bits: 22/21
c ---[1777]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1776]---> Adder-cost: 86   maxlim: 1120254   bits: 22/21
c ---[1775]---> Adder-cost: 81   maxlim: 1082622   bits: 22/21
c ---[1774]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1773]---> Adder-cost: 97   maxlim: 1069054   bits: 22/21
c ---[1772]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1771]---> Adder-cost: 97   maxlim: 1069054   bits: 22/21
c ---[1770]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1769]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[1768]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1767]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[1766]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1765]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1764]---> Adder-cost: 94   maxlim: 1073662   bits: 22/21
c ---[1763]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1762]---> Adder-cost: 94   maxlim: 1073662   bits: 22/21
c ---[1761]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1760]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1759]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1758]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1757]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1756]---> Adder-cost: 80   maxlim: 1100542   bits: 22/21
c ---[1755]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1754]---> Adder-cost: 90   maxlim: 1088766   bits: 22/21
c ---[1753]---> Adder-cost: 80   maxlim: 1100542   bits: 22/21
c ---[1752]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1751]---> Adder-cost: 93   maxlim: 1070846   bits: 22/21
c ---[1750]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1749]---> Adder-cost: 93   maxlim: 1070846   bits: 22/21
c ---[1748]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1747]---> Adder-cost: 96   maxlim: 1063678   bits: 22/21
c ---[1746]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1745]---> Adder-cost: 96   maxlim: 1063678   bits: 22/21
c ---[1744]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1743]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1742]---> Adder-cost: 84   maxlim: 1071870   bits: 22/21
c ---[1741]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1740]---> Adder-cost: 84   maxlim: 1071870   bits: 22/21
c ---[1739]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1738]---> Adder-cost: 100   maxlim: 1069054   bits: 22/21
c ---[1737]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1736]---> Adder-cost: 100   maxlim: 1069054   bits: 22/21
c ---[1735]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1734]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[1733]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1732]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[1731]---> Adder-cost: 90   maxlim: 1088766   bits: 22/21
c ---[1730]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[1729]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1728]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1727]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1726]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1725]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1724]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1723]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1722]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1721]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1720]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1719]---> Adder-cost: 73   maxlim: 1075454   bits: 22/21
c ---[1718]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1717]---> Adder-cost: 73   maxlim: 1075454   bits: 22/21
c ---[1716]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1715]---> Adder-cost: 88   maxlim: 1071870   bits: 22/21
c ---[1714]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1713]---> Adder-cost: 88   maxlim: 1071870   bits: 22/21
c ---[1712]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1711]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[1710]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1709]---> Adder-cost: 90   maxlim: 1088766   bits: 22/21
c ---[1708]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[1707]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1706]---> Adder-cost: 77   maxlim: 1078014   bits: 22/21
c ---[1705]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1704]---> Adder-cost: 77   maxlim: 1078014   bits: 22/21
c ---[1703]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1702]---> Adder-cost: 97   maxlim: 1070846   bits: 22/21
c ---[1701]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1700]---> Adder-cost: 97   maxlim: 1070846   bits: 22/21
c ---[1699]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1698]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1697]---> Adder-cost: 82   maxlim: 1082622   bits: 22/21
c ---[1696]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1695]---> Adder-cost: 82   maxlim: 1082622   bits: 22/21
c ---[1694]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1693]---> Adder-cost: 116   maxlim: 1069054   bits: 22/21
c ---[1692]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1691]---> Adder-cost: 116   maxlim: 1069054   bits: 22/21
c ---[1690]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1689]---> Adder-cost: 82   maxlim: 1086206   bits: 22/21
c ---[1688]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1687]---> Adder-cost: 90   maxlim: 1088766   bits: 22/21
c ---[1686]---> Adder-cost: 82   maxlim: 1086206   bits: 22/21
c ---[1685]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1684]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1683]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1682]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1681]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1680]---> Adder-cost: 78   maxlim: 1112062   bits: 22/21
c ---[1679]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1678]---> Adder-cost: 78   maxlim: 1112062   bits: 22/21
c ---[1677]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1676]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1675]---> Adder-cost: 81   maxlim: 1100542   bits: 22/21
c ---[1674]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1673]---> Adder-cost: 81   maxlim: 1100542   bits: 22/21
c ---[1672]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1671]---> Adder-cost: 112   maxlim: 1070846   bits: 22/21
c ---[1670]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1669]---> Adder-cost: 112   maxlim: 1070846   bits: 22/21
c ---[1668]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1667]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1666]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1665]---> Adder-cost: 86   maxlim: 1093374   bits: 22/21
c ---[1664]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1663]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1662]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[1661]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1660]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[1659]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1658]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1657]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1656]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1655]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1654]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1653]---> Adder-cost: 78   maxlim: 1096958   bits: 22/21
c ---[1652]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1651]---> Adder-cost: 78   maxlim: 1096958   bits: 22/21
c ---[1650]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1649]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[1648]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1647]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[1646]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1645]---> Adder-cost: 88   maxlim: 1096958   bits: 22/21
c ---[1644]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1643]---> Adder-cost: 86   maxlim: 1093374   bits: 22/21
c ---[1642]---> Adder-cost: 88   maxlim: 1096958   bits: 22/21
c ---[1641]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1640]---> Adder-cost: 74   maxlim: 1075454   bits: 22/21
c ---[1639]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1638]---> Adder-cost: 74   maxlim: 1075454   bits: 22/21
c ---[1637]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1636]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1635]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1634]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1633]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1632]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1631]---> Adder-cost: 90   maxlim: 1088766   bits: 22/21
c ---[1630]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1629]---> Adder-cost: 90   maxlim: 1088766   bits: 22/21
c ---[1628]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1627]---> Adder-cost: 76   maxlim: 1078014   bits: 22/21
c ---[1626]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1625]---> Adder-cost: 76   maxlim: 1078014   bits: 22/21
c ---[1624]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1623]---> Adder-cost: 114   maxlim: 1070846   bits: 22/21
c ---[1622]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[1621]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[1620]---> Adder-cost: 82   maxlim: 1086206   bits: 22/21
c ---[1619]---> Adder-cost: 114   maxlim: 1070846   bits: 22/21
c ---[1618]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1617]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1616]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1615]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1614]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1613]---> Adder-cost: 77   maxlim: 1086206   bits: 22/21
c ---[1612]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1611]---> Adder-cost: 77   maxlim: 1086206   bits: 22/21
c ---[1610]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1609]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1608]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1607]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1606]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1605]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1604]---> Adder-cost: 73   maxlim: 1112062   bits: 22/21
c ---[1603]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1602]---> Adder-cost: 73   maxlim: 1112062   bits: 22/21
c ---[1601]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1600]---> Adder-cost: 82   maxlim: 1100542   bits: 22/21
c ---[1599]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1598]---> Adder-cost: 82   maxlim: 1086206   bits: 22/21
c ---[1597]---> Adder-cost: 82   maxlim: 1100542   bits: 22/21
c ---[1596]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1595]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1594]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1593]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1592]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1591]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1590]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1589]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1588]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1587]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1586]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1585]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1584]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1583]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1582]---> Adder-cost: 112   maxlim: 1069054   bits: 22/21
c ---[1581]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1580]---> Adder-cost: 112   maxlim: 1069054   bits: 22/21
c ---[1579]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1578]---> Adder-cost: 71   maxlim: 1096958   bits: 22/21
c ---[1577]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1576]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[1575]---> Adder-cost: 71   maxlim: 1096958   bits: 22/21
c ---[1574]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1573]---> Adder-cost: 81   maxlim: 1091582   bits: 22/21
c ---[1572]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1571]---> Adder-cost: 81   maxlim: 1091582   bits: 22/21
c ---[1570]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1569]---> Adder-cost: 85   maxlim: 1096958   bits: 22/21
c ---[1568]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1567]---> Adder-cost: 85   maxlim: 1096958   bits: 22/21
c ---[1566]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1565]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1564]---> Adder-cost: 70   maxlim: 1075454   bits: 22/21
c ---[1563]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1562]---> Adder-cost: 70   maxlim: 1075454   bits: 22/21
c ---[1561]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1560]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1559]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1558]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1557]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1556]---> Adder-cost: 85   maxlim: 1088766   bits: 22/21
c ---[1555]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1554]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[1553]---> Adder-cost: 85   maxlim: 1088766   bits: 22/21
c ---[1552]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1551]---> Adder-cost: 76   maxlim: 1078014   bits: 22/21
c ---[1550]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1549]---> Adder-cost: 76   maxlim: 1078014   bits: 22/21
c ---[1548]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1547]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[1546]---> Adder-cost: 83   maxlim: 1082622   bits: 22/21
c ---[1545]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[1544]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1543]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1542]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[1541]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1540]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[1539]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1538]---> Adder-cost: 80   maxlim: 1073662   bits: 22/21
c ---[1537]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1536]---> Adder-cost: 80   maxlim: 1073662   bits: 22/21
c ---[1535]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1534]---> Adder-cost: 77   maxlim: 1112062   bits: 22/21
c ---[1533]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1532]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1531]---> Adder-cost: 77   maxlim: 1112062   bits: 22/21
c ---[1530]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1529]---> Adder-cost: 80   maxlim: 1100542   bits: 22/21
c ---[1528]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1527]---> Adder-cost: 80   maxlim: 1100542   bits: 22/21
c ---[1526]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1525]---> Adder-cost: 82   maxlim: 1070846   bits: 22/21
c ---[1524]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1523]---> Adder-cost: 82   maxlim: 1070846   bits: 22/21
c ---[1522]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1521]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1520]---> Adder-cost: 98   maxlim: 1063678   bits: 22/21
c ---[1519]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1518]---> Adder-cost: 98   maxlim: 1063678   bits: 22/21
c ---[1517]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1516]---> Adder-cost: 75   maxlim: 1071870   bits: 22/21
c ---[1515]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1514]---> Adder-cost: 75   maxlim: 1071870   bits: 22/21
c ---[1513]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1512]---> Adder-cost: 87   maxlim: 1069054   bits: 22/21
c ---[1511]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1510]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[1509]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1508]---> Adder-cost: 87   maxlim: 1069054   bits: 22/21
c ---[1507]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1506]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[1505]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1504]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[1503]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1502]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1501]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1500]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1499]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1498]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1497]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1496]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1495]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1494]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1493]---> Adder-cost: 62   maxlim: 1075454   bits: 22/21
c ---[1492]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1491]---> Adder-cost: 62   maxlim: 1075454   bits: 22/21
c ---[1490]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1489]---> Adder-cost: 79   maxlim: 1071870   bits: 22/21
c ---[1488]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1487]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1486]---> Adder-cost: 79   maxlim: 1071870   bits: 22/21
c ---[1485]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1484]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[1483]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1482]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[1481]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1480]---> Adder-cost: 64   maxlim: 1078014   bits: 22/21
c ---[1479]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1478]---> Adder-cost: 64   maxlim: 1078014   bits: 22/21
c ---[1477]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1476]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1475]---> Adder-cost: 84   maxlim: 1070846   bits: 22/21
c ---[1474]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1473]---> Adder-cost: 84   maxlim: 1070846   bits: 22/21
c ---[1472]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1471]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1470]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1469]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1468]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1467]---> Adder-cost: 74   maxlim: 1112062   bits: 22/21
c ---[1466]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1465]---> Adder-cost: 107   maxlim: 1074430   bits: 22/21
c ---[1464]---> Adder-cost: 74   maxlim: 1112062   bits: 22/21
c ---[1463]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1462]---> Adder-cost: 80   maxlim: 1100542   bits: 22/21
c ---[1461]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1460]---> Adder-cost: 80   maxlim: 1100542   bits: 22/21
c ---[1459]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1458]---> Adder-cost: 113   maxlim: 1070846   bits: 22/21
c ---[1457]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1456]---> Adder-cost: 113   maxlim: 1070846   bits: 22/21
c ---[1455]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1454]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1453]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1452]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1451]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1450]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1449]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[1448]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1447]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[1446]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1445]---> Adder-cost: 113   maxlim: 1069054   bits: 22/21
c ---[1444]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1443]---> Adder-cost: 86   maxlim: 1095934   bits: 22/21
c ---[1442]---> Adder-cost: 113   maxlim: 1069054   bits: 22/21
c ---[1441]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1440]---> Adder-cost: 72   maxlim: 1096958   bits: 22/21
c ---[1439]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1438]---> Adder-cost: 72   maxlim: 1096958   bits: 22/21
c ---[1437]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1436]---> Adder-cost: 82   maxlim: 1091582   bits: 22/21
c ---[1435]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1434]---> Adder-cost: 82   maxlim: 1091582   bits: 22/21
c ---[1433]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1432]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1431]---> Adder-cost: 86   maxlim: 1096958   bits: 22/21
c ---[1430]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1429]---> Adder-cost: 86   maxlim: 1096958   bits: 22/21
c ---[1428]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1427]---> Adder-cost: 68   maxlim: 1075454   bits: 22/21
c ---[1426]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1425]---> Adder-cost: 68   maxlim: 1075454   bits: 22/21
c ---[1424]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1423]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1422]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1421]---> Adder-cost: 86   maxlim: 1095934   bits: 22/21
c ---[1420]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1419]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1418]---> Adder-cost: 85   maxlim: 1088766   bits: 22/21
c ---[1417]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1416]---> Adder-cost: 85   maxlim: 1088766   bits: 22/21
c ---[1415]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1414]---> Adder-cost: 74   maxlim: 1078014   bits: 22/21
c ---[1413]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1412]---> Adder-cost: 74   maxlim: 1078014   bits: 22/21
c ---[1411]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1410]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1409]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1408]---> Adder-cost: 85   maxlim: 1086206   bits: 22/21
c ---[1407]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1406]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1405]---> Adder-cost: 77   maxlim: 1112062   bits: 22/21
c ---[1404]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1403]---> Adder-cost: 77   maxlim: 1112062   bits: 22/21
c ---[1402]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1401]---> Adder-cost: 83   maxlim: 1100542   bits: 22/21
c ---[1400]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1399]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[1398]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1397]---> Adder-cost: 83   maxlim: 1100542   bits: 22/21
c ---[1396]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1395]---> Adder-cost: 85   maxlim: 1070846   bits: 22/21
c ---[1394]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1393]---> Adder-cost: 85   maxlim: 1070846   bits: 22/21
c ---[1392]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1391]---> Adder-cost: 100   maxlim: 1063678   bits: 22/21
c ---[1390]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1389]---> Adder-cost: 100   maxlim: 1063678   bits: 22/21
c ---[1388]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1387]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1386]---> Adder-cost: 79   maxlim: 1071870   bits: 22/21
c ---[1385]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1384]---> Adder-cost: 79   maxlim: 1071870   bits: 22/21
c ---[1383]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1382]---> Adder-cost: 87   maxlim: 1069054   bits: 22/21
c ---[1381]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1380]---> Adder-cost: 87   maxlim: 1069054   bits: 22/21
c ---[1379]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1378]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[1377]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1376]---> Adder-cost: 107   maxlim: 1063678   bits: 22/21
c ---[1375]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[1374]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1373]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1372]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1371]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1370]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1369]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1368]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1367]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1366]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1365]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1364]---> Adder-cost: 64   maxlim: 1075454   bits: 22/21
c ---[1363]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1362]---> Adder-cost: 64   maxlim: 1075454   bits: 22/21
c ---[1361]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1360]---> Adder-cost: 79   maxlim: 1071870   bits: 22/21
c ---[1359]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1358]---> Adder-cost: 79   maxlim: 1071870   bits: 22/21
c ---[1357]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1356]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[1355]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1354]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1353]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[1352]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1351]---> Adder-cost: 66   maxlim: 1078014   bits: 22/21
c ---[1350]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1349]---> Adder-cost: 66   maxlim: 1078014   bits: 22/21
c ---[1348]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1347]---> Adder-cost: 87   maxlim: 1070846   bits: 22/21
c ---[1346]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1345]---> Adder-cost: 87   maxlim: 1070846   bits: 22/21
c ---[1344]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1343]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1342]---> Adder-cost: 82   maxlim: 1100542   bits: 22/21
c ---[1341]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1340]---> Adder-cost: 82   maxlim: 1100542   bits: 22/21
c ---[1339]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1338]---> Adder-cost: 113   maxlim: 1070846   bits: 22/21
c ---[1337]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1336]---> Adder-cost: 113   maxlim: 1070846   bits: 22/21
c ---[1335]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1334]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1333]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1332]---> Adder-cost: 119   maxlim: 1064702   bits: 22/21
c ---[1331]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1330]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1329]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[1328]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1327]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[1326]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1325]---> Adder-cost: 110   maxlim: 1069054   bits: 22/21
c ---[1324]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1323]---> Adder-cost: 110   maxlim: 1069054   bits: 22/21
c ---[1322]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1321]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1320]---> Adder-cost: 69   maxlim: 1096958   bits: 22/21
c ---[1319]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1318]---> Adder-cost: 69   maxlim: 1096958   bits: 22/21
c ---[1317]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1316]---> Adder-cost: 81   maxlim: 1091582   bits: 22/21
c ---[1315]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1314]---> Adder-cost: 81   maxlim: 1091582   bits: 22/21
c ---[1313]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1312]---> Adder-cost: 85   maxlim: 1096958   bits: 22/21
c ---[1311]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1310]---> Adder-cost: 86   maxlim: 1091582   bits: 22/21
c ---[1309]---> Adder-cost: 85   maxlim: 1096958   bits: 22/21
c ---[1308]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1307]---> Adder-cost: 68   maxlim: 1075454   bits: 22/21
c ---[1306]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1305]---> Adder-cost: 68   maxlim: 1075454   bits: 22/21
c ---[1304]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1303]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[1302]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1301]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[1300]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1299]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1298]---> Adder-cost: 88   maxlim: 1088766   bits: 22/21
c ---[1297]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1296]---> Adder-cost: 88   maxlim: 1088766   bits: 22/21
c ---[1295]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1294]---> Adder-cost: 72   maxlim: 1078014   bits: 22/21
c ---[1293]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1292]---> Adder-cost: 72   maxlim: 1078014   bits: 22/21
c ---[1291]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1290]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1289]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[1288]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[1287]---> Adder-cost: 86   maxlim: 1091582   bits: 22/21
c ---[1286]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1285]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1284]---> Adder-cost: 110   maxlim: 1070846   bits: 22/21
c ---[1283]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1282]---> Adder-cost: 110   maxlim: 1070846   bits: 22/21
c ---[1281]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1280]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1279]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1278]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1277]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1276]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1275]---> Adder-cost: 105   maxlim: 1071870   bits: 22/21
c ---[1274]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1273]---> Adder-cost: 105   maxlim: 1071870   bits: 22/21
c ---[1272]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1271]---> Adder-cost: 115   maxlim: 1069054   bits: 22/21
c ---[1270]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1269]---> Adder-cost: 115   maxlim: 1069054   bits: 22/21
c ---[1268]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1267]---> Adder-cost: 74   maxlim: 1096958   bits: 22/21
c ---[1266]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1265]---> Adder-cost: 82   maxlim: 1082622   bits: 22/21
c ---[1264]---> Adder-cost: 74   maxlim: 1096958   bits: 22/21
c ---[1263]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1262]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[1261]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1260]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[1259]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1258]---> Adder-cost: 88   maxlim: 1096958   bits: 22/21
c ---[1257]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1256]---> Adder-cost: 88   maxlim: 1096958   bits: 22/21
c ---[1255]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1254]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1253]---> Adder-cost: 70   maxlim: 1075454   bits: 22/21
c ---[1252]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1251]---> Adder-cost: 70   maxlim: 1075454   bits: 22/21
c ---[1250]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1249]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[1248]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1247]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[1246]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1245]---> Adder-cost: 88   maxlim: 1088766   bits: 22/21
c ---[1244]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1243]---> Adder-cost: 82   maxlim: 1082622   bits: 22/21
c ---[1242]---> Adder-cost: 88   maxlim: 1088766   bits: 22/21
c ---[1241]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1240]---> Adder-cost: 74   maxlim: 1078014   bits: 22/21
c ---[1239]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1238]---> Adder-cost: 74   maxlim: 1078014   bits: 22/21
c ---[1237]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1236]---> Adder-cost: 112   maxlim: 1070846   bits: 22/21
c ---[1235]---> Adder-cost: 85   maxlim: 1100542   bits: 22/21
c ---[1234]---> Adder-cost: 112   maxlim: 1070846   bits: 22/21
c ---[1233]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1232]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1231]---> Adder-cost: 100   maxlim: 1063678   bits: 22/21
c ---[1230]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1229]---> Adder-cost: 100   maxlim: 1063678   bits: 22/21
c ---[1228]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1227]---> Adder-cost: 75   maxlim: 1071870   bits: 22/21
c ---[1226]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1225]---> Adder-cost: 75   maxlim: 1071870   bits: 22/21
c ---[1224]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1223]---> Adder-cost: 87   maxlim: 1069054   bits: 22/21
c ---[1222]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1221]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1220]---> Adder-cost: 87   maxlim: 1069054   bits: 22/21
c ---[1219]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1218]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[1217]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1216]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[1215]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1214]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1213]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1212]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1211]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1210]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1209]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1208]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1207]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1206]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1205]---> Adder-cost: 62   maxlim: 1075454   bits: 22/21
c ---[1204]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1203]---> Adder-cost: 62   maxlim: 1075454   bits: 22/21
c ---[1202]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1201]---> Adder-cost: 77   maxlim: 1071870   bits: 22/21
c ---[1200]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1199]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[1198]---> Adder-cost: 77   maxlim: 1071870   bits: 22/21
c ---[1197]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1196]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[1195]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1194]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[1193]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1192]---> Adder-cost: 64   maxlim: 1078014   bits: 22/21
c ---[1191]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1190]---> Adder-cost: 64   maxlim: 1078014   bits: 22/21
c ---[1189]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1188]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1187]---> Adder-cost: 84   maxlim: 1070846   bits: 22/21
c ---[1186]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1185]---> Adder-cost: 84   maxlim: 1070846   bits: 22/21
c ---[1184]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1183]---> Adder-cost: 88   maxlim: 1071870   bits: 22/21
c ---[1182]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1181]---> Adder-cost: 88   maxlim: 1071870   bits: 22/21
c ---[1180]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1179]---> Adder-cost: 100   maxlim: 1069054   bits: 22/21
c ---[1178]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1177]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[1176]---> Adder-cost: 84   maxlim: 1086206   bits: 22/21
c ---[1175]---> Adder-cost: 100   maxlim: 1069054   bits: 22/21
c ---[1174]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1173]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1172]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1171]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1170]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1169]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1168]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1167]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1166]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1165]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1164]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1163]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1162]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1161]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1160]---> Adder-cost: 77   maxlim: 1075454   bits: 22/21
c ---[1159]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1158]---> Adder-cost: 77   maxlim: 1075454   bits: 22/21
c ---[1157]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1156]---> Adder-cost: 90   maxlim: 1071870   bits: 22/21
c ---[1155]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1154]---> Adder-cost: 84   maxlim: 1086206   bits: 22/21
c ---[1153]---> Adder-cost: 90   maxlim: 1071870   bits: 22/21
c ---[1152]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1151]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[1150]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1149]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[1148]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1147]---> Adder-cost: 79   maxlim: 1078014   bits: 22/21
c ---[1146]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1145]---> Adder-cost: 79   maxlim: 1078014   bits: 22/21
c ---[1144]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1143]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1142]---> Adder-cost: 100   maxlim: 1070846   bits: 22/21
c ---[1141]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[1140]---> Adder-cost: 100   maxlim: 1070846   bits: 22/21
c ---[1139]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1138]---> Adder-cost: 87   maxlim: 1069054   bits: 22/21
c ---[1137]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1136]---> Adder-cost: 87   maxlim: 1069054   bits: 22/21
c ---[1135]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1134]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[1133]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1132]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1131]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[1130]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1129]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1128]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1127]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1126]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1125]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1124]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1123]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1122]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1121]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1120]---> Adder-cost: 62   maxlim: 1075454   bits: 22/21
c ---[1119]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1118]---> Adder-cost: 62   maxlim: 1075454   bits: 22/21
c ---[1117]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1116]---> Adder-cost: 75   maxlim: 1071870   bits: 22/21
c ---[1115]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1114]---> Adder-cost: 75   maxlim: 1071870   bits: 22/21
c ---[1113]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1112]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[1111]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1110]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[1109]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[1108]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1107]---> Adder-cost: 64   maxlim: 1078014   bits: 22/21
c ---[1106]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1105]---> Adder-cost: 64   maxlim: 1078014   bits: 22/21
c ---[1104]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1103]---> Adder-cost: 85   maxlim: 1070846   bits: 22/21
c ---[1102]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1101]---> Adder-cost: 85   maxlim: 1070846   bits: 22/21
c ---[1100]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1099]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1098]---> Adder-cost: 72   maxlim: 1096958   bits: 22/21
c ---[1097]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1096]---> Adder-cost: 72   maxlim: 1096958   bits: 22/21
c ---[1095]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1094]---> Adder-cost: 82   maxlim: 1091582   bits: 22/21
c ---[1093]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1092]---> Adder-cost: 82   maxlim: 1091582   bits: 22/21
c ---[1091]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1090]---> Adder-cost: 86   maxlim: 1096958   bits: 22/21
c ---[1089]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1088]---> Adder-cost: 78   maxlim: 1112062   bits: 22/21
c ---[1087]---> Adder-cost: 86   maxlim: 1096958   bits: 22/21
c ---[1086]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1085]---> Adder-cost: 60   maxlim: 1075454   bits: 22/21
c ---[1084]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1083]---> Adder-cost: 60   maxlim: 1075454   bits: 22/21
c ---[1082]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1081]---> Adder-cost: 79   maxlim: 1071870   bits: 22/21
c ---[1080]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1079]---> Adder-cost: 79   maxlim: 1071870   bits: 22/21
c ---[1078]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1077]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1076]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[1075]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1074]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[1073]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1072]---> Adder-cost: 64   maxlim: 1078014   bits: 22/21
c ---[1071]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1070]---> Adder-cost: 64   maxlim: 1078014   bits: 22/21
c ---[1069]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1068]---> Adder-cost: 87   maxlim: 1070846   bits: 22/21
c ---[1067]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[1066]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1065]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[1064]---> Adder-cost: 78   maxlim: 1112062   bits: 22/21
c ---[1063]---> Adder-cost: 87   maxlim: 1070846   bits: 22/21
c ---[1062]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1061]---> Adder-cost: 81   maxlim: 1091582   bits: 22/21
c ---[1060]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1059]---> Adder-cost: 81   maxlim: 1091582   bits: 22/21
c ---[1058]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1057]---> Adder-cost: 85   maxlim: 1096958   bits: 22/21
c ---[1056]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1055]---> Adder-cost: 85   maxlim: 1096958   bits: 22/21
c ---[1054]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1053]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1052]---> Adder-cost: 64   maxlim: 1075454   bits: 22/21
c ---[1051]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1050]---> Adder-cost: 64   maxlim: 1075454   bits: 22/21
c ---[1049]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1048]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[1047]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1046]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[1045]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1044]---> Adder-cost: 86   maxlim: 1088766   bits: 22/21
c ---[1043]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1042]---> Adder-cost: 84   maxlim: 1100542   bits: 22/21
c ---[1041]---> Adder-cost: 86   maxlim: 1088766   bits: 22/21
c ---[1040]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1039]---> Adder-cost: 72   maxlim: 1078014   bits: 22/21
c ---[1038]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1037]---> Adder-cost: 72   maxlim: 1078014   bits: 22/21
c ---[1036]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1035]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1034]---> Adder-cost: 79   maxlim: 1096958   bits: 22/21
c ---[1033]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[1032]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1031]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1030]---> Adder-cost: 85   maxlim: 1096958   bits: 22/21
c ---[1029]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1028]---> Adder-cost: 85   maxlim: 1096958   bits: 22/21
c ---[1027]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1026]---> Adder-cost: 74   maxlim: 1075454   bits: 22/21
c ---[1025]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1024]---> Adder-cost: 74   maxlim: 1075454   bits: 22/21
c ---[1023]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1022]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1021]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1020]---> Adder-cost: 84   maxlim: 1100542   bits: 22/21
c ---[1019]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[1018]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1017]---> Adder-cost: 90   maxlim: 1088766   bits: 22/21
c ---[1016]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1015]---> Adder-cost: 90   maxlim: 1088766   bits: 22/21
c ---[1014]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1013]---> Adder-cost: 78   maxlim: 1078014   bits: 22/21
c ---[1012]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1011]---> Adder-cost: 78   maxlim: 1078014   bits: 22/21
c ---[1010]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1009]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[1008]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[1007]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[1006]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[1005]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1004]---> Adder-cost: 74   maxlim: 1075454   bits: 22/21
c ---[1003]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1002]---> Adder-cost: 74   maxlim: 1075454   bits: 22/21
c ---[1001]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[1000]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 999]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[ 998]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[ 997]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 996]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[ 995]---> Adder-cost: 90   maxlim: 1088766   bits: 22/21
c ---[ 994]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[ 993]---> Adder-cost: 90   maxlim: 1088766   bits: 22/21
c ---[ 992]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[ 991]---> Adder-cost: 78   maxlim: 1078014   bits: 22/21
c ---[ 990]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[ 989]---> Adder-cost: 78   maxlim: 1078014   bits: 22/21
c ---[ 988]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[ 987]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 986]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[ 985]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[ 984]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[ 983]---> Adder-cost: 77   maxlim: 1075454   bits: 22/21
c ---[ 982]---> Adder-cost: 96   maxlim: 1071870   bits: 22/21
c ---[ 981]---> Adder-cost: 77   maxlim: 1075454   bits: 22/21
c ---[ 980]---> Adder-cost: 96   maxlim: 1071870   bits: 22/21
c ---[ 979]---> Adder-cost: 77   maxlim: 1075454   bits: 22/21
c ---[ 978]---> Adder-cost: 86   maxlim: 1088766   bits: 22/21
c ---[ 977]---> Adder-cost: 77   maxlim: 1075454   bits: 22/21
c ---[ 976]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[ 975]---> Adder-cost: 86   maxlim: 1088766   bits: 22/21
c ---[ 974]---> Adder-cost: 77   maxlim: 1075454   bits: 22/21
c ---[ 973]---> Adder-cost: 59   maxlim: 1078014   bits: 22/21
c ---[ 972]---> Adder-cost: 77   maxlim: 1075454   bits: 22/21
c ---[ 971]---> Adder-cost: 59   maxlim: 1078014   bits: 22/21
c ---[ 970]---> Adder-cost: 77   maxlim: 1075454   bits: 22/21
c ---[ 969]---> Adder-cost: 102   maxlim: 1070846   bits: 22/21
c ---[ 968]---> Adder-cost: 77   maxlim: 1075454   bits: 22/21
c ---[ 967]---> Adder-cost: 102   maxlim: 1070846   bits: 22/21
c ---[ 966]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 965]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 964]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 963]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 962]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 961]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 960]---> Adder-cost: 66   maxlim: 1078014   bits: 22/21
c ---[ 959]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 958]---> Adder-cost: 66   maxlim: 1078014   bits: 22/21
c ---[ 957]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 956]---> Adder-cost: 87   maxlim: 1070846   bits: 22/21
c ---[ 955]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 954]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 953]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[ 952]---> Adder-cost: 87   maxlim: 1070846   bits: 22/21
c ---[ 951]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 950]---> Adder-cost: 76   maxlim: 1078014   bits: 22/21
c ---[ 949]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 948]---> Adder-cost: 76   maxlim: 1078014   bits: 22/21
c ---[ 947]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 946]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[ 945]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 944]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[ 943]---> Adder-cost: 79   maxlim: 1078014   bits: 22/21
c ---[ 942]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 941]---> Adder-cost: 102   maxlim: 1070846   bits: 22/21
c ---[ 940]---> Adder-cost: 79   maxlim: 1078014   bits: 22/21
c ---[ 939]---> Adder-cost: 102   maxlim: 1070846   bits: 22/21
c ---[ 938]---> Adder-cost: 66   maxlim: 1063678   bits: 22/21
c ---[ 937]---> Adder-cost: 66   maxlim: 1063678   bits: 22/21
c ---[ 936]---> Adder-cost: 66   maxlim: 1094142   bits: 22/21
c ---[ 935]---> Adder-cost: 66   maxlim: 1094142   bits: 22/21
c ---[ 934]---> Adder-cost: 62   maxlim: 1066494   bits: 22/21
c ---[ 933]---> Adder-cost: 62   maxlim: 1066494   bits: 22/21
c ---[ 932]---> Adder-cost: 64   maxlim: 1120254   bits: 22/21
c ---[ 931]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[ 930]---> Adder-cost: 64   maxlim: 1120254   bits: 22/21
c ---[ 929]---> Adder-cost: 66   maxlim: 1088766   bits: 22/21
c ---[ 928]---> Adder-cost: 66   maxlim: 1088766   bits: 22/21
c ---[ 927]---> Adder-cost: 66   maxlim: 1088766   bits: 22/21
c ---[ 926]---> Adder-cost: 66   maxlim: 1088766   bits: 22/21
c ---[ 925]---> Adder-cost: 62   maxlim: 1093374   bits: 22/21
c ---[ 924]---> Adder-cost: 62   maxlim: 1093374   bits: 22/21
c ---[ 923]---> Adder-cost: 66   maxlim: 1086206   bits: 22/21
c ---[ 922]---> Adder-cost: 66   maxlim: 1086206   bits: 22/21
c ---[ 921]---> Adder-cost: 66   maxlim: 1063678   bits: 22/21
c ---[ 920]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 919]---> Adder-cost: 66   maxlim: 1063678   bits: 22/21
c ---[ 918]---> Adder-cost: 64   maxlim: 1074430   bits: 22/21
c ---[ 917]---> Adder-cost: 64   maxlim: 1074430   bits: 22/21
c ---[ 916]---> Adder-cost: 64   maxlim: 1074430   bits: 22/21
c ---[ 915]---> Adder-cost: 64   maxlim: 1074430   bits: 22/21
c ---[ 914]---> Adder-cost: 64   maxlim: 1095934   bits: 22/21
c ---[ 913]---> Adder-cost: 64   maxlim: 1095934   bits: 22/21
c ---[ 912]---> Adder-cost: 40   maxlim: 1063678   bits: 21/21
c ---[ 911]---> Adder-cost: 40   maxlim: 1063678   bits: 21/21
c ---[ 910]---> Adder-cost: 62   maxlim: 1064702   bits: 22/21
c ---[ 909]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 908]---> Adder-cost: 62   maxlim: 1064702   bits: 22/21
c ---[ 907]---> Adder-cost: 66   maxlim: 1091582   bits: 22/21
c ---[ 906]---> Adder-cost: 66   maxlim: 1091582   bits: 22/21
c ---[ 905]---> Adder-cost: 64   maxlim: 1082622   bits: 22/21
c ---[ 904]---> Adder-cost: 64   maxlim: 1082622   bits: 22/21
c ---[ 903]---> Adder-cost: 66   maxlim: 1069054   bits: 22/21
c ---[ 902]---> Adder-cost: 66   maxlim: 1069054   bits: 22/21
c ---[ 901]---> Adder-cost: 60   maxlim: 1086206   bits: 22/21
c ---[ 900]---> Adder-cost: 60   maxlim: 1086206   bits: 22/21
c ---[ 899]---> Adder-cost: 66   maxlim: 1073662   bits: 22/21
c ---[ 898]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 897]---> Adder-cost: 66   maxlim: 1073662   bits: 22/21
c ---[ 896]---> Adder-cost: 64   maxlim: 1112062   bits: 22/21
c ---[ 895]---> Adder-cost: 64   maxlim: 1112062   bits: 22/21
c ---[ 894]---> Adder-cost: 66   maxlim: 1100542   bits: 22/21
c ---[ 893]---> Adder-cost: 66   maxlim: 1100542   bits: 22/21
c ---[ 892]---> Adder-cost: 62   maxlim: 1070846   bits: 22/21
c ---[ 891]---> Adder-cost: 62   maxlim: 1070846   bits: 22/21
c ---[ 890]---> Adder-cost: 66   maxlim: 1063678   bits: 22/21
c ---[ 889]---> Adder-cost: 66   maxlim: 1063678   bits: 22/21
c ---[ 888]---> Adder-cost: 56   maxlim: 1071870   bits: 22/21
c ---[ 887]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 886]---> Adder-cost: 56   maxlim: 1071870   bits: 22/21
c ---[ 885]---> Adder-cost: 64   maxlim: 1069054   bits: 22/21
c ---[ 884]---> Adder-cost: 64   maxlim: 1069054   bits: 22/21
c ---[ 883]---> Adder-cost: 64   maxlim: 1096958   bits: 22/21
c ---[ 882]---> Adder-cost: 64   maxlim: 1096958   bits: 22/21
c ---[ 881]---> Adder-cost: 64   maxlim: 1091582   bits: 22/21
c ---[ 880]---> Adder-cost: 64   maxlim: 1091582   bits: 22/21
c ---[ 879]---> Adder-cost: 64   maxlim: 1096958   bits: 22/21
c ---[ 878]---> Adder-cost: 64   maxlim: 1096958   bits: 22/21
c ---[ 877]---> Adder-cost: 40   maxlim: 1075454   bits: 21/21
c ---[ 876]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 875]---> Adder-cost: 40   maxlim: 1075454   bits: 21/21
c ---[ 874]---> Adder-cost: 64   maxlim: 1071870   bits: 22/21
c ---[ 873]---> Adder-cost: 64   maxlim: 1071870   bits: 22/21
c ---[ 872]---> Adder-cost: 66   maxlim: 1088766   bits: 22/21
c ---[ 871]---> Adder-cost: 66   maxlim: 1088766   bits: 22/21
c ---[ 870]---> Adder-cost: 66   maxlim: 1078014   bits: 22/21
c ---[ 869]---> Adder-cost: 66   maxlim: 1078014   bits: 22/21
c ---[ 868]---> Adder-cost: 66   maxlim: 1070846   bits: 22/21
c ---[ 867]---> Adder-cost: 66   maxlim: 1070846   bits: 22/21
c ---[ 866]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[ 865]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 864]---> Adder-cost: 83   maxlim: 1093374   bits: 22/21
c ---[ 863]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[ 862]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 861]---> Adder-cost: 78   maxlim: 1096958   bits: 22/21
c ---[ 860]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 859]---> Adder-cost: 78   maxlim: 1096958   bits: 22/21
c ---[ 858]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 857]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[ 856]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 855]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[ 854]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 853]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 852]---> Adder-cost: 88   maxlim: 1096958   bits: 22/21
c ---[ 851]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 850]---> Adder-cost: 88   maxlim: 1096958   bits: 22/21
c ---[ 849]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 848]---> Adder-cost: 76   maxlim: 1075454   bits: 22/21
c ---[ 847]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 846]---> Adder-cost: 76   maxlim: 1075454   bits: 22/21
c ---[ 845]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 844]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 843]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 842]---> Adder-cost: 83   maxlim: 1093374   bits: 22/21
c ---[ 841]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 840]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 839]---> Adder-cost: 90   maxlim: 1088766   bits: 22/21
c ---[ 838]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 837]---> Adder-cost: 90   maxlim: 1088766   bits: 22/21
c ---[ 836]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 835]---> Adder-cost: 78   maxlim: 1078014   bits: 22/21
c ---[ 834]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 833]---> Adder-cost: 78   maxlim: 1078014   bits: 22/21
c ---[ 832]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 831]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 830]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[ 829]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 828]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[ 827]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 826]---> Adder-cost: 85   maxlim: 1120254   bits: 22/21
c ---[ 825]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 824]---> Adder-cost: 85   maxlim: 1120254   bits: 22/21
c ---[ 823]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 822]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 821]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 820]---> Adder-cost: 79   maxlim: 1086206   bits: 22/21
c ---[ 819]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 818]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 817]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 816]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 815]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 814]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 813]---> Adder-cost: 85   maxlim: 1093374   bits: 22/21
c ---[ 812]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 811]---> Adder-cost: 85   maxlim: 1093374   bits: 22/21
c ---[ 810]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 809]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 808]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 807]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 806]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 805]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 804]---> Adder-cost: 98   maxlim: 1063678   bits: 22/21
c ---[ 803]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 802]---> Adder-cost: 98   maxlim: 1063678   bits: 22/21
c ---[ 801]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 800]---> Adder-cost: 77   maxlim: 1074430   bits: 22/21
c ---[ 799]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 798]---> Adder-cost: 79   maxlim: 1086206   bits: 22/21
c ---[ 797]---> Adder-cost: 77   maxlim: 1074430   bits: 22/21
c ---[ 796]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 795]---> Adder-cost: 77   maxlim: 1074430   bits: 22/21
c ---[ 794]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 793]---> Adder-cost: 77   maxlim: 1074430   bits: 22/21
c ---[ 792]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 791]---> Adder-cost: 85   maxlim: 1095934   bits: 22/21
c ---[ 790]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 789]---> Adder-cost: 85   maxlim: 1095934   bits: 22/21
c ---[ 788]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 787]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 786]---> Adder-cost: 90   maxlim: 1063678   bits: 22/21
c ---[ 785]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 784]---> Adder-cost: 90   maxlim: 1063678   bits: 22/21
c ---[ 783]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 782]---> Adder-cost: 102   maxlim: 1064702   bits: 22/21
c ---[ 781]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 780]---> Adder-cost: 102   maxlim: 1064702   bits: 22/21
c ---[ 779]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 778]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[ 777]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 776]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 775]---> Adder-cost: 76   maxlim: 1063678   bits: 22/21
c ---[ 774]---> Adder-cost: 87   maxlim: 1091582   bits: 22/21
c ---[ 773]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 772]---> Adder-cost: 81   maxlim: 1082622   bits: 22/21
c ---[ 771]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 770]---> Adder-cost: 81   maxlim: 1082622   bits: 22/21
c ---[ 769]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 768]---> Adder-cost: 89   maxlim: 1069054   bits: 22/21
c ---[ 767]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 766]---> Adder-cost: 89   maxlim: 1069054   bits: 22/21
c ---[ 765]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 764]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 763]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 762]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 761]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 760]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 759]---> Adder-cost: 81   maxlim: 1073662   bits: 22/21
c ---[ 758]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 757]---> Adder-cost: 81   maxlim: 1073662   bits: 22/21
c ---[ 756]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 755]---> Adder-cost: 75   maxlim: 1112062   bits: 22/21
c ---[ 754]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 753]---> Adder-cost: 76   maxlim: 1063678   bits: 22/21
c ---[ 752]---> Adder-cost: 75   maxlim: 1112062   bits: 22/21
c ---[ 751]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 750]---> Adder-cost: 83   maxlim: 1100542   bits: 22/21
c ---[ 749]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 748]---> Adder-cost: 83   maxlim: 1100542   bits: 22/21
c ---[ 747]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 746]---> Adder-cost: 85   maxlim: 1070846   bits: 22/21
c ---[ 745]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 744]---> Adder-cost: 85   maxlim: 1070846   bits: 22/21
c ---[ 743]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 742]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 741]---> Adder-cost: 100   maxlim: 1063678   bits: 22/21
c ---[ 740]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 739]---> Adder-cost: 100   maxlim: 1063678   bits: 22/21
c ---[ 738]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 737]---> Adder-cost: 79   maxlim: 1071870   bits: 22/21
c ---[ 736]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 735]---> Adder-cost: 79   maxlim: 1071870   bits: 22/21
c ---[ 734]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 733]---> Adder-cost: 85   maxlim: 1069054   bits: 22/21
c ---[ 732]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 731]---> Adder-cost: 88   maxlim: 1074430   bits: 22/21
c ---[ 730]---> Adder-cost: 85   maxlim: 1069054   bits: 22/21
c ---[ 729]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 728]---> Adder-cost: 75   maxlim: 1096958   bits: 22/21
c ---[ 727]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 726]---> Adder-cost: 75   maxlim: 1096958   bits: 22/21
c ---[ 725]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 724]---> Adder-cost: 83   maxlim: 1091582   bits: 22/21
c ---[ 723]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 722]---> Adder-cost: 83   maxlim: 1091582   bits: 22/21
c ---[ 721]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 720]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 719]---> Adder-cost: 87   maxlim: 1096958   bits: 22/21
c ---[ 718]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 717]---> Adder-cost: 87   maxlim: 1096958   bits: 22/21
c ---[ 716]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 715]---> Adder-cost: 62   maxlim: 1075454   bits: 22/21
c ---[ 714]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 713]---> Adder-cost: 62   maxlim: 1075454   bits: 22/21
c ---[ 712]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 711]---> Adder-cost: 79   maxlim: 1071870   bits: 22/21
c ---[ 710]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 709]---> Adder-cost: 88   maxlim: 1074430   bits: 22/21
c ---[ 708]---> Adder-cost: 79   maxlim: 1071870   bits: 22/21
c ---[ 707]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 706]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 705]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 704]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 703]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 702]---> Adder-cost: 66   maxlim: 1078014   bits: 22/21
c ---[ 701]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 700]---> Adder-cost: 66   maxlim: 1078014   bits: 22/21
c ---[ 699]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 698]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 697]---> Adder-cost: 87   maxlim: 1070846   bits: 22/21
c ---[ 696]---> Adder-cost: 105   maxlim: 1066494   bits: 22/21
c ---[ 695]---> Adder-cost: 87   maxlim: 1070846   bits: 22/21
c ---[ 694]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 693]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[ 692]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 691]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[ 690]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 689]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[ 688]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 687]---> Adder-cost: 88   maxlim: 1074430   bits: 22/21
c ---[ 686]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[ 685]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 684]---> Adder-cost: 81   maxlim: 1093374   bits: 22/21
c ---[ 683]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 682]---> Adder-cost: 81   maxlim: 1093374   bits: 22/21
c ---[ 681]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 680]---> Adder-cost: 79   maxlim: 1086206   bits: 22/21
c ---[ 679]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 678]---> Adder-cost: 79   maxlim: 1086206   bits: 22/21
c ---[ 677]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 676]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 675]---> Adder-cost: 113   maxlim: 1063678   bits: 22/21
c ---[ 674]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 673]---> Adder-cost: 113   maxlim: 1063678   bits: 22/21
c ---[ 672]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 671]---> Adder-cost: 105   maxlim: 1074430   bits: 22/21
c ---[ 670]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 669]---> Adder-cost: 105   maxlim: 1074430   bits: 22/21
c ---[ 668]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 667]---> Adder-cost: 105   maxlim: 1074430   bits: 22/21
c ---[ 666]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 665]---> Adder-cost: 93   maxlim: 1094142   bits: 22/21
c ---[ 664]---> Adder-cost: 88   maxlim: 1074430   bits: 22/21
c ---[ 663]---> Adder-cost: 105   maxlim: 1074430   bits: 22/21
c ---[ 662]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 661]---> Adder-cost: 80   maxlim: 1095934   bits: 22/21
c ---[ 660]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 659]---> Adder-cost: 80   maxlim: 1095934   bits: 22/21
c ---[ 658]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 657]---> Adder-cost: 105   maxlim: 1063678   bits: 22/21
c ---[ 656]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 655]---> Adder-cost: 105   maxlim: 1063678   bits: 22/21
c ---[ 654]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 653]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 652]---> Adder-cost: 117   maxlim: 1064702   bits: 22/21
c ---[ 651]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 650]---> Adder-cost: 117   maxlim: 1064702   bits: 22/21
c ---[ 649]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 648]---> Adder-cost: 86   maxlim: 1091582   bits: 22/21
c ---[ 647]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 646]---> Adder-cost: 86   maxlim: 1091582   bits: 22/21
c ---[ 645]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 644]---> Adder-cost: 76   maxlim: 1082622   bits: 22/21
c ---[ 643]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 642]---> Adder-cost: 85   maxlim: 1095934   bits: 22/21
c ---[ 641]---> Adder-cost: 76   maxlim: 1082622   bits: 22/21
c ---[ 640]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 639]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[ 638]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 637]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[ 636]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 635]---> Adder-cost: 79   maxlim: 1086206   bits: 22/21
c ---[ 634]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 633]---> Adder-cost: 79   maxlim: 1086206   bits: 22/21
c ---[ 632]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 631]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 630]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[ 629]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 628]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[ 627]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 626]---> Adder-cost: 75   maxlim: 1112062   bits: 22/21
c ---[ 625]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 624]---> Adder-cost: 75   maxlim: 1112062   bits: 22/21
c ---[ 623]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 622]---> Adder-cost: 82   maxlim: 1100542   bits: 22/21
c ---[ 621]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 620]---> Adder-cost: 85   maxlim: 1095934   bits: 22/21
c ---[ 619]---> Adder-cost: 82   maxlim: 1100542   bits: 22/21
c ---[ 618]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 617]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[ 616]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 615]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[ 614]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 613]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[ 612]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 611]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[ 610]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 609]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 608]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 607]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 606]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 605]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 604]---> Adder-cost: 114   maxlim: 1069054   bits: 22/21
c ---[ 603]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 602]---> Adder-cost: 114   maxlim: 1069054   bits: 22/21
c ---[ 601]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 600]---> Adder-cost: 73   maxlim: 1096958   bits: 22/21
c ---[ 599]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 598]---> Adder-cost: 69   maxlim: 1063678   bits: 22/21
c ---[ 597]---> Adder-cost: 73   maxlim: 1096958   bits: 22/21
c ---[ 596]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 595]---> Adder-cost: 81   maxlim: 1091582   bits: 22/21
c ---[ 594]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 593]---> Adder-cost: 81   maxlim: 1091582   bits: 22/21
c ---[ 592]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 591]---> Adder-cost: 85   maxlim: 1096958   bits: 22/21
c ---[ 590]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 589]---> Adder-cost: 85   maxlim: 1096958   bits: 22/21
c ---[ 588]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 587]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 586]---> Adder-cost: 72   maxlim: 1075454   bits: 22/21
c ---[ 585]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 584]---> Adder-cost: 72   maxlim: 1075454   bits: 22/21
c ---[ 583]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 582]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 581]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 580]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 579]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 578]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[ 577]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 576]---> Adder-cost: 69   maxlim: 1063678   bits: 22/21
c ---[ 575]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[ 574]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 573]---> Adder-cost: 78   maxlim: 1078014   bits: 22/21
c ---[ 572]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 571]---> Adder-cost: 78   maxlim: 1078014   bits: 22/21
c ---[ 570]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 569]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[ 568]---> Adder-cost: 87   maxlim: 1120254   bits: 22/21
c ---[ 567]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[ 566]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 565]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 564]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[ 563]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 562]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[ 561]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 560]---> Adder-cost: 83   maxlim: 1093374   bits: 22/21
c ---[ 559]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 558]---> Adder-cost: 83   maxlim: 1093374   bits: 22/21
c ---[ 557]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 556]---> Adder-cost: 77   maxlim: 1086206   bits: 22/21
c ---[ 555]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 554]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 553]---> Adder-cost: 83   maxlim: 1064702   bits: 22/21
c ---[ 552]---> Adder-cost: 77   maxlim: 1086206   bits: 22/21
c ---[ 551]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 550]---> Adder-cost: 113   maxlim: 1063678   bits: 22/21
c ---[ 549]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 548]---> Adder-cost: 113   maxlim: 1063678   bits: 22/21
c ---[ 547]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 546]---> Adder-cost: 103   maxlim: 1074430   bits: 22/21
c ---[ 545]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 544]---> Adder-cost: 103   maxlim: 1074430   bits: 22/21
c ---[ 543]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 542]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 541]---> Adder-cost: 103   maxlim: 1074430   bits: 22/21
c ---[ 540]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 539]---> Adder-cost: 103   maxlim: 1074430   bits: 22/21
c ---[ 538]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 537]---> Adder-cost: 83   maxlim: 1095934   bits: 22/21
c ---[ 536]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 535]---> Adder-cost: 83   maxlim: 1095934   bits: 22/21
c ---[ 534]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 533]---> Adder-cost: 105   maxlim: 1063678   bits: 22/21
c ---[ 532]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 531]---> Adder-cost: 83   maxlim: 1064702   bits: 22/21
c ---[ 530]---> Adder-cost: 105   maxlim: 1063678   bits: 22/21
c ---[ 529]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 528]---> Adder-cost: 117   maxlim: 1064702   bits: 22/21
c ---[ 527]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 526]---> Adder-cost: 117   maxlim: 1064702   bits: 22/21
c ---[ 525]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 524]---> Adder-cost: 86   maxlim: 1091582   bits: 22/21
c ---[ 523]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 522]---> Adder-cost: 86   maxlim: 1091582   bits: 22/21
c ---[ 521]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 520]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 519]---> Adder-cost: 77   maxlim: 1082622   bits: 22/21
c ---[ 518]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 517]---> Adder-cost: 77   maxlim: 1082622   bits: 22/21
c ---[ 516]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 515]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[ 514]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 513]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[ 512]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 511]---> Adder-cost: 79   maxlim: 1086206   bits: 22/21
c ---[ 510]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 509]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[ 508]---> Adder-cost: 79   maxlim: 1086206   bits: 22/21
c ---[ 507]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 506]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[ 505]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 504]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[ 503]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 502]---> Adder-cost: 76   maxlim: 1112062   bits: 22/21
c ---[ 501]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 500]---> Adder-cost: 76   maxlim: 1112062   bits: 22/21
c ---[ 499]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 498]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 497]---> Adder-cost: 82   maxlim: 1100542   bits: 22/21
c ---[ 496]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 495]---> Adder-cost: 82   maxlim: 1100542   bits: 22/21
c ---[ 494]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 493]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[ 492]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 491]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[ 490]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 489]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[ 488]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 487]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[ 486]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[ 485]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 484]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 483]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 482]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 481]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 480]---> Adder-cost: 115   maxlim: 1069054   bits: 22/21
c ---[ 479]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 478]---> Adder-cost: 115   maxlim: 1069054   bits: 22/21
c ---[ 477]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 476]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 475]---> Adder-cost: 74   maxlim: 1096958   bits: 22/21
c ---[ 474]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 473]---> Adder-cost: 74   maxlim: 1096958   bits: 22/21
c ---[ 472]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 471]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[ 470]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 469]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[ 468]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 467]---> Adder-cost: 88   maxlim: 1096958   bits: 22/21
c ---[ 466]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 465]---> Adder-cost: 81   maxlim: 1082622   bits: 22/21
c ---[ 464]---> Adder-cost: 88   maxlim: 1096958   bits: 22/21
c ---[ 463]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 462]---> Adder-cost: 72   maxlim: 1075454   bits: 22/21
c ---[ 461]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 460]---> Adder-cost: 72   maxlim: 1075454   bits: 22/21
c ---[ 459]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 458]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 457]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 456]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 455]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 454]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 453]---> Adder-cost: 85   maxlim: 1088766   bits: 22/21
c ---[ 452]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 451]---> Adder-cost: 85   maxlim: 1088766   bits: 22/21
c ---[ 450]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 449]---> Adder-cost: 76   maxlim: 1078014   bits: 22/21
c ---[ 448]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 447]---> Adder-cost: 76   maxlim: 1078014   bits: 22/21
c ---[ 446]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 445]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[ 444]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 443]---> Adder-cost: 88   maxlim: 1066494   bits: 22/21
c ---[ 442]---> Adder-cost: 81   maxlim: 1082622   bits: 22/21
c ---[ 441]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[ 440]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 439]---> Adder-cost: 83   maxlim: 1093374   bits: 22/21
c ---[ 438]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 437]---> Adder-cost: 83   maxlim: 1093374   bits: 22/21
c ---[ 436]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 435]---> Adder-cost: 79   maxlim: 1086206   bits: 22/21
c ---[ 434]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 433]---> Adder-cost: 79   maxlim: 1086206   bits: 22/21
c ---[ 432]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 431]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 430]---> Adder-cost: 113   maxlim: 1063678   bits: 22/21
c ---[ 429]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 428]---> Adder-cost: 113   maxlim: 1063678   bits: 22/21
c ---[ 427]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 426]---> Adder-cost: 105   maxlim: 1074430   bits: 22/21
c ---[ 425]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 424]---> Adder-cost: 105   maxlim: 1074430   bits: 22/21
c ---[ 423]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 422]---> Adder-cost: 105   maxlim: 1074430   bits: 22/21
c ---[ 421]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 420]---> Adder-cost: 98   maxlim: 1069054   bits: 22/21
c ---[ 419]---> Adder-cost: 105   maxlim: 1074430   bits: 22/21
c ---[ 418]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 417]---> Adder-cost: 83   maxlim: 1095934   bits: 22/21
c ---[ 416]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 415]---> Adder-cost: 83   maxlim: 1095934   bits: 22/21
c ---[ 414]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 413]---> Adder-cost: 105   maxlim: 1063678   bits: 22/21
c ---[ 412]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 411]---> Adder-cost: 105   maxlim: 1063678   bits: 22/21
c ---[ 410]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 409]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 408]---> Adder-cost: 117   maxlim: 1064702   bits: 22/21
c ---[ 407]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 406]---> Adder-cost: 117   maxlim: 1064702   bits: 22/21
c ---[ 405]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 404]---> Adder-cost: 86   maxlim: 1091582   bits: 22/21
c ---[ 403]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 402]---> Adder-cost: 86   maxlim: 1091582   bits: 22/21
c ---[ 401]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 400]---> Adder-cost: 79   maxlim: 1082622   bits: 22/21
c ---[ 399]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 398]---> Adder-cost: 98   maxlim: 1069054   bits: 22/21
c ---[ 397]---> Adder-cost: 79   maxlim: 1082622   bits: 22/21
c ---[ 396]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 395]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[ 394]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 393]---> Adder-cost: 119   maxlim: 1069054   bits: 22/21
c ---[ 392]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 391]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[ 390]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 389]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[ 388]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 387]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 386]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[ 385]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 384]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[ 383]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 382]---> Adder-cost: 78   maxlim: 1112062   bits: 22/21
c ---[ 381]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 380]---> Adder-cost: 78   maxlim: 1112062   bits: 22/21
c ---[ 379]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 378]---> Adder-cost: 82   maxlim: 1100542   bits: 22/21
c ---[ 377]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 376]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[ 375]---> Adder-cost: 82   maxlim: 1100542   bits: 22/21
c ---[ 374]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 373]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[ 372]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 371]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[ 370]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 369]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[ 368]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 367]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[ 366]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 365]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 364]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 363]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 362]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 361]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 360]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[ 359]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 358]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[ 357]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 356]---> Adder-cost: 76   maxlim: 1096958   bits: 22/21
c ---[ 355]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 354]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[ 353]---> Adder-cost: 76   maxlim: 1096958   bits: 22/21
c ---[ 352]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 351]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[ 350]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 349]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[ 348]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 347]---> Adder-cost: 88   maxlim: 1096958   bits: 22/21
c ---[ 346]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 345]---> Adder-cost: 88   maxlim: 1096958   bits: 22/21
c ---[ 344]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 343]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 342]---> Adder-cost: 74   maxlim: 1075454   bits: 22/21
c ---[ 341]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 340]---> Adder-cost: 74   maxlim: 1075454   bits: 22/21
c ---[ 339]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 338]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 337]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 336]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 335]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 334]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[ 333]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 332]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 331]---> Adder-cost: 94   maxlim: 1073662   bits: 22/21
c ---[ 330]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[ 329]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 328]---> Adder-cost: 78   maxlim: 1078014   bits: 22/21
c ---[ 327]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 326]---> Adder-cost: 78   maxlim: 1078014   bits: 22/21
c ---[ 325]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 324]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[ 323]---> Adder-cost: 91   maxlim: 1088766   bits: 22/21
c ---[ 322]---> Adder-cost: 117   maxlim: 1070846   bits: 22/21
c ---[ 321]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 320]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 319]---> Adder-cost: 77   maxlim: 1086206   bits: 22/21
c ---[ 318]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 317]---> Adder-cost: 77   maxlim: 1086206   bits: 22/21
c ---[ 316]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 315]---> Adder-cost: 111   maxlim: 1063678   bits: 22/21
c ---[ 314]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 313]---> Adder-cost: 111   maxlim: 1063678   bits: 22/21
c ---[ 312]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 311]---> Adder-cost: 105   maxlim: 1074430   bits: 22/21
c ---[ 310]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 309]---> Adder-cost: 94   maxlim: 1073662   bits: 22/21
c ---[ 308]---> Adder-cost: 105   maxlim: 1074430   bits: 22/21
c ---[ 307]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 306]---> Adder-cost: 105   maxlim: 1074430   bits: 22/21
c ---[ 305]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 304]---> Adder-cost: 105   maxlim: 1074430   bits: 22/21
c ---[ 303]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 302]---> Adder-cost: 81   maxlim: 1095934   bits: 22/21
c ---[ 301]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 300]---> Adder-cost: 81   maxlim: 1095934   bits: 22/21
c ---[ 299]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 298]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 297]---> Adder-cost: 103   maxlim: 1063678   bits: 22/21
c ---[ 296]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 295]---> Adder-cost: 103   maxlim: 1063678   bits: 22/21
c ---[ 294]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 293]---> Adder-cost: 114   maxlim: 1064702   bits: 22/21
c ---[ 292]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 291]---> Adder-cost: 114   maxlim: 1064702   bits: 22/21
c ---[ 290]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 289]---> Adder-cost: 83   maxlim: 1091582   bits: 22/21
c ---[ 288]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 287]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[ 286]---> Adder-cost: 83   maxlim: 1091582   bits: 22/21
c ---[ 285]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 284]---> Adder-cost: 77   maxlim: 1082622   bits: 22/21
c ---[ 283]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 282]---> Adder-cost: 77   maxlim: 1082622   bits: 22/21
c ---[ 281]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 280]---> Adder-cost: 116   maxlim: 1069054   bits: 22/21
c ---[ 279]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 278]---> Adder-cost: 116   maxlim: 1069054   bits: 22/21
c ---[ 277]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 276]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 275]---> Adder-cost: 77   maxlim: 1086206   bits: 22/21
c ---[ 274]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 273]---> Adder-cost: 77   maxlim: 1086206   bits: 22/21
c ---[ 272]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 271]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[ 270]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 269]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[ 268]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 267]---> Adder-cost: 76   maxlim: 1112062   bits: 22/21
c ---[ 266]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 265]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[ 264]---> Adder-cost: 76   maxlim: 1112062   bits: 22/21
c ---[ 263]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 262]---> Adder-cost: 79   maxlim: 1100542   bits: 22/21
c ---[ 261]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 260]---> Adder-cost: 79   maxlim: 1100542   bits: 22/21
c ---[ 259]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 258]---> Adder-cost: 112   maxlim: 1070846   bits: 22/21
c ---[ 257]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 256]---> Adder-cost: 112   maxlim: 1070846   bits: 22/21
c ---[ 255]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 254]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 253]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[ 252]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 251]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[ 250]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 249]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[ 248]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 247]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[ 246]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 245]---> Adder-cost: 115   maxlim: 1069054   bits: 22/21
c ---[ 244]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 243]---> Adder-cost: 81   maxlim: 1100542   bits: 22/21
c ---[ 242]---> Adder-cost: 115   maxlim: 1069054   bits: 22/21
c ---[ 241]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 240]---> Adder-cost: 74   maxlim: 1096958   bits: 22/21
c ---[ 239]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 238]---> Adder-cost: 74   maxlim: 1096958   bits: 22/21
c ---[ 237]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 236]---> Adder-cost: 82   maxlim: 1091582   bits: 22/21
c ---[ 235]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 234]---> Adder-cost: 82   maxlim: 1091582   bits: 22/21
c ---[ 233]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 232]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 231]---> Adder-cost: 86   maxlim: 1096958   bits: 22/21
c ---[ 230]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 229]---> Adder-cost: 86   maxlim: 1096958   bits: 22/21
c ---[ 228]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 227]---> Adder-cost: 70   maxlim: 1075454   bits: 22/21
c ---[ 226]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 225]---> Adder-cost: 70   maxlim: 1075454   bits: 22/21
c ---[ 224]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 223]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 222]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 221]---> Adder-cost: 88   maxlim: 1066494   bits: 22/21
c ---[ 220]---> Adder-cost: 81   maxlim: 1100542   bits: 22/21
c ---[ 219]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 218]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 217]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[ 216]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 215]---> Adder-cost: 87   maxlim: 1088766   bits: 22/21
c ---[ 214]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 213]---> Adder-cost: 76   maxlim: 1078014   bits: 22/21
c ---[ 212]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 211]---> Adder-cost: 76   maxlim: 1078014   bits: 22/21
c ---[ 210]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 209]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 208]---> Adder-cost: 114   maxlim: 1070846   bits: 22/21
c ---[ 207]---> Adder-cost: 87   maxlim: 1093374   bits: 22/21
c ---[ 206]---> Adder-cost: 114   maxlim: 1070846   bits: 22/21
c ---[ 205]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 204]---> Adder-cost: 111   maxlim: 1063678   bits: 22/21
c ---[ 203]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 202]---> Adder-cost: 111   maxlim: 1063678   bits: 22/21
c ---[ 201]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 200]---> Adder-cost: 103   maxlim: 1074430   bits: 22/21
c ---[ 199]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 198]---> Adder-cost: 96   maxlim: 1070846   bits: 22/21
c ---[ 197]---> Adder-cost: 103   maxlim: 1074430   bits: 22/21
c ---[ 196]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 195]---> Adder-cost: 103   maxlim: 1074430   bits: 22/21
c ---[ 194]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 193]---> Adder-cost: 103   maxlim: 1074430   bits: 22/21
c ---[ 192]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 191]---> Adder-cost: 83   maxlim: 1095934   bits: 22/21
c ---[ 190]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 189]---> Adder-cost: 83   maxlim: 1095934   bits: 22/21
c ---[ 188]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 187]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 186]---> Adder-cost: 103   maxlim: 1063678   bits: 22/21
c ---[ 185]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 184]---> Adder-cost: 103   maxlim: 1063678   bits: 22/21
c ---[ 183]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 182]---> Adder-cost: 115   maxlim: 1064702   bits: 22/21
c ---[ 181]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 180]---> Adder-cost: 115   maxlim: 1064702   bits: 22/21
c ---[ 179]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 178]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[ 177]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 176]---> Adder-cost: 96   maxlim: 1070846   bits: 22/21
c ---[ 175]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[ 174]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 173]---> Adder-cost: 77   maxlim: 1082622   bits: 22/21
c ---[ 172]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 171]---> Adder-cost: 77   maxlim: 1082622   bits: 22/21
c ---[ 170]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 169]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[ 168]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 167]---> Adder-cost: 117   maxlim: 1069054   bits: 22/21
c ---[ 166]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 165]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 164]---> Adder-cost: 77   maxlim: 1086206   bits: 22/21
c ---[ 163]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 162]---> Adder-cost: 77   maxlim: 1086206   bits: 22/21
c ---[ 161]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 160]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[ 159]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 158]---> Adder-cost: 111   maxlim: 1073662   bits: 22/21
c ---[ 157]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 156]---> Adder-cost: 74   maxlim: 1112062   bits: 22/21
c ---[ 155]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 154]---> Adder-cost: 98   maxlim: 1063678   bits: 22/21
c ---[ 153]---> Adder-cost: 74   maxlim: 1112062   bits: 22/21
c ---[ 152]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 151]---> Adder-cost: 80   maxlim: 1100542   bits: 22/21
c ---[ 150]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 149]---> Adder-cost: 80   maxlim: 1100542   bits: 22/21
c ---[ 148]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 147]---> Adder-cost: 113   maxlim: 1070846   bits: 22/21
c ---[ 146]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 145]---> Adder-cost: 113   maxlim: 1070846   bits: 22/21
c ---[ 144]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 143]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 142]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[ 141]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 140]---> Adder-cost: 117   maxlim: 1063678   bits: 22/21
c ---[ 139]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 138]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[ 137]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 136]---> Adder-cost: 107   maxlim: 1071870   bits: 22/21
c ---[ 135]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 134]---> Adder-cost: 115   maxlim: 1069054   bits: 22/21
c ---[ 133]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 132]---> Adder-cost: 98   maxlim: 1063678   bits: 22/21
c ---[ 131]---> Adder-cost: 115   maxlim: 1069054   bits: 22/21
c ---[ 130]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 129]---> Adder-cost: 72   maxlim: 1096958   bits: 22/21
c ---[ 128]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 127]---> Adder-cost: 72   maxlim: 1096958   bits: 22/21
c ---[ 126]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 125]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[ 124]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 123]---> Adder-cost: 84   maxlim: 1091582   bits: 22/21
c ---[ 122]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 121]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[ 120]---> Adder-cost: 88   maxlim: 1096958   bits: 22/21
c ---[ 119]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 118]---> Adder-cost: 88   maxlim: 1096958   bits: 22/21
c ---[ 117]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 116]---> Adder-cost: 68   maxlim: 1075454   bits: 22/21
c ---[ 115]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 114]---> Adder-cost: 68   maxlim: 1075454   bits: 22/21
c ---[ 113]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 112]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 111]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 110]---> Adder-cost: 113   maxlim: 1063678   bits: 22/21
c ---[ 109]---> Adder-cost: 86   maxlim: 1071870   bits: 22/21
c ---[ 108]---> Adder-cost: 109   maxlim: 1071870   bits: 22/21
c ---[ 107]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 106]---> Adder-cost: 85   maxlim: 1088766   bits: 22/21
c ---[ 105]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 104]---> Adder-cost: 85   maxlim: 1088766   bits: 22/21
c ---[ 103]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 102]---> Adder-cost: 72   maxlim: 1078014   bits: 22/21
c ---[ 101]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[ 100]---> Adder-cost: 72   maxlim: 1078014   bits: 22/21
c ---[  99]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[  98]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  97]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[  96]---> Adder-cost: 83   maxlim: 1086206   bits: 22/21
c ---[  95]---> Adder-cost: 115   maxlim: 1070846   bits: 22/21
c ---[  94]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  93]---> Adder-cost: 88   maxlim: 1074430   bits: 22/21
c ---[  92]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  91]---> Adder-cost: 88   maxlim: 1074430   bits: 22/21
c ---[  90]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  89]---> Adder-cost: 88   maxlim: 1074430   bits: 22/21
c ---[  88]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  87]---> Adder-cost: 86   maxlim: 1071870   bits: 22/21
c ---[  86]---> Adder-cost: 88   maxlim: 1074430   bits: 22/21
c ---[  85]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  84]---> Adder-cost: 85   maxlim: 1095934   bits: 22/21
c ---[  83]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  82]---> Adder-cost: 85   maxlim: 1095934   bits: 22/21
c ---[  81]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  80]---> Adder-cost: 69   maxlim: 1063678   bits: 22/21
c ---[  79]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  78]---> Adder-cost: 69   maxlim: 1063678   bits: 22/21
c ---[  77]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  76]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  75]---> Adder-cost: 83   maxlim: 1064702   bits: 22/21
c ---[  74]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  73]---> Adder-cost: 83   maxlim: 1064702   bits: 22/21
c ---[  72]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  71]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[  70]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  69]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[  68]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  67]---> Adder-cost: 81   maxlim: 1082622   bits: 22/21
c ---[  66]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  65]---> Adder-cost: 100   maxlim: 1069054   bits: 22/21
c ---[  64]---> Adder-cost: 81   maxlim: 1082622   bits: 22/21
c ---[  63]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  62]---> Adder-cost: 98   maxlim: 1069054   bits: 22/21
c ---[  61]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  60]---> Adder-cost: 98   maxlim: 1069054   bits: 22/21
c ---[  59]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  58]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[  57]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  56]---> Adder-cost: 81   maxlim: 1086206   bits: 22/21
c ---[  55]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  54]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  53]---> Adder-cost: 94   maxlim: 1073662   bits: 22/21
c ---[  52]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  51]---> Adder-cost: 94   maxlim: 1073662   bits: 22/21
c ---[  50]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  49]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[  48]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  47]---> Adder-cost: 79   maxlim: 1112062   bits: 22/21
c ---[  46]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  45]---> Adder-cost: 81   maxlim: 1100542   bits: 22/21
c ---[  44]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  43]---> Adder-cost: 100   maxlim: 1069054   bits: 22/21
c ---[  42]---> Adder-cost: 81   maxlim: 1100542   bits: 22/21
c ---[  41]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  40]---> Adder-cost: 96   maxlim: 1070846   bits: 22/21
c ---[  39]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  38]---> Adder-cost: 96   maxlim: 1070846   bits: 22/21
c ---[  37]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  36]---> Adder-cost: 98   maxlim: 1063678   bits: 22/21
c ---[  35]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  34]---> Adder-cost: 98   maxlim: 1063678   bits: 22/21
c ---[  33]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  32]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  31]---> Adder-cost: 86   maxlim: 1071870   bits: 22/21
c ---[  30]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  29]---> Adder-cost: 86   maxlim: 1071870   bits: 22/21
c ---[  28]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  27]---> Adder-cost: 100   maxlim: 1069054   bits: 22/21
c ---[  26]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  25]---> Adder-cost: 100   maxlim: 1069054   bits: 22/21
c ---[  24]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  23]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[  22]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  21]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[  20]---> Adder-cost: 77   maxlim: 1096958   bits: 22/21
c ---[  19]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  18]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[  17]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  16]---> Adder-cost: 85   maxlim: 1091582   bits: 22/21
c ---[  15]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  14]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[  13]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  12]---> Adder-cost: 89   maxlim: 1096958   bits: 22/21
c ---[  11]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[  10]---> Adder-cost: 113   maxlim: 1063678   bits: 22/21
c ---[   9]---> Adder-cost: 73   maxlim: 1075454   bits: 22/21
c ---[   8]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[   7]---> Adder-cost: 73   maxlim: 1075454   bits: 22/21
c ---[   6]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[   5]---> Adder-cost: 92   maxlim: 1071870   bits: 22/21
c ---[   4]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[   3]---> Adder-cost: 92   maxlim: 1071870   bits: 22/21
c ---[   2]---> Adder-cost: 115   maxlim: 1063678   bits: 22/21
c ---[   1]---> Adder-cost: 89   maxlim: 1088766   bits: 22/21
c ---[   0]---> Adder-cost: 113   maxlim: 1063678   bits: 22/21
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1226278  4603454 |  408759       0        0     nan |  0.000 % |
c |       102 | 1226278  4603454 |  449634     102      417     4.1 | 12.201 % |
c |       252 | 1226278  4603454 |  494598     252     1034     4.1 | 12.201 % |
c |       478 | 1226278  4603454 |  544058     478     2358     4.9 | 12.201 % |
c |       816 | 1226278  4603454 |  598464     816     4486     5.5 | 12.201 % |
c |      1323 | 1226278  4603454 |  658310    1323     7706     5.8 | 12.201 % |
c |      2082 | 1226266  4603420 |  724141    2080    12769     6.1 | 12.201 % |
c |      3222 | 1226266  4603420 |  796555    3220    22347     6.9 | 12.201 % |
c |      4930 | 1226266  4603420 |  876211    4928    38959     7.9 | 12.201 % |
c |      7492 | 1226254  4603386 |  963832    7488    58734     7.8 | 12.202 % |
c |     11336 | 1226242  4603352 | 1060215   11330    89358     7.9 | 12.203 % |
c |     17102 | 1226236  4603335 | 1166237   17095   136084     8.0 | 12.204 % |
c |     25751 | 1226218  4603284 | 1282860   25740   231396     9.0 | 12.205 % |
c |     38727 | 1226200  4603233 | 1411146   38713   347000     9.0 | 12.206 % |
c |     58189 | 1226200  4603233 | 1552261   58175   504932     8.7 | 12.206 % |
c |     87381 | 1226182  4603182 | 1707487   87363   750758     8.6 | 12.207 % |
c |    131172 | 1226140  4603063 | 1878236  131144  1147943     8.8 | 12.210 % |
c |    196856 | 1226122  4603012 | 2066060  196822  1899266     9.6 | 12.212 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.92 2/54 28681
Raw data (stat): 28681 (runsolver) R 28680 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546434227 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.87 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 32305 0 0 0 919 79 0 0 25 0 1 0 546434227 138354688 29671 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33778 29671 603 41 0 33737 0
vsize: 135112
[startup+20.0021 s]
Raw data (loadavg): 0.89 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 32883 0 0 0 1917 81 0 0 25 0 1 0 546434227 140664832 30249 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34342 30249 603 41 0 34301 0
vsize: 137368
[startup+30.0026 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 33090 0 0 0 2916 83 0 0 25 0 1 0 546434227 141475840 30456 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34540 30456 603 41 0 34499 0
vsize: 138160
[startup+40.003 s]
Raw data (loadavg): 0.92 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 33242 0 0 0 3915 83 0 0 25 0 1 0 546434227 142016512 30608 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34672 30608 603 41 0 34631 0
vsize: 138688
[startup+50.0039 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 33387 0 0 0 4915 84 0 0 25 0 1 0 546434227 142692352 30753 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34837 30753 603 41 0 34796 0
vsize: 139348
[startup+60.0044 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 33517 0 0 0 5914 84 0 0 25 0 1 0 546434227 143253504 30883 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34974 30883 603 41 0 34933 0
vsize: 139896
[startup+70.0058 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 33646 0 0 0 6914 85 0 0 25 0 1 0 546434227 143659008 31012 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35073 31012 603 41 0 35032 0
vsize: 140292
[startup+80.0067 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 33740 0 0 0 7913 86 0 0 25 0 1 0 546434227 144064512 31106 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35172 31106 603 41 0 35131 0
vsize: 140688
[startup+90.0072 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 33863 0 0 0 8912 87 0 0 25 0 1 0 546434227 144732160 31229 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35335 31229 603 41 0 35294 0
vsize: 141340
[startup+100.008 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 33903 0 0 0 9911 88 0 0 25 0 1 0 546434227 144867328 31269 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35368 31269 603 41 0 35327 0
vsize: 141472
[startup+110.01 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 33978 0 0 0 10911 88 0 0 25 0 1 0 546434227 145137664 31344 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35434 31344 603 41 0 35393 0
vsize: 141736
[startup+120.01 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34042 0 0 0 11910 89 0 0 25 0 1 0 546434227 145408000 31408 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35500 31408 603 41 0 35459 0
vsize: 142000
[startup+130.01 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34098 0 0 0 12910 89 0 0 25 0 1 0 546434227 145678336 31464 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35566 31464 603 41 0 35525 0
vsize: 142264
[startup+140.011 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34158 0 0 0 13910 90 0 0 25 0 1 0 546434227 145813504 31524 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35599 31524 603 41 0 35558 0
vsize: 142396
[startup+150.011 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34226 0 0 0 14909 90 0 0 25 0 1 0 546434227 146083840 31592 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35665 31592 603 41 0 35624 0
vsize: 142660
[startup+160.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34280 0 0 0 15909 91 0 0 25 0 1 0 546434227 146354176 31646 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35731 31646 603 41 0 35690 0
vsize: 142924
[startup+170.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34332 0 0 0 16909 91 0 0 25 0 1 0 546434227 146489344 31698 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35764 31698 603 41 0 35723 0
vsize: 143056
[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34383 0 0 0 17908 92 0 0 25 0 1 0 546434227 146759680 31749 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35830 31749 603 41 0 35789 0
vsize: 143320
[startup+190.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34450 0 0 0 18908 92 0 0 25 0 1 0 546434227 147030016 31816 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35896 31816 603 41 0 35855 0
vsize: 143584
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34509 0 0 0 19907 92 0 0 25 0 1 0 546434227 147165184 31875 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35929 31875 603 41 0 35888 0
vsize: 143716
[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34562 0 0 0 20907 93 0 0 25 0 1 0 546434227 147697664 31928 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36059 31928 603 41 0 36018 0
vsize: 144236
[startup+220.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34614 0 0 0 21907 93 0 0 25 0 1 0 546434227 147963904 31980 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36124 31980 603 41 0 36083 0
vsize: 144496
[startup+230.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34674 0 0 0 22907 93 0 0 25 0 1 0 546434227 148099072 32040 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36157 32040 603 41 0 36116 0
vsize: 144628
[startup+240.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34735 0 0 0 23906 94 0 0 25 0 1 0 546434227 148369408 32101 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36223 32101 603 41 0 36182 0
vsize: 144892
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34781 0 0 0 24906 94 0 0 25 0 1 0 546434227 148504576 32147 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36256 32147 603 41 0 36215 0
vsize: 145024
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34827 0 0 0 25906 94 0 0 25 0 1 0 546434227 148774912 32193 4294967295 134512640 134672761 3221224544 3221223668 134566045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36322 32193 603 41 0 36281 0
vsize: 145288
[startup+270.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34880 0 0 0 26906 95 0 0 25 0 1 0 546434227 148910080 32246 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36355 32246 603 41 0 36314 0
vsize: 145420
[startup+280.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34927 0 0 0 27906 95 0 0 25 0 1 0 546434227 149180416 32293 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36421 32293 603 41 0 36380 0
vsize: 145684
[startup+290.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 34985 0 0 0 28906 95 0 0 25 0 1 0 546434227 149315584 32351 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36454 32351 603 41 0 36413 0
vsize: 145816
[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35054 0 0 0 29906 96 0 0 25 0 1 0 546434227 149585920 32420 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36520 32420 603 41 0 36479 0
vsize: 146080
[startup+310.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35100 0 0 0 30906 96 0 0 25 0 1 0 546434227 149721088 32466 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36553 32466 603 41 0 36512 0
vsize: 146212
[startup+320.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35142 0 0 0 31906 96 0 0 25 0 1 0 546434227 149991424 32508 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36619 32508 603 41 0 36578 0
vsize: 146476
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35200 0 0 0 32906 96 0 0 25 0 1 0 546434227 150126592 32566 4294967295 134512640 134672761 3221224544 3221223676 134565974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36652 32566 603 41 0 36611 0
vsize: 146608
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35247 0 0 0 33906 96 0 0 25 0 1 0 546434227 150396928 32613 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36718 32613 603 41 0 36677 0
vsize: 146872
[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35302 0 0 0 34906 96 0 0 25 0 1 0 546434227 150532096 32668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36751 32668 603 41 0 36710 0
vsize: 147004
[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35355 0 0 0 35906 96 0 0 25 0 1 0 546434227 150802432 32721 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36817 32721 603 41 0 36776 0
vsize: 147268
[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35403 0 0 0 36906 97 0 0 25 0 1 0 546434227 150933504 32769 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36849 32769 603 41 0 36808 0
vsize: 147396
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35450 0 0 0 37906 97 0 0 25 0 1 0 546434227 151068672 32816 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36882 32816 603 41 0 36841 0
vsize: 147528
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35505 0 0 0 38906 97 0 0 25 0 1 0 546434227 151339008 32871 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36948 32871 603 41 0 36907 0
vsize: 147792
[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35563 0 0 0 39906 97 0 0 25 0 1 0 546434227 151609344 32929 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37014 32929 603 41 0 36973 0
vsize: 148056
[startup+410.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35650 0 0 0 40906 97 0 0 25 0 1 0 546434227 151875584 33016 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37079 33016 603 41 0 37038 0
vsize: 148316
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35697 0 0 0 41906 98 0 0 25 0 1 0 546434227 152145920 33063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37145 33063 603 41 0 37104 0
vsize: 148580
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35741 0 0 0 42906 98 0 0 25 0 1 0 546434227 152281088 33107 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37178 33107 603 41 0 37137 0
vsize: 148712
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35786 0 0 0 43906 98 0 0 25 0 1 0 546434227 152416256 33152 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37211 33152 603 41 0 37170 0
vsize: 148844
[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35831 0 0 0 44906 98 0 0 25 0 1 0 546434227 152547328 33197 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37243 33197 603 41 0 37202 0
vsize: 148972
[startup+460.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35876 0 0 0 45906 98 0 0 25 0 1 0 546434227 153341952 33242 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37437 33242 603 41 0 37396 0
vsize: 149748
[startup+470.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35927 0 0 0 46906 98 0 0 25 0 1 0 546434227 153477120 33293 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37470 33293 603 41 0 37429 0
vsize: 149880
[startup+480.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 35973 0 0 0 47906 99 0 0 25 0 1 0 546434227 153747456 33339 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37536 33339 603 41 0 37495 0
vsize: 150144
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36024 0 0 0 48906 99 0 0 25 0 1 0 546434227 153882624 33390 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37569 33390 603 41 0 37528 0
vsize: 150276
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36061 0 0 0 49906 99 0 0 25 0 1 0 546434227 154017792 33427 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37602 33427 603 41 0 37561 0
vsize: 150408
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36098 0 0 0 50906 99 0 0 25 0 1 0 546434227 154148864 33464 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37634 33464 603 41 0 37593 0
vsize: 150536
[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36136 0 0 0 51906 99 0 0 25 0 1 0 546434227 154284032 33502 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37667 33502 603 41 0 37626 0
vsize: 150668
[startup+530.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36173 0 0 0 52906 99 0 0 25 0 1 0 546434227 154419200 33539 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37700 33539 603 41 0 37659 0
vsize: 150800
[startup+540.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36209 0 0 0 53906 100 0 0 25 0 1 0 546434227 154550272 33575 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37732 33575 603 41 0 37691 0
vsize: 150928
[startup+550.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36266 0 0 0 54906 100 0 0 25 0 1 0 546434227 154820608 33632 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37798 33632 603 41 0 37757 0
vsize: 151192
[startup+560.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36317 0 0 0 55906 100 0 0 25 0 1 0 546434227 155090944 33683 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37864 33683 603 41 0 37823 0
vsize: 151456
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36356 0 0 0 56906 101 0 0 25 0 1 0 546434227 155226112 33722 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37897 33722 603 41 0 37856 0
vsize: 151588
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36398 0 0 0 57906 101 0 0 25 0 1 0 546434227 155365376 33764 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37931 33764 603 41 0 37890 0
vsize: 151724
[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36441 0 0 0 58906 101 0 0 25 0 1 0 546434227 155500544 33807 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37964 33807 603 41 0 37923 0
vsize: 151856
[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36485 0 0 0 59906 101 0 0 25 0 1 0 546434227 155635712 33851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37997 33851 603 41 0 37956 0
vsize: 151988
[startup+610.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36538 0 0 0 60906 101 0 0 25 0 1 0 546434227 155906048 33904 4294967295 134512640 134672761 3221224544 3221223668 134566136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38063 33904 603 41 0 38022 0
vsize: 152252
[startup+620.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36592 0 0 0 61906 101 0 0 25 0 1 0 546434227 156041216 33958 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38096 33958 603 41 0 38055 0
vsize: 152384
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36632 0 0 0 62906 102 0 0 25 0 1 0 546434227 156311552 33998 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38162 33998 603 41 0 38121 0
vsize: 152648
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36677 0 0 0 63906 102 0 0 25 0 1 0 546434227 156446720 34043 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38195 34043 603 41 0 38154 0
vsize: 152780
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36725 0 0 0 64906 102 0 0 25 0 1 0 546434227 156577792 34091 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38227 34091 603 41 0 38186 0
vsize: 152908
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36867 0 0 0 65905 103 0 0 25 0 1 0 546434227 157110272 34233 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38357 34233 603 41 0 38316 0
vsize: 153428
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 36994 0 0 0 66905 103 0 0 25 0 1 0 546434227 157646848 34360 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38488 34360 603 41 0 38447 0
vsize: 153952
[startup+680.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37109 0 0 0 67904 104 0 0 25 0 1 0 546434227 158187520 34475 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38620 34475 603 41 0 38579 0
vsize: 154480
[startup+690.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37242 0 0 0 68904 104 0 0 25 0 1 0 546434227 158584832 34608 4294967295 134512640 134672761 3221224544 3221223712 134561027 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38717 34608 603 41 0 38676 0
vsize: 154868
[startup+700.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37293 0 0 0 69904 105 0 0 25 0 1 0 546434227 158855168 34659 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38783 34659 603 41 0 38742 0
vsize: 155132
[startup+710.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37341 0 0 0 70904 105 0 0 25 0 1 0 546434227 158990336 34707 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38816 34707 603 41 0 38775 0
vsize: 155264
[startup+720.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37390 0 0 0 71904 105 0 0 25 0 1 0 546434227 159260672 34756 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38882 34756 603 41 0 38841 0
vsize: 155528
[startup+730.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37424 0 0 0 72904 105 0 0 25 0 1 0 546434227 159391744 34790 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38914 34790 603 41 0 38873 0
vsize: 155656
[startup+740.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37460 0 0 0 73904 105 0 0 25 0 1 0 546434227 159526912 34826 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38947 34826 603 41 0 38906 0
vsize: 155788
[startup+750.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37493 0 0 0 74904 106 0 0 25 0 1 0 546434227 159662080 34859 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38980 34859 603 41 0 38939 0
vsize: 155920
[startup+760.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37525 0 0 0 75904 106 0 0 25 0 1 0 546434227 159797248 34891 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39013 34891 603 41 0 38972 0
vsize: 156052
[startup+770.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37560 0 0 0 76904 106 0 0 25 0 1 0 546434227 159932416 34926 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39046 34926 603 41 0 39005 0
vsize: 156184
[startup+780.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37604 0 0 0 77904 106 0 0 25 0 1 0 546434227 160067584 34970 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39079 34970 603 41 0 39038 0
vsize: 156316
[startup+790.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37636 0 0 0 78904 106 0 0 25 0 1 0 546434227 160202752 35002 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39112 35002 603 41 0 39071 0
vsize: 156448
[startup+800.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37675 0 0 0 79904 106 0 0 25 0 1 0 546434227 160337920 35041 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39145 35041 603 41 0 39104 0
vsize: 156580
[startup+810.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37709 0 0 0 80904 106 0 0 25 0 1 0 546434227 160473088 35075 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39178 35075 603 41 0 39137 0
vsize: 156712
[startup+820.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37739 0 0 0 81904 107 0 0 25 0 1 0 546434227 160604160 35105 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39210 35105 603 41 0 39169 0
vsize: 156840
[startup+830.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37779 0 0 0 82904 107 0 0 25 0 1 0 546434227 160739328 35145 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39243 35145 603 41 0 39202 0
vsize: 156972
[startup+840.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37820 0 0 0 83904 107 0 0 25 0 1 0 546434227 160874496 35186 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39276 35186 603 41 0 39235 0
vsize: 157104
[startup+850.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37848 0 0 0 84904 107 0 0 25 0 1 0 546434227 161009664 35214 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39309 35214 603 41 0 39268 0
vsize: 157236
[startup+860.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37882 0 0 0 85904 107 0 0 25 0 1 0 546434227 161144832 35248 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39342 35248 603 41 0 39301 0
vsize: 157368
[startup+870.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37912 0 0 0 86904 108 0 0 25 0 1 0 546434227 161280000 35278 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39375 35278 603 41 0 39334 0
vsize: 157500
[startup+880.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37947 0 0 0 87904 108 0 0 25 0 1 0 546434227 161415168 35313 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39408 35313 603 41 0 39367 0
vsize: 157632
[startup+890.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 37989 0 0 0 88904 108 0 0 25 0 1 0 546434227 161550336 35355 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39441 35355 603 41 0 39400 0
vsize: 157764
[startup+900.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38026 0 0 0 89904 108 0 0 25 0 1 0 546434227 161685504 35392 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39474 35392 603 41 0 39433 0
vsize: 157896
[startup+910.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38065 0 0 0 90904 108 0 0 25 0 1 0 546434227 161820672 35431 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39507 35431 603 41 0 39466 0
vsize: 158028
[startup+920.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38107 0 0 0 91904 108 0 0 25 0 1 0 546434227 162091008 35473 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39573 35473 603 41 0 39532 0
vsize: 158292
[startup+930.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38148 0 0 0 92905 108 0 0 25 0 1 0 546434227 162226176 35514 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39606 35514 603 41 0 39565 0
vsize: 158424
[startup+940.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38185 0 0 0 93905 108 0 0 25 0 1 0 546434227 162361344 35551 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39639 35551 603 41 0 39598 0
vsize: 158556
[startup+950.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38214 0 0 0 94905 109 0 0 25 0 1 0 546434227 162496512 35580 4294967295 134512640 134672761 3221224544 3221223712 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39672 35580 603 41 0 39631 0
vsize: 158688
[startup+960.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38251 0 0 0 95905 109 0 0 25 0 1 0 546434227 162631680 35617 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39705 35617 603 41 0 39664 0
vsize: 158820
[startup+970.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38282 0 0 0 96905 109 0 0 25 0 1 0 546434227 162770944 35648 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39739 35648 603 41 0 39698 0
vsize: 158956
[startup+980.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38314 0 0 0 97905 109 0 0 25 0 1 0 546434227 162906112 35680 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39772 35680 603 41 0 39731 0
vsize: 159088
[startup+990.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38341 0 0 0 98906 109 0 0 25 0 1 0 546434227 162906112 35707 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39772 35707 603 41 0 39731 0
vsize: 159088
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38379 0 0 0 99906 109 0 0 25 0 1 0 546434227 163045376 35745 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39806 35745 603 41 0 39765 0
vsize: 159224
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38422 0 0 0 100906 109 0 0 25 0 1 0 546434227 163311616 35788 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39871 35788 603 41 0 39830 0
vsize: 159484
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38456 0 0 0 101906 109 0 0 25 0 1 0 546434227 163446784 35822 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39904 35822 603 41 0 39863 0
vsize: 159616
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38490 0 0 0 102906 109 0 0 25 0 1 0 546434227 163581952 35856 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39937 35856 603 41 0 39896 0
vsize: 159748
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38524 0 0 0 103906 109 0 0 25 0 1 0 546434227 163717120 35890 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39970 35890 603 41 0 39929 0
vsize: 159880
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38563 0 0 0 104906 109 0 0 25 0 1 0 546434227 163848192 35929 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40002 35929 603 41 0 39961 0
vsize: 160008
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38600 0 0 0 105906 110 0 0 25 0 1 0 546434227 163983360 35966 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40035 35966 603 41 0 39994 0
vsize: 160140
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38640 0 0 0 106906 110 0 0 25 0 1 0 546434227 165167104 36006 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40324 36006 603 41 0 40283 0
vsize: 161296
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38675 0 0 0 107906 110 0 0 25 0 1 0 546434227 165302272 36041 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40357 36041 603 41 0 40316 0
vsize: 161428
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38712 0 0 0 108906 110 0 0 25 0 1 0 546434227 165437440 36078 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40390 36078 603 41 0 40349 0
vsize: 161560
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38751 0 0 0 109906 110 0 0 25 0 1 0 546434227 165572608 36117 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40423 36117 603 41 0 40382 0
vsize: 161692
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38790 0 0 0 110906 110 0 0 25 0 1 0 546434227 165707776 36156 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40456 36156 603 41 0 40415 0
vsize: 161824
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38819 0 0 0 111906 110 0 0 25 0 1 0 546434227 165842944 36185 4294967295 134512640 134672761 3221224544 3221223668 134566045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40489 36185 603 41 0 40448 0
vsize: 161956
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38849 0 0 0 112906 110 0 0 25 0 1 0 546434227 165978112 36215 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40522 36215 603 41 0 40481 0
vsize: 162088
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38882 0 0 0 113906 111 0 0 25 0 1 0 546434227 166113280 36248 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40555 36248 603 41 0 40514 0
vsize: 162220
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38932 0 0 0 114906 111 0 0 25 0 1 0 546434227 166248448 36298 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40588 36298 603 41 0 40547 0
vsize: 162352
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38960 0 0 0 115906 111 0 0 25 0 1 0 546434227 166383616 36326 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40621 36326 603 41 0 40580 0
vsize: 162484
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 38988 0 0 0 116906 111 0 0 25 0 1 0 546434227 166518784 36354 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40654 36354 603 41 0 40613 0
vsize: 162616
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 39019 0 0 0 117906 112 0 0 25 0 1 0 546434227 166653952 36385 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40687 36385 603 41 0 40646 0
vsize: 162748
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 39047 0 0 0 118906 112 0 0 25 0 1 0 546434227 166653952 36413 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40687 36413 603 41 0 40646 0
vsize: 162748
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 28681
Raw data (stat): 28681 (minisat+) R 28680 23176 23175 0 -1 0 39077 0 0 0 119906 112 0 0 25 0 1 0 546434227 166789120 36443 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40720 36443 603 41 0 40679 0
vsize: 162880
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 28681
Raw data (stat): 28681 (minisat+) Z 28680 23176 23175 0 -1 12 39079 0 0 0 119906 119 0 0 24 0 1 0 546434227 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.14
CPU time (s): 1200.26
CPU user time (s): 1199.07
CPU system time (s): 1.19882
CPU usage (%): 100.01
Max. virtual memory (Kb): 162880
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####