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/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-dg012142.opb
MD5SUM	d2a2dc4ff7a501b7efb12f8e274e186d
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	16640
Biggest coefficient in the objective function	5242880000
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	1683190350400
Number of bits of the sum of numbers in the objective function	41
Biggest number in a constraint	5242880000
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	1683190350400
Number of bits of the biggest sum of numbers	41
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1269.98
Number of variables	29440
Total number of constraints	6310
Number of constraints which are clauses	40
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	6270
Minimum length of a constraint	1
Maximum length of a constraint	251
Trace number 13941

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        696724 kB
Buffers:         33856 kB
Cached:         278008 kB
SwapCached:        528 kB
Active:         187212 kB
Inactive:       126684 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        696444 kB
SwapTotal:     2097892 kB
SwapFree:      2096468 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            18360 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 22:37:52 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 20108 7 1200.33 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2731 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[2771]---> Adder-cost: 121   maxlim: 16382   bits: 15/14
c ---[2768]---> Adder-cost: 128   maxlim: 32766   bits: 16/15
c ---[2766]---> Adder-cost: 132   maxlim: 32766   bits: 16/15
c ---[2758]---> Adder-cost: 144   maxlim: 98301   bits: 18/17
c ---[2744]---> Adder-cost: 173   maxlim: 524287   bits: 20/19
c ---[2742]---> Adder-cost: 173   maxlim: 524287   bits: 20/19
c ---[2740]---> Adder-cost: 237   maxlim: 524287   bits: 20/19
c ---[2738]---> Adder-cost: 205   maxlim: 524287   bits: 20/19
c ---[2736]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2734]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2732]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2730]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2728]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2726]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2724]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2722]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2720]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2718]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2716]---> Adder-cost: 117   maxlim: 1048575   bits: 21/20
c ---[2714]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2712]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2710]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2708]---> Adder-cost: 117   maxlim: 1048575   bits: 21/20
c ---[2706]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2704]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2702]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2700]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2698]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2696]---> Adder-cost: 120   maxlim: 1048575   bits: 21/20
c ---[2694]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2692]---> Adder-cost: 117   maxlim: 1048575   bits: 21/20
c ---[2690]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2688]---> Adder-cost: 79   maxlim: 1048575   bits: 21/20
c ---[2686]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2684]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2682]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2680]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2678]---> Adder-cost: 75   maxlim: 524287   bits: 20/19
c ---[2676]---> Adder-cost: 213   maxlim: 1048574   bits: 21/20
c ---[2674]---> Adder-cost: 214   maxlim: 1572862   bits: 22/21
c ---[2672]---> Adder-cost: 214   maxlim: 1572862   bits: 22/21
c ---[2670]---> Adder-cost: 214   maxlim: 1310718   bits: 22/21
c ---[2668]---> Adder-cost: 214   maxlim: 1310718   bits: 22/21
c ---[2666]---> Adder-cost: 214   maxlim: 1310718   bits: 22/21
c ---[2664]---> Adder-cost: 206   maxlim: 1310718   bits: 22/21
c ---[2662]---> Adder-cost: 206   maxlim: 1179646   bits: 22/21
c ---[2660]---> Adder-cost: 206   maxlim: 1179646   bits: 22/21
c ---[2658]---> Adder-cost: 198   maxlim: 1179646   bits: 22/21
c ---[2656]---> Adder-cost: 198   maxlim: 1114110   bits: 22/21
c ---[2654]---> Adder-cost: 198   maxlim: 1114110   bits: 22/21
c ---[2652]---> Adder-cost: 190   maxlim: 1114110   bits: 22/21
c ---[2650]---> Adder-cost: 190   maxlim: 1081342   bits: 22/21
c ---[2648]---> Adder-cost: 174   maxlim: 1064958   bits: 22/21
c ---[2646]---> Adder-cost: 181   maxlim: 1048574   bits: 21/20
c ---[2644]---> Adder-cost: 182   maxlim: 1572862   bits: 22/21
c ---[2642]---> Adder-cost: 182   maxlim: 1572862   bits: 22/21
c ---[2640]---> Adder-cost: 184   maxlim: 1310718   bits: 22/21
c ---[2638]---> Adder-cost: 184   maxlim: 1310718   bits: 22/21
c ---[2636]---> Adder-cost: 184   maxlim: 1310718   bits: 22/21
c ---[2634]---> Adder-cost: 176   maxlim: 1310718   bits: 22/21
c ---[2632]---> Adder-cost: 178   maxlim: 1179646   bits: 22/21
c ---[2630]---> Adder-cost: 178   maxlim: 1179646   bits: 22/21
c ---[2628]---> Adder-cost: 170   maxlim: 1179646   bits: 22/21
c ---[2626]---> Adder-cost: 170   maxlim: 1114110   bits: 22/21
c ---[2624]---> Adder-cost: 172   maxlim: 1114110   bits: 22/21
c ---[2622]---> Adder-cost: 164   maxlim: 1114110   bits: 22/21
c ---[2620]---> Adder-cost: 166   maxlim: 1081342   bits: 22/21
c ---[2618]---> Adder-cost: 152   maxlim: 1064958   bits: 22/21
c ---[2616]---> Adder-cost: 241   maxlim: 1048574   bits: 21/20
c ---[2614]---> Adder-cost: 242   maxlim: 1572862   bits: 22/21
c ---[2612]---> Adder-cost: 242   maxlim: 1572862   bits: 22/21
c ---[2610]---> Adder-cost: 244   maxlim: 1572862   bits: 22/21
c ---[2608]---> Adder-cost: 240   maxlim: 1572862   bits: 22/21
c ---[2606]---> Adder-cost: 240   maxlim: 1572862   bits: 22/21
c ---[2604]---> Adder-cost: 240   maxlim: 1310718   bits: 22/21
c ---[2602]---> Adder-cost: 262   maxlim: 1310718   bits: 22/21
c ---[2600]---> Adder-cost: 262   maxlim: 1310718   bits: 22/21
c ---[2598]---> Adder-cost: 230   maxlim: 1179646   bits: 22/21
c ---[2596]---> Adder-cost: 222   maxlim: 1179646   bits: 22/21
c ---[2594]---> Adder-cost: 220   maxlim: 1114110   bits: 22/21
c ---[2592]---> Adder-cost: 212   maxlim: 1114110   bits: 22/21
c ---[2590]---> Adder-cost: 210   maxlim: 1081342   bits: 22/21
c ---[2588]---> Adder-cost: 198   maxlim: 1064958   bits: 22/21
c ---[2586]---> Adder-cost: 241   maxlim: 1048574   bits: 21/20
c ---[2584]---> Adder-cost: 242   maxlim: 1572862   bits: 22/21
c ---[2582]---> Adder-cost: 242   maxlim: 1572862   bits: 22/21
c ---[2580]---> Adder-cost: 242   maxlim: 1572862   bits: 22/21
c ---[2578]---> Adder-cost: 238   maxlim: 1572862   bits: 22/21
c ---[2576]---> Adder-cost: 238   maxlim: 1572862   bits: 22/21
c ---[2574]---> Adder-cost: 240   maxlim: 1310718   bits: 22/21
c ---[2572]---> Adder-cost: 232   maxlim: 1310718   bits: 22/21
c ---[2570]---> Adder-cost: 232   maxlim: 1310718   bits: 22/21
c ---[2568]---> Adder-cost: 230   maxlim: 1179646   bits: 22/21
c ---[2566]---> Adder-cost: 222   maxlim: 1179646   bits: 22/21
c ---[2564]---> Adder-cost: 218   maxlim: 1114110   bits: 22/21
c ---[2562]---> Adder-cost: 212   maxlim: 1114110   bits: 22/21
c ---[2560]---> Adder-cost: 210   maxlim: 1081342   bits: 22/21
c ---[2558]---> Adder-cost: 198   maxlim: 1064958   bits: 22/21
c ---[2556]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2554]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2552]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2550]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2548]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2546]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2544]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2542]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2540]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2538]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2536]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2534]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2532]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2530]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2528]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2526]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2524]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2522]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2520]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2518]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2516]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2514]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2512]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2510]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2508]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2506]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2504]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2502]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2500]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2498]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2496]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2494]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2492]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2490]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2488]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2486]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2484]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2482]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2480]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2478]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2476]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2474]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2472]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2470]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2468]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2466]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2464]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2462]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2460]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2458]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2456]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2454]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2452]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2450]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2448]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2446]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2444]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2442]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2440]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2438]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2436]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2434]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2432]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2430]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2428]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2426]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2424]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2422]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2420]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2418]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2416]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2414]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2412]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2410]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2408]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2406]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2404]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2402]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2400]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2398]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2396]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2394]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2392]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2390]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2388]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2386]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2384]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2382]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2380]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2378]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2376]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2374]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2372]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2370]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2368]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2366]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2364]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2362]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2360]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2358]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2356]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2354]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2352]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2350]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2348]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2346]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2344]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2342]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2340]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2338]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2336]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2334]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2332]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2330]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2328]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2326]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2324]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2322]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2320]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2318]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2316]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2314]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2312]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2310]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2308]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2306]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2304]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2302]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2300]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2298]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2296]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2294]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2292]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2290]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2288]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2286]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2284]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2282]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2280]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2278]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2276]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2274]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2272]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2270]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2268]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2266]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2264]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2262]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2260]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2258]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2256]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[2254]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[2252]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[2250]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[2248]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[2246]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[2244]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[2242]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[2240]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[2238]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[2236]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[2234]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[2232]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[2230]---> Adder-cost: 138   maxlim: 1114110   bits: 22/21
c ---[2228]---> Adder-cost: 134   maxlim: 1081342   bits: 22/21
c ---[2226]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2224]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2222]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2220]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2218]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2216]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2214]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2212]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2210]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2208]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2206]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2204]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2202]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2200]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2198]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2196]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2194]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2192]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2190]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2188]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2186]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2184]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2182]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2180]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2178]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2176]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2174]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2172]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2170]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2168]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2166]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2164]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2162]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2160]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2158]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2156]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2154]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2152]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2150]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2148]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2146]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2144]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2142]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2140]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2138]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2136]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[2134]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[2132]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[2130]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[2128]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[2126]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[2124]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[2122]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[2120]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[2118]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[2116]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[2114]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[2112]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[2110]---> Adder-cost: 138   maxlim: 1114110   bits: 22/21
c ---[2108]---> Adder-cost: 134   maxlim: 1081342   bits: 22/21
c ---[2106]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2104]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2102]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2100]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2098]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2096]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2094]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2092]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2090]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2088]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2086]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2084]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2082]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2080]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2078]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2076]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2074]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2072]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2070]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2068]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2066]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2064]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2062]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2060]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2058]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2056]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2054]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2052]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2050]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2048]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2046]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2044]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2042]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2040]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2038]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2036]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2034]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2032]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2030]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2028]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2026]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[2024]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2022]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[2020]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[2018]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[2016]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[2014]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2012]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2010]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2008]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2006]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[2004]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2002]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[2000]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1998]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1996]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1994]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1992]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1990]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[1988]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[1986]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[1984]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1982]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1980]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1978]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1976]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1974]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1972]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1970]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1968]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1966]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1964]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1962]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1960]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[1958]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[1956]---> Adder-cost: 159   maxlim: 2097150   bits: 22/21
c ---[1954]---> Adder-cost: 159   maxlim: 2097150   bits: 22/21
c ---[1952]---> Adder-cost: 159   maxlim: 2097150   bits: 22/21
c ---[1950]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[1948]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[1946]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[1944]---> Adder-cost: 154   maxlim: 1572862   bits: 22/21
c ---[1942]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1940]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1938]---> Adder-cost: 150   maxlim: 1310718   bits: 22/21
c ---[1936]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1934]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1932]---> Adder-cost: 146   maxlim: 1179646   bits: 22/21
c ---[1930]---> Adder-cost: 142   maxlim: 1114110   bits: 22/21
c ---[1928]---> Adder-cost: 138   maxlim: 1081342   bits: 22/21
c ---[1926]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[1924]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1922]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1920]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1918]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1916]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1914]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1912]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1910]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1908]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1906]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1904]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1902]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1900]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[1898]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[1896]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[1894]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[1892]---> Adder-cost: 154   maxlim: 2097150   bits: 22/21
c ---[1890]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1888]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1886]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1884]---> Adder-cost: 150   maxlim: 1572862   bits: 22/21
c ---[1882]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1880]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1878]---> Adder-cost: 146   maxlim: 1310718   bits: 22/21
c ---[1876]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[1874]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[1872]---> Adder-cost: 142   maxlim: 1179646   bits: 22/21
c ---[1870]---> Adder-cost: 138   maxlim: 1114110   bits: 22/21
c ---[1868]---> Adder-cost: 134   maxlim: 1081342   bits: 22/21
c ---[1866]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[1864]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1862]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1860]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1858]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1856]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1854]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1852]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1850]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1848]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1846]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1844]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1842]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1840]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[1838]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[1836]---> Adder-cost: 120   maxlim: 2097150   bits: 22/21
c ---[1834]---> Adder-cost: 120   maxlim: 2097150   bits: 22/21
c ---[1832]---> Adder-cost: 120   maxlim: 2097150   bits: 22/21
c ---[1830]---> Adder-cost: 120   maxlim: 2097150   bits: 22/21
c ---[1828]---> Adder-cost: 120   maxlim: 2097150   bits: 22/21
c ---[1826]---> Adder-cost: 120   maxlim: 2097150   bits: 22/21
c ---[1824]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1822]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1820]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1818]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1816]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1814]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1812]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1810]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1808]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[1806]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[1804]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1802]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1800]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1798]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1796]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1794]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1792]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1790]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1788]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1786]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1784]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1782]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1780]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[1778]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[1776]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[1774]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1772]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1770]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1768]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1766]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1764]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1762]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1760]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1758]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1756]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1754]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1752]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1750]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[1748]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[1746]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[1744]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1742]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1740]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1738]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1736]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1734]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1732]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1730]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1728]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1726]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1724]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1722]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1720]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[1718]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[1716]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[1714]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1712]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1710]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1708]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1706]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1704]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1702]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1700]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1698]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1696]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1694]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1692]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1690]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[1688]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[1686]---> Adder-cost: 117   maxlim: 1048574   bits: 21/20
c ---[1684]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1682]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1680]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1678]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1676]---> Adder-cost: 118   maxlim: 1572862   bits: 22/21
c ---[1674]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1672]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1670]---> Adder-cost: 116   maxlim: 1310718   bits: 22/21
c ---[1668]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1666]---> Adder-cost: 114   maxlim: 1179646   bits: 22/21
c ---[1664]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1662]---> Adder-cost: 112   maxlim: 1114110   bits: 22/21
c ---[1660]---> Adder-cost: 110   maxlim: 1081342   bits: 22/21
c ---[1658]---> Adder-cost: 108   maxlim: 1064958   bits: 22/21
c ---[1656]---> Adder-cost: 34   maxlim: 128383   bits: 18/17
c ---[1654]---> Adder-cost: 32   maxlim: 63999   bits: 17/16
c ---[1652]---> Adder-cost: 32   maxlim: 63487   bits: 17/16
c ---[1650]---> Adder-cost: 34   maxlim: 127871   bits: 18/17
c ---[1648]---> Adder-cost: 32   maxlim: 64511   bits: 17/16
c ---[1646]---> Adder-cost: 32   maxlim: 63999   bits: 17/16
c ---[1644]---> Adder-cost: 68   maxlim: 258302   bits: 19/18
c ---[1642]---> Adder-cost: 72   maxlim: 388478   bits: 20/19
c ---[1640]---> Adder-cost: 76   maxlim: 650110   bits: 21/20
c ---[1638]---> Adder-cost: 80   maxlim: 1107966   bits: 22/21
c ---[1636]---> Adder-cost: 80   maxlim: 1105918   bits: 22/21
c ---[1634]---> Adder-cost: 80   maxlim: 1104638   bits: 22/21
c ---[1632]---> Adder-cost: 80   maxlim: 1107454   bits: 22/21
c ---[1630]---> Adder-cost: 80   maxlim: 1105406   bits: 22/21
c ---[1628]---> Adder-cost: 80   maxlim: 1077118   bits: 22/21
c ---[1626]---> Adder-cost: 80   maxlim: 1074686   bits: 22/21
c ---[1624]---> Adder-cost: 80   maxlim: 1060222   bits: 22/21
c ---[1622]---> Adder-cost: 80   maxlim: 1062526   bits: 22/21
c ---[1620]---> Adder-cost: 80   maxlim: 1054078   bits: 22/21
c ---[1618]---> Adder-cost: 80   maxlim: 1053822   bits: 22/21
c ---[1616]---> Adder-cost: 80   maxlim: 1050366   bits: 22/21
c ---[1614]---> Adder-cost: 64   maxlim: 129534   bits: 18/17
c ---[1612]---> Adder-cost: 68   maxlim: 194430   bits: 19/18
c ---[1610]---> Adder-cost: 72   maxlim: 324350   bits: 20/19
c ---[1608]---> Adder-cost: 76   maxlim: 553726   bits: 21/20
c ---[1606]---> Adder-cost: 80   maxlim: 1077374   bits: 22/21
c ---[1604]---> Adder-cost: 80   maxlim: 1077886   bits: 22/21
c ---[1602]---> Adder-cost: 80   maxlim: 1076478   bits: 22/21
c ---[1600]---> Adder-cost: 80   maxlim: 1062014   bits: 22/21
c ---[1598]---> Adder-cost: 80   maxlim: 1063166   bits: 22/21
c ---[1596]---> Adder-cost: 80   maxlim: 1062526   bits: 22/21
c ---[1594]---> Adder-cost: 80   maxlim: 1062910   bits: 22/21
c ---[1592]---> Adder-cost: 80   maxlim: 1054590   bits: 22/21
c ---[1590]---> Adder-cost: 80   maxlim: 1055230   bits: 22/21
c ---[1588]---> Adder-cost: 80   maxlim: 1051262   bits: 22/21
c ---[1586]---> Adder-cost: 80   maxlim: 1049470   bits: 22/21
c ---[1584]---> Adder-cost: 64   maxlim: 128510   bits: 18/17
c ---[1582]---> Adder-cost: 68   maxlim: 192382   bits: 19/18
c ---[1580]---> Adder-cost: 72   maxlim: 324222   bits: 20/19
c ---[1578]---> Adder-cost: 76   maxlim: 584574   bits: 21/20
c ---[1576]---> Adder-cost: 80   maxlim: 1109630   bits: 22/21
c ---[1574]---> Adder-cost: 80   maxlim: 1108990   bits: 22/21
c ---[1572]---> Adder-cost: 80   maxlim: 1074558   bits: 22/21
c ---[1570]---> Adder-cost: 80   maxlim: 1077502   bits: 22/21
c ---[1568]---> Adder-cost: 80   maxlim: 1076094   bits: 22/21
c ---[1566]---> Adder-cost: 80   maxlim: 1062142   bits: 22/21
c ---[1564]---> Adder-cost: 80   maxlim: 1061502   bits: 22/21
c ---[1562]---> Adder-cost: 80   maxlim: 1061758   bits: 22/21
c ---[1560]---> Adder-cost: 80   maxlim: 1054974   bits: 22/21
c ---[1558]---> Adder-cost: 80   maxlim: 1054078   bits: 22/21
c ---[1556]---> Adder-cost: 80   maxlim: 1048702   bits: 22/21
c ---[1554]---> Adder-cost: 68   maxlim: 257278   bits: 19/18
c ---[1552]---> Adder-cost: 72   maxlim: 384638   bits: 20/19
c ---[1550]---> Adder-cost: 76   maxlim: 647678   bits: 21/20
c ---[1548]---> Adder-cost: 80   maxlim: 1170686   bits: 22/21
c ---[1546]---> Adder-cost: 80   maxlim: 1168510   bits: 22/21
c ---[1544]---> Adder-cost: 80   maxlim: 1165694   bits: 22/21
c ---[1542]---> Adder-cost: 80   maxlim: 1165566   bits: 22/21
c ---[1540]---> Adder-cost: 80   maxlim: 1103870   bits: 22/21
c ---[1538]---> Adder-cost: 80   maxlim: 1103998   bits: 22/21
c ---[1536]---> Adder-cost: 80   maxlim: 1106814   bits: 22/21
c ---[1534]---> Adder-cost: 80   maxlim: 1075198   bits: 22/21
c ---[1532]---> Adder-cost: 80   maxlim: 1076990   bits: 22/21
c ---[1530]---> Adder-cost: 80   maxlim: 1058686   bits: 22/21
c ---[1528]---> Adder-cost: 80   maxlim: 1060478   bits: 22/21
c ---[1526]---> Adder-cost: 80   maxlim: 1052286   bits: 22/21
c ---[1524]---> Adder-cost: 64   maxlim: 128894   bits: 18/17
c ---[1522]---> Adder-cost: 68   maxlim: 194686   bits: 19/18
c ---[1520]---> Adder-cost: 72   maxlim: 325886   bits: 20/19
c ---[1518]---> Adder-cost: 76   maxlim: 588030   bits: 21/20
c ---[1516]---> Adder-cost: 80   maxlim: 1078142   bits: 22/21
c ---[1514]---> Adder-cost: 80   maxlim: 1077246   bits: 22/21
c ---[1512]---> Adder-cost: 80   maxlim: 1077758   bits: 22/21
c ---[1510]---> Adder-cost: 80   maxlim: 1077630   bits: 22/21
c ---[1508]---> Adder-cost: 80   maxlim: 1077246   bits: 22/21
c ---[1506]---> Adder-cost: 80   maxlim: 1062142   bits: 22/21
c ---[1504]---> Adder-cost: 80   maxlim: 1061758   bits: 22/21
c ---[1502]---> Adder-cost: 80   maxlim: 1054206   bits: 22/21
c ---[1500]---> Adder-cost: 80   maxlim: 1055230   bits: 22/21
c ---[1498]---> Adder-cost: 80   maxlim: 1051518   bits: 22/21
c ---[1496]---> Adder-cost: 80   maxlim: 1049214   bits: 22/21
c ---[1494]---> Adder-cost: 64   maxlim: 128510   bits: 18/17
c ---[1492]---> Adder-cost: 68   maxlim: 193406   bits: 19/18
c ---[1490]---> Adder-cost: 72   maxlim: 323582   bits: 20/19
c ---[1488]---> Adder-cost: 76   maxlim: 585598   bits: 21/20
c ---[1486]---> Adder-cost: 80   maxlim: 1110398   bits: 22/21
c ---[1484]---> Adder-cost: 80   maxlim: 1107454   bits: 22/21
c ---[1482]---> Adder-cost: 80   maxlim: 1107710   bits: 22/21
c ---[1480]---> Adder-cost: 80   maxlim: 1075070   bits: 22/21
c ---[1478]---> Adder-cost: 80   maxlim: 1075710   bits: 22/21
c ---[1476]---> Adder-cost: 80   maxlim: 1075326   bits: 22/21
c ---[1474]---> Adder-cost: 80   maxlim: 1061758   bits: 22/21
c ---[1472]---> Adder-cost: 80   maxlim: 1061374   bits: 22/21
c ---[1470]---> Adder-cost: 80   maxlim: 1054846   bits: 22/21
c ---[1468]---> Adder-cost: 80   maxlim: 1050494   bits: 22/21
c ---[1466]---> Adder-cost: 80   maxlim: 1049598   bits: 22/21
c ---[1465]---> Adder-cost: 37   maxlim: 103422   bits: 18/17
c ---[1464]---> Adder-cost: 52   maxlim: 131070   bits: 18/17
c ---[1463]---> Adder-cost: 52   maxlim: 131070   bits: 18/17
c ---[1462]---> Adder-cost: 52   maxlim: 131070   bits: 18/17
c ---[1461]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1460]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1459]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1458]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1457]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1456]---> Adder-cost: 36   maxlim: 37886   bits: 17/16
c ---[1455]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1454]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1453]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1452]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[1451]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[1450]---> Adder-cost: 36   maxlim: 37886   bits: 17/16
c ---[1449]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1448]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1447]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1446]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1445]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1444]---> Adder-cost: 49   maxlim: 65534   bits: 17/16
c ---[1443]---> Adder-cost: 46   maxlim: 32766   bits: 16/15
c ---[1442]---> Adder-cost: 37   maxlim: 100606   bits: 18/17
c ---[1441]---> Adder-cost: 56   maxlim: 131070   bits: 18/17
c ---[1440]---> Adder-cost: 56   maxlim: 131070   bits: 18/17
c ---[1439]---> Adder-cost: 56   maxlim: 131070   bits: 18/17
c ---[1438]---> Adder-cost: 56   maxlim: 131070   bits: 18/17
c ---[1437]---> Adder-cost: 56   maxlim: 131070   bits: 18/17
c ---[1436]---> Adder-cost: 56   maxlim: 131070   bits: 18/17
c ---[1435]---> Adder-cost: 56   maxlim: 131070   bits: 18/17
c ---[1434]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1433]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1432]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1431]---> Adder-cost: 36   maxlim: 35070   bits: 17/16
c ---[1430]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1429]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1428]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1427]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1426]---> Adder-cost: 50   maxlim: 32766   bits: 16/15
c ---[1425]---> Adder-cost: 36   maxlim: 35070   bits: 17/16
c ---[1424]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1423]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1422]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1421]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1420]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1419]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1418]---> Adder-cost: 53   maxlim: 65534   bits: 17/16
c ---[1417]---> Adder-cost: 39   maxlim: 402686   bits: 20/19
c ---[1416]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1415]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1414]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1413]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1412]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1411]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1410]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1409]---> Adder-cost: 56   maxlim: 131070   bits: 18/17
c ---[1408]---> Adder-cost: 39   maxlim: 402686   bits: 20/19
c ---[1407]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1406]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1405]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1404]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1403]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1402]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1401]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1400]---> Adder-cost: 56   maxlim: 131070   bits: 18/17
c ---[1399]---> Adder-cost: 39   maxlim: 402686   bits: 20/19
c ---[1398]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1397]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1396]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1395]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1394]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1393]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1392]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1391]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1390]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1389]---> Adder-cost: 39   maxlim: 402686   bits: 20/19
c ---[1388]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1387]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1386]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1385]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1384]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1383]---> Adder-cost: 62   maxlim: 524286   bits: 20/19
c ---[1382]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1381]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1380]---> Adder-cost: 59   maxlim: 262142   bits: 19/18
c ---[1379]---> Adder-cost: 39   maxlim: 250750   bits: 19/18
c ---[1378]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1377]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1376]---> Adder-cost: 39   maxlim: 250750   bits: 19/18
c ---[1375]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1374]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1373]---> Adder-cost: 39   maxlim: 250750   bits: 19/18
c ---[1372]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1371]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1370]---> Adder-cost: 39   maxlim: 250750   bits: 19/18
c ---[1369]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1368]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1367]---> Adder-cost: 39   maxlim: 250750   bits: 19/18
c ---[1366]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1365]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1364]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1363]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1362]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1361]---> Adder-cost: 39   maxlim: 250750   bits: 19/18
c ---[1360]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1359]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1358]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1357]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1356]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1355]---> Adder-cost: 39   maxlim: 250750   bits: 19/18
c ---[1354]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1353]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1352]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1351]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1350]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1349]---> Adder-cost: 39   maxlim: 250750   bits: 19/18
c ---[1348]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1347]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1346]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1345]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1344]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1343]---> Adder-cost: 39   maxlim: 250750   bits: 19/18
c ---[1342]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1341]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1340]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1339]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1338]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1337]---> Adder-cost: 40   maxlim: 709758   bits: 21/20
c ---[1336]---> Adder-cost: 67   maxlim: 1048574   bits: 21/20
c ---[1335]---> Adder-cost: 67   maxlim: 1048574   bits: 21/20
c ---[1334]---> Adder-cost: 67   maxlim: 1048574   bits: 21/20
c ---[1333]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1332]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1331]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1330]---> Adder-cost: 40   maxlim: 709758   bits: 21/20
c ---[1329]---> Adder-cost: 67   maxlim: 1048574   bits: 21/20
c ---[1328]---> Adder-cost: 67   maxlim: 1048574   bits: 21/20
c ---[1327]---> Adder-cost: 67   maxlim: 1048574   bits: 21/20
c ---[1326]---> Adder-cost: 67   maxlim: 1048574   bits: 21/20
c ---[1325]---> Adder-cost: 67   maxlim: 1048574   bits: 21/20
c ---[1324]---> Adder-cost: 67   maxlim: 1048574   bits: 21/20
c ---[1323]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1322]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1321]---> Adder-cost: 39   maxlim: 185470   bits: 19/18
c ---[1320]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1319]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1318]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1317]---> Adder-cost: 39   maxlim: 185470   bits: 19/18
c ---[1316]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1315]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1314]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1313]---> Adder-cost: 39   maxlim: 185470   bits: 19/18
c ---[1312]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1311]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1310]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1309]---> Adder-cost: 39   maxlim: 185470   bits: 19/18
c ---[1308]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1307]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1306]---> Adder-cost: 64   maxlim: 524286   bits: 20/19
c ---[1305]---> Adder-cost: 40   maxlim: 648702   bits: 21/20
c ---[1304]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1303]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1302]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1301]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1300]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1299]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1298]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[1297]---> Adder-cost: 40   maxlim: 648702   bits: 21/20
c ---[1296]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1295]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1294]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1293]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[1292]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[1291]---> Adder-cost: 40   maxlim: 648702   bits: 21/20
c ---[1290]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1289]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1288]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1287]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1286]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1285]---> Adder-cost: 63   maxlim: 1048574   bits: 21/20
c ---[1284]---> Adder-cost: 60   maxlim: 524286   bits: 20/19
c ---[1283]---> Adder-cost: 39   maxlim: 124414   bits: 18/17
c ---[1282]---> Adder-cost: 39   maxlim: 124414   bits: 18/17
c ---[1281]---> Adder-cost: 39   maxlim: 124414   bits: 18/17
c ---[1280]---> Adder-cost: 39   maxlim: 124414   bits: 18/17
c ---[1279]---> Adder-cost: 39   maxlim: 124414   bits: 18/17
c ---[1278]---> Adder-cost: 32   maxlim: 49406   bits: 17/16
c ---[1277]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1276]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1275]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[1274]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1273]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1272]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1271]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1270]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1269]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1268]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[1267]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[1266]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1265]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[1264]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[1263]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[1262]---> Adder-cost: 30   maxlim: 25854   bits: 16/15
c ---[1261]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1260]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1259]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1258]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1257]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1256]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[1255]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1254]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1253]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[1252]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[1251]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1250]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[1249]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[1248]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[1247]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[1245]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[1244]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[1243]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1242]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[1241]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1240]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[1239]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[1238]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1237]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1236]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[1235]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[1234]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1233]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[1232]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[1231]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[1229]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[1228]---> Adder-cost: 14   maxlim: 131070   bits: 18/17
c ---[1227]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1226]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1225]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1224]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1223]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1222]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1221]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1220]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1219]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1218]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1217]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1216]---> Adder-cost: 12   maxlim: 16382   bits: 15/14
c ---[1215]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[1214]---> Adder-cost: 30   maxlim: 25470   bits: 16/15
c ---[1213]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1212]---> Adder-cost: 8   maxlim: 65534   bits: 17/16
c ---[1211]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1210]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1209]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1208]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[1207]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[1206]---> Adder-cost: 6   maxlim: 32766   bits: 16/15
c ---[1205]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1204]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1203]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1202]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[1201]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[1200]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[1199]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[1197]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1196]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1195]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1194]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1193]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[1192]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1191]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1190]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1189]---> Adder-cost: 10   maxlim: 32766   bits: 16/15
c ---[1188]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[1187]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1186]---> Adder-cost: 10   maxlim: 16382   bits: 15/14
c ---[1185]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[1184]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[1183]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[1182]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[1181]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1180]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1179]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1178]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1177]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[1176]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1175]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1174]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1173]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1172]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1171]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1170]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1169]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1168]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1167]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1166]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[1165]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1164]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1163]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1162]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1161]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[1160]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1159]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1158]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1157]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1156]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1155]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1154]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1153]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1152]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1151]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1150]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[1149]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[1148]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1147]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1146]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1145]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1144]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[1143]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[1142]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1141]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[1140]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1139]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[1138]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1137]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1136]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[1135]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[1134]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[1133]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[1132]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1131]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1130]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1129]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1128]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[1127]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[1126]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1125]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[1124]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1123]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[1122]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1121]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1120]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[1119]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[1118]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[1117]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1116]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1115]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1114]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1113]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[1112]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1111]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1110]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1109]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1108]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1107]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1106]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1105]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1104]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1103]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1102]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[1101]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1100]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1099]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1098]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1097]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[1096]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1095]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1094]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1093]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1092]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1091]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1090]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1089]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1088]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1087]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1086]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[1085]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1084]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1083]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1082]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1081]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[1080]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1079]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1078]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1077]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1076]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1075]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1074]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1073]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1072]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1071]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1070]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[1069]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1068]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1067]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1066]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1065]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[1064]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1063]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1062]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1061]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1060]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[1059]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1058]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1057]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1056]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[1055]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[1054]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[1053]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[1052]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1051]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1050]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1049]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1048]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[1047]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[1046]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1045]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[1044]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1043]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[1042]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1041]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1040]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[1039]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[1038]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[1037]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[1036]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1035]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1034]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1033]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1032]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[1031]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[1030]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1029]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[1028]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1027]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[1026]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1025]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1024]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[1023]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[1022]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[1021]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[1020]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1019]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1018]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1017]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1016]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[1015]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[1014]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[1013]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[1012]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[1011]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[1010]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[1009]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[1008]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[1007]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[1006]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[1005]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[1004]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1003]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1002]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1001]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[1000]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 999]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[ 998]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 997]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 996]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 995]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 994]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 993]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 992]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 991]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 990]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[ 989]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[ 988]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 987]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 986]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 985]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 984]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 983]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[ 982]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 981]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 980]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 979]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 978]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 977]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 976]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 975]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 974]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[ 973]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 972]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 971]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 970]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 969]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 968]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 967]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 966]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 965]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 964]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 963]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 962]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 961]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 960]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 959]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 958]---> Adder-cost: 38   maxlim: 436478   bits: 20/19
c ---[ 957]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 956]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 955]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 954]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 953]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[ 952]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 951]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 950]---> Adder-cost: 16   maxlim: 262142   bits: 19/18
c ---[ 949]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 948]---> Adder-cost: 16   maxlim: 262142   bits: 19/18
c ---[ 947]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 946]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 945]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 944]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 943]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[ 942]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[ 941]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 940]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 939]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 938]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 937]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 936]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 935]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 934]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 933]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 932]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 931]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 930]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 929]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 928]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 927]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 926]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[ 925]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 924]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 923]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 922]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 921]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 920]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 919]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 918]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 917]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 916]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 915]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 914]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 913]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 912]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 911]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 910]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[ 909]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 908]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 907]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 906]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 905]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 904]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 903]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 902]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 901]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 900]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 899]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 898]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 897]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 896]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 895]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 894]---> Adder-cost: 61   maxlim: 231934   bits: 19/18
c ---[ 893]---> Adder-cost: 18   maxlim: 1048574   bits: 21/20
c ---[ 892]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 891]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 890]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 889]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 888]---> Adder-cost: 22   maxlim: 1048574   bits: 21/20
c ---[ 887]---> Adder-cost: 10   maxlim: 524286   bits: 20/19
c ---[ 886]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 885]---> Adder-cost: 20   maxlim: 524286   bits: 20/19
c ---[ 884]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 883]---> Adder-cost: 12   maxlim: 262142   bits: 19/18
c ---[ 882]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 881]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 880]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 879]---> Adder-cost: 4   maxlim: 32766   bits: 16/15
c ---[ 878]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[ 877]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[ 876]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 875]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 874]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 873]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 872]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 871]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[ 870]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 869]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 868]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 867]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 866]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 865]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 864]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 863]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 862]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[ 861]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[ 860]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 859]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 858]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 857]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 856]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 855]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[ 854]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 853]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 852]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 851]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 850]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 849]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 848]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 847]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 846]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[ 845]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[ 844]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 843]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 842]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 841]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 840]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 839]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[ 838]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 837]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 836]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 835]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 834]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 833]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 832]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 831]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 830]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[ 829]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[ 828]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 827]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 826]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 825]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 824]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 823]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[ 822]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 821]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 820]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 819]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 818]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 817]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 816]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 815]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 814]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[ 813]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 812]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 811]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 810]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 809]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 808]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 807]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 806]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 805]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 804]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 803]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 802]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 801]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 800]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 799]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 797]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 796]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 795]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 794]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 793]---> Adder-cost: 22   maxlim: 1048574   bits: 21/20
c ---[ 792]---> Adder-cost: 26   maxlim: 1048574   bits: 21/20
c ---[ 791]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 790]---> Adder-cost: 20   maxlim: 524286   bits: 20/19
c ---[ 789]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 788]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 787]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 786]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 785]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 784]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 783]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 782]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[ 781]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 780]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 779]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 778]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 777]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 776]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 775]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 774]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 773]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 772]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 771]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 770]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 769]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 768]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 767]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 766]---> Adder-cost: 38   maxlim: 436478   bits: 20/19
c ---[ 765]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 764]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 763]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 762]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 761]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[ 760]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 759]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 758]---> Adder-cost: 16   maxlim: 262142   bits: 19/18
c ---[ 757]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 756]---> Adder-cost: 16   maxlim: 262142   bits: 19/18
c ---[ 755]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 754]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 753]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 752]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 751]---> Adder-cost: 14   maxlim: 32766   bits: 16/15
c ---[ 750]---> Adder-cost: 36   maxlim: 218238   bits: 19/18
c ---[ 749]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 748]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 747]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 746]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 745]---> Adder-cost: 18   maxlim: 262142   bits: 19/18
c ---[ 744]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 743]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 742]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 741]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 740]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 739]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 738]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 737]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 736]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 735]---> Adder-cost: 14   maxlim: 16382   bits: 15/14
c ---[ 734]---> Adder-cost: 61   maxlim: 231934   bits: 19/18
c ---[ 733]---> Adder-cost: 18   maxlim: 1048574   bits: 21/20
c ---[ 732]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 731]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 730]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 729]---> Adder-cost: 24   maxlim: 1048574   bits: 21/20
c ---[ 728]---> Adder-cost: 22   maxlim: 1048574   bits: 21/20
c ---[ 727]---> Adder-cost: 10   maxlim: 524286   bits: 20/19
c ---[ 726]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 725]---> Adder-cost: 20   maxlim: 524286   bits: 20/19
c ---[ 724]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 723]---> Adder-cost: 12   maxlim: 262142   bits: 19/18
c ---[ 722]---> Adder-cost: 16   maxlim: 131070   bits: 18/17
c ---[ 721]---> Adder-cost: 18   maxlim: 131070   bits: 18/17
c ---[ 720]---> Adder-cost: 12   maxlim: 65534   bits: 17/16
c ---[ 719]---> Adder-cost: 4   maxlim: 32766   bits: 16/15
c ---[ 718]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[ 717]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[ 716]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 715]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 714]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 713]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 712]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 711]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[ 710]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 709]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 708]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 707]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 706]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 705]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 704]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 703]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 702]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[ 701]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[ 700]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 699]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 698]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 697]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 696]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 695]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[ 694]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 693]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 692]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 691]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 690]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 689]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 688]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 687]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 686]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[ 685]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[ 684]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 683]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 682]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 681]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 680]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 679]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[ 678]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 677]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 676]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 675]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 674]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 673]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 672]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 671]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 670]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[ 669]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[ 668]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 667]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 666]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 665]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 664]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 663]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[ 662]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 661]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 660]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 659]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 658]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 657]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 656]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 655]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 654]---> Adder-cost: 57   maxlim: 115966   bits: 18/17
c ---[ 653]---> Adder-cost: 18   maxlim: 524286   bits: 20/19
c ---[ 652]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 651]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 650]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 649]---> Adder-cost: 24   maxlim: 524286   bits: 20/19
c ---[ 648]---> Adder-cost: 22   maxlim: 524286   bits: 20/19
c ---[ 647]---> Adder-cost: 10   maxlim: 262142   bits: 19/18
c ---[ 646]---> Adder-cost: 22   maxlim: 262142   bits: 19/18
c ---[ 645]---> Adder-cost: 20   maxlim: 262142   bits: 19/18
c ---[ 644]---> Adder-cost: 20   maxlim: 131070   bits: 18/17
c ---[ 643]---> Adder-cost: 12   maxlim: 131070   bits: 18/17
c ---[ 642]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 641]---> Adder-cost: 18   maxlim: 65534   bits: 17/16
c ---[ 640]---> Adder-cost: 12   maxlim: 32766   bits: 16/15
c ---[ 639]---> Adder-cost: 4   maxlim: 16382   bits: 15/14
c ---[ 638]---> Adder-cost: 158   maxlim: 247292   bits: 19/18
c ---[ 637]---> Adder-cost: 174   maxlim: 247292   bits: 19/18
c ---[ 636]---> Adder-cost: 174   maxlim: 247292   bits: 19/18
c ---[ 635]---> Adder-cost: 174   maxlim: 247292   bits: 19/18
c ---[ 634]---> Adder-cost: 165   maxlim: 148988   bits: 19/18
c ---[ 633]---> Adder-cost: 165   maxlim: 148988   bits: 19/18
c ---[ 632]---> Adder-cost: 165   maxlim: 148988   bits: 19/18
c ---[ 623]---> Adder-cost: 160   maxlim: 244476   bits: 19/18
c ---[ 622]---> Adder-cost: 182   maxlim: 244476   bits: 19/18
c ---[ 621]---> Adder-cost: 182   maxlim: 244476   bits: 19/18
c ---[ 620]---> Adder-cost: 182   maxlim: 244476   bits: 19/18
c ---[ 619]---> Adder-cost: 182   maxlim: 244476   bits: 19/18
c ---[ 618]---> Adder-cost: 180   maxlim: 211708   bits: 19/18
c ---[ 617]---> Adder-cost: 180   maxlim: 211708   bits: 19/18
c ---[ 616]---> Adder-cost: 180   maxlim: 211708   bits: 19/18
c ---[ 608]---> Adder-cost: 152   maxlim: 1994747   bits: 22/21
c ---[ 607]---> Adder-cost: 186   maxlim: 1994747   bits: 22/21
c ---[ 606]---> Adder-cost: 186   maxlim: 1994747   bits: 22/21
c ---[ 605]---> Adder-cost: 186   maxlim: 1994747   bits: 22/21
c ---[ 604]---> Adder-cost: 182   maxlim: 1470459   bits: 22/21
c ---[ 603]---> Adder-cost: 182   maxlim: 1470459   bits: 22/21
c ---[ 602]---> Adder-cost: 182   maxlim: 1470459   bits: 22/21
c ---[ 601]---> Adder-cost: 179   maxlim: 946171   bits: 21/20
c ---[ 600]---> Adder-cost: 172   maxlim: 684027   bits: 21/20
c ---[ 599]---> Adder-cost: 172   maxlim: 684027   bits: 21/20
c ---[ 598]---> Adder-cost: 191   maxlim: 421883   bits: 20/19
c ---[ 597]---> Adder-cost: 187   maxlim: 290811   bits: 20/19
c ---[ 596]---> Adder-cost: 212   maxlim: 159739   bits: 19/18
c ---[ 595]---> Adder-cost: 212   maxlim: 159739   bits: 19/18
c ---[ 593]---> Adder-cost: 344   maxlim: 4486006   bits: 23/23
c ---[ 592]---> Adder-cost: 386   maxlim: 4486006   bits: 23/23
c ---[ 591]---> Adder-cost: 386   maxlim: 4486006   bits: 23/23
c ---[ 590]---> Adder-cost: 386   maxlim: 4486006   bits: 23/23
c ---[ 589]---> Adder-cost: 380   maxlim: 3437430   bits: 23/22
c ---[ 588]---> Adder-cost: 380   maxlim: 3437430   bits: 23/22
c ---[ 587]---> Adder-cost: 380   maxlim: 3437430   bits: 23/22
c ---[ 586]---> Adder-cost: 368   maxlim: 2126710   bits: 22/22
c ---[ 585]---> Adder-cost: 360   maxlim: 1602422   bits: 22/21
c ---[ 584]---> Adder-cost: 360   maxlim: 1602422   bits: 22/21
c ---[ 583]---> Adder-cost: 351   maxlim: 947062   bits: 21/20
c ---[ 582]---> Adder-cost: 340   maxlim: 684918   bits: 21/20
c ---[ 581]---> Adder-cost: 357   maxlim: 357238   bits: 20/19
c ---[ 580]---> Adder-cost: 357   maxlim: 357238   bits: 20/19
c ---[ 578]---> Adder-cost: 384   maxlim: 5988469   bits: 23/23
c ---[ 577]---> Adder-cost: 462   maxlim: 5988469   bits: 23/23
c ---[ 576]---> Adder-cost: 462   maxlim: 5988469   bits: 23/23
c ---[ 575]---> Adder-cost: 462   maxlim: 5988469   bits: 23/23
c ---[ 574]---> Adder-cost: 452   maxlim: 4415605   bits: 23/23
c ---[ 573]---> Adder-cost: 452   maxlim: 4415605   bits: 23/23
c ---[ 572]---> Adder-cost: 452   maxlim: 4415605   bits: 23/23
c ---[ 571]---> Adder-cost: 446   maxlim: 2842741   bits: 23/22
c ---[ 570]---> Adder-cost: 432   maxlim: 2056309   bits: 22/21
c ---[ 569]---> Adder-cost: 432   maxlim: 2056309   bits: 22/21
c ---[ 568]---> Adder-cost: 424   maxlim: 1269877   bits: 22/21
c ---[ 567]---> Adder-cost: 413   maxlim: 876661   bits: 21/20
c ---[ 566]---> Adder-cost: 414   maxlim: 483445   bits: 20/19
c ---[ 565]---> Adder-cost: 414   maxlim: 483445   bits: 20/19
c ---[ 563]---> Adder-cost: 424   maxlim: 6967028   bits: 23/23
c ---[ 562]---> Adder-cost: 484   maxlim: 6967028   bits: 24/23
c ---[ 561]---> Adder-cost: 484   maxlim: 6967028   bits: 24/23
c ---[ 560]---> Adder-cost: 484   maxlim: 6967028   bits: 24/23
c ---[ 559]---> Adder-cost: 470   maxlim: 5656308   bits: 23/23
c ---[ 558]---> Adder-cost: 470   maxlim: 5656308   bits: 23/23
c ---[ 557]---> Adder-cost: 470   maxlim: 5656308   bits: 23/23
c ---[ 556]---> Adder-cost: 460   maxlim: 3297012   bits: 23/22
c ---[ 555]---> Adder-cost: 446   maxlim: 2641652   bits: 22/22
c ---[ 554]---> Adder-cost: 446   maxlim: 2641652   bits: 22/22
c ---[ 553]---> Adder-cost: 436   maxlim: 1462004   bits: 22/21
c ---[ 552]---> Adder-cost: 426   maxlim: 1134324   bits: 22/21
c ---[ 551]---> Adder-cost: 419   maxlim: 675572   bits: 21/20
c ---[ 550]---> Adder-cost: 412   maxlim: 544500   bits: 21/20
c ---[ 548]---> Adder-cost: 6   maxlim: 1791   bits: 12/11
c ---[ 547]---> Adder-cost: 12   maxlim: 6271   bits: 14/13
c ---[ 546]---> Adder-cost: 192   maxlim: 22783   bits: 16/15
c ---[ 545]---> Adder-cost: 131   maxlim: 22783   bits: 16/15
c ---[ 544]---> Adder-cost: 148   maxlim: 28543   bits: 16/15
c ---[ 543]---> Adder-cost: 148   maxlim: 28543   bits: 16/15
c ---[ 542]---> Adder-cost: 162   maxlim: 22783   bits: 16/15
c ---[ 541]---> Adder-cost: 162   maxlim: 22783   bits: 16/15
c ---[ 540]---> Adder-cost: 162   maxlim: 22783   bits: 16/15
c ---[ 539]---> Adder-cost: 162   maxlim: 22783   bits: 16/15
c ---[ 538]---> Adder-cost: 283   maxlim: 56063   bits: 17/16
c ---[ 537]---> Adder-cost: 220   maxlim: 45567   bits: 17/16
c ---[ 536]---> Adder-cost: 187   maxlim: 22783   bits: 16/15
c ---[ 535]---> Adder-cost: 222   maxlim: 56063   bits: 17/16
c ---[ 534]---> Adder-cost: 218   maxlim: 22783   bits: 16/15
c ---[ 533]---> Adder-cost: 177   maxlim: 22783   bits: 16/15
c ---[ 532]---> Adder-cost: 187   maxlim: 22783   bits: 16/15
c ---[ 531]---> Adder-cost: 12   maxlim: 9471   bits: 15/14
c ---[ 530]---> Adder-cost: 12   maxlim: 4223   bits: 14/13
c ---[ 529]---> Adder-cost: 8   maxlim: 6655   bits: 14/13
c ---[ 528]---> Adder-cost: 10   maxlim: 2431   bits: 13/12
c ---[ 527]---> Adder-cost: 10   maxlim: 4863   bits: 14/13
c ---[ 526]---> Adder-cost: 10   maxlim: 2175   bits: 13/12
c ---[ 525]---> Adder-cost: 12   maxlim: 5247   bits: 14/13
c ---[ 524]---> Adder-cost: 10   maxlim: 3455   bits: 13/12
c ---[ 523]---> Adder-cost: 10   maxlim: 3199   bits: 13/12
c ---[ 522]---> Adder-cost: 12   maxlim: 8959   bits: 15/14
c ---[ 521]---> Adder-cost: 14   maxlim: 11135   bits: 15/14
c ---[ 520]---> Adder-cost: 14   maxlim: 13951   bits: 15/14
c ---[ 519]---> Adder-cost: 12   maxlim: 14079   bits: 15/14
c ---[ 518]---> Adder-cost: 6   maxlim: 10239   bits: 15/14
c ---[ 517]---> Adder-cost: 12   maxlim: 7295   bits: 14/13
c ---[ 516]---> Adder-cost: 10   maxlim: 4351   bits: 14/13
c ---[ 515]---> Adder-cost: 10   maxlim: 3199   bits: 13/12
c ---[ 514]---> Adder-cost: 6   maxlim: 2559   bits: 13/12
c ---[ 513]---> Adder-cost: 12   maxlim: 6015   bits: 14/13
c ---[ 512]---> Adder-cost: 10   maxlim: 3199   bits: 13/12
c ---[ 511]---> Adder-cost: 6   maxlim: 3583   bits: 13/12
c ---[ 510]---> Adder-cost: 146   maxlim: 39423   bits: 17/16
c ---[ 509]---> Adder-cost: 155   maxlim: 43391   bits: 17/16
c ---[ 508]---> Adder-cost: 157   maxlim: 59775   bits: 17/16
c ---[ 507]---> Adder-cost: 102   maxlim: 19199   bits: 16/15
c ---[ 506]---> Adder-cost: 82   maxlim: 16383   bits: 15/14
c ---[ 505]---> Adder-cost: 143   maxlim: 32511   bits: 16/15
c ---[ 504]---> Adder-cost: 151   maxlim: 51455   bits: 17/16
c ---[ 503]---> Adder-cost: 159   maxlim: 64383   bits: 17/16
c ---[ 502]---> Adder-cost: 82   maxlim: 16383   bits: 15/14
c ---[ 501]---> Adder-cost: 187   maxlim: 42367   bits: 17/16
c ---[ 500]---> Adder-cost: 181   maxlim: 50431   bits: 17/16
c ---[ 499]---> Adder-cost: 194   maxlim: 31103   bits: 16/15
c ---[ 498]---> Adder-cost: 208   maxlim: 42367   bits: 17/16
c ---[ 497]---> Adder-cost: 133   maxlim: 28031   bits: 16/15
c ---[ 496]---> Adder-cost: 178   maxlim: 83455   bits: 18/17
c ---[ 495]---> Adder-cost: 158   maxlim: 59775   bits: 17/16
c ---[ 494]---> Adder-cost: 160   maxlim: 64383   bits: 17/16
c ---[ 493]---> Adder-cost: 133   maxlim: 19199   bits: 16/15
c ---[ 492]---> Adder-cost: 158   maxlim: 59775   bits: 17/16
c ---[ 491]---> Adder-cost: 133   maxlim: 19199   bits: 16/15
c ---[ 490]---> Adder-cost: 160   maxlim: 64383   bits: 17/16
c ---[ 489]---> Adder-cost: 111   maxlim: 16383   bits: 15/14
c ---[ 488]---> Adder-cost: 164   maxlim: 31103   bits: 16/15
c ---[ 487]---> Adder-cost: 164   maxlim: 31103   bits: 16/15
c ---[ 486]---> Adder-cost: 197   maxlim: 78079   bits: 18/17
c ---[ 485]---> Adder-cost: 164   maxlim: 31103   bits: 16/15
c ---[ 484]---> Adder-cost: 229   maxlim: 85119   bits: 18/17
c ---[ 483]---> Adder-cost: 192   maxlim: 78079   bits: 18/17
c ---[ 482]---> Adder-cost: 164   maxlim: 28031   bits: 16/15
c ---[ 481]---> Adder-cost: 192   maxlim: 85119   bits: 18/17
c ---[ 480]---> Adder-cost: 164   maxlim: 31103   bits: 16/15
c ---[ 479]---> Adder-cost: 164   maxlim: 28031   bits: 16/15
c ---[ 478]---> Adder-cost: 183   maxlim: 58111   bits: 17/16
c ---[ 477]---> Adder-cost: 131   maxlim: 19199   bits: 16/15
c ---[ 476]---> Adder-cost: 138   maxlim: 16383   bits: 15/14
c ---[ 475]---> Adder-cost: 169   maxlim: 32767   bits: 16/15
c ---[ 474]---> Adder-cost: 156   maxlim: 59775   bits: 17/16
c ---[ 473]---> Adder-cost: 191   maxlim: 64383   bits: 17/16
c ---[ 472]---> Adder-cost: 131   maxlim: 19199   bits: 16/15
c ---[ 471]---> Adder-cost: 110   maxlim: 16383   bits: 15/14
c ---[ 470]---> Adder-cost: 158   maxlim: 64383   bits: 17/16
c ---[ 469]---> Adder-cost: 110   maxlim: 16383   bits: 15/14
c ---[ 468]---> Adder-cost: 110   maxlim: 16383   bits: 15/14
c ---[ 467]---> Adder-cost: 303   maxlim: 71423   bits: 18/17
c ---[ 466]---> Adder-cost: 189   maxlim: 31103   bits: 16/15
c ---[ 465]---> Adder-cost: 263   maxlim: 107135   bits: 18/17
c ---[ 464]---> Adder-cost: 221   maxlim: 85119   bits: 18/17
c ---[ 463]---> Adder-cost: 221   maxlim: 85119   bits: 18/17
c ---[ 462]---> Adder-cost: 189   maxlim: 31103   bits: 16/15
c ---[ 461]---> Adder-cost: 221   maxlim: 78079   bits: 18/17
c ---[ 460]---> Adder-cost: 189   maxlim: 31103   bits: 16/15
c ---[ 459]---> Adder-cost: 162   maxlim: 19199   bits: 16/15
c ---[ 458]---> Adder-cost: 139   maxlim: 16383   bits: 15/14
c ---[ 457]---> Adder-cost: 438   maxlim: 64127   bits: 17/16
c ---[ 456]---> Adder-cost: 406   maxlim: 49151   bits: 17/16
c ---[ 455]---> Adder-cost: 244   maxlim: 83455   bits: 18/17
c ---[ 454]---> Adder-cost: 139   maxlim: 16383   bits: 15/14
c ---[ 453]---> Adder-cost: 314   maxlim: 142335   bits: 19/18
c ---[ 452]---> Adder-cost: 294   maxlim: 128767   bits: 18/17
c ---[ 451]---> Adder-cost: 229   maxlim: 32767   bits: 16/15
c ---[ 450]---> Adder-cost: 139   maxlim: 16383   bits: 15/14
c ---[ 449]---> Adder-cost: 238   maxlim: 71423   bits: 18/17
c ---[ 448]---> Adder-cost: 274   maxlim: 80127   bits: 18/17
c ---[ 447]---> Adder-cost: 230   maxlim: 107135   bits: 18/17
c ---[ 446]---> Adder-cost: 220   maxlim: 28031   bits: 16/15
c ---[ 445]---> Adder-cost: 265   maxlim: 107135   bits: 18/17
c ---[ 444]---> Adder-cost: 221   maxlim: 85119   bits: 18/17
c ---[ 443]---> Adder-cost: 189   maxlim: 31103   bits: 16/15
c ---[ 442]---> Adder-cost: 220   maxlim: 28031   bits: 16/15
c ---[ 441]---> Adder-cost: 210   maxlim: 107135   bits: 18/17
c ---[ 440]---> Adder-cost: 199   maxlim: 85119   bits: 18/17
c ---[ 439]---> Adder-cost: 175   maxlim: 31103   bits: 16/15
c ---[ 438]---> Adder-cost: 175   maxlim: 28031   bits: 16/15
c ---[ 437]---> Adder-cost: 265   maxlim: 107135   bits: 18/17
c ---[ 436]---> Adder-cost: 256   maxlim: 85119   bits: 18/17
c ---[ 435]---> Adder-cost: 189   maxlim: 31103   bits: 16/15
c ---[ 434]---> Adder-cost: 220   maxlim: 28031   bits: 16/15
c ---[ 433]---> Adder-cost: 8   maxlim: 3839   bits: 13/12
c ---[ 432]---> Adder-cost: 12   maxlim: 5247   bits: 14/13
c ---[ 431]---> Adder-cost: 4   maxlim: 6143   bits: 14/13
c ---[ 430]---> Adder-cost: 12   maxlim: 4735   bits: 14/13
c ---[ 429]---> Adder-cost: 21   maxlim: 5503   bits: 14/13
c ---[ 428]---> Adder-cost: 8   maxlim: 3327   bits: 13/12
c ---[ 427]---> Adder-cost: 10   maxlim: 3967   bits: 13/12
c ---[ 426]---> Adder-cost: 10   maxlim: 3455   bits: 13/12
c ---[ 425]---> Adder-cost: 6   maxlim: 1791   bits: 12/11
c ---[ 424]---> Adder-cost: 10   maxlim: 2431   bits: 13/12
c ---[ 423]---> Adder-cost: 6   maxlim: 2559   bits: 13/12
c ---[ 422]---> Adder-cost: 12   maxlim: 5247   bits: 14/13
c ---[ 421]---> Adder-cost: 12   maxlim: 4479   bits: 14/13
c ---[ 420]---> Adder-cost: 6   maxlim: 5119   bits: 14/13
c ---[ 419]---> Adder-cost: 8   maxlim: 3839   bits: 13/12
c ---[ 418]---> Adder-cost: 8   maxlim: 2815   bits: 13/12
c ---[ 417]---> Adder-cost: 10   maxlim: 4863   bits: 14/13
c ---[ 416]---> Adder-cost: 14   maxlim: 8575   bits: 15/14
c ---[ 415]---> Adder-cost: 8   maxlim: 7679   bits: 14/13
c ---[ 414]---> Adder-cost: 4   maxlim: 6143   bits: 14/13
c ---[ 413]---> Adder-cost: 15   maxlim: 3583   bits: 13/12
c ---[ 412]---> Adder-cost: 12   maxlim: 4991   bits: 14/13
c ---[ 411]---> Adder-cost: 15   maxlim: 7679   bits: 14/13
c ---[ 410]---> Adder-cost: 6   maxlim: 3583   bits: 13/12
c ---[ 409]---> Adder-cost: 8   maxlim: 2815   bits: 13/12
c ---[ 408]---> Adder-cost: 15   maxlim: 7295   bits: 14/13
c ---[ 407]---> Adder-cost: 21   maxlim: 7935   bits: 14/13
c ---[ 406]---> Adder-cost: 8   maxlim: 6655   bits: 14/13
c ---[ 405]---> Adder-cost: 10   maxlim: 6399   bits: 14/13
c ---[ 404]---> Adder-cost: 113   maxlim: 32511   bits: 16/15
c ---[ 403]---> Adder-cost: 104   maxlim: 32383   bits: 16/15
c ---[ 402]---> Adder-cost: 104   maxlim: 25727   bits: 16/15
c ---[ 401]---> Adder-cost: 104   maxlim: 21375   bits: 16/15
c ---[ 400]---> Adder-cost: 125   maxlim: 59775   bits: 17/16
c ---[ 399]---> Adder-cost: 104   maxlim: 32383   bits: 16/15
c ---[ 398]---> Adder-cost: 104   maxlim: 25727   bits: 16/15
c ---[ 397]---> Adder-cost: 104   maxlim: 21375   bits: 16/15
c ---[ 396]---> Adder-cost: 102   maxlim: 19199   bits: 16/15
c ---[ 395]---> Adder-cost: 179   maxlim: 55295   bits: 17/16
c ---[ 394]---> Adder-cost: 161   maxlim: 64383   bits: 17/16
c ---[ 393]---> Adder-cost: 142   maxlim: 42751   bits: 17/16
c ---[ 392]---> Adder-cost: 143   maxlim: 42367   bits: 17/16
c ---[ 391]---> Adder-cost: 143   maxlim: 35711   bits: 17/16
c ---[ 390]---> Adder-cost: 133   maxlim: 28031   bits: 16/15
c ---[ 389]---> Adder-cost: 152   maxlim: 42367   bits: 17/16
c ---[ 388]---> Adder-cost: 157   maxlim: 85119   bits: 18/17
c ---[ 387]---> Adder-cost: 143   maxlim: 35711   bits: 17/16
c ---[ 386]---> Adder-cost: 133   maxlim: 31103   bits: 16/15
c ---[ 385]---> Adder-cost: 144   maxlim: 32511   bits: 16/15
c ---[ 384]---> Adder-cost: 135   maxlim: 25727   bits: 16/15
c ---[ 383]---> Adder-cost: 135   maxlim: 21375   bits: 16/15
c ---[ 382]---> Adder-cost: 144   maxlim: 32511   bits: 16/15
c ---[ 381]---> Adder-cost: 135   maxlim: 25727   bits: 16/15
c ---[ 380]---> Adder-cost: 135   maxlim: 21375   bits: 16/15
c ---[ 379]---> Adder-cost: 147   maxlim: 39423   bits: 17/16
c ---[ 378]---> Adder-cost: 135   maxlim: 32383   bits: 16/15
c ---[ 377]---> Adder-cost: 135   maxlim: 25727   bits: 16/15
c ---[ 376]---> Adder-cost: 135   maxlim: 21375   bits: 16/15
c ---[ 375]---> Adder-cost: 133   maxlim: 19199   bits: 16/15
c ---[ 374]---> Adder-cost: 170   maxlim: 71167   bits: 18/17
c ---[ 373]---> Adder-cost: 160   maxlim: 64383   bits: 17/16
c ---[ 372]---> Adder-cost: 135   maxlim: 21375   bits: 16/15
c ---[ 371]---> Adder-cost: 133   maxlim: 19199   bits: 16/15
c ---[ 370]---> Adder-cost: 233   maxlim: 77439   bits: 18/17
c ---[ 369]---> Adder-cost: 176   maxlim: 42367   bits: 17/16
c ---[ 368]---> Adder-cost: 176   maxlim: 35711   bits: 17/16
c ---[ 367]---> Adder-cost: 164   maxlim: 28031   bits: 16/15
c ---[ 366]---> Adder-cost: 205   maxlim: 80127   bits: 18/17
c ---[ 365]---> Adder-cost: 222   maxlim: 89983   bits: 18/17
c ---[ 364]---> Adder-cost: 193   maxlim: 64383   bits: 17/16
c ---[ 363]---> Adder-cost: 176   maxlim: 35711   bits: 17/16
c ---[ 362]---> Adder-cost: 164   maxlim: 28031   bits: 16/15
c ---[ 361]---> Adder-cost: 219   maxlim: 89983   bits: 18/17
c ---[ 360]---> Adder-cost: 196   maxlim: 77439   bits: 18/17
c ---[ 359]---> Adder-cost: 176   maxlim: 35711   bits: 17/16
c ---[ 358]---> Adder-cost: 164   maxlim: 28031   bits: 16/15
c ---[ 357]---> Adder-cost: 162   maxlim: 22783   bits: 16/15
c ---[ 356]---> Adder-cost: 176   maxlim: 35711   bits: 17/16
c ---[ 355]---> Adder-cost: 164   maxlim: 31103   bits: 16/15
c ---[ 354]---> Adder-cost: 205   maxlim: 80127   bits: 18/17
c ---[ 353]---> Adder-cost: 219   maxlim: 89983   bits: 18/17
c ---[ 352]---> Adder-cost: 176   maxlim: 35711   bits: 17/16
c ---[ 351]---> Adder-cost: 225   maxlim: 18303   bits: 16/15
c ---[ 350]---> Adder-cost: 174   maxlim: 83455   bits: 18/17
c ---[ 349]---> Adder-cost: 158   maxlim: 64383   bits: 17/16
c ---[ 348]---> Adder-cost: 133   maxlim: 21375   bits: 16/15
c ---[ 347]---> Adder-cost: 206   maxlim: 65023   bits: 17/16
c ---[ 346]---> Adder-cost: 226   maxlim: 128767   bits: 18/17
c ---[ 345]---> Adder-cost: 197   maxlim: 64767   bits: 17/16
c ---[ 344]---> Adder-cost: 197   maxlim: 51455   bits: 17/16
c ---[ 343]---> Adder-cost: 197   maxlim: 42751   bits: 17/16
c ---[ 342]---> Adder-cost: 195   maxlim: 38399   bits: 17/16
c ---[ 341]---> Adder-cost: 142   maxlim: 32511   bits: 16/15
c ---[ 340]---> Adder-cost: 133   maxlim: 25727   bits: 16/15
c ---[ 339]---> Adder-cost: 133   maxlim: 21375   bits: 16/15
c ---[ 338]---> Adder-cost: 173   maxlim: 32511   bits: 16/15
c ---[ 337]---> Adder-cost: 133   maxlim: 32383   bits: 16/15
c ---[ 336]---> Adder-cost: 133   maxlim: 25727   bits: 16/15
c ---[ 335]---> Adder-cost: 133   maxlim: 21375   bits: 16/15
c ---[ 334]---> Adder-cost: 131   maxlim: 19199   bits: 16/15
c ---[ 333]---> Adder-cost: 168   maxlim: 71167   bits: 18/17
c ---[ 332]---> Adder-cost: 158   maxlim: 64383   bits: 17/16
c ---[ 331]---> Adder-cost: 133   maxlim: 21375   bits: 16/15
c ---[ 330]---> Adder-cost: 131   maxlim: 19199   bits: 16/15
c ---[ 329]---> Adder-cost: 262   maxlim: 154879   bits: 19/18
c ---[ 328]---> Adder-cost: 222   maxlim: 62207   bits: 17/16
c ---[ 327]---> Adder-cost: 221   maxlim: 85119   bits: 18/17
c ---[ 326]---> Adder-cost: 221   maxlim: 78079   bits: 18/17
c ---[ 325]---> Adder-cost: 203   maxlim: 35711   bits: 17/16
c ---[ 324]---> Adder-cost: 189   maxlim: 28031   bits: 16/15
c ---[ 323]---> Adder-cost: 187   maxlim: 22783   bits: 16/15
c ---[ 322]---> Adder-cost: 203   maxlim: 35711   bits: 17/16
c ---[ 321]---> Adder-cost: 189   maxlim: 31103   bits: 16/15
c ---[ 320]---> Adder-cost: 234   maxlim: 80127   bits: 18/17
c ---[ 319]---> Adder-cost: 203   maxlim: 35711   bits: 17/16
c ---[ 318]---> Adder-cost: 189   maxlim: 18303   bits: 16/15
c ---[ 317]---> Adder-cost: 234   maxlim: 80127   bits: 18/17
c ---[ 316]---> Adder-cost: 203   maxlim: 35711   bits: 17/16
c ---[ 315]---> Adder-cost: 209   maxlim: 83455   bits: 18/17
c ---[ 314]---> Adder-cost: 191   maxlim: 64383   bits: 17/16
c ---[ 313]---> Adder-cost: 183   maxlim: 58111   bits: 17/16
c ---[ 312]---> Adder-cost: 164   maxlim: 25727   bits: 16/15
c ---[ 311]---> Adder-cost: 164   maxlim: 21375   bits: 16/15
c ---[ 310]---> Adder-cost: 492   maxlim: 179327   bits: 19/18
c ---[ 309]---> Adder-cost: 490   maxlim: 193151   bits: 19/18
c ---[ 308]---> Adder-cost: 450   maxlim: 77183   bits: 18/17
c ---[ 307]---> Adder-cost: 436   maxlim: 57599   bits: 17/16
c ---[ 306]---> Adder-cost: 191   maxlim: 64383   bits: 17/16
c ---[ 305]---> Adder-cost: 164   maxlim: 25727   bits: 16/15
c ---[ 304]---> Adder-cost: 164   maxlim: 21375   bits: 16/15
c ---[ 303]---> Adder-cost: 162   maxlim: 19199   bits: 16/15
c ---[ 302]---> Adder-cost: 261   maxlim: 51455   bits: 17/16
c ---[ 301]---> Adder-cost: 261   maxlim: 42751   bits: 17/16
c ---[ 300]---> Adder-cost: 259   maxlim: 38399   bits: 17/16
c ---[ 299]---> Adder-cost: 222   maxlim: 59775   bits: 17/16
c ---[ 298]---> Adder-cost: 191   maxlim: 64383   bits: 17/16
c ---[ 297]---> Adder-cost: 164   maxlim: 21375   bits: 16/15
c ---[ 296]---> Adder-cost: 162   maxlim: 19199   bits: 16/15
c ---[ 295]---> Adder-cost: 304   maxlim: 214271   bits: 19/18
c ---[ 294]---> Adder-cost: 262   maxlim: 154879   bits: 19/18
c ---[ 293]---> Adder-cost: 222   maxlim: 62207   bits: 17/16
c ---[ 292]---> Adder-cost: 220   maxlim: 45567   bits: 17/16
c ---[ 291]---> Adder-cost: 265   maxlim: 107135   bits: 18/17
c ---[ 290]---> Adder-cost: 260   maxlim: 77439   bits: 18/17
c ---[ 289]---> Adder-cost: 221   maxlim: 85119   bits: 18/17
c ---[ 288]---> Adder-cost: 203   maxlim: 35711   bits: 17/16
c ---[ 287]---> Adder-cost: 189   maxlim: 31103   bits: 16/15
c ---[ 286]---> Adder-cost: 189   maxlim: 28031   bits: 16/15
c ---[ 285]---> Adder-cost: 187   maxlim: 22783   bits: 16/15
c ---[ 284]---> Adder-cost: 264   maxlim: 67967   bits: 18/17
c ---[ 283]---> Adder-cost: 256   maxlim: 78079   bits: 18/17
c ---[ 282]---> Adder-cost: 203   maxlim: 35711   bits: 17/16
c ---[ 281]---> Adder-cost: 189   maxlim: 31103   bits: 16/15
c ---[ 280]---> Adder-cost: 262   maxlim: 67967   bits: 18/17
c ---[ 279]---> Adder-cost: 234   maxlim: 80127   bits: 18/17
c ---[ 278]---> Adder-cost: 203   maxlim: 35711   bits: 17/16
c ---[ 277]---> Adder-cost: 214   maxlim: 67967   bits: 18/17
c ---[ 276]---> Adder-cost: 216   maxlim: 80127   bits: 18/17
c ---[ 275]---> Adder-cost: 191   maxlim: 35711   bits: 17/16
c ---[ 274]---> Adder-cost: 262   maxlim: 67967   bits: 18/17
c ---[ 273]---> Adder-cost: 234   maxlim: 80127   bits: 18/17
c ---[ 272]---> Adder-cost: 203   maxlim: 35711   bits: 17/16
c ---[ 271]---> Adder-cost: 10   maxlim: 2687   bits: 13/12
c ---[ 270]---> Adder-cost: 4   maxlim: 1535   bits: 12/11
c ---[ 269]---> Adder-cost: 10   maxlim: 2175   bits: 13/12
c ---[ 268]---> Adder-cost: 8   maxlim: 3327   bits: 13/12
c ---[ 267]---> Adder-cost: 4   maxlim: 1535   bits: 12/11
c ---[ 266]---> Adder-cost: 10   maxlim: 3455   bits: 13/12
c ---[ 265]---> Adder-cost: 6   maxlim: 1791   bits: 12/11
c ---[ 264]---> Adder-cost: 10   maxlim: 3199   bits: 13/12
c ---[ 263]---> Adder-cost: 12   maxlim: 4223   bits: 14/13
c ---[ 262]---> Adder-cost: 10   maxlim: 3711   bits: 13/12
c ---[ 261]---> Adder-cost: 123   maxlim: 43391   bits: 17/16
c ---[ 260]---> Adder-cost: 96   maxlim: 12159   bits: 15/14
c ---[ 259]---> Adder-cost: 161   maxlim: 77439   bits: 18/17
c ---[ 258]---> Adder-cost: 125   maxlim: 12159   bits: 15/14
c ---[ 257]---> Adder-cost: 152   maxlim: 51455   bits: 17/16
c ---[ 256]---> Adder-cost: 113   maxlim: 32511   bits: 16/15
c ---[ 255]---> Adder-cost: 158   maxlim: 59775   bits: 17/16
c ---[ 254]---> Adder-cost: 47   maxlim: 16383   bits: 15/14
c ---[ 253]---> Adder-cost: 144   maxlim: 32511   bits: 16/15
c ---[ 252]---> Adder-cost: 125   maxlim: 59775   bits: 17/16
c ---[ 251]---> Adder-cost: 135   maxlim: 32383   bits: 16/15
c ---[ 250]---> Adder-cost: 135   maxlim: 25727   bits: 16/15
c ---[ 249]---> Adder-cost: 185   maxlim: 42367   bits: 17/16
c ---[ 248]---> Adder-cost: 193   maxlim: 64383   bits: 17/16
c ---[ 247]---> Adder-cost: 192   maxlim: 85119   bits: 18/17
c ---[ 246]---> Adder-cost: 192   maxlim: 85119   bits: 18/17
c ---[ 245]---> Adder-cost: 176   maxlim: 42367   bits: 17/16
c ---[ 244]---> Adder-cost: 192   maxlim: 85119   bits: 18/17
c ---[ 243]---> Adder-cost: 205   maxlim: 80127   bits: 18/17
c ---[ 242]---> Adder-cost: 219   maxlim: 89983   bits: 18/17
c ---[ 241]---> Adder-cost: 196   maxlim: 77439   bits: 18/17
c ---[ 240]---> Adder-cost: 196   maxlim: 77439   bits: 18/17
c ---[ 239]---> Adder-cost: 195   maxlim: 63103   bits: 17/16
c ---[ 238]---> Adder-cost: 162   maxlim: 63103   bits: 17/16
c ---[ 237]---> Adder-cost: 156   maxlim: 59775   bits: 17/16
c ---[ 236]---> Adder-cost: 142   maxlim: 32511   bits: 16/15
c ---[ 235]---> Adder-cost: 156   maxlim: 59775   bits: 17/16
c ---[ 234]---> Adder-cost: 133   maxlim: 25727   bits: 16/15
c ---[ 233]---> Adder-cost: 247   maxlim: 84735   bits: 18/17
c ---[ 232]---> Adder-cost: 285   maxlim: 179967   bits: 19/18
c ---[ 231]---> Adder-cost: 258   maxlim: 170239   bits: 19/18
c ---[ 230]---> Adder-cost: 234   maxlim: 80127   bits: 18/17
c ---[ 229]---> Adder-cost: 244   maxlim: 89983   bits: 18/17
c ---[ 228]---> Adder-cost: 225   maxlim: 77439   bits: 18/17
c ---[ 227]---> Adder-cost: 158   maxlim: 28031   bits: 16/15
c ---[ 226]---> Adder-cost: 187   maxlim: 22783   bits: 16/15
c ---[ 225]---> Adder-cost: 244   maxlim: 89983   bits: 18/17
c ---[ 224]---> Adder-cost: 225   maxlim: 77439   bits: 18/17
c ---[ 223]---> Adder-cost: 158   maxlim: 28031   bits: 16/15
c ---[ 222]---> Adder-cost: 156   maxlim: 22783   bits: 16/15
c ---[ 221]---> Adder-cost: 244   maxlim: 89983   bits: 18/17
c ---[ 220]---> Adder-cost: 186   maxlim: 85119   bits: 18/17
c ---[ 219]---> Adder-cost: 158   maxlim: 28031   bits: 16/15
c ---[ 218]---> Adder-cost: 190   maxlim: 52223   bits: 17/16
c ---[ 217]---> Adder-cost: 474   maxlim: 118271   bits: 18/17
c ---[ 216]---> Adder-cost: 481   maxlim: 130175   bits: 18/17
c ---[ 215]---> Adder-cost: 492   maxlim: 154367   bits: 19/18
c ---[ 214]---> Adder-cost: 420   maxlim: 36479   bits: 17/16
c ---[ 213]---> Adder-cost: 238   maxlim: 71167   bits: 18/17
c ---[ 212]---> Adder-cost: 189   maxlim: 59775   bits: 17/16
c ---[ 211]---> Adder-cost: 298   maxlim: 126207   bits: 18/17
c ---[ 210]---> Adder-cost: 292   maxlim: 119551   bits: 18/17
c ---[ 209]---> Adder-cost: 261   maxlim: 64767   bits: 17/16
c ---[ 208]---> Adder-cost: 243   maxlim: 24319   bits: 16/15
c ---[ 207]---> Adder-cost: 214   maxlim: 103167   bits: 18/17
c ---[ 206]---> Adder-cost: 164   maxlim: 32383   bits: 16/15
c ---[ 205]---> Adder-cost: 164   maxlim: 25727   bits: 16/15
c ---[ 204]---> Adder-cost: 181   maxlim: 12159   bits: 15/14
c ---[ 203]---> Adder-cost: 308   maxlim: 160255   bits: 19/18
c ---[ 202]---> Adder-cost: 285   maxlim: 179967   bits: 19/18
c ---[ 201]---> Adder-cost: 258   maxlim: 170239   bits: 19/18
c ---[ 200]---> Adder-cost: 221   maxlim: 85119   bits: 18/17
c ---[ 199]---> Adder-cost: 187   maxlim: 22783   bits: 16/15
c ---[ 198]---> Adder-cost: 248   maxlim: 89983   bits: 18/17
c ---[ 197]---> Adder-cost: 225   maxlim: 77439   bits: 18/17
c ---[ 196]---> Adder-cost: 236   maxlim: 42367   bits: 17/16
c ---[ 195]---> Adder-cost: 226   maxlim: 89983   bits: 18/17
c ---[ 194]---> Adder-cost: 205   maxlim: 77439   bits: 18/17
c ---[ 193]---> Adder-cost: 191   maxlim: 42367   bits: 17/16
c ---[ 192]---> Adder-cost: 248   maxlim: 89983   bits: 18/17
c ---[ 191]---> Adder-cost: 260   maxlim: 77439   bits: 18/17
c ---[ 190]---> Adder-cost: 204   maxlim: 42367   bits: 17/16
c ---[ 189]---> Adder-cost: 16   maxlim: 9983   bits: 15/14
c ---[ 188]---> Adder-cost: 17   maxlim: 3711   bits: 13/12
c ---[ 187]---> Adder-cost: 161   maxlim: 77439   bits: 18/17
c ---[ 186]---> Adder-cost: 170   maxlim: 71167   bits: 18/17
c ---[ 185]---> Adder-cost: 105   maxlim: 32383   bits: 16/15
c ---[ 184]---> Adder-cost: 83   maxlim: 16383   bits: 15/14
c ---[ 183]---> Adder-cost: 164   maxlim: 63103   bits: 17/16
c ---[ 182]---> Adder-cost: 170   maxlim: 71167   bits: 18/17
c ---[ 181]---> Adder-cost: 135   maxlim: 32383   bits: 16/15
c ---[ 180]---> Adder-cost: 47   maxlim: 16383   bits: 15/14
c ---[ 179]---> Adder-cost: 185   maxlim: 42367   bits: 17/16
c ---[ 178]---> Adder-cost: 196   maxlim: 77439   bits: 18/17
c ---[ 177]---> Adder-cost: 205   maxlim: 80127   bits: 18/17
c ---[ 176]---> Adder-cost: 185   maxlim: 42367   bits: 17/16
c ---[ 175]---> Adder-cost: 185   maxlim: 42367   bits: 17/16
c ---[ 174]---> Adder-cost: 156   maxlim: 59775   bits: 17/16
c ---[ 173]---> Adder-cost: 133   maxlim: 25727   bits: 16/15
c ---[ 172]---> Adder-cost: 240   maxlim: 142335   bits: 19/18
c ---[ 171]---> Adder-cost: 224   maxlim: 119551   bits: 18/17
c ---[ 170]---> Adder-cost: 133   maxlim: 32383   bits: 16/15
c ---[ 169]---> Adder-cost: 178   maxlim: 39423   bits: 17/16
c ---[ 168]---> Adder-cost: 183   maxlim: 51455   bits: 17/16
c ---[ 167]---> Adder-cost: 238   maxlim: 84735   bits: 18/17
c ---[ 166]---> Adder-cost: 244   maxlim: 89983   bits: 18/17
c ---[ 165]---> Adder-cost: 193   maxlim: 107135   bits: 18/17
c ---[ 164]---> Adder-cost: 190   maxlim: 77439   bits: 18/17
c ---[ 163]---> Adder-cost: 105   maxlim: 42367   bits: 17/16
c ---[ 162]---> Adder-cost: 207   maxlim: 103167   bits: 18/17
c ---[ 161]---> Adder-cost: 216   maxlim: 92159   bits: 18/17
c ---[ 160]---> Adder-cost: 96   maxlim: 32383   bits: 16/15
c ---[ 159]---> Adder-cost: 450   maxlim: 97151   bits: 18/17
c ---[ 158]---> Adder-cost: 190   maxlim: 52223   bits: 17/16
c ---[ 157]---> Adder-cost: 164   maxlim: 32383   bits: 16/15
c ---[ 156]---> Adder-cost: 286   maxlim: 102911   bits: 18/17
c ---[ 155]---> Adder-cost: 190   maxlim: 52223   bits: 17/16
c ---[ 154]---> Adder-cost: 212   maxlim: 83455   bits: 18/17
c ---[ 153]---> Adder-cost: 238   maxlim: 84735   bits: 18/17
c ---[ 152]---> Adder-cost: 264   maxlim: 67967   bits: 18/17
c ---[ 151]---> Adder-cost: 248   maxlim: 89983   bits: 18/17
c ---[ 150]---> Adder-cost: 203   maxlim: 42367   bits: 17/16
c ---[ 149]---> Adder-cost: 234   maxlim: 80127   bits: 18/17
c ---[ 148]---> Adder-cost: 225   maxlim: 77439   bits: 18/17
c ---[ 147]---> Adder-cost: 127   maxlim: 64383   bits: 17/16
c ---[ 146]---> Adder-cost: 107   maxlim: 85119   bits: 18/17
c ---[ 145]---> Adder-cost: 127   maxlim: 64383   bits: 17/16
c ---[ 144]---> Adder-cost: 176   maxlim: 42367   bits: 17/16
c ---[ 143]---> Adder-cost: 230   maxlim: 126207   bits: 18/17
c ---[ 142]---> Adder-cost: 218   maxlim: 102911   bits: 18/17
c ---[ 141]---> Adder-cost: 162   maxlim: 63103   bits: 17/16
c ---[ 140]---> Adder-cost: 168   maxlim: 71167   bits: 18/17
c ---[ 139]---> Adder-cost: 150   maxlim: 51455   bits: 17/16
c ---[ 138]---> Adder-cost: 234   maxlim: 160255   bits: 19/18
c ---[ 137]---> Adder-cost: 219   maxlim: 128767   bits: 18/17
c ---[ 136]---> Adder-cost: 199   maxlim: 80127   bits: 18/17
c ---[ 135]---> Adder-cost: 167   maxlim: 42367   bits: 17/16
c ---[ 134]---> Adder-cost: 170   maxlim: 42367   bits: 17/16
c ---[ 133]---> Adder-cost: 212   maxlim: 90879   bits: 18/17
c ---[ 132]---> Adder-cost: 125   maxlim: 59775   bits: 17/16
c ---[ 131]---> Adder-cost: 116   maxlim: 28543   bits: 16/15
c ---[ 130]---> Adder-cost: 460   maxlim: 97535   bits: 18/17
c ---[ 129]---> Adder-cost: 225   maxlim: 189311   bits: 19/18
c ---[ 128]---> Adder-cost: 251   maxlim: 213503   bits: 19/18
c ---[ 127]---> Adder-cost: 101   maxlim: 32511   bits: 16/15
c ---[ 126]---> Adder-cost: 248   maxlim: 89983   bits: 18/17
c ---[ 125]---> Adder-cost: 113   maxlim: 42367   bits: 17/16
c ---[ 124]---> Adder-cost: 19   maxlim: 7679   bits: 14/13
c ---[ 123]---> Adder-cost: 14   maxlim: 8703   bits: 15/14
c ---[ 122]---> Adder-cost: 25   maxlim: 16255   bits: 15/14
c ---[ 121]---> Adder-cost: 131   maxlim: 63103   bits: 17/16
c ---[ 120]---> Adder-cost: 170   maxlim: 80127   bits: 18/17
c ---[ 119]---> Adder-cost: 184   maxlim: 89983   bits: 18/17
c ---[ 118]---> Adder-cost: 160   maxlim: 64383   bits: 17/16
c ---[ 117]---> Adder-cost: 89   maxlim: 63103   bits: 17/16
c ---[ 116]---> Adder-cost: 135   maxlim: 71167   bits: 18/17
c ---[ 115]---> Adder-cost: 120   maxlim: 51455   bits: 17/16
c ---[ 114]---> Adder-cost: 131   maxlim: 63103   bits: 17/16
c ---[ 113]---> Adder-cost: 141   maxlim: 83455   bits: 18/17
c ---[ 112]---> Adder-cost: 205   maxlim: 80127   bits: 18/17
c ---[ 111]---> Adder-cost: 219   maxlim: 89983   bits: 18/17
c ---[ 110]---> Adder-cost: 198   maxlim: 67967   bits: 18/17
c ---[ 109]---> Adder-cost: 193   maxlim: 64383   bits: 17/16
c ---[ 108]---> Adder-cost: 193   maxlim: 64383   bits: 17/16
c ---[ 107]---> Adder-cost: 168   maxlim: 71167   bits: 18/17
c ---[ 106]---> Adder-cost: 133   maxlim: 32383   bits: 16/15
c ---[ 105]---> Adder-cost: 178   maxlim: 42367   bits: 17/16
c ---[ 104]---> Adder-cost: 178   maxlim: 42367   bits: 17/16
c ---[ 103]---> Adder-cost: 178   maxlim: 42367   bits: 17/16
c ---[ 102]---> Adder-cost: 188   maxlim: 64383   bits: 17/16
c ---[ 101]---> Adder-cost: 188   maxlim: 64383   bits: 17/16
c ---[ 100]---> Adder-cost: 140   maxlim: 103167   bits: 18/17
c ---[  99]---> Adder-cost: 270   maxlim: 65023   bits: 17/16
c ---[  98]---> Adder-cost: 195   maxlim: 63103   bits: 17/16
c ---[  97]---> Adder-cost: 129   maxlim: 71167   bits: 18/17
c ---[  96]---> Adder-cost: 126   maxlim: 42367   bits: 17/16
c ---[  95]---> Adder-cost: 126   maxlim: 42367   bits: 17/16
c ---[  94]---> Adder-cost: 122   maxlim: 42367   bits: 17/16
c ---[  93]---> Adder-cost: 140   maxlim: 64383   bits: 17/16
c ---[  92]---> Adder-cost: 127   maxlim: 42367   bits: 17/16
c ---[  91]---> Adder-cost: 16   maxlim: 9599   bits: 15/14
c ---[  90]---> Adder-cost: 14   maxlim: 16639   bits: 16/15
c ---[  89]---> Adder-cost: 11   maxlim: 4095   bits: 13/12
c ---[  88]---> Adder-cost: 19   maxlim: 5759   bits: 14/13
c ---[  87]---> Adder-cost: 10   maxlim: 3199   bits: 13/12
c ---[  86]---> Adder-cost: 67   maxlim: 31999   bits: 16/15
c ---[  85]---> Adder-cost: 195   maxlim: 67967   bits: 18/17
c ---[  84]---> Adder-cost: 190   maxlim: 77439   bits: 18/17
c ---[  83]---> Adder-cost: 133   maxlim: 63103   bits: 17/16
c ---[  82]---> Adder-cost: 194   maxlim: 95999   bits: 18/17
c ---[  81]---> Adder-cost: 195   maxlim: 63103   bits: 17/16
c ---[  80]---> Adder-cost: 101   maxlim: 32511   bits: 16/15
c ---[  79]---> Adder-cost: 247   maxlim: 84735   bits: 18/17
c ---[  78]---> Adder-cost: 155   maxlim: 128767   bits: 18/17
c ---[  77]---> Adder-cost: 9   maxlim: 14335   bits: 15/14
c ---[  76]---> Adder-cost: 21   maxlim: 7423   bits: 14/13
c ---[  75]---> Adder-cost: 14   maxlim: 8319   bits: 15/14
c ---[  74]---> Adder-cost: 21   maxlim: 10367   bits: 15/14
c ---[  73]---> Adder-cost: 114   maxlim: 39423   bits: 17/16
c ---[  72]---> Adder-cost: 88   maxlim: 43391   bits: 17/16
c ---[  71]---> Adder-cost: 109   maxlim: 42367   bits: 17/16
c ---[  70]---> Adder-cost: 193   maxlim: 64383   bits: 17/16
c ---[  69]---> Adder-cost: 222   maxlim: 36607   bits: 17/16
c ---[  68]---> Adder-cost: 189   maxlim: 18303   bits: 16/15
c ---[  67]---> Adder-cost: 101   maxlim: 32511   bits: 16/15
c ---[  66]---> Adder-cost: 126   maxlim: 42367   bits: 17/16
c ---[  65]---> Adder-cost: 169   maxlim: 114815   bits: 18/17
c ---[  64]---> Adder-cost: 169   maxlim: 114815   bits: 18/17
c ---[  63]---> Adder-cost: 50   maxlim: 12799   bits: 15/14
c ---[  62]---> Adder-cost: 141   maxlim: 83455   bits: 18/17
c ---[  61]---> Adder-cost: 122   maxlim: 67967   bits: 18/17
c ---[  60]---> Adder-cost: 154   maxlim: 52223   bits: 17/16
c ---[  59]---> Adder-cost: 150   maxlim: 51455   bits: 17/16
c ---[  58]---> Adder-cost: 154   maxlim: 38399   bits: 17/16
c ---[  57]---> Adder-cost: 235   maxlim: 250367   bits: 19/18
c ---[  56]---> Adder-cost: 220   maxlim: 18303   bits: 16/15
c ---[  55]---> Adder-cost: 10   maxlim: 3711   bits: 13/12
c ---[  54]---> Adder-cost: 17   maxlim: 13439   bits: 15/14
c ---[  53]---> Adder-cost: 50   maxlim: 12799   bits: 15/14
c ---[  52]---> Adder-cost: 179   maxlim: 103167   bits: 18/17
c ---[  51]---> Adder-cost: 158   maxlim: 166911   bits: 19/18
c ---[  50]---> Adder-cost: 156   maxlim: 119807   bits: 18/17
c ---[  49]---> Adder-cost: 99   maxlim: 71167   bits: 18/17
c ---[  48]---> Adder-cost: 129   maxlim: 107135   bits: 18/17
c ---[  47]---> Adder-cost: 115   maxlim: 11135   bits: 15/14
c ---[  46]---> Adder-cost: 99   maxlim: 21247   bits: 16/15
c ---[  45]---> Adder-cost: 88   maxlim: 11391   bits: 15/14
c ---[  44]---> Adder-cost: 96   maxlim: 14207   bits: 15/14
c ---[  43]---> Adder-cost: 88   maxlim: 15103   bits: 15/14
c ---[  42]---> Adder-cost: 63   maxlim: 11391   bits: 15/14
c ---[  41]---> Adder-cost: 100   maxlim: 15487   bits: 15/14
c ---[  40]---> Adder-cost: 23   maxlim: 16127   bits: 15/14
c ---[  39]---> Adder-cost: 19   maxlim: 7295   bits: 14/13
c ---[  38]---> Adder-cost: 14   maxlim: 8319   bits: 15/14
c ---[  37]---> Adder-cost: 110   maxlim: 71167   bits: 18/17
c ---[  36]---> Adder-cost: 108   maxlim: 63103   bits: 17/16
c ---[  35]---> Adder-cost: 139   maxlim: 64383   bits: 17/16
c ---[  34]---> Adder-cost: 97   maxlim: 16255   bits: 15/14
c ---[  33]---> Adder-cost: 87   maxlim: 25087   bits: 16/15
c ---[  32]---> Adder-cost: 15   maxlim: 7295   bits: 14/13
c ---[  31]---> Adder-cost: 105   maxlim: 55295   bits: 17/16
c ---[  30]---> Adder-cost: 129   maxlim: 119807   bits: 18/17
c ---[  29]---> Adder-cost: 101   maxlim: 24063   bits: 16/15
c ---[  28]---> Adder-cost: 132   maxlim: 75903   bits: 18/17
c ---[  27]---> Adder-cost: 107   maxlim: 100863   bits: 18/17
c ---[  26]---> Adder-cost: 118   maxlim: 20095   bits: 16/15
c ---[  25]---> Adder-cost: 95   maxlim: 28031   bits: 16/15
c ---[  24]---> Adder-cost: 35   maxlim: 25087   bits: 16/15
c ---[  23]---> Adder-cost: 115   maxlim: 14079   bits: 15/14
c ---[  22]---> Adder-cost: 26   maxlim: 6654   bits: 14/13
c ---[  21]---> Adder-cost: 26   maxlim: 5246   bits: 14/13
c ---[  20]---> Adder-cost: 24   maxlim: 3326   bits: 13/12
c ---[  19]---> Adder-cost: 34   maxlim: 130430   bits: 18/17
c ---[  18]---> Adder-cost: 150   maxlim: 116220   bits: 18/17
c ---[  17]---> Adder-cost: 143   maxlim: 99836   bits: 18/17
c ---[  16]---> Adder-cost: 141   maxlim: 67068   bits: 18/17
c ---[  15]---> Adder-cost: 140   maxlim: 50684   bits: 17/16
c ---[  14]---> Adder-cost: 135   maxlim: 34300   bits: 17/16
c ---[  13]---> Adder-cost: 132   maxlim: 26108   bits: 16/15
c ---[  12]---> Adder-cost: 125   maxlim: 9724   bits: 15/14
c ---[  11]---> Adder-cost: 101   maxlim: 5628   bits: 14/13
c ---[  10]---> Adder-cost: 150   maxlim: 113404   bits: 18/17
c ---[   9]---> Adder-cost: 150   maxlim: 113404   bits: 18/17
c ---[   8]---> Adder-cost: 145   maxlim: 97020   bits: 18/17
c ---[   7]---> Adder-cost: 140   maxlim: 47868   bits: 17/16
c ---[   6]---> Adder-cost: 133   maxlim: 39676   bits: 17/16
c ---[   5]---> Adder-cost: 126   maxlim: 15100   bits: 15/14
c ---[   4]---> Adder-cost: 115   maxlim: 6908   bits: 14/13
c ---[   3]---> Adder-cost: 165   maxlim: 28667   bits: 16/15
c ---[   2]---> Adder-cost: 332   maxlim: 62326   bits: 17/16
c ---[   1]---> Adder-cost: 387   maxlim: 90229   bits: 18/17
c ---[   0]---> Adder-cost: 410   maxlim: 85748   bits: 18/17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1287370  4664593 |  429123       0        0     nan |  0.000 % |
c |       100 | 1287370  4664593 |  472035     100      402     4.0 | 17.841 % |
c |       250 | 1287370  4664593 |  519238     250      951     3.8 | 17.841 % |
c |       475 | 1287370  4664593 |  571162     475     1964     4.1 | 17.841 % |
c |       812 | 1287308  4664391 |  628278     799     3483     4.4 | 17.845 % |
c |      1318 | 1287214  4664089 |  691106    1289     5543     4.3 | 17.850 % |
c |      2077 | 1287029  4663490 |  760217    2015     9027     4.5 | 17.860 % |
c |      3216 | 1286829  4662850 |  836239    3115    13947     4.5 | 17.872 % |
c |      4924 | 1286438  4661579 |  919863    4706    21264     4.5 | 17.893 % |
c |      7486 | 1286222  4660885 | 1011849    7217    34725     4.8 | 17.905 % |
c |     11330 | 1286037  4660286 | 1113034   11017    74857     6.8 | 17.916 % |
c |     17096 | 1285453  4658378 | 1224338   16598   148650     9.0 | 17.948 % |
c |     25745 | 1284836  4656369 | 1346771   25089   248233     9.9 | 17.981 % |
c |     38720 | 1283943  4653456 | 1481448   37786   383747    10.2 | 18.030 % |
c |     58181 | 1282838  4649853 | 1629593   56937   606758    10.7 | 18.090 % |
c |     87374 | 1282511  4648788 | 1792553   86047  1214179    14.1 | 18.108 % |
c |    131164 | 1282490  4648719 | 1971808  129833  2106375    16.2 | 18.109 % |
c |    196849 | 1281971  4647024 | 2168989  195393  4044325    20.7 | 18.138 % |
c |    295375 | 1281494  4645469 | 2385888  293826 10334642    35.2 | 18.164 % |
c |    443164 | 1280622  4642624 | 2624477  441430 15793319    35.8 | 18.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.90 0.98 0.91 2/54 23996
Raw data (stat): 23996 (runsolver) R 23995 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539976031 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99956 s]
Raw data (loadavg): 0.92 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 30714 0 0 0 917 81 0 0 25 0 1 0 539976031 149925888 29195 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36603 29195 603 41 0 36562 0
vsize: 146412
[startup+20.0003 s]
Raw data (loadavg): 0.93 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 30716 0 0 0 1917 82 0 0 25 0 1 0 539976031 149925888 29197 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36603 29197 603 41 0 36562 0
vsize: 146412
[startup+30 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 30778 0 0 0 2917 82 0 0 25 0 1 0 539976031 150196224 29259 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36669 29259 603 41 0 36628 0
vsize: 146676
[startup+40.0008 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 30935 0 0 0 3916 83 0 0 25 0 1 0 539976031 150872064 29416 4294967295 134512640 134672761 3221224544 3221223744 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36834 29416 603 41 0 36793 0
vsize: 147336
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31068 0 0 0 4915 84 0 0 25 0 1 0 539976031 151437312 29549 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36972 29549 603 41 0 36931 0
vsize: 147888
[startup+60.0011 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31134 0 0 0 5915 85 0 0 25 0 1 0 539976031 151707648 29615 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37038 29615 603 41 0 36997 0
vsize: 148152
[startup+70.0009 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31256 0 0 0 6914 86 0 0 25 0 1 0 539976031 152113152 29737 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37137 29737 603 41 0 37096 0
vsize: 148548
[startup+80.001 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31318 0 0 0 7913 86 0 0 25 0 1 0 539976031 152383488 29799 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37203 29799 603 41 0 37162 0
vsize: 148812
[startup+90.0013 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31454 0 0 0 8913 87 0 0 25 0 1 0 539976031 153083904 29935 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37374 29935 603 41 0 37333 0
vsize: 149496
[startup+100.001 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31520 0 0 0 9913 87 0 0 25 0 1 0 539976031 153219072 30001 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37407 30001 603 41 0 37366 0
vsize: 149628
[startup+110.001 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31555 0 0 0 10913 87 0 0 25 0 1 0 539976031 153354240 30036 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37440 30036 603 41 0 37399 0
vsize: 149760
[startup+120.001 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31646 0 0 0 11913 88 0 0 25 0 1 0 539976031 153759744 30127 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37539 30127 603 41 0 37498 0
vsize: 150156
[startup+130.001 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31721 0 0 0 12912 88 0 0 25 0 1 0 539976031 154030080 30202 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37605 30202 603 41 0 37564 0
vsize: 150420
[startup+140.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31779 0 0 0 13912 89 0 0 25 0 1 0 539976031 154300416 30260 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37671 30260 603 41 0 37630 0
vsize: 150684
[startup+150.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31851 0 0 0 14912 89 0 0 25 0 1 0 539976031 154570752 30332 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37737 30332 603 41 0 37696 0
vsize: 150948
[startup+160.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31957 0 0 0 15912 89 0 0 25 0 1 0 539976031 155103232 30438 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37867 30438 603 41 0 37826 0
vsize: 151468
[startup+170.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 31993 0 0 0 16912 90 0 0 25 0 1 0 539976031 155238400 30474 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37900 30474 603 41 0 37859 0
vsize: 151600
[startup+180.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 32056 0 0 0 17912 90 0 0 25 0 1 0 539976031 155508736 30537 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37966 30537 603 41 0 37925 0
vsize: 151864
[startup+190.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 32106 0 0 0 18912 90 0 0 25 0 1 0 539976031 155779072 30587 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38032 30587 603 41 0 37991 0
vsize: 152128
[startup+200.002 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 32264 0 0 0 19912 90 0 0 25 0 1 0 539976031 156319744 30745 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38164 30745 603 41 0 38123 0
vsize: 152656
[startup+210.01 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 32321 0 0 0 20912 91 0 0 25 0 1 0 539976031 156590080 30802 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38230 30802 603 41 0 38189 0
vsize: 152920
[startup+220.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 32396 0 0 0 21913 91 0 0 25 0 1 0 539976031 156860416 30877 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38296 30877 603 41 0 38255 0
vsize: 153184
[startup+230.017 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 32462 0 0 0 22913 91 0 0 25 0 1 0 539976031 157130752 30943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38362 30943 603 41 0 38321 0
vsize: 153448
[startup+240.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 32512 0 0 0 23913 91 0 0 25 0 1 0 539976031 157401088 30993 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38428 30993 603 41 0 38387 0
vsize: 153712
[startup+250.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 32563 0 0 0 24913 92 0 0 25 0 1 0 539976031 157536256 31044 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38461 31044 603 41 0 38420 0
vsize: 153844
[startup+260.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 32624 0 0 0 25912 92 0 0 25 0 1 0 539976031 157806592 31105 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38527 31105 603 41 0 38486 0
vsize: 154108
[startup+270.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 32688 0 0 0 26913 92 0 0 25 0 1 0 539976031 158076928 31169 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38593 31169 603 41 0 38552 0
vsize: 154372
[startup+280.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 33201 0 0 0 27911 94 0 0 25 0 1 0 539976031 160354304 31682 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39149 31682 603 41 0 39108 0
vsize: 156596
[startup+290.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 33335 0 0 0 28911 94 0 0 25 0 1 0 539976031 160894976 31816 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39281 31816 603 41 0 39240 0
vsize: 157124
[startup+300.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 33777 0 0 0 29910 95 0 0 25 0 1 0 539976031 162639872 32258 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39707 32258 603 41 0 39666 0
vsize: 158828
[startup+310.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 34291 0 0 0 30909 97 0 0 25 0 1 0 539976031 164679680 32772 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40205 32772 603 41 0 40164 0
vsize: 160820
[startup+320.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 34710 0 0 0 31908 98 0 0 25 0 1 0 539976031 166440960 33191 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40635 33191 603 41 0 40594 0
vsize: 162540
[startup+330.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 34920 0 0 0 32908 98 0 0 25 0 1 0 539976031 167383040 33401 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40865 33401 603 41 0 40824 0
vsize: 163460
[startup+340.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 35004 0 0 0 33908 98 0 0 25 0 1 0 539976031 168177664 33485 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41059 33485 603 41 0 41018 0
vsize: 164236
[startup+350.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 35167 0 0 0 34908 99 0 0 25 0 1 0 539976031 168849408 33648 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41223 33648 603 41 0 41182 0
vsize: 164892
[startup+360.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 35377 0 0 0 35907 99 0 0 25 0 1 0 539976031 169660416 33858 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41421 33858 603 41 0 41380 0
vsize: 165684
[startup+370.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 35550 0 0 0 36907 100 0 0 25 0 1 0 539976031 170336256 34031 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41586 34031 603 41 0 41545 0
vsize: 166344
[startup+380.018 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 35934 0 0 0 37906 101 0 0 25 0 1 0 539976031 171950080 34415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41980 34415 603 41 0 41939 0
vsize: 167920
[startup+390.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 36069 0 0 0 38905 102 0 0 25 0 1 0 539976031 172498944 34550 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42114 34550 603 41 0 42073 0
vsize: 168456
[startup+400.019 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 36497 0 0 0 39904 103 0 0 25 0 1 0 539976031 174247936 34978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42541 34978 603 41 0 42500 0
vsize: 170164
[startup+410.02 s]
Raw data (loadavg): 0.99 0.98 0.91 3/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 36938 0 0 0 40903 105 0 0 25 0 1 0 539976031 176021504 35419 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42974 35419 603 41 0 42933 0
vsize: 171896
[startup+420.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 37337 0 0 0 41902 106 0 0 25 0 1 0 539976031 177655808 35818 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43373 35818 603 41 0 43332 0
vsize: 173492
[startup+430.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 37605 0 0 0 42901 107 0 0 25 0 1 0 539976031 178733056 36086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43636 36086 603 41 0 43595 0
vsize: 174544
[startup+440.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 37707 0 0 0 43901 107 0 0 25 0 1 0 539976031 179142656 36188 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43736 36188 603 41 0 43695 0
vsize: 174944
[startup+450.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 38033 0 0 0 44900 108 0 0 25 0 1 0 539976031 180490240 36514 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44065 36514 603 41 0 44024 0
vsize: 176260
[startup+460.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 38461 0 0 0 45898 110 0 0 25 0 1 0 539976031 182239232 36942 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44492 36942 603 41 0 44451 0
vsize: 177968
[startup+470.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 38674 0 0 0 46898 111 0 0 25 0 1 0 539976031 183054336 37155 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44691 37155 603 41 0 44650 0
vsize: 178764
[startup+480.02 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 38761 0 0 0 47898 111 0 0 25 0 1 0 539976031 183459840 37242 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44790 37242 603 41 0 44749 0
vsize: 179160
[startup+490.021 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 39041 0 0 0 48897 112 0 0 25 0 1 0 539976031 184549376 37522 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45056 37522 603 41 0 45015 0
vsize: 180224
[startup+500.028 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 39162 0 0 0 49897 112 0 0 25 0 1 0 539976031 184954880 37643 4294967295 134512640 134672761 3221224544 3221223712 134564467 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45155 37643 603 41 0 45114 0
vsize: 180620
[startup+510.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 39322 0 0 0 50897 113 0 0 25 0 1 0 539976031 185626624 37803 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45319 37803 603 41 0 45278 0
vsize: 181276
[startup+520.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 39865 0 0 0 51895 115 0 0 25 0 1 0 539976031 187908096 38346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45876 38346 603 41 0 45835 0
vsize: 183504
[startup+530.027 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 40134 0 0 0 52894 116 0 0 25 0 1 0 539976031 188993536 38615 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46141 38615 603 41 0 46100 0
vsize: 184564
[startup+540.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 40209 0 0 0 53895 116 0 0 25 0 1 0 539976031 189267968 38690 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46208 38690 603 41 0 46167 0
vsize: 184832
[startup+550.032 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 40288 0 0 0 54894 117 0 0 25 0 1 0 539976031 189542400 38769 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46275 38769 603 41 0 46234 0
vsize: 185100
[startup+560.033 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 40670 0 0 0 55893 118 0 0 25 0 1 0 539976031 191164416 39151 4294967295 134512640 134672761 3221224544 3221223648 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46671 39151 603 41 0 46630 0
vsize: 186684
[startup+570.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 41224 0 0 0 56892 120 0 0 25 0 1 0 539976031 193335296 39705 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47201 39705 603 41 0 47160 0
vsize: 188804
[startup+580.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 41753 0 0 0 57890 122 0 0 25 0 1 0 539976031 196546560 40234 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47985 40234 603 41 0 47944 0
vsize: 191940
[startup+590.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 42286 0 0 0 58888 124 0 0 25 0 1 0 539976031 198705152 40767 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48512 40767 603 41 0 48471 0
vsize: 194048
[startup+600.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 42780 0 0 0 59885 127 0 0 25 0 1 0 539976031 200744960 41261 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49010 41261 603 41 0 48969 0
vsize: 196040
[startup+610.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 43030 0 0 0 60885 128 0 0 25 0 1 0 539976031 201834496 41511 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49276 41511 603 41 0 49235 0
vsize: 197104
[startup+620.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 43332 0 0 0 61884 129 0 0 25 0 1 0 539976031 203042816 41813 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49571 41813 603 41 0 49530 0
vsize: 198284
[startup+630.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 43668 0 0 0 62883 130 0 0 25 0 1 0 539976031 204390400 42149 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49900 42149 603 41 0 49859 0
vsize: 199600
[startup+640.035 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 43937 0 0 0 63881 132 0 0 25 0 1 0 539976031 205463552 42418 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50162 42418 603 41 0 50121 0
vsize: 200648
[startup+650.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 44244 0 0 0 64880 133 0 0 25 0 1 0 539976031 206671872 42725 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50457 42725 603 41 0 50416 0
vsize: 201828
[startup+660.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 44567 0 0 0 65879 134 0 0 25 0 1 0 539976031 208011264 43048 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50784 43048 603 41 0 50743 0
vsize: 203136
[startup+670.034 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 44917 0 0 0 66878 135 0 0 25 0 1 0 539976031 209522688 43398 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51153 43398 603 41 0 51112 0
vsize: 204612
[startup+680.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 45123 0 0 0 67877 136 0 0 25 0 1 0 539976031 210354176 43604 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51356 43604 603 41 0 51315 0
vsize: 205424
[startup+690.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 45232 0 0 0 68876 137 0 0 25 0 1 0 539976031 210763776 43713 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51456 43713 603 41 0 51415 0
vsize: 205824
[startup+700.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 45297 0 0 0 69876 137 0 0 25 0 1 0 539976031 211034112 43778 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51522 43778 603 41 0 51481 0
vsize: 206088
[startup+710.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 45637 0 0 0 70875 138 0 0 25 0 1 0 539976031 212398080 44118 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51855 44118 603 41 0 51814 0
vsize: 207420
[startup+720.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 45753 0 0 0 71875 138 0 0 25 0 1 0 539976031 212938752 44234 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51987 44234 603 41 0 51946 0
vsize: 207948
[startup+730.036 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 46082 0 0 0 72874 140 0 0 25 0 1 0 539976031 214290432 44563 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52317 44563 603 41 0 52276 0
vsize: 209268
[startup+740.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 46553 0 0 0 73872 141 0 0 25 0 1 0 539976031 216158208 45034 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52773 45034 603 41 0 52732 0
vsize: 211092
[startup+750.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 46991 0 0 0 74872 142 0 0 25 0 1 0 539976031 218034176 45472 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53231 45472 603 41 0 53190 0
vsize: 212924
[startup+760.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 47373 0 0 0 75871 143 0 0 25 0 1 0 539976031 219529216 45854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53596 45854 603 41 0 53555 0
vsize: 214384
[startup+770.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 47695 0 0 0 76870 145 0 0 25 0 1 0 539976031 220897280 46176 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53930 46176 603 41 0 53889 0
vsize: 215720
[startup+780.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 47996 0 0 0 77867 146 0 0 25 0 1 0 539976031 222105600 46477 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54225 46477 603 41 0 54184 0
vsize: 216900
[startup+790.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 48257 0 0 0 78866 148 0 0 25 0 1 0 539976031 223211520 46738 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54495 46738 603 41 0 54454 0
vsize: 217980
[startup+800.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 48489 0 0 0 79865 149 0 0 25 0 1 0 539976031 224153600 46970 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54725 46970 603 41 0 54684 0
vsize: 218900
[startup+810.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 48683 0 0 0 80864 150 0 0 25 0 1 0 539976031 224972800 47164 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54925 47164 603 41 0 54884 0
vsize: 219700
[startup+820.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 48757 0 0 0 81864 150 0 0 25 0 1 0 539976031 225251328 47238 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54993 47238 603 41 0 54952 0
vsize: 219972
[startup+830.037 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 48799 0 0 0 82864 150 0 0 25 0 1 0 539976031 225386496 47280 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55026 47280 603 41 0 54985 0
vsize: 220104
[startup+840.038 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 48971 0 0 0 83864 150 0 0 25 0 1 0 539976031 226058240 47452 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55190 47452 603 41 0 55149 0
vsize: 220760
[startup+850.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 49074 0 0 0 84864 151 0 0 25 0 1 0 539976031 226459648 47555 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55288 47555 603 41 0 55247 0
vsize: 221152
[startup+860.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 49264 0 0 0 85864 151 0 0 25 0 1 0 539976031 227270656 47745 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55486 47745 603 41 0 55445 0
vsize: 221944
[startup+870.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 49603 0 0 0 86863 152 0 0 25 0 1 0 539976031 228614144 48084 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55814 48084 603 41 0 55773 0
vsize: 223256
[startup+880.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 49688 0 0 0 87863 152 0 0 25 0 1 0 539976031 229019648 48169 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55913 48169 603 41 0 55872 0
vsize: 223652
[startup+890.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 49893 0 0 0 88863 153 0 0 25 0 1 0 539976031 229822464 48374 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56109 48374 603 41 0 56068 0
vsize: 224436
[startup+900.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 50280 0 0 0 89861 155 0 0 25 0 1 0 539976031 231432192 48761 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56502 48761 603 41 0 56461 0
vsize: 226008
[startup+910.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 50337 0 0 0 90860 155 0 0 25 0 1 0 539976031 231571456 48818 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56536 48818 603 41 0 56495 0
vsize: 226144
[startup+920.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 50424 0 0 0 91860 156 0 0 25 0 1 0 539976031 232001536 48905 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56641 48905 603 41 0 56600 0
vsize: 226564
[startup+930.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 50643 0 0 0 92860 156 0 0 25 0 1 0 539976031 232808448 49124 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56838 49124 603 41 0 56797 0
vsize: 227352
[startup+940.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 50939 0 0 0 93859 158 0 0 25 0 1 0 539976031 234029056 49420 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57136 49420 603 41 0 57095 0
vsize: 228544
[startup+950.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 51180 0 0 0 94859 158 0 0 25 0 1 0 539976031 235089920 49661 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57395 49661 603 41 0 57354 0
vsize: 229580
[startup+960.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 51305 0 0 0 95858 158 0 0 25 0 1 0 539976031 235487232 49786 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57492 49786 603 41 0 57451 0
vsize: 229968
[startup+970.039 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 51345 0 0 0 96858 158 0 0 25 0 1 0 539976031 235622400 49826 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57525 49826 603 41 0 57484 0
vsize: 230100
[startup+980.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 51403 0 0 0 97859 158 0 0 25 0 1 0 539976031 235892736 49884 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57591 49884 603 41 0 57550 0
vsize: 230364
[startup+990.041 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 51625 0 0 0 98858 159 0 0 25 0 1 0 539976031 236834816 50106 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57821 50106 603 41 0 57780 0
vsize: 231284
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 51835 0 0 0 99858 160 0 0 25 0 1 0 539976031 237633536 50316 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58016 50316 603 41 0 57975 0
vsize: 232064
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 51859 0 0 0 100858 160 0 0 25 0 1 0 539976031 237768704 50340 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58049 50340 603 41 0 58008 0
vsize: 232196
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 51927 0 0 0 101858 160 0 0 25 0 1 0 539976031 238096384 50408 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58129 50408 603 41 0 58088 0
vsize: 232516
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 51980 0 0 0 102858 160 0 0 25 0 1 0 539976031 238387200 50461 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58200 50461 603 41 0 58159 0
vsize: 232800
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 52089 0 0 0 103857 161 0 0 25 0 1 0 539976031 238792704 50570 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58299 50570 603 41 0 58258 0
vsize: 233196
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 52175 0 0 0 104857 161 0 0 25 0 1 0 539976031 239063040 50656 4294967295 134512640 134672761 3221224544 3221223680 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58365 50656 603 41 0 58324 0
vsize: 233460
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 52339 0 0 0 105856 162 0 0 25 0 1 0 539976031 239738880 50820 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58530 50820 603 41 0 58489 0
vsize: 234120
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 52428 0 0 0 106856 163 0 0 25 0 1 0 539976031 240144384 50909 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58629 50909 603 41 0 58588 0
vsize: 234516
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 52598 0 0 0 107855 163 0 0 25 0 1 0 539976031 240812032 51079 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58792 51079 603 41 0 58751 0
vsize: 235168
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 53095 0 0 0 108854 164 0 0 25 0 1 0 539976031 242831360 51576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59285 51576 603 41 0 59244 0
vsize: 237140
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 53597 0 0 0 109853 166 0 0 25 0 1 0 539976031 244862976 52078 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59781 52078 603 41 0 59740 0
vsize: 239124
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 53998 0 0 0 110852 168 0 0 25 0 1 0 539976031 246505472 52479 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60182 52479 603 41 0 60141 0
vsize: 240728
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 54204 0 0 0 111851 168 0 0 25 0 1 0 539976031 247324672 52685 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60382 52685 603 41 0 60341 0
vsize: 241528
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 54396 0 0 0 112851 169 0 0 25 0 1 0 539976031 248184832 52877 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60592 52877 603 41 0 60551 0
vsize: 242368
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 54445 0 0 0 113851 169 0 0 25 0 1 0 539976031 248320000 52926 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60625 52926 603 41 0 60584 0
vsize: 242500
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 54950 0 0 0 114849 171 0 0 25 0 1 0 539976031 250339328 53431 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61118 53431 603 41 0 61077 0
vsize: 244472
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 55429 0 0 0 115847 173 0 0 25 0 1 0 539976031 252362752 53910 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61612 53910 603 41 0 61571 0
vsize: 246448
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 55869 0 0 0 116847 174 0 0 25 0 1 0 539976031 254111744 54350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62039 54350 603 41 0 61998 0
vsize: 248156
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 56273 0 0 0 117846 175 0 0 25 0 1 0 539976031 255737856 54754 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62436 54754 603 41 0 62395 0
vsize: 249744
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 56623 0 0 0 118845 176 0 0 25 0 1 0 539976031 257228800 55104 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62800 55104 603 41 0 62759 0
vsize: 251200
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 23996
Raw data (stat): 23996 (minisat+) R 23995 27565 27564 0 -1 0 56966 0 0 0 119844 177 0 0 25 0 1 0 539976031 258633728 55447 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63143 55447 603 41 0 63102 0
vsize: 252572
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.98 0.91 1/54 23996
Raw data (stat): 23996 (minisat+) Z 23995 27565 27564 0 -1 12 56968 0 0 0 119844 188 0 0 25 0 1 0 539976031 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.15
CPU time (s): 1200.33
CPU user time (s): 1198.44
CPU system time (s): 1.88171
CPU usage (%): 100.015
Max. virtual memory (Kb): 252572
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####