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-dc1l.opb
MD5SUM	5b92932a8bc350218da666e6f064f13f
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	68818
Biggest coefficient in the objective function	524288000000000000
Number of bits for the biggest coefficient in the objective function	59
Sum of the numbers in the objective function	6652856940207324781
Number of bits of the sum of numbers in the objective function	63
Biggest number in a constraint	524288000000000000
Number of bits of the biggest number in a constraint	59
Biggest sum of numbers in a constraint	6652856940207324781
Number of bits of the biggest sum of numbers	63
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.758884
Number of variables	68678
Total number of constraints	37291
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	35639
Number of constraints which are nor clauses,nor cardinality constraints	1652
Minimum length of a constraint	1
Maximum length of a constraint	35119
Trace number 31335

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-05-26 00:17:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22730 boxname=wulflinc15 idbench=1546 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  5b92932a8bc350218da666e6f064f13f  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-dc1l.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-dc1l.opb
IDLAUNCH: 22730
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        868848 kB
Buffers:         32636 kB
Cached:         111052 kB
SwapCached:        608 kB
Active:          39888 kB
Inactive:       105788 kB
HighTotal:      131008 kB
HighFree:        35140 kB
LowTotal:       903652 kB
LowFree:        833708 kB
SwapTotal:     2097136 kB
SwapFree:      2095624 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5084 kB
Slab:            14584 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:37:59 (client local time) WITH STATUS 152 IN 1230.44 SECONDS
stats: 22730 7 1230.44 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c PARSE ERROR! [line 37301] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 3286 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sss
c ---[3287]---> Adder-cost: 204   maxlim: 12544   bits: 15/14
c ---[3285]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[3283]---> Adder-cost: 196   maxlim: 12288   bits: 15/14
c ---[3281]---> Adder-cost: 70   maxlim: 12288   bits: 15/14
c ---[3279]---> Adder-cost: 120   maxlim: 7424   bits: 14/13
c ---[3277]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[3275]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[3273]---> Adder-cost: 162   maxlim: 10112   bits: 15/14
c ---[3271]---> Adder-cost: 366   maxlim: 28544   bits: 16/15
c ---[3269]---> Adder-cost: 280   maxlim: 29824   bits: 16/15
c ---[3267]---> Adder-cost: 1036   maxlim: 66816   bits: 18/17
c ---[3265]---> Adder-cost: 1074   maxlim: 82944   bits: 18/17
c ---[3263]---> Adder-cost: 1174   maxlim: 75392   bits: 18/17
c ---[3261]---> Adder-cost: 686   maxlim: 49408   bits: 17/16
c ---[3259]---> Adder-cost: 508   maxlim: 32640   bits: 16/15
c ---[3257]---> Adder-cost: 490   maxlim: 34688   bits: 17/16
c ---[3255]---> Adder-cost: 306   maxlim: 19968   bits: 16/15
c ---[3253]---> Adder-cost: 222   maxlim: 19968   bits: 16/15
c ---[3251]---> Adder-cost: 238   maxlim: 14976   bits: 15/14
c ---[3249]---> Adder-cost: 170   maxlim: 14592   bits: 15/14
c ---[3247]---> Adder-cost: 292   maxlim: 19968   bits: 16/15
c ---[3245]---> Adder-cost: 300   maxlim: 22656   bits: 16/15
c ---[3243]---> Adder-cost: 532   maxlim: 36608   bits: 17/16
c ---[3241]---> Adder-cost: 498   maxlim: 36736   bits: 17/16
c ---[3239]---> Adder-cost: 356   maxlim: 24960   bits: 16/15
c ---[3237]---> Adder-cost: 300   maxlim: 22016   bits: 16/15
c ---[3235]---> Adder-cost: 560   maxlim: 35584   bits: 17/16
c ---[3233]---> Adder-cost: 398   maxlim: 29184   bits: 16/15
c ---[3231]---> Adder-cost: 222   maxlim: 14720   bits: 15/14
c ---[3229]---> Adder-cost: 208   maxlim: 13568   bits: 15/14
c ---[3227]---> Adder-cost: 322   maxlim: 20864   bits: 16/15
c ---[3225]---> Adder-cost: 224   maxlim: 15744   bits: 15/14
c ---[3223]---> Adder-cost: 240   maxlim: 15488   bits: 15/14
c ---[3221]---> Adder-cost: 182   maxlim: 12288   bits: 15/14
c ---[3219]---> Adder-cost: 406   maxlim: 25728   bits: 16/15
c ---[3217]---> Adder-cost: 242   maxlim: 20352   bits: 16/15
c ---[3215]---> Adder-cost: 184   maxlim: 12672   bits: 15/14
c ---[3213]---> Adder-cost: 160   maxlim: 11776   bits: 15/14
c ---[3211]---> Adder-cost: 94   maxlim: 5888   bits: 14/13
c ---[3209]---> Adder-cost: 178   maxlim: 11008   bits: 15/14
c ---[3207]---> Adder-cost: 164   maxlim: 13056   bits: 15/14
c ---[3205]---> Adder-cost: 202   maxlim: 14080   bits: 15/14
c ---[3203]---> Adder-cost: 316   maxlim: 19840   bits: 16/15
c ---[3201]---> Adder-cost: 92   maxlim: 19840   bits: 16/15
c ---[3199]---> Adder-cost: 308   maxlim: 19712   bits: 16/15
c ---[3197]---> Adder-cost: 414   maxlim: 28672   bits: 16/15
c ---[3195]---> Adder-cost: 410   maxlim: 30080   bits: 16/15
c ---[3193]---> Adder-cost: 120   maxlim: 30080   bits: 16/15
c ---[3191]---> Adder-cost: 430   maxlim: 28032   bits: 16/15
c ---[3189]---> Adder-cost: 334   maxlim: 24064   bits: 16/15
c ---[3187]---> Adder-cost: 268   maxlim: 16512   bits: 16/15
c ---[3185]---> Adder-cost: 90   maxlim: 16512   bits: 16/15
c ---[3183]---> Adder-cost: 274   maxlim: 17408   bits: 16/15
c ---[3181]---> Adder-cost: 152   maxlim: 17408   bits: 16/15
c ---[3179]---> Adder-cost: 292   maxlim: 19200   bits: 16/15
c ---[3177]---> Adder-cost: 92   maxlim: 19200   bits: 16/15
c ---[3175]---> Adder-cost: 362   maxlim: 23424   bits: 16/15
c ---[3173]---> Adder-cost: 346   maxlim: 23168   bits: 16/15
c ---[3171]---> Adder-cost: 382   maxlim: 25216   bits: 16/15
c ---[3169]---> Adder-cost: 114   maxlim: 25216   bits: 16/15
c ---[3167]---> Adder-cost: 254   maxlim: 16128   bits: 15/14
c ---[3165]---> Adder-cost: 184   maxlim: 12544   bits: 15/14
c ---[3163]---> Adder-cost: 222   maxlim: 16640   bits: 16/15
c ---[3161]---> Adder-cost: 272   maxlim: 16768   bits: 16/15
c ---[3159]---> Adder-cost: 84   maxlim: 16768   bits: 16/15
c ---[3157]---> Adder-cost: 206   maxlim: 13440   bits: 15/14
c ---[3155]---> Adder-cost: 202   maxlim: 13312   bits: 15/14
c ---[3153]---> Adder-cost: 118   maxlim: 8960   bits: 15/14
c ---[3151]---> Adder-cost: 182   maxlim: 11264   bits: 15/14
c ---[3149]---> Adder-cost: 72   maxlim: 11264   bits: 15/14
c ---[3147]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[3145]---> Adder-cost: 412   maxlim: 25856   bits: 16/15
c ---[3143]---> Adder-cost: 114   maxlim: 25856   bits: 16/15
c ---[3141]---> Adder-cost: 166   maxlim: 10752   bits: 15/14
c ---[3139]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[3137]---> Adder-cost: 204   maxlim: 12672   bits: 15/14
c ---[3135]---> Adder-cost: 72   maxlim: 12672   bits: 15/14
c ---[3133]---> Adder-cost: 290   maxlim: 17920   bits: 16/15
c ---[3131]---> Adder-cost: 90   maxlim: 17920   bits: 16/15
c ---[3129]---> Adder-cost: 492   maxlim: 31616   bits: 16/15
c ---[3127]---> Adder-cost: 360   maxlim: 22656   bits: 16/15
c ---[3125]---> Adder-cost: 126   maxlim: 31616   bits: 16/15
c ---[3123]---> Adder-cost: 338   maxlim: 20992   bits: 16/15
c ---[3121]---> Adder-cost: 104   maxlim: 20992   bits: 16/15
c ---[3119]---> Adder-cost: 306   maxlim: 21248   bits: 16/15
c ---[3117]---> Adder-cost: 102   maxlim: 21248   bits: 16/15
c ---[3115]---> Adder-cost: 276   maxlim: 16896   bits: 16/15
c ---[3113]---> Adder-cost: 88   maxlim: 16896   bits: 16/15
c ---[3111]---> Adder-cost: 222   maxlim: 13952   bits: 15/14
c ---[3109]---> Adder-cost: 72   maxlim: 13952   bits: 15/14
c ---[3107]---> Adder-cost: 202   maxlim: 12288   bits: 15/14
c ---[3105]---> Adder-cost: 430   maxlim: 27648   bits: 16/15
c ---[3103]---> Adder-cost: 70   maxlim: 12288   bits: 15/14
c ---[3101]---> Adder-cost: 162   maxlim: 9984   bits: 15/14
c ---[3099]---> Adder-cost: 62   maxlim: 9984   bits: 15/14
c ---[3097]---> Adder-cost: 110   maxlim: 7552   bits: 14/13
c ---[3095]---> Adder-cost: 48   maxlim: 7552   bits: 14/13
c ---[3093]---> Adder-cost: 380   maxlim: 24192   bits: 16/15
c ---[3091]---> Adder-cost: 108   maxlim: 24192   bits: 16/15
c ---[3089]---> Adder-cost: 492   maxlim: 34176   bits: 17/16
c ---[3087]---> Adder-cost: 142   maxlim: 34176   bits: 17/16
c ---[3085]---> Adder-cost: 542   maxlim: 33920   bits: 17/16
c ---[3083]---> Adder-cost: 116   maxlim: 27648   bits: 16/15
c ---[3081]---> Adder-cost: 140   maxlim: 33920   bits: 17/16
c ---[3079]---> Adder-cost: 626   maxlim: 39808   bits: 17/16
c ---[3077]---> Adder-cost: 152   maxlim: 39808   bits: 17/16
c ---[3075]---> Adder-cost: 428   maxlim: 27520   bits: 16/15
c ---[3073]---> Adder-cost: 110   maxlim: 27520   bits: 16/15
c ---[3071]---> Adder-cost: 400   maxlim: 25600   bits: 16/15
c ---[3069]---> Adder-cost: 118   maxlim: 25600   bits: 16/15
c ---[3067]---> Adder-cost: 358   maxlim: 23808   bits: 16/15
c ---[3065]---> Adder-cost: 106   maxlim: 23808   bits: 16/15
c ---[3063]---> Adder-cost: 314   maxlim: 20096   bits: 16/15
c ---[3061]---> Adder-cost: 284   maxlim: 17792   bits: 16/15
c ---[3059]---> Adder-cost: 94   maxlim: 20096   bits: 16/15
c ---[3057]---> Adder-cost: 256   maxlim: 16768   bits: 16/15
c ---[3055]---> Adder-cost: 178   maxlim: 16384   bits: 16/15
c ---[3053]---> Adder-cost: 276   maxlim: 16896   bits: 16/15
c ---[3051]---> Adder-cost: 360   maxlim: 23040   bits: 16/15
c ---[3049]---> Adder-cost: 104   maxlim: 23040   bits: 16/15
c ---[3047]---> Adder-cost: 932   maxlim: 59776   bits: 17/16
c ---[3045]---> Adder-cost: 184   maxlim: 59776   bits: 17/16
c ---[3043]---> Adder-cost: 396   maxlim: 27392   bits: 16/15
c ---[3041]---> Adder-cost: 114   maxlim: 27392   bits: 16/15
c ---[3039]---> Adder-cost: 92   maxlim: 17792   bits: 16/15
c ---[3037]---> Adder-cost: 336   maxlim: 21632   bits: 16/15
c ---[3035]---> Adder-cost: 100   maxlim: 21632   bits: 16/15
c ---[3033]---> Adder-cost: 342   maxlim: 21632   bits: 16/15
c ---[3031]---> Adder-cost: 250   maxlim: 22016   bits: 16/15
c ---[3029]---> Adder-cost: 422   maxlim: 26880   bits: 16/15
c ---[3027]---> Adder-cost: 118   maxlim: 26880   bits: 16/15
c ---[3025]---> Adder-cost: 302   maxlim: 18944   bits: 16/15
c ---[3023]---> Adder-cost: 96   maxlim: 18944   bits: 16/15
c ---[3021]---> Adder-cost: 366   maxlim: 23424   bits: 16/15
c ---[3019]---> Adder-cost: 102   maxlim: 23424   bits: 16/15
c ---[3017]---> Adder-cost: 282   maxlim: 17792   bits: 16/15
c ---[3015]---> Adder-cost: 560   maxlim: 35328   bits: 17/16
c ---[3013]---> Adder-cost: 140   maxlim: 35328   bits: 17/16
c ---[3011]---> Adder-cost: 396   maxlim: 25856   bits: 16/15
c ---[3009]---> Adder-cost: 374   maxlim: 25216   bits: 16/15
c ---[3007]---> Adder-cost: 438   maxlim: 30080   bits: 16/15
c ---[3005]---> Adder-cost: 120   maxlim: 30080   bits: 16/15
c ---[3003]---> Adder-cost: 362   maxlim: 24320   bits: 16/15
c ---[3001]---> Adder-cost: 110   maxlim: 24320   bits: 16/15
c ---[2999]---> Adder-cost: 312   maxlim: 19584   bits: 16/15
c ---[2997]---> Adder-cost: 264   maxlim: 19456   bits: 16/15
c ---[2995]---> Adder-cost: 92   maxlim: 17792   bits: 16/15
c ---[2993]---> Adder-cost: 336   maxlim: 21120   bits: 16/15
c ---[2991]---> Adder-cost: 100   maxlim: 21120   bits: 16/15
c ---[2989]---> Adder-cost: 364   maxlim: 23040   bits: 16/15
c ---[2987]---> Adder-cost: 104   maxlim: 23040   bits: 16/15
c ---[2985]---> Adder-cost: 240   maxlim: 15872   bits: 15/14
c ---[2983]---> Adder-cost: 78   maxlim: 15872   bits: 15/14
c ---[2981]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[2979]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[2977]---> Adder-cost: 138   maxlim: 8320   bits: 15/14
c ---[2975]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[2973]---> Adder-cost: 252   maxlim: 19328   bits: 16/15
c ---[2971]---> Adder-cost: 154   maxlim: 9216   bits: 15/14
c ---[2969]---> Adder-cost: 62   maxlim: 9216   bits: 15/14
c ---[2967]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[2965]---> Adder-cost: 404   maxlim: 25344   bits: 16/15
c ---[2963]---> Adder-cost: 112   maxlim: 25344   bits: 16/15
c ---[2961]---> Adder-cost: 332   maxlim: 31488   bits: 16/15
c ---[2959]---> Adder-cost: 466   maxlim: 30080   bits: 16/15
c ---[2957]---> Adder-cost: 126   maxlim: 31488   bits: 16/15
c ---[2955]---> Adder-cost: 874   maxlim: 59648   bits: 17/16
c ---[2953]---> Adder-cost: 184   maxlim: 59648   bits: 17/16
c ---[2951]---> Adder-cost: 876   maxlim: 59008   bits: 17/16
c ---[2949]---> Adder-cost: 190   maxlim: 59008   bits: 17/16
c ---[2947]---> Adder-cost: 404   maxlim: 29952   bits: 16/15
c ---[2945]---> Adder-cost: 1208   maxlim: 82944   bits: 18/17
c ---[2943]---> Adder-cost: 234   maxlim: 82944   bits: 18/17
c ---[2941]---> Adder-cost: 1068   maxlim: 75904   bits: 18/17
c ---[2939]---> Adder-cost: 230   maxlim: 75904   bits: 18/17
c ---[2937]---> Adder-cost: 1664   maxlim: 113280   bits: 18/17
c ---[2935]---> Adder-cost: 288   maxlim: 22272   bits: 16/15
c ---[2933]---> Adder-cost: 282   maxlim: 113280   bits: 18/17
c ---[2931]---> Adder-cost: 1996   maxlim: 136064   bits: 19/18
c ---[2929]---> Adder-cost: 1880   maxlim: 133888   bits: 19/18
c ---[2927]---> Adder-cost: 1680   maxlim: 116864   bits: 18/17
c ---[2925]---> Adder-cost: 1552   maxlim: 106368   bits: 18/17
c ---[2923]---> Adder-cost: 102   maxlim: 22272   bits: 16/15
c ---[2921]---> Adder-cost: 1408   maxlim: 103552   bits: 18/17
c ---[2919]---> Adder-cost: 1240   maxlim: 88320   bits: 18/17
c ---[2917]---> Adder-cost: 964   maxlim: 66560   bits: 18/17
c ---[2915]---> Adder-cost: 1018   maxlim: 69376   bits: 18/17
c ---[2913]---> Adder-cost: 210   maxlim: 69376   bits: 18/17
c ---[2911]---> Adder-cost: 886   maxlim: 62464   bits: 17/16
c ---[2909]---> Adder-cost: 424   maxlim: 26624   bits: 16/15
c ---[2907]---> Adder-cost: 198   maxlim: 62464   bits: 17/16
c ---[2905]---> Adder-cost: 1086   maxlim: 75008   bits: 18/17
c ---[2903]---> Adder-cost: 230   maxlim: 75008   bits: 18/17
c ---[2901]---> Adder-cost: 1218   maxlim: 82304   bits: 18/17
c ---[2899]---> Adder-cost: 240   maxlim: 82304   bits: 18/17
c ---[2897]---> Adder-cost: 1304   maxlim: 88448   bits: 18/17
c ---[2895]---> Adder-cost: 1014   maxlim: 69376   bits: 18/17
c ---[2893]---> Adder-cost: 210   maxlim: 69376   bits: 18/17
c ---[2891]---> Adder-cost: 122   maxlim: 26624   bits: 16/15
c ---[2889]---> Adder-cost: 698   maxlim: 46080   bits: 17/16
c ---[2887]---> Adder-cost: 160   maxlim: 46080   bits: 17/16
c ---[2885]---> Adder-cost: 718   maxlim: 51072   bits: 17/16
c ---[2883]---> Adder-cost: 170   maxlim: 51072   bits: 17/16
c ---[2881]---> Adder-cost: 636   maxlim: 42624   bits: 17/16
c ---[2879]---> Adder-cost: 350   maxlim: 23040   bits: 16/15
c ---[2877]---> Adder-cost: 152   maxlim: 42624   bits: 17/16
c ---[2875]---> Adder-cost: 716   maxlim: 49280   bits: 17/16
c ---[2873]---> Adder-cost: 166   maxlim: 49280   bits: 17/16
c ---[2871]---> Adder-cost: 612   maxlim: 42496   bits: 17/16
c ---[2869]---> Adder-cost: 154   maxlim: 42496   bits: 17/16
c ---[2867]---> Adder-cost: 264   maxlim: 19328   bits: 16/15
c ---[2865]---> Adder-cost: 104   maxlim: 23040   bits: 16/15
c ---[2863]---> Adder-cost: 92   maxlim: 19328   bits: 16/15
c ---[2861]---> Adder-cost: 190   maxlim: 13184   bits: 15/14
c ---[2859]---> Adder-cost: 74   maxlim: 13184   bits: 15/14
c ---[2857]---> Adder-cost: 82   maxlim: 5632   bits: 14/13
c ---[2855]---> Adder-cost: 348   maxlim: 21760   bits: 16/15
c ---[2853]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[2851]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[2849]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[2847]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[2845]---> Adder-cost: 844   maxlim: 54528   bits: 17/16
c ---[2843]---> Adder-cost: 770   maxlim: 55936   bits: 17/16
c ---[2841]---> Adder-cost: 546   maxlim: 37760   bits: 17/16
c ---[2839]---> Adder-cost: 304   maxlim: 25856   bits: 16/15
c ---[2837]---> Adder-cost: 106   maxlim: 21760   bits: 16/15
c ---[2835]---> Adder-cost: 472   maxlim: 31360   bits: 16/15
c ---[2833]---> Adder-cost: 466   maxlim: 34176   bits: 17/16
c ---[2831]---> Adder-cost: 520   maxlim: 35712   bits: 17/16
c ---[2829]---> Adder-cost: 568   maxlim: 39040   bits: 17/16
c ---[2827]---> Adder-cost: 562   maxlim: 36352   bits: 17/16
c ---[2825]---> Adder-cost: 436   maxlim: 35200   bits: 17/16
c ---[2823]---> Adder-cost: 278   maxlim: 17792   bits: 16/15
c ---[2821]---> Adder-cost: 220   maxlim: 14976   bits: 15/14
c ---[2819]---> Adder-cost: 284   maxlim: 17664   bits: 16/15
c ---[2817]---> Adder-cost: 284   maxlim: 19712   bits: 16/15
c ---[2815]---> Adder-cost: 388   maxlim: 25088   bits: 16/15
c ---[2813]---> Adder-cost: 408   maxlim: 28416   bits: 16/15
c ---[2811]---> Adder-cost: 414   maxlim: 27904   bits: 16/15
c ---[2809]---> Adder-cost: 614   maxlim: 40576   bits: 17/16
c ---[2807]---> Adder-cost: 750   maxlim: 56704   bits: 17/16
c ---[2805]---> Adder-cost: 676   maxlim: 47104   bits: 17/16
c ---[2803]---> Adder-cost: 394   maxlim: 30848   bits: 16/15
c ---[2801]---> Adder-cost: 526   maxlim: 32768   bits: 17/16
c ---[2799]---> Adder-cost: 434   maxlim: 30208   bits: 16/15
c ---[2797]---> Adder-cost: 396   maxlim: 25728   bits: 16/15
c ---[2795]---> Adder-cost: 414   maxlim: 27776   bits: 16/15
c ---[2793]---> Adder-cost: 116   maxlim: 25088   bits: 16/15
c ---[2791]---> Adder-cost: 340   maxlim: 22272   bits: 16/15
c ---[2789]---> Adder-cost: 252   maxlim: 18176   bits: 16/15
c ---[2787]---> Adder-cost: 216   maxlim: 13696   bits: 15/14
c ---[2785]---> Adder-cost: 204   maxlim: 15104   bits: 15/14
c ---[2783]---> Adder-cost: 278   maxlim: 18432   bits: 16/15
c ---[2781]---> Adder-cost: 94   maxlim: 11520   bits: 15/14
c ---[2779]---> Adder-cost: 396   maxlim: 24960   bits: 16/15
c ---[2777]---> Adder-cost: 114   maxlim: 24960   bits: 16/15
c ---[2775]---> Adder-cost: 516   maxlim: 33024   bits: 17/16
c ---[2773]---> Adder-cost: 138   maxlim: 33024   bits: 17/16
c ---[2771]---> Adder-cost: 362   maxlim: 22784   bits: 16/15
c ---[2769]---> Adder-cost: 376   maxlim: 24832   bits: 16/15
c ---[2767]---> Adder-cost: 116   maxlim: 24832   bits: 16/15
c ---[2765]---> Adder-cost: 334   maxlim: 21376   bits: 16/15
c ---[2763]---> Adder-cost: 100   maxlim: 21376   bits: 16/15
c ---[2761]---> Adder-cost: 396   maxlim: 25472   bits: 16/15
c ---[2759]---> Adder-cost: 110   maxlim: 25472   bits: 16/15
c ---[2757]---> Adder-cost: 402   maxlim: 25472   bits: 16/15
c ---[2755]---> Adder-cost: 354   maxlim: 25984   bits: 16/15
c ---[2753]---> Adder-cost: 372   maxlim: 23808   bits: 16/15
c ---[2751]---> Adder-cost: 106   maxlim: 23808   bits: 16/15
c ---[2749]---> Adder-cost: 106   maxlim: 22784   bits: 16/15
c ---[2747]---> Adder-cost: 330   maxlim: 20992   bits: 16/15
c ---[2745]---> Adder-cost: 104   maxlim: 20992   bits: 16/15
c ---[2743]---> Adder-cost: 280   maxlim: 17664   bits: 16/15
c ---[2741]---> Adder-cost: 264   maxlim: 17408   bits: 16/15
c ---[2739]---> Adder-cost: 344   maxlim: 22528   bits: 16/15
c ---[2737]---> Adder-cost: 110   maxlim: 22528   bits: 16/15
c ---[2735]---> Adder-cost: 262   maxlim: 16512   bits: 16/15
c ---[2733]---> Adder-cost: 90   maxlim: 16512   bits: 16/15
c ---[2731]---> Adder-cost: 226   maxlim: 15232   bits: 15/14
c ---[2729]---> Adder-cost: 80   maxlim: 15232   bits: 15/14
c ---[2727]---> Adder-cost: 330   maxlim: 20992   bits: 16/15
c ---[2725]---> Adder-cost: 466   maxlim: 29440   bits: 16/15
c ---[2723]---> Adder-cost: 126   maxlim: 29440   bits: 16/15
c ---[2721]---> Adder-cost: 332   maxlim: 20736   bits: 16/15
c ---[2719]---> Adder-cost: 188   maxlim: 19584   bits: 16/15
c ---[2717]---> Adder-cost: 184   maxlim: 11264   bits: 15/14
c ---[2715]---> Adder-cost: 72   maxlim: 11264   bits: 15/14
c ---[2713]---> Adder-cost: 192   maxlim: 12032   bits: 15/14
c ---[2711]---> Adder-cost: 68   maxlim: 12032   bits: 15/14
c ---[2709]---> Adder-cost: 208   maxlim: 13184   bits: 15/14
c ---[2707]---> Adder-cost: 74   maxlim: 13184   bits: 15/14
c ---[2705]---> Adder-cost: 104   maxlim: 20992   bits: 16/15
c ---[2703]---> Adder-cost: 228   maxlim: 15104   bits: 15/14
c ---[2701]---> Adder-cost: 80   maxlim: 15104   bits: 15/14
c ---[2699]---> Adder-cost: 124   maxlim: 8064   bits: 14/13
c ---[2697]---> Adder-cost: 50   maxlim: 8064   bits: 14/13
c ---[2695]---> Adder-cost: 98   maxlim: 6144   bits: 14/13
c ---[2693]---> Adder-cost: 84   maxlim: 5888   bits: 14/13
c ---[2691]---> Adder-cost: 214   maxlim: 13824   bits: 15/14
c ---[2689]---> Adder-cost: 236   maxlim: 16128   bits: 15/14
c ---[2687]---> Adder-cost: 76   maxlim: 16128   bits: 15/14
c ---[2685]---> Adder-cost: 172   maxlim: 10496   bits: 15/14
c ---[2683]---> Adder-cost: 262   maxlim: 18048   bits: 16/15
c ---[2681]---> Adder-cost: 68   maxlim: 10496   bits: 15/14
c ---[2679]---> Adder-cost: 224   maxlim: 14464   bits: 15/14
c ---[2677]---> Adder-cost: 76   maxlim: 14464   bits: 15/14
c ---[2675]---> Adder-cost: 434   maxlim: 28032   bits: 16/15
c ---[2673]---> Adder-cost: 114   maxlim: 28032   bits: 16/15
c ---[2671]---> Adder-cost: 358   maxlim: 23296   bits: 16/15
c ---[2669]---> Adder-cost: 106   maxlim: 23296   bits: 16/15
c ---[2667]---> Adder-cost: 310   maxlim: 19712   bits: 16/15
c ---[2665]---> Adder-cost: 92   maxlim: 19712   bits: 16/15
c ---[2663]---> Adder-cost: 340   maxlim: 21632   bits: 16/15
c ---[2661]---> Adder-cost: 90   maxlim: 18048   bits: 16/15
c ---[2659]---> Adder-cost: 100   maxlim: 21632   bits: 16/15
c ---[2657]---> Adder-cost: 150   maxlim: 9472   bits: 15/14
c ---[2655]---> Adder-cost: 136   maxlim: 9344   bits: 15/14
c ---[2653]---> Adder-cost: 156   maxlim: 9472   bits: 15/14
c ---[2651]---> Adder-cost: 64   maxlim: 9472   bits: 15/14
c ---[2649]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[2647]---> Adder-cost: 272   maxlim: 16640   bits: 16/15
c ---[2645]---> Adder-cost: 244   maxlim: 21248   bits: 16/15
c ---[2643]---> Adder-cost: 102   maxlim: 21248   bits: 16/15
c ---[2641]---> Adder-cost: 372   maxlim: 23936   bits: 16/15
c ---[2639]---> Adder-cost: 204   maxlim: 13056   bits: 15/14
c ---[2637]---> Adder-cost: 104   maxlim: 23936   bits: 16/15
c ---[2635]---> Adder-cost: 312   maxlim: 20096   bits: 16/15
c ---[2633]---> Adder-cost: 94   maxlim: 20096   bits: 16/15
c ---[2631]---> Adder-cost: 610   maxlim: 39552   bits: 17/16
c ---[2629]---> Adder-cost: 154   maxlim: 39552   bits: 17/16
c ---[2627]---> Adder-cost: 516   maxlim: 32896   bits: 17/16
c ---[2625]---> Adder-cost: 138   maxlim: 32896   bits: 17/16
c ---[2623]---> Adder-cost: 382   maxlim: 24832   bits: 16/15
c ---[2621]---> Adder-cost: 116   maxlim: 24832   bits: 16/15
c ---[2619]---> Adder-cost: 270   maxlim: 17792   bits: 16/15
c ---[2617]---> Adder-cost: 124   maxlim: 8960   bits: 15/14
c ---[2615]---> Adder-cost: 92   maxlim: 17792   bits: 16/15
c ---[2613]---> Adder-cost: 360   maxlim: 22656   bits: 16/15
c ---[2611]---> Adder-cost: 106   maxlim: 22656   bits: 16/15
c ---[2609]---> Adder-cost: 532   maxlim: 35072   bits: 17/16
c ---[2607]---> Adder-cost: 136   maxlim: 35072   bits: 17/16
c ---[2605]---> Adder-cost: 374   maxlim: 24576   bits: 16/15
c ---[2603]---> Adder-cost: 114   maxlim: 24576   bits: 16/15
c ---[2601]---> Adder-cost: 384   maxlim: 24320   bits: 16/15
c ---[2599]---> Adder-cost: 110   maxlim: 24320   bits: 16/15
c ---[2597]---> Adder-cost: 222   maxlim: 14208   bits: 15/14
c ---[2595]---> Adder-cost: 364   maxlim: 23168   bits: 16/15
c ---[2593]---> Adder-cost: 72   maxlim: 14208   bits: 15/14
c ---[2591]---> Adder-cost: 174   maxlim: 10880   bits: 15/14
c ---[2589]---> Adder-cost: 66   maxlim: 10880   bits: 15/14
c ---[2587]---> Adder-cost: 290   maxlim: 18176   bits: 16/15
c ---[2585]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[2583]---> Adder-cost: 144   maxlim: 9344   bits: 15/14
c ---[2581]---> Adder-cost: 60   maxlim: 9344   bits: 15/14
c ---[2579]---> Adder-cost: 240   maxlim: 15104   bits: 15/14
c ---[2577]---> Adder-cost: 200   maxlim: 14976   bits: 15/14
c ---[2575]---> Adder-cost: 160   maxlim: 10624   bits: 15/14
c ---[2573]---> Adder-cost: 394   maxlim: 24832   bits: 16/15
c ---[2571]---> Adder-cost: 256   maxlim: 28032   bits: 16/15
c ---[2569]---> Adder-cost: 114   maxlim: 28032   bits: 16/15
c ---[2567]---> Adder-cost: 286   maxlim: 18688   bits: 16/15
c ---[2565]---> Adder-cost: 290   maxlim: 21120   bits: 16/15
c ---[2563]---> Adder-cost: 340   maxlim: 21504   bits: 16/15
c ---[2561]---> Adder-cost: 102   maxlim: 21504   bits: 16/15
c ---[2559]---> Adder-cost: 352   maxlim: 23168   bits: 16/15
c ---[2557]---> Adder-cost: 248   maxlim: 19328   bits: 16/15
c ---[2555]---> Adder-cost: 208   maxlim: 12928   bits: 15/14
c ---[2553]---> Adder-cost: 76   maxlim: 12928   bits: 15/14
c ---[2551]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2549]---> Adder-cost: 558   maxlim: 35200   bits: 17/16
c ---[2547]---> Adder-cost: 384   maxlim: 33152   bits: 17/16
c ---[2545]---> Adder-cost: 426   maxlim: 29056   bits: 16/15
c ---[2543]---> Adder-cost: 124   maxlim: 29056   bits: 16/15
c ---[2541]---> Adder-cost: 236   maxlim: 15232   bits: 15/14
c ---[2539]---> Adder-cost: 180   maxlim: 11776   bits: 15/14
c ---[2537]---> Adder-cost: 250   maxlim: 16000   bits: 15/14
c ---[2535]---> Adder-cost: 78   maxlim: 16000   bits: 15/14
c ---[2533]---> Adder-cost: 274   maxlim: 17280   bits: 16/15
c ---[2531]---> Adder-cost: 134   maxlim: 11136   bits: 15/14
c ---[2529]---> Adder-cost: 172   maxlim: 10752   bits: 15/14
c ---[2527]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[2525]---> Adder-cost: 120   maxlim: 7808   bits: 14/13
c ---[2523]---> Adder-cost: 76   maxlim: 4864   bits: 14/13
c ---[2521]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[2519]---> Adder-cost: 102   maxlim: 23168   bits: 16/15
c ---[2517]---> Adder-cost: 228   maxlim: 14464   bits: 15/14
c ---[2515]---> Adder-cost: 160   maxlim: 14848   bits: 15/14
c ---[2513]---> Adder-cost: 80   maxlim: 14848   bits: 15/14
c ---[2511]---> Adder-cost: 136   maxlim: 8192   bits: 15/14
c ---[2509]---> Adder-cost: 62   maxlim: 8192   bits: 15/14
c ---[2507]---> Adder-cost: 288   maxlim: 18176   bits: 16/15
c ---[2505]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[2503]---> Adder-cost: 312   maxlim: 19584   bits: 16/15
c ---[2501]---> Adder-cost: 96   maxlim: 19584   bits: 16/15
c ---[2499]---> Adder-cost: 288   maxlim: 18944   bits: 16/15
c ---[2497]---> Adder-cost: 214   maxlim: 13440   bits: 15/14
c ---[2495]---> Adder-cost: 78   maxlim: 13440   bits: 15/14
c ---[2493]---> Adder-cost: 208   maxlim: 13056   bits: 15/14
c ---[2491]---> Adder-cost: 74   maxlim: 13056   bits: 15/14
c ---[2489]---> Adder-cost: 234   maxlim: 14720   bits: 15/14
c ---[2487]---> Adder-cost: 76   maxlim: 14720   bits: 15/14
c ---[2485]---> Adder-cost: 222   maxlim: 13952   bits: 15/14
c ---[2483]---> Adder-cost: 72   maxlim: 13952   bits: 15/14
c ---[2481]---> Adder-cost: 248   maxlim: 15872   bits: 15/14
c ---[2479]---> Adder-cost: 78   maxlim: 15872   bits: 15/14
c ---[2477]---> Adder-cost: 242   maxlim: 21120   bits: 16/15
c ---[2475]---> Adder-cost: 170   maxlim: 10240   bits: 15/14
c ---[2473]---> Adder-cost: 68   maxlim: 10240   bits: 15/14
c ---[2471]---> Adder-cost: 136   maxlim: 8320   bits: 15/14
c ---[2469]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[2467]---> Adder-cost: 244   maxlim: 15360   bits: 15/14
c ---[2465]---> Adder-cost: 286   maxlim: 21248   bits: 16/15
c ---[2463]---> Adder-cost: 102   maxlim: 21248   bits: 16/15
c ---[2461]---> Adder-cost: 604   maxlim: 39808   bits: 17/16
c ---[2459]---> Adder-cost: 152   maxlim: 39808   bits: 17/16
c ---[2457]---> Adder-cost: 222   maxlim: 13824   bits: 15/14
c ---[2455]---> Adder-cost: 74   maxlim: 13824   bits: 15/14
c ---[2453]---> Adder-cost: 328   maxlim: 20480   bits: 16/15
c ---[2451]---> Adder-cost: 102   maxlim: 20480   bits: 16/15
c ---[2449]---> Adder-cost: 246   maxlim: 15360   bits: 15/14
c ---[2447]---> Adder-cost: 80   maxlim: 15360   bits: 15/14
c ---[2445]---> Adder-cost: 262   maxlim: 17536   bits: 16/15
c ---[2443]---> Adder-cost: 94   maxlim: 17536   bits: 16/15
c ---[2441]---> Adder-cost: 224   maxlim: 14080   bits: 15/14
c ---[2439]---> Adder-cost: 74   maxlim: 14080   bits: 15/14
c ---[2437]---> Adder-cost: 252   maxlim: 15872   bits: 15/14
c ---[2435]---> Adder-cost: 78   maxlim: 15872   bits: 15/14
c ---[2433]---> Adder-cost: 146   maxlim: 8960   bits: 15/14
c ---[2431]---> Adder-cost: 60   maxlim: 8960   bits: 15/14
c ---[2429]---> Adder-cost: 118   maxlim: 7424   bits: 14/13
c ---[2427]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[2425]---> Adder-cost: 218   maxlim: 13568   bits: 15/14
c ---[2423]---> Adder-cost: 412   maxlim: 31488   bits: 16/15
c ---[2421]---> Adder-cost: 126   maxlim: 31488   bits: 16/15
c ---[2419]---> Adder-cost: 642   maxlim: 40704   bits: 17/16
c ---[2417]---> Adder-cost: 654   maxlim: 44032   bits: 17/16
c ---[2415]---> Adder-cost: 508   maxlim: 35584   bits: 17/16
c ---[2413]---> Adder-cost: 672   maxlim: 47616   bits: 17/16
c ---[2411]---> Adder-cost: 552   maxlim: 34816   bits: 17/16
c ---[2409]---> Adder-cost: 326   maxlim: 34048   bits: 17/16
c ---[2407]---> Adder-cost: 418   maxlim: 27648   bits: 16/15
c ---[2405]---> Adder-cost: 312   maxlim: 22272   bits: 16/15
c ---[2403]---> Adder-cost: 288   maxlim: 19328   bits: 16/15
c ---[2401]---> Adder-cost: 306   maxlim: 20864   bits: 16/15
c ---[2399]---> Adder-cost: 100   maxlim: 21120   bits: 16/15
c ---[2397]---> Adder-cost: 864   maxlim: 55296   bits: 17/16
c ---[2395]---> Adder-cost: 610   maxlim: 60288   bits: 17/16
c ---[2393]---> Adder-cost: 820   maxlim: 57856   bits: 17/16
c ---[2391]---> Adder-cost: 846   maxlim: 57344   bits: 17/16
c ---[2389]---> Adder-cost: 490   maxlim: 33664   bits: 17/16
c ---[2387]---> Adder-cost: 312   maxlim: 20736   bits: 16/15
c ---[2385]---> Adder-cost: 654   maxlim: 42752   bits: 17/16
c ---[2383]---> Adder-cost: 664   maxlim: 43008   bits: 17/16
c ---[2381]---> Adder-cost: 566   maxlim: 36864   bits: 17/16
c ---[2379]---> Adder-cost: 482   maxlim: 36096   bits: 17/16
c ---[2377]---> Adder-cost: 1092   maxlim: 72064   bits: 18/17
c ---[2375]---> Adder-cost: 408   maxlim: 26880   bits: 16/15
c ---[2373]---> Adder-cost: 330   maxlim: 22528   bits: 16/15
c ---[2371]---> Adder-cost: 322   maxlim: 22656   bits: 16/15
c ---[2369]---> Adder-cost: 234   maxlim: 16640   bits: 16/15
c ---[2367]---> Adder-cost: 356   maxlim: 23296   bits: 16/15
c ---[2365]---> Adder-cost: 236   maxlim: 16640   bits: 16/15
c ---[2363]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[2361]---> Sorter-cost:  567     Base: 2 2 2 2 2 2 2 7
c ---[2359]---> Adder-cost: 104   maxlim: 6528   bits: 14/13
c ---[2357]---> Adder-cost: 210   maxlim: 13184   bits: 15/14
c ---[2355]---> Adder-cost: 634   maxlim: 72192   bits: 18/17
c ---[2353]---> Adder-cost: 270   maxlim: 18304   bits: 16/15
c ---[2351]---> Adder-cost: 252   maxlim: 20992   bits: 16/15
c ---[2349]---> Adder-cost: 276   maxlim: 17280   bits: 16/15
c ---[2347]---> Adder-cost: 88   maxlim: 17280   bits: 16/15
c ---[2345]---> Adder-cost: 412   maxlim: 25984   bits: 16/15
c ---[2343]---> Adder-cost: 464   maxlim: 30720   bits: 16/15
c ---[2341]---> Adder-cost: 372   maxlim: 24704   bits: 16/15
c ---[2339]---> Adder-cost: 112   maxlim: 24704   bits: 16/15
c ---[2337]---> Adder-cost: 378   maxlim: 24448   bits: 16/15
c ---[2335]---> Adder-cost: 338   maxlim: 24704   bits: 16/15
c ---[2333]---> Adder-cost: 262   maxlim: 17024   bits: 16/15
c ---[2331]---> Adder-cost: 88   maxlim: 17024   bits: 16/15
c ---[2329]---> Adder-cost: 284   maxlim: 18048   bits: 16/15
c ---[2327]---> Adder-cost: 100   maxlim: 14592   bits: 15/14
c ---[2325]---> Adder-cost: 118   maxlim: 7168   bits: 14/13
c ---[2323]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[2321]---> Adder-cost: 240   maxlim: 15104   bits: 15/14
c ---[2319]---> Adder-cost: 304   maxlim: 19200   bits: 16/15
c ---[2317]---> Adder-cost: 280   maxlim: 17792   bits: 16/15
c ---[2315]---> Adder-cost: 92   maxlim: 17792   bits: 16/15
c ---[2313]---> Adder-cost: 358   maxlim: 22656   bits: 16/15
c ---[2311]---> Adder-cost: 224   maxlim: 15488   bits: 15/14
c ---[2309]---> Adder-cost: 188   maxlim: 12160   bits: 15/14
c ---[2307]---> Adder-cost: 64   maxlim: 12160   bits: 15/14
c ---[2305]---> Adder-cost: 270   maxlim: 16768   bits: 16/15
c ---[2303]---> Adder-cost: 222   maxlim: 14720   bits: 15/14
c ---[2301]---> Adder-cost: 154   maxlim: 10496   bits: 15/14
c ---[2299]---> Adder-cost: 134   maxlim: 10368   bits: 15/14
c ---[2297]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[2295]---> Adder-cost: 252   maxlim: 15872   bits: 15/14
c ---[2293]---> Adder-cost: 148   maxlim: 17024   bits: 16/15
c ---[2291]---> Adder-cost: 300   maxlim: 21376   bits: 16/15
c ---[2289]---> Adder-cost: 308   maxlim: 20864   bits: 16/15
c ---[2287]---> Adder-cost: 376   maxlim: 24320   bits: 16/15
c ---[2285]---> Adder-cost: 406   maxlim: 28032   bits: 16/15
c ---[2283]---> Adder-cost: 418   maxlim: 27264   bits: 16/15
c ---[2281]---> Adder-cost: 506   maxlim: 35584   bits: 17/16
c ---[2279]---> Adder-cost: 376   maxlim: 23808   bits: 16/15
c ---[2277]---> Adder-cost: 346   maxlim: 26880   bits: 16/15
c ---[2275]---> Adder-cost: 290   maxlim: 18304   bits: 16/15
c ---[2273]---> Adder-cost: 218   maxlim: 72192   bits: 18/17
c ---[2271]---> Adder-cost: 268   maxlim: 16896   bits: 16/15
c ---[2269]---> Adder-cost: 456   maxlim: 28928   bits: 16/15
c ---[2267]---> Adder-cost: 412   maxlim: 26880   bits: 16/15
c ---[2265]---> Adder-cost: 454   maxlim: 32384   bits: 16/15
c ---[2263]---> Adder-cost: 480   maxlim: 35200   bits: 17/16
c ---[2261]---> Adder-cost: 410   maxlim: 26368   bits: 16/15
c ---[2259]---> Adder-cost: 302   maxlim: 25472   bits: 16/15
c ---[2257]---> Adder-cost: 302   maxlim: 21376   bits: 16/15
c ---[2255]---> Adder-cost: 208   maxlim: 14592   bits: 15/14
c ---[2253]---> Adder-cost: 1136   maxlim: 87680   bits: 18/17
c ---[2251]---> Sorter-cost:  689     Base: 2 2 2 2 2 2 2 7
c ---[2249]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2247]---> Adder-cost: 124   maxlim: 7808   bits: 14/13
c ---[2245]---> Adder-cost: 166   maxlim: 11008   bits: 15/14
c ---[2243]---> Adder-cost: 366   maxlim: 24320   bits: 16/15
c ---[2241]---> Adder-cost: 284   maxlim: 19584   bits: 16/15
c ---[2239]---> Adder-cost: 194   maxlim: 14080   bits: 15/14
c ---[2237]---> Adder-cost: 194   maxlim: 13696   bits: 15/14
c ---[2235]---> Adder-cost: 204   maxlim: 13952   bits: 15/14
c ---[2233]---> Adder-cost: 106   maxlim: 8960   bits: 15/14
c ---[2231]---> Adder-cost: 242   maxlim: 87680   bits: 18/17
c ---[2229]---> Adder-cost: 216   maxlim: 13440   bits: 15/14
c ---[2227]---> Adder-cost: 78   maxlim: 13440   bits: 15/14
c ---[2225]---> Adder-cost: 220   maxlim: 14976   bits: 15/14
c ---[2223]---> Adder-cost: 80   maxlim: 14976   bits: 15/14
c ---[2221]---> Adder-cost: 288   maxlim: 18048   bits: 16/15
c ---[2219]---> Adder-cost: 90   maxlim: 18048   bits: 16/15
c ---[2217]---> Adder-cost: 348   maxlim: 22912   bits: 16/15
c ---[2215]---> Adder-cost: 104   maxlim: 22912   bits: 16/15
c ---[2213]---> Adder-cost: 428   maxlim: 27392   bits: 16/15
c ---[2211]---> Adder-cost: 114   maxlim: 27392   bits: 16/15
c ---[2209]---> Adder-cost: 242   maxlim: 87680   bits: 18/17
c ---[2207]---> Adder-cost: 420   maxlim: 27264   bits: 16/15
c ---[2205]---> Adder-cost: 396   maxlim: 27776   bits: 16/15
c ---[2203]---> Adder-cost: 492   maxlim: 32128   bits: 16/15
c ---[2201]---> Adder-cost: 132   maxlim: 32128   bits: 16/15
c ---[2199]---> Adder-cost: 362   maxlim: 23808   bits: 16/15
c ---[2197]---> Adder-cost: 106   maxlim: 23808   bits: 16/15
c ---[2195]---> Adder-cost: 954   maxlim: 63104   bits: 17/16
c ---[2193]---> Adder-cost: 190   maxlim: 63104   bits: 17/16
c ---[2191]---> Adder-cost: 536   maxlim: 34688   bits: 17/16
c ---[2189]---> Adder-cost: 136   maxlim: 34688   bits: 17/16
c ---[2187]---> Adder-cost: 242   maxlim: 87680   bits: 18/17
c ---[2185]---> Adder-cost: 694   maxlim: 44544   bits: 17/16
c ---[2183]---> Adder-cost: 156   maxlim: 44544   bits: 17/16
c ---[2181]---> Adder-cost: 668   maxlim: 42752   bits: 17/16
c ---[2179]---> Adder-cost: 152   maxlim: 42752   bits: 17/16
c ---[2177]---> Adder-cost: 544   maxlim: 34304   bits: 17/16
c ---[2175]---> Adder-cost: 148   maxlim: 34304   bits: 17/16
c ---[2173]---> Adder-cost: 376   maxlim: 24320   bits: 16/15
c ---[2171]---> Adder-cost: 282   maxlim: 21632   bits: 16/15
c ---[2169]---> Adder-cost: 292   maxlim: 19072   bits: 16/15
c ---[2167]---> Adder-cost: 94   maxlim: 19072   bits: 16/15
c ---[2165]---> Adder-cost: 242   maxlim: 87680   bits: 18/17
c ---[2163]---> Adder-cost: 118   maxlim: 7808   bits: 14/13
c ---[2161]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[2159]---> Sorter-cost:  730     Base: 2 2 2 2 2 2 2 7
c ---[2157]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2155]---> Adder-cost: 206   maxlim: 12800   bits: 15/14
c ---[2153]---> Adder-cost: 76   maxlim: 12800   bits: 15/14
c ---[2151]---> Adder-cost: 144   maxlim: 10752   bits: 15/14
c ---[2149]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[2147]---> Adder-cost: 154   maxlim: 9344   bits: 15/14
c ---[2145]---> Adder-cost: 182   maxlim: 12800   bits: 15/14
c ---[2143]---> Adder-cost: 242   maxlim: 87680   bits: 18/17
c ---[2141]---> Adder-cost: 76   maxlim: 12800   bits: 15/14
c ---[2139]---> Adder-cost: 214   maxlim: 14720   bits: 15/14
c ---[2137]---> Adder-cost: 76   maxlim: 14720   bits: 15/14
c ---[2135]---> Adder-cost: 310   maxlim: 19968   bits: 16/15
c ---[2133]---> Adder-cost: 94   maxlim: 19968   bits: 16/15
c ---[2131]---> Adder-cost: 442   maxlim: 29312   bits: 16/15
c ---[2129]---> Adder-cost: 120   maxlim: 29312   bits: 16/15
c ---[2127]---> Adder-cost: 344   maxlim: 22400   bits: 16/15
c ---[2125]---> Adder-cost: 100   maxlim: 22400   bits: 16/15
c ---[2123]---> Adder-cost: 418   maxlim: 27264   bits: 16/15
c ---[2121]---> Adder-cost: 502   maxlim: 33664   bits: 17/16
c ---[2119]---> Adder-cost: 116   maxlim: 27264   bits: 16/15
c ---[2117]---> Adder-cost: 500   maxlim: 32256   bits: 16/15
c ---[2115]---> Adder-cost: 126   maxlim: 32256   bits: 16/15
c ---[2113]---> Adder-cost: 322   maxlim: 24448   bits: 16/15
c ---[2111]---> Adder-cost: 108   maxlim: 24448   bits: 16/15
c ---[2109]---> Adder-cost: 168   maxlim: 10240   bits: 15/14
c ---[2107]---> Adder-cost: 110   maxlim: 10624   bits: 15/14
c ---[2105]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[2103]---> Adder-cost: 200   maxlim: 12288   bits: 15/14
c ---[2101]---> Adder-cost: 70   maxlim: 12288   bits: 15/14
c ---[2099]---> Adder-cost: 144   maxlim: 33664   bits: 17/16
c ---[2097]---> Adder-cost: 250   maxlim: 16128   bits: 15/14
c ---[2095]---> Adder-cost: 76   maxlim: 16128   bits: 15/14
c ---[2093]---> Adder-cost: 332   maxlim: 20608   bits: 16/15
c ---[2091]---> Adder-cost: 100   maxlim: 20608   bits: 16/15
c ---[2089]---> Adder-cost: 566   maxlim: 36480   bits: 17/16
c ---[2087]---> Adder-cost: 146   maxlim: 36480   bits: 17/16
c ---[2085]---> Adder-cost: 396   maxlim: 26368   bits: 16/15
c ---[2083]---> Adder-cost: 262   maxlim: 25600   bits: 16/15
c ---[2081]---> Adder-cost: 432   maxlim: 27520   bits: 16/15
c ---[2079]---> Adder-cost: 110   maxlim: 27520   bits: 16/15
c ---[2077]---> Adder-cost: 144   maxlim: 33664   bits: 17/16
c ---[2075]---> Adder-cost: 206   maxlim: 12928   bits: 15/14
c ---[2073]---> Adder-cost: 76   maxlim: 12928   bits: 15/14
c ---[2071]---> Adder-cost: 272   maxlim: 16896   bits: 16/15
c ---[2069]---> Adder-cost: 88   maxlim: 16896   bits: 16/15
c ---[2067]---> Adder-cost: 178   maxlim: 11264   bits: 15/14
c ---[2065]---> Adder-cost: 72   maxlim: 11264   bits: 15/14
c ---[2063]---> Adder-cost: 184   maxlim: 11392   bits: 15/14
c ---[2061]---> Adder-cost: 116   maxlim: 10624   bits: 15/14
c ---[2059]---> Adder-cost: 300   maxlim: 19072   bits: 16/15
c ---[2057]---> Adder-cost: 194   maxlim: 21376   bits: 16/15
c ---[2055]---> Adder-cost: 144   maxlim: 33664   bits: 17/16
c ---[2053]---> Adder-cost: 100   maxlim: 21376   bits: 16/15
c ---[2051]---> Adder-cost: 274   maxlim: 17024   bits: 16/15
c ---[2049]---> Adder-cost: 88   maxlim: 17024   bits: 16/15
c ---[2047]---> Adder-cost: 182   maxlim: 11648   bits: 15/14
c ---[2045]---> Adder-cost: 64   maxlim: 11648   bits: 15/14
c ---[2043]---> Adder-cost: 412   maxlim: 26240   bits: 16/15
c ---[2041]---> Adder-cost: 112   maxlim: 26240   bits: 16/15
c ---[2039]---> Adder-cost: 396   maxlim: 25216   bits: 16/15
c ---[2037]---> Adder-cost: 114   maxlim: 25216   bits: 16/15
c ---[2035]---> Adder-cost: 628   maxlim: 42368   bits: 17/16
c ---[2033]---> Adder-cost: 144   maxlim: 33664   bits: 17/16
c ---[2031]---> Adder-cost: 156   maxlim: 42368   bits: 17/16
c ---[2029]---> Adder-cost: 268   maxlim: 16384   bits: 16/15
c ---[2027]---> Adder-cost: 90   maxlim: 16384   bits: 16/15
c ---[2025]---> Adder-cost: 302   maxlim: 18944   bits: 16/15
c ---[2023]---> Adder-cost: 96   maxlim: 18944   bits: 16/15
c ---[2021]---> Adder-cost: 300   maxlim: 19840   bits: 16/15
c ---[2019]---> Adder-cost: 92   maxlim: 19840   bits: 16/15
c ---[2017]---> Adder-cost: 236   maxlim: 15104   bits: 15/14
c ---[2015]---> Adder-cost: 80   maxlim: 15104   bits: 15/14
c ---[2013]---> Adder-cost: 192   maxlim: 12032   bits: 15/14
c ---[2011]---> Adder-cost: 144   maxlim: 33664   bits: 17/16
c ---[2009]---> Adder-cost: 158   maxlim: 11392   bits: 15/14
c ---[2007]---> Adder-cost: 146   maxlim: 8704   bits: 15/14
c ---[2005]---> Adder-cost: 156   maxlim: 11520   bits: 15/14
c ---[2003]---> Adder-cost: 66   maxlim: 11520   bits: 15/14
c ---[2001]---> Adder-cost: 524   maxlim: 37120   bits: 17/16
c ---[1999]---> Adder-cost: 790   maxlim: 63616   bits: 17/16
c ---[1997]---> Adder-cost: 896   maxlim: 59392   bits: 17/16
c ---[1995]---> Adder-cost: 610   maxlim: 42752   bits: 17/16
c ---[1993]---> Adder-cost: 432   maxlim: 29824   bits: 16/15
c ---[1991]---> Adder-cost: 474   maxlim: 32768   bits: 17/16
c ---[1989]---> Adder-cost: 504   maxlim: 32768   bits: 17/16
c ---[1987]---> Adder-cost: 250   maxlim: 16128   bits: 15/14
c ---[1985]---> Adder-cost: 162   maxlim: 10112   bits: 15/14
c ---[1983]---> Adder-cost: 218   maxlim: 16384   bits: 16/15
c ---[1981]---> Adder-cost: 564   maxlim: 35456   bits: 17/16
c ---[1979]---> Adder-cost: 544   maxlim: 34816   bits: 17/16
c ---[1977]---> Adder-cost: 430   maxlim: 31104   bits: 16/15
c ---[1975]---> Adder-cost: 356   maxlim: 28032   bits: 16/15
c ---[1973]---> Adder-cost: 140   maxlim: 32768   bits: 17/16
c ---[1971]---> Adder-cost: 626   maxlim: 40320   bits: 17/16
c ---[1969]---> Adder-cost: 600   maxlim: 44928   bits: 17/16
c ---[1967]---> Adder-cost: 526   maxlim: 38144   bits: 17/16
c ---[1965]---> Adder-cost: 320   maxlim: 23552   bits: 16/15
c ---[1963]---> Adder-cost: 526   maxlim: 34048   bits: 17/16
c ---[1961]---> Adder-cost: 446   maxlim: 30464   bits: 16/15
c ---[1959]---> Adder-cost: 350   maxlim: 25344   bits: 16/15
c ---[1957]---> Adder-cost: 208   maxlim: 15104   bits: 15/14
c ---[1955]---> Adder-cost: 266   maxlim: 18048   bits: 16/15
c ---[1953]---> Adder-cost: 126   maxlim: 12288   bits: 15/14
c ---[1951]---> Adder-cost: 140   maxlim: 32768   bits: 17/16
c ---[1949]---> Adder-cost: 190   maxlim: 11776   bits: 15/14
c ---[1947]---> Adder-cost: 186   maxlim: 13056   bits: 15/14
c ---[1945]---> Adder-cost: 286   maxlim: 22656   bits: 16/15
c ---[1943]---> Adder-cost: 272   maxlim: 22400   bits: 16/15
c ---[1941]---> Adder-cost: 310   maxlim: 20224   bits: 16/15
c ---[1939]---> Adder-cost: 376   maxlim: 26880   bits: 16/15
c ---[1937]---> Adder-cost: 254   maxlim: 18048   bits: 16/15
c ---[1935]---> Adder-cost: 200   maxlim: 16384   bits: 16/15
c ---[1933]---> Adder-cost: 332   maxlim: 20992   bits: 16/15
c ---[1931]---> Adder-cost: 274   maxlim: 19584   bits: 16/15
c ---[1929]---> Adder-cost: 140   maxlim: 32768   bits: 17/16
c ---[1927]---> Adder-cost: 318   maxlim: 20480   bits: 16/15
c ---[1925]---> Adder-cost: 350   maxlim: 24192   bits: 16/15
c ---[1923]---> Adder-cost: 382   maxlim: 29184   bits: 16/15
c ---[1921]---> Adder-cost: 462   maxlim: 35456   bits: 17/16
c ---[1919]---> Adder-cost: 520   maxlim: 37504   bits: 17/16
c ---[1917]---> Adder-cost: 394   maxlim: 26112   bits: 16/15
c ---[1915]---> Adder-cost: 692   maxlim: 47232   bits: 17/16
c ---[1913]---> Adder-cost: 630   maxlim: 42496   bits: 17/16
c ---[1911]---> Adder-cost: 572   maxlim: 44800   bits: 17/16
c ---[1909]---> Adder-cost: 508   maxlim: 35840   bits: 17/16
c ---[1907]---> Adder-cost: 140   maxlim: 32768   bits: 17/16
c ---[1905]---> Adder-cost: 404   maxlim: 26368   bits: 16/15
c ---[1903]---> Adder-cost: 250   maxlim: 20352   bits: 16/15
c ---[1901]---> Adder-cost: 188   maxlim: 11904   bits: 15/14
c ---[1899]---> Adder-cost: 194   maxlim: 13440   bits: 15/14
c ---[1897]---> Adder-cost: 368   maxlim: 24064   bits: 16/15
c ---[1895]---> Adder-cost: 236   maxlim: 16256   bits: 15/14
c ---[1893]---> Adder-cost: 150   maxlim: 10368   bits: 15/14
c ---[1891]---> Adder-cost: 156   maxlim: 10112   bits: 15/14
c ---[1889]---> Adder-cost: 184   maxlim: 11520   bits: 15/14
c ---[1887]---> Adder-cost: 82   maxlim: 5504   bits: 14/13
c ---[1885]---> Adder-cost: 140   maxlim: 32768   bits: 17/16
c ---[1883]---> Adder-cost: 284   maxlim: 17536   bits: 16/15
c ---[1881]---> Adder-cost: 94   maxlim: 17536   bits: 16/15
c ---[1879]---> Adder-cost: 344   maxlim: 22272   bits: 16/15
c ---[1877]---> Adder-cost: 102   maxlim: 22272   bits: 16/15
c ---[1875]---> Adder-cost: 288   maxlim: 17920   bits: 16/15
c ---[1873]---> Adder-cost: 90   maxlim: 17920   bits: 16/15
c ---[1871]---> Adder-cost: 90   maxlim: 17920   bits: 16/15
c ---[1869]---> Adder-cost: 90   maxlim: 17920   bits: 16/15
c ---[1867]---> Adder-cost: 240   maxlim: 15360   bits: 15/14
c ---[1865]---> Adder-cost: 80   maxlim: 15360   bits: 15/14
c ---[1863]---> Adder-cost: 448   maxlim: 30208   bits: 16/15
c ---[1861]---> Adder-cost: 96   maxlim: 6528   bits: 14/13
c ---[1859]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[1857]---> Adder-cost: 252   maxlim: 15872   bits: 15/14
c ---[1855]---> Adder-cost: 78   maxlim: 15872   bits: 15/14
c ---[1853]---> Adder-cost: 362   maxlim: 23424   bits: 16/15
c ---[1851]---> Adder-cost: 340   maxlim: 23552   bits: 16/15
c ---[1849]---> Adder-cost: 376   maxlim: 23808   bits: 16/15
c ---[1847]---> Adder-cost: 106   maxlim: 23808   bits: 16/15
c ---[1845]---> Adder-cost: 106   maxlim: 23808   bits: 16/15
c ---[1843]---> Adder-cost: 106   maxlim: 23808   bits: 16/15
c ---[1841]---> Adder-cost: 126   maxlim: 30208   bits: 16/15
c ---[1839]---> Adder-cost: 198   maxlim: 12544   bits: 15/14
c ---[1837]---> Adder-cost: 122   maxlim: 12160   bits: 15/14
c ---[1835]---> Adder-cost: 96   maxlim: 6784   bits: 14/13
c ---[1833]---> Adder-cost: 46   maxlim: 6784   bits: 14/13
c ---[1831]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[1829]---> Sorter-cost:  952     Base: 2 2 2 2 2 2 2 7
c ---[1827]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1825]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1823]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1821]---> Adder-cost: 270   maxlim: 16768   bits: 16/15
c ---[1819]---> Adder-cost: 84   maxlim: 16768   bits: 16/15
c ---[1817]---> Adder-cost: 232   maxlim: 14848   bits: 15/14
c ---[1815]---> Adder-cost: 80   maxlim: 14848   bits: 15/14
c ---[1813]---> Adder-cost: 80   maxlim: 14848   bits: 15/14
c ---[1811]---> Adder-cost: 80   maxlim: 14848   bits: 15/14
c ---[1809]---> Adder-cost: 106   maxlim: 6400   bits: 14/13
c ---[1807]---> Adder-cost: 150   maxlim: 9344   bits: 15/14
c ---[1805]---> Adder-cost: 60   maxlim: 9344   bits: 15/14
c ---[1803]---> Adder-cost: 330   maxlim: 20736   bits: 16/15
c ---[1801]---> Adder-cost: 262   maxlim: 20864   bits: 16/15
c ---[1799]---> Adder-cost: 522   maxlim: 32896   bits: 17/16
c ---[1797]---> Adder-cost: 138   maxlim: 32896   bits: 17/16
c ---[1795]---> Adder-cost: 316   maxlim: 20608   bits: 16/15
c ---[1793]---> Adder-cost: 100   maxlim: 20608   bits: 16/15
c ---[1791]---> Adder-cost: 218   maxlim: 15488   bits: 15/14
c ---[1789]---> Adder-cost: 78   maxlim: 15488   bits: 15/14
c ---[1787]---> Adder-cost: 222   maxlim: 13952   bits: 15/14
c ---[1785]---> Adder-cost: 178   maxlim: 13696   bits: 15/14
c ---[1783]---> Adder-cost: 212   maxlim: 13824   bits: 15/14
c ---[1781]---> Adder-cost: 74   maxlim: 13824   bits: 15/14
c ---[1779]---> Adder-cost: 350   maxlim: 22144   bits: 16/15
c ---[1777]---> Adder-cost: 100   maxlim: 22144   bits: 16/15
c ---[1775]---> Adder-cost: 244   maxlim: 16128   bits: 15/14
c ---[1773]---> Adder-cost: 76   maxlim: 16128   bits: 15/14
c ---[1771]---> Adder-cost: 278   maxlim: 17792   bits: 16/15
c ---[1769]---> Adder-cost: 92   maxlim: 17792   bits: 16/15
c ---[1767]---> Adder-cost: 188   maxlim: 12160   bits: 15/14
c ---[1765]---> Adder-cost: 64   maxlim: 12160   bits: 15/14
c ---[1763]---> Adder-cost: 244   maxlim: 15872   bits: 15/14
c ---[1761]---> Adder-cost: 78   maxlim: 15872   bits: 15/14
c ---[1759]---> Adder-cost: 126   maxlim: 30208   bits: 16/15
c ---[1757]---> Adder-cost: 206   maxlim: 13056   bits: 15/14
c ---[1755]---> Adder-cost: 176   maxlim: 11648   bits: 15/14
c ---[1753]---> Adder-cost: 90   maxlim: 6784   bits: 14/13
c ---[1751]---> Adder-cost: 376   maxlim: 23552   bits: 16/15
c ---[1749]---> Adder-cost: 106   maxlim: 23552   bits: 16/15
c ---[1747]---> Adder-cost: 274   maxlim: 16896   bits: 16/15
c ---[1745]---> Adder-cost: 88   maxlim: 16896   bits: 16/15
c ---[1743]---> Adder-cost: 88   maxlim: 16896   bits: 16/15
c ---[1741]---> Adder-cost: 88   maxlim: 16896   bits: 16/15
c ---[1739]---> Adder-cost: 270   maxlim: 16512   bits: 16/15
c ---[1737]---> Adder-cost: 582   maxlim: 38400   bits: 17/16
c ---[1735]---> Adder-cost: 90   maxlim: 16512   bits: 16/15
c ---[1733]---> Adder-cost: 138   maxlim: 10112   bits: 15/14
c ---[1731]---> Adder-cost: 62   maxlim: 10112   bits: 15/14
c ---[1729]---> Adder-cost: 288   maxlim: 18176   bits: 16/15
c ---[1727]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[1725]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[1723]---> Adder-cost: 372   maxlim: 24320   bits: 16/15
c ---[1721]---> Adder-cost: 110   maxlim: 24320   bits: 16/15
c ---[1719]---> Adder-cost: 244   maxlim: 15488   bits: 15/14
c ---[1717]---> Adder-cost: 78   maxlim: 15488   bits: 15/14
c ---[1715]---> Adder-cost: 146   maxlim: 38400   bits: 17/16
c ---[1713]---> Adder-cost: 78   maxlim: 15488   bits: 15/14
c ---[1711]---> Adder-cost: 78   maxlim: 15488   bits: 15/14
c ---[1709]---> Adder-cost: 130   maxlim: 8576   bits: 15/14
c ---[1707]---> Adder-cost: 106   maxlim: 6400   bits: 14/13
c ---[1705]---> Adder-cost: 176   maxlim: 11264   bits: 15/14
c ---[1703]---> Adder-cost: 128   maxlim: 10624   bits: 15/14
c ---[1701]---> Adder-cost: 414   maxlim: 26368   bits: 16/15
c ---[1699]---> Adder-cost: 380   maxlim: 24704   bits: 16/15
c ---[1697]---> Adder-cost: 194   maxlim: 14080   bits: 15/14
c ---[1695]---> Adder-cost: 138   maxlim: 10496   bits: 15/14
c ---[1693]---> Adder-cost: 202   maxlim: 13056   bits: 15/14
c ---[1691]---> Adder-cost: 252   maxlim: 16128   bits: 15/14
c ---[1689]---> Adder-cost: 76   maxlim: 16128   bits: 15/14
c ---[1687]---> Adder-cost: 362   maxlim: 23296   bits: 16/15
c ---[1685]---> Adder-cost: 106   maxlim: 23296   bits: 16/15
c ---[1683]---> Adder-cost: 284   maxlim: 17408   bits: 16/15
c ---[1681]---> Adder-cost: 94   maxlim: 17408   bits: 16/15
c ---[1679]---> Adder-cost: 94   maxlim: 17408   bits: 16/15
c ---[1677]---> Adder-cost: 94   maxlim: 17408   bits: 16/15
c ---[1675]---> Adder-cost: 326   maxlim: 21120   bits: 16/15
c ---[1673]---> Adder-cost: 298   maxlim: 20864   bits: 16/15
c ---[1671]---> Adder-cost: 104   maxlim: 6144   bits: 14/13
c ---[1669]---> Adder-cost: 88   maxlim: 7040   bits: 14/13
c ---[1667]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[1665]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[1663]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[1661]---> Adder-cost: 234   maxlim: 14720   bits: 15/14
c ---[1659]---> Adder-cost: 76   maxlim: 14720   bits: 15/14
c ---[1657]---> Adder-cost: 136   maxlim: 8320   bits: 15/14
c ---[1655]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[1653]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[1651]---> Adder-cost: 144   maxlim: 8832   bits: 15/14
c ---[1649]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[1647]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[1645]---> Adder-cost: 244   maxlim: 15744   bits: 15/14
c ---[1643]---> Adder-cost: 78   maxlim: 15744   bits: 15/14
c ---[1641]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[1639]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[1637]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[1635]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[1633]---> Adder-cost: 146   maxlim: 38400   bits: 17/16
c ---[1631]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1629]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[1627]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[1625]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[1623]---> Adder-cost: 570   maxlim: 35968   bits: 17/16
c ---[1621]---> Adder-cost: 150   maxlim: 35968   bits: 17/16
c ---[1619]---> Adder-cost: 818   maxlim: 54400   bits: 17/16
c ---[1617]---> Adder-cost: 182   maxlim: 54400   bits: 17/16
c ---[1615]---> Adder-cost: 796   maxlim: 51072   bits: 17/16
c ---[1613]---> Adder-cost: 170   maxlim: 51072   bits: 17/16
c ---[1611]---> Adder-cost: 1024   maxlim: 69248   bits: 18/17
c ---[1609]---> Adder-cost: 360   maxlim: 23168   bits: 16/15
c ---[1607]---> Adder-cost: 102   maxlim: 23168   bits: 16/15
c ---[1605]---> Adder-cost: 394   maxlim: 28544   bits: 16/15
c ---[1603]---> Adder-cost: 412   maxlim: 28416   bits: 16/15
c ---[1601]---> Adder-cost: 332   maxlim: 24192   bits: 16/15
c ---[1599]---> Adder-cost: 108   maxlim: 24192   bits: 16/15
c ---[1597]---> Adder-cost: 284   maxlim: 17408   bits: 16/15
c ---[1595]---> Adder-cost: 94   maxlim: 17408   bits: 16/15
c ---[1593]---> Adder-cost: 104   maxlim: 6528   bits: 14/13
c ---[1591]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[1589]---> Adder-cost: 630   maxlim: 66048   bits: 18/17
c ---[1587]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[1585]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1583]---> Adder-cost: 166   maxlim: 10240   bits: 15/14
c ---[1581]---> Adder-cost: 68   maxlim: 10240   bits: 15/14
c ---[1579]---> Adder-cost: 98   maxlim: 7040   bits: 14/13
c ---[1577]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[1575]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[1573]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[1571]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[1569]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[1567]---> Adder-cost: 208   maxlim: 66048   bits: 18/17
c ---[1565]---> Adder-cost: 148   maxlim: 9472   bits: 15/14
c ---[1563]---> Adder-cost: 184   maxlim: 13568   bits: 15/14
c ---[1561]---> Adder-cost: 494   maxlim: 31360   bits: 16/15
c ---[1559]---> Adder-cost: 440   maxlim: 32256   bits: 16/15
c ---[1557]---> Adder-cost: 224   maxlim: 14592   bits: 15/14
c ---[1555]---> Adder-cost: 182   maxlim: 13312   bits: 15/14
c ---[1553]---> Adder-cost: 172   maxlim: 11008   bits: 15/14
c ---[1551]---> Adder-cost: 222   maxlim: 13824   bits: 15/14
c ---[1549]---> Adder-cost: 74   maxlim: 13824   bits: 15/14
c ---[1547]---> Adder-cost: 252   maxlim: 16256   bits: 15/14
c ---[1545]---> Adder-cost: 208   maxlim: 66048   bits: 18/17
c ---[1543]---> Adder-cost: 74   maxlim: 16256   bits: 15/14
c ---[1541]---> Adder-cost: 536   maxlim: 33920   bits: 17/16
c ---[1539]---> Adder-cost: 140   maxlim: 33920   bits: 17/16
c ---[1537]---> Adder-cost: 140   maxlim: 33920   bits: 17/16
c ---[1535]---> Adder-cost: 140   maxlim: 33920   bits: 17/16
c ---[1533]---> Adder-cost: 132   maxlim: 9472   bits: 15/14
c ---[1531]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[1529]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[1527]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[1525]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[1523]---> Adder-cost: 208   maxlim: 66048   bits: 18/17
c ---[1521]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[1519]---> Adder-cost: 228   maxlim: 14464   bits: 15/14
c ---[1517]---> Adder-cost: 76   maxlim: 14464   bits: 15/14
c ---[1515]---> Adder-cost: 84   maxlim: 6400   bits: 14/13
c ---[1513]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[1511]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[1509]---> Adder-cost: 130   maxlim: 9472   bits: 15/14
c ---[1507]---> Adder-cost: 64   maxlim: 9472   bits: 15/14
c ---[1505]---> Adder-cost: 666   maxlim: 43008   bits: 17/16
c ---[1503]---> Adder-cost: 552   maxlim: 40832   bits: 17/16
c ---[1501]---> Adder-cost: 208   maxlim: 66048   bits: 18/17
c ---[1499]---> Adder-cost: 510   maxlim: 36352   bits: 17/16
c ---[1497]---> Adder-cost: 146   maxlim: 36352   bits: 17/16
c ---[1495]---> Adder-cost: 488   maxlim: 31872   bits: 16/15
c ---[1493]---> Adder-cost: 276   maxlim: 24192   bits: 16/15
c ---[1491]---> Adder-cost: 240   maxlim: 17024   bits: 16/15
c ---[1489]---> Adder-cost: 88   maxlim: 17024   bits: 16/15
c ---[1487]---> Adder-cost: 112   maxlim: 6912   bits: 14/13
c ---[1485]---> Adder-cost: 230   maxlim: 14592   bits: 15/14
c ---[1483]---> Adder-cost: 78   maxlim: 14592   bits: 15/14
c ---[1481]---> Adder-cost: 220   maxlim: 13824   bits: 15/14
c ---[1479]---> Adder-cost: 560   maxlim: 43648   bits: 17/16
c ---[1477]---> Adder-cost: 74   maxlim: 13824   bits: 15/14
c ---[1475]---> Adder-cost: 172   maxlim: 10496   bits: 15/14
c ---[1473]---> Adder-cost: 68   maxlim: 10496   bits: 15/14
c ---[1471]---> Adder-cost: 488   maxlim: 31744   bits: 16/15
c ---[1469]---> Adder-cost: 132   maxlim: 31744   bits: 16/15
c ---[1467]---> Adder-cost: 156   maxlim: 9856   bits: 15/14
c ---[1465]---> Adder-cost: 196   maxlim: 12544   bits: 15/14
c ---[1463]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[1461]---> Adder-cost: 466   maxlim: 29696   bits: 16/15
c ---[1459]---> Adder-cost: 384   maxlim: 26752   bits: 16/15
c ---[1457]---> Adder-cost: 426   maxlim: 29696   bits: 16/15
c ---[1455]---> Adder-cost: 128   maxlim: 29696   bits: 16/15
c ---[1453]---> Adder-cost: 470   maxlim: 31360   bits: 16/15
c ---[1451]---> Adder-cost: 460   maxlim: 31360   bits: 16/15
c ---[1449]---> Adder-cost: 484   maxlim: 33024   bits: 17/16
c ---[1447]---> Adder-cost: 138   maxlim: 33024   bits: 17/16
c ---[1445]---> Adder-cost: 160   maxlim: 11264   bits: 15/14
c ---[1443]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[1441]---> Adder-cost: 98   maxlim: 7168   bits: 14/13
c ---[1439]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[1437]---> Adder-cost: 306   maxlim: 18944   bits: 16/15
c ---[1435]---> Adder-cost: 96   maxlim: 18944   bits: 16/15
c ---[1433]---> Adder-cost: 276   maxlim: 19712   bits: 16/15
c ---[1431]---> Adder-cost: 92   maxlim: 19712   bits: 16/15
c ---[1429]---> Adder-cost: 570   maxlim: 35840   bits: 17/16
c ---[1427]---> Adder-cost: 496   maxlim: 35712   bits: 17/16
c ---[1425]---> Adder-cost: 454   maxlim: 33920   bits: 17/16
c ---[1423]---> Adder-cost: 140   maxlim: 33920   bits: 17/16
c ---[1421]---> Adder-cost: 544   maxlim: 34816   bits: 17/16
c ---[1419]---> Adder-cost: 148   maxlim: 34816   bits: 17/16
c ---[1417]---> Adder-cost: 672   maxlim: 43904   bits: 17/16
c ---[1415]---> Adder-cost: 152   maxlim: 43904   bits: 17/16
c ---[1413]---> Adder-cost: 400   maxlim: 25088   bits: 16/15
c ---[1411]---> Adder-cost: 116   maxlim: 25088   bits: 16/15
c ---[1409]---> Adder-cost: 454   maxlim: 29312   bits: 16/15
c ---[1407]---> Adder-cost: 348   maxlim: 24192   bits: 16/15
c ---[1405]---> Adder-cost: 108   maxlim: 24192   bits: 16/15
c ---[1403]---> Adder-cost: 288   maxlim: 18304   bits: 16/15
c ---[1401]---> Adder-cost: 88   maxlim: 18304   bits: 16/15
c ---[1399]---> Adder-cost: 238   maxlim: 15360   bits: 15/14
c ---[1397]---> Adder-cost: 80   maxlim: 15360   bits: 15/14
c ---[1395]---> Adder-cost: 204   maxlim: 12800   bits: 15/14
c ---[1393]---> Adder-cost: 132   maxlim: 12416   bits: 15/14
c ---[1391]---> Adder-cost: 140   maxlim: 9472   bits: 15/14
c ---[1389]---> Adder-cost: 426   maxlim: 26624   bits: 16/15
c ---[1387]---> Adder-cost: 122   maxlim: 26624   bits: 16/15
c ---[1385]---> Adder-cost: 548   maxlim: 36736   bits: 17/16
c ---[1383]---> Adder-cost: 376   maxlim: 38272   bits: 17/16
c ---[1381]---> Adder-cost: 146   maxlim: 38272   bits: 17/16
c ---[1379]---> Adder-cost: 722   maxlim: 48256   bits: 17/16
c ---[1377]---> Adder-cost: 562   maxlim: 48384   bits: 17/16
c ---[1375]---> Adder-cost: 160   maxlim: 48384   bits: 17/16
c ---[1373]---> Adder-cost: 736   maxlim: 49792   bits: 17/16
c ---[1371]---> Adder-cost: 178   maxlim: 49792   bits: 17/16
c ---[1369]---> Adder-cost: 178   maxlim: 49792   bits: 17/16
c ---[1367]---> Adder-cost: 496   maxlim: 34432   bits: 17/16
c ---[1365]---> Adder-cost: 148   maxlim: 34432   bits: 17/16
c ---[1363]---> Adder-cost: 148   maxlim: 34432   bits: 17/16
c ---[1361]---> Adder-cost: 890   maxlim: 63360   bits: 17/16
c ---[1359]---> Adder-cost: 192   maxlim: 63360   bits: 17/16
c ---[1358]---> Adder-cost: 4555   maxlim: 320383   bits: 20/19
c ---[1357]---> Adder-cost: 49746   maxlim: 3327615   bits: 23/22
c ---[1356]---> Adder-cost: 4861   maxlim: 348415   bits: 20/19
c ---[1354]---> Adder-cost: 7502   maxlim: 540032   bits: 21/20
c ---[1353]---> Adder-cost: 8305   maxlim: 371583   bits: 20/19
c ---[1351]---> Adder-cost: 6043   maxlim: 310271   bits: 20/19
c ---[1348]---> Adder-cost: 7808   maxlim: 643327   bits: 21/20
c ---[1347]---> Adder-cost: 155827   maxlim: 43954687   bits: 27/26
c ---[1346]---> Adder-cost: 9968   maxlim: 2646015   bits: 23/22
c ---[1345]---> Adder-cost: 90834   maxlim: 37596415   bits: 27/26
c ---[1344]---> Adder-cost: 10623   maxlim: 2079615   bits: 22/21
c ---[1343]---> Adder-cost: 20997   maxlim: 1632639   bits: 22/21
c ---[1341]---> Adder-cost: 192   maxlim: 63360   bits: 17/16
c ---[1339]---> Adder-cost: 714   maxlim: 52992   bits: 17/16
c ---[1337]---> Adder-cost: 172   maxlim: 52992   bits: 17/16
c ---[1335]---> Adder-cost: 172   maxlim: 52992   bits: 17/16
c ---[1333]---> Adder-cost: 448   maxlim: 30848   bits: 16/15
c ---[1331]---> Adder-cost: 128   maxlim: 30848   bits: 16/15
c ---[1329]---> Adder-cost: 128   maxlim: 30848   bits: 16/15
c ---[1327]---> Adder-cost: 318   maxlim: 20736   bits: 16/15
c ---[1325]---> Adder-cost: 182   maxlim: 20352   bits: 16/15
c ---[1323]---> Adder-cost: 92   maxlim: 20352   bits: 16/15
c ---[1321]---> Adder-cost: 88   maxlim: 8832   bits: 15/14
c ---[1319]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[1317]---> Adder-cost: 124   maxlim: 9472   bits: 15/14
c ---[1315]---> Adder-cost: 64   maxlim: 9472   bits: 15/14
c ---[1313]---> Adder-cost: 566   maxlim: 39040   bits: 17/16
c ---[1311]---> Adder-cost: 382   maxlim: 30336   bits: 16/15
c ---[1309]---> Adder-cost: 354   maxlim: 24704   bits: 16/15
c ---[1307]---> Adder-cost: 112   maxlim: 24704   bits: 16/15
c ---[1305]---> Adder-cost: 470   maxlim: 32000   bits: 16/15
c ---[1303]---> Adder-cost: 416   maxlim: 28416   bits: 16/15
c ---[1301]---> Adder-cost: 250   maxlim: 17792   bits: 16/15
c ---[1299]---> Adder-cost: 92   maxlim: 17792   bits: 16/15
c ---[1297]---> Adder-cost: 112   maxlim: 8576   bits: 15/14
c ---[1295]---> Adder-cost: 192   maxlim: 12160   bits: 15/14
c ---[1293]---> Adder-cost: 196   maxlim: 14336   bits: 15/14
c ---[1291]---> Adder-cost: 76   maxlim: 14336   bits: 15/14
c ---[1289]---> Adder-cost: 338   maxlim: 21376   bits: 16/15
c ---[1287]---> Adder-cost: 100   maxlim: 21376   bits: 16/15
c ---[1285]---> Adder-cost: 270   maxlim: 17792   bits: 16/15
c ---[1283]---> Adder-cost: 92   maxlim: 17792   bits: 16/15
c ---[1281]---> Adder-cost: 294   maxlim: 18944   bits: 16/15
c ---[1279]---> Adder-cost: 96   maxlim: 18944   bits: 16/15
c ---[1277]---> Adder-cost: 234   maxlim: 15488   bits: 15/14
c ---[1275]---> Adder-cost: 78   maxlim: 15488   bits: 15/14
c ---[1273]---> Adder-cost: 360   maxlim: 23040   bits: 16/15
c ---[1271]---> Adder-cost: 104   maxlim: 23040   bits: 16/15
c ---[1269]---> Adder-cost: 350   maxlim: 23168   bits: 16/15
c ---[1267]---> Adder-cost: 102   maxlim: 23168   bits: 16/15
c ---[1265]---> Adder-cost: 256   maxlim: 16384   bits: 16/15
c ---[1263]---> Adder-cost: 90   maxlim: 16384   bits: 16/15
c ---[1261]---> Adder-cost: 218   maxlim: 15360   bits: 15/14
c ---[1259]---> Adder-cost: 180   maxlim: 15232   bits: 15/14
c ---[1257]---> Adder-cost: 158   maxlim: 11008   bits: 15/14
c ---[1255]---> Adder-cost: 68   maxlim: 11008   bits: 15/14
c ---[1253]---> Adder-cost: 144   maxlim: 9728   bits: 15/14
c ---[1251]---> Adder-cost: 64   maxlim: 9728   bits: 15/14
c ---[1249]---> Adder-cost: 134   maxlim: 8960   bits: 15/14
c ---[1247]---> Adder-cost: 96   maxlim: 8576   bits: 15/14
c ---[1245]---> Adder-cost: 84   maxlim: 5376   bits: 14/13
c ---[1243]---> Adder-cost: 586   maxlim: 39040   bits: 17/16
c ---[1241]---> Adder-cost: 510   maxlim: 43392   bits: 17/16
c ---[1239]---> Adder-cost: 644   maxlim: 43904   bits: 17/16
c ---[1237]---> Adder-cost: 152   maxlim: 43904   bits: 17/16
c ---[1235]---> Adder-cost: 572   maxlim: 39424   bits: 17/16
c ---[1233]---> Adder-cost: 546   maxlim: 37376   bits: 17/16
c ---[1231]---> Adder-cost: 258   maxlim: 17408   bits: 16/15
c ---[1229]---> Adder-cost: 94   maxlim: 17408   bits: 16/15
c ---[1227]---> Adder-cost: 158   maxlim: 11392   bits: 15/14
c ---[1225]---> Adder-cost: 408   maxlim: 27008   bits: 16/15
c ---[1223]---> Adder-cost: 116   maxlim: 27008   bits: 16/15
c ---[1221]---> Adder-cost: 586   maxlim: 40832   bits: 17/16
c ---[1219]---> Adder-cost: 448   maxlim: 41728   bits: 17/16
c ---[1217]---> Adder-cost: 154   maxlim: 41728   bits: 17/16
c ---[1215]---> Adder-cost: 534   maxlim: 37248   bits: 17/16
c ---[1213]---> Adder-cost: 142   maxlim: 37248   bits: 17/16
c ---[1211]---> Adder-cost: 142   maxlim: 37248   bits: 17/16
c ---[1209]---> Adder-cost: 682   maxlim: 48768   bits: 17/16
c ---[1207]---> Adder-cost: 162   maxlim: 48768   bits: 17/16
c ---[1205]---> Adder-cost: 162   maxlim: 48768   bits: 17/16
c ---[1203]---> Adder-cost: 706   maxlim: 48768   bits: 17/16
c ---[1201]---> Adder-cost: 162   maxlim: 48768   bits: 17/16
c ---[1199]---> Adder-cost: 162   maxlim: 48768   bits: 17/16
c ---[1197]---> Adder-cost: 700   maxlim: 48640   bits: 17/16
c ---[1195]---> Adder-cost: 164   maxlim: 48640   bits: 17/16
c ---[1193]---> Adder-cost: 164   maxlim: 48640   bits: 17/16
c ---[1191]---> Adder-cost: 164   maxlim: 48640   bits: 17/16
c ---[1189]---> Adder-cost: 164   maxlim: 48640   bits: 17/16
c ---[1187]---> Adder-cost: 164   maxlim: 48640   bits: 17/16
c ---[1185]---> Adder-cost: 522   maxlim: 38272   bits: 17/16
c ---[1183]---> Adder-cost: 146   maxlim: 38272   bits: 17/16
c ---[1181]---> Adder-cost: 146   maxlim: 38272   bits: 17/16
c ---[1179]---> Adder-cost: 146   maxlim: 38272   bits: 17/16
c ---[1177]---> Adder-cost: 146   maxlim: 38272   bits: 17/16
c ---[1175]---> Adder-cost: 146   maxlim: 38272   bits: 17/16
c ---[1173]---> Adder-cost: 482   maxlim: 33280   bits: 17/16
c ---[1171]---> Adder-cost: 332   maxlim: 32896   bits: 17/16
c ---[1169]---> Adder-cost: 138   maxlim: 32896   bits: 17/16
c ---[1167]---> Adder-cost: 138   maxlim: 32896   bits: 17/16
c ---[1165]---> Adder-cost: 138   maxlim: 32896   bits: 17/16
c ---[1163]---> Adder-cost: 138   maxlim: 32896   bits: 17/16
c ---[1161]---> Adder-cost: 236   maxlim: 15488   bits: 15/14
c ---[1159]---> Adder-cost: 150   maxlim: 12672   bits: 15/14
c ---[1157]---> Adder-cost: 72   maxlim: 12672   bits: 15/14
c ---[1155]---> Adder-cost: 106   maxlim: 8320   bits: 15/14
c ---[1153]---> Adder-cost: 210   maxlim: 13440   bits: 15/14
c ---[1151]---> Adder-cost: 242   maxlim: 18304   bits: 16/15
c ---[1149]---> Adder-cost: 88   maxlim: 18304   bits: 16/15
c ---[1147]---> Adder-cost: 606   maxlim: 41984   bits: 17/16
c ---[1145]---> Adder-cost: 574   maxlim: 38784   bits: 17/16
c ---[1143]---> Adder-cost: 438   maxlim: 29952   bits: 16/15
c ---[1141]---> Adder-cost: 122   maxlim: 29952   bits: 16/15
c ---[1139]---> Adder-cost: 490   maxlim: 33280   bits: 17/16
c ---[1137]---> Adder-cost: 234   maxlim: 30976   bits: 16/15
c ---[1135]---> Adder-cost: 322   maxlim: 22016   bits: 16/15
c ---[1133]---> Adder-cost: 102   maxlim: 22016   bits: 16/15
c ---[1131]---> Adder-cost: 84   maxlim: 5888   bits: 14/13
c ---[1129]---> Adder-cost: 106   maxlim: 6912   bits: 14/13
c ---[1127]---> Adder-cost: 122   maxlim: 7936   bits: 14/13
c ---[1125]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[1123]---> Adder-cost: 244   maxlim: 16256   bits: 15/14
c ---[1121]---> Adder-cost: 74   maxlim: 16256   bits: 15/14
c ---[1119]---> Adder-cost: 258   maxlim: 17152   bits: 16/15
c ---[1117]---> Adder-cost: 88   maxlim: 17152   bits: 16/15
c ---[1115]---> Adder-cost: 410   maxlim: 25984   bits: 16/15
c ---[1113]---> Adder-cost: 350   maxlim: 25472   bits: 16/15
c ---[1111]---> Adder-cost: 350   maxlim: 25472   bits: 16/15
c ---[1109]---> Adder-cost: 110   maxlim: 25472   bits: 16/15
c ---[1107]---> Adder-cost: 268   maxlim: 17024   bits: 16/15
c ---[1105]---> Adder-cost: 88   maxlim: 17024   bits: 16/15
c ---[1103]---> Adder-cost: 376   maxlim: 24320   bits: 16/15
c ---[1101]---> Adder-cost: 110   maxlim: 24320   bits: 16/15
c ---[1099]---> Adder-cost: 218   maxlim: 13568   bits: 15/14
c ---[1097]---> Adder-cost: 78   maxlim: 13568   bits: 15/14
c ---[1095]---> Adder-cost: 184   maxlim: 11648   bits: 15/14
c ---[1093]---> Adder-cost: 64   maxlim: 11648   bits: 15/14
c ---[1091]---> Adder-cost: 208   maxlim: 13184   bits: 15/14
c ---[1089]---> Adder-cost: 74   maxlim: 13184   bits: 15/14
c ---[1087]---> Adder-cost: 174   maxlim: 11648   bits: 15/14
c ---[1085]---> Adder-cost: 64   maxlim: 11648   bits: 15/14
c ---[1083]---> Adder-cost: 134   maxlim: 8704   bits: 15/14
c ---[1081]---> Adder-cost: 98   maxlim: 7680   bits: 14/13
c ---[1079]---> Adder-cost: 112   maxlim: 7424   bits: 14/13
c ---[1077]---> Adder-cost: 106   maxlim: 8192   bits: 15/14
c ---[1075]---> Adder-cost: 62   maxlim: 8192   bits: 15/14
c ---[1073]---> Adder-cost: 334   maxlim: 21888   bits: 16/15
c ---[1071]---> Adder-cost: 264   maxlim: 21120   bits: 16/15
c ---[1069]---> Adder-cost: 304   maxlim: 22016   bits: 16/15
c ---[1067]---> Adder-cost: 102   maxlim: 22016   bits: 16/15
c ---[1065]---> Adder-cost: 384   maxlim: 25088   bits: 16/15
c ---[1063]---> Adder-cost: 308   maxlim: 21760   bits: 16/15
c ---[1061]---> Adder-cost: 286   maxlim: 21632   bits: 16/15
c ---[1059]---> Adder-cost: 100   maxlim: 21632   bits: 16/15
c ---[1057]---> Adder-cost: 292   maxlim: 18688   bits: 16/15
c ---[1055]---> Adder-cost: 214   maxlim: 22528   bits: 16/15
c ---[1053]---> Adder-cost: 110   maxlim: 22528   bits: 16/15
c ---[1051]---> Adder-cost: 382   maxlim: 25216   bits: 16/15
c ---[1049]---> Adder-cost: 114   maxlim: 25216   bits: 16/15
c ---[1047]---> Adder-cost: 430   maxlim: 31104   bits: 16/15
c ---[1045]---> Adder-cost: 128   maxlim: 31104   bits: 16/15
c ---[1043]---> Adder-cost: 510   maxlim: 33280   bits: 17/16
c ---[1041]---> Adder-cost: 142   maxlim: 33280   bits: 17/16
c ---[1039]---> Adder-cost: 462   maxlim: 31104   bits: 16/15
c ---[1037]---> Adder-cost: 128   maxlim: 31104   bits: 16/15
c ---[1035]---> Adder-cost: 520   maxlim: 34048   bits: 17/16
c ---[1033]---> Adder-cost: 142   maxlim: 34048   bits: 17/16
c ---[1031]---> Adder-cost: 316   maxlim: 22016   bits: 16/15
c ---[1029]---> Adder-cost: 102   maxlim: 22016   bits: 16/15
c ---[1027]---> Adder-cost: 490   maxlim: 35328   bits: 17/16
c ---[1025]---> Adder-cost: 140   maxlim: 35328   bits: 17/16
c ---[1023]---> Adder-cost: 322   maxlim: 22016   bits: 16/15
c ---[1021]---> Adder-cost: 102   maxlim: 22016   bits: 16/15
c ---[1019]---> Adder-cost: 66   maxlim: 4736   bits: 14/13
c ---[1017]---> Adder-cost: 246   maxlim: 16384   bits: 16/15
c ---[1015]---> Adder-cost: 90   maxlim: 16384   bits: 16/15
c ---[1013]---> Adder-cost: 90   maxlim: 16384   bits: 16/15
c ---[1011]---> Adder-cost: 338   maxlim: 22272   bits: 16/15
c ---[1009]---> Adder-cost: 388   maxlim: 24832   bits: 16/15
c ---[1007]---> Adder-cost: 472   maxlim: 33024   bits: 17/16
c ---[1005]---> Adder-cost: 138   maxlim: 33024   bits: 17/16
c ---[1003]---> Adder-cost: 592   maxlim: 40064   bits: 17/16
c ---[1001]---> Adder-cost: 608   maxlim: 42112   bits: 17/16
c ---[ 999]---> Adder-cost: 298   maxlim: 19840   bits: 16/15
c ---[ 997]---> Adder-cost: 92   maxlim: 19840   bits: 16/15
c ---[ 995]---> Adder-cost: 440   maxlim: 29312   bits: 16/15
c ---[ 993]---> Adder-cost: 342   maxlim: 28928   bits: 16/15
c ---[ 991]---> Adder-cost: 218   maxlim: 14592   bits: 15/14
c ---[ 989]---> Adder-cost: 78   maxlim: 14592   bits: 15/14
c ---[ 987]---> Adder-cost: 340   maxlim: 25344   bits: 16/15
c ---[ 985]---> Adder-cost: 360   maxlim: 27520   bits: 16/15
c ---[ 983]---> Adder-cost: 386   maxlim: 26368   bits: 16/15
c ---[ 981]---> Adder-cost: 114   maxlim: 26368   bits: 16/15
c ---[ 979]---> Adder-cost: 354   maxlim: 23040   bits: 16/15
c ---[ 977]---> Adder-cost: 228   maxlim: 17408   bits: 16/15
c ---[ 975]---> Adder-cost: 272   maxlim: 17536   bits: 16/15
c ---[ 973]---> Adder-cost: 94   maxlim: 17536   bits: 16/15
c ---[ 971]---> Adder-cost: 390   maxlim: 26368   bits: 16/15
c ---[ 969]---> Adder-cost: 216   maxlim: 15872   bits: 15/14
c ---[ 967]---> Adder-cost: 94   maxlim: 6656   bits: 14/13
c ---[ 965]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[ 963]---> Adder-cost: 218   maxlim: 14464   bits: 15/14
c ---[ 961]---> Adder-cost: 164   maxlim: 11264   bits: 15/14
c ---[ 959]---> Adder-cost: 84   maxlim: 7552   bits: 14/13
c ---[ 957]---> Adder-cost: 148   maxlim: 9472   bits: 15/14
c ---[ 955]---> Adder-cost: 64   maxlim: 9472   bits: 15/14
c ---[ 953]---> Adder-cost: 268   maxlim: 17408   bits: 16/15
c ---[ 951]---> Adder-cost: 94   maxlim: 17408   bits: 16/15
c ---[ 949]---> Adder-cost: 744   maxlim: 50816   bits: 17/16
c ---[ 947]---> Adder-cost: 166   maxlim: 50816   bits: 17/16
c ---[ 945]---> Adder-cost: 708   maxlim: 49664   bits: 17/16
c ---[ 943]---> Adder-cost: 178   maxlim: 49664   bits: 17/16
c ---[ 941]---> Adder-cost: 254   maxlim: 16256   bits: 15/14
c ---[ 939]---> Adder-cost: 74   maxlim: 16256   bits: 15/14
c ---[ 937]---> Adder-cost: 468   maxlim: 32000   bits: 16/15
c ---[ 935]---> Adder-cost: 350   maxlim: 31488   bits: 16/15
c ---[ 933]---> Adder-cost: 520   maxlim: 38144   bits: 17/16
c ---[ 931]---> Adder-cost: 146   maxlim: 38144   bits: 17/16
c ---[ 929]---> Adder-cost: 328   maxlim: 21632   bits: 16/15
c ---[ 927]---> Adder-cost: 100   maxlim: 21632   bits: 16/15
c ---[ 925]---> Adder-cost: 192   maxlim: 12672   bits: 15/14
c ---[ 923]---> Adder-cost: 72   maxlim: 12672   bits: 15/14
c ---[ 921]---> Adder-cost: 280   maxlim: 18432   bits: 16/15
c ---[ 919]---> Adder-cost: 94   maxlim: 18432   bits: 16/15
c ---[ 917]---> Adder-cost: 134   maxlim: 8576   bits: 15/14
c ---[ 915]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[ 913]---> Adder-cost: 68   maxlim: 4992   bits: 14/13
c ---[ 911]---> Adder-cost: 346   maxlim: 23552   bits: 16/15
c ---[ 909]---> Adder-cost: 106   maxlim: 23552   bits: 16/15
c ---[ 907]---> Adder-cost: 280   maxlim: 18176   bits: 16/15
c ---[ 905]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[ 903]---> Adder-cost: 334   maxlim: 21632   bits: 16/15
c ---[ 901]---> Adder-cost: 100   maxlim: 21632   bits: 16/15
c ---[ 899]---> Adder-cost: 350   maxlim: 23296   bits: 16/15
c ---[ 897]---> Adder-cost: 106   maxlim: 23296   bits: 16/15
c ---[ 895]---> Adder-cost: 174   maxlim: 11520   bits: 15/14
c ---[ 893]---> Adder-cost: 66   maxlim: 11520   bits: 15/14
c ---[ 891]---> Adder-cost: 224   maxlim: 14336   bits: 15/14
c ---[ 889]---> Adder-cost: 214   maxlim: 14208   bits: 15/14
c ---[ 887]---> Adder-cost: 428   maxlim: 28800   bits: 16/15
c ---[ 885]---> Adder-cost: 124   maxlim: 28800   bits: 16/15
c ---[ 883]---> Adder-cost: 408   maxlim: 27648   bits: 16/15
c ---[ 881]---> Adder-cost: 116   maxlim: 27648   bits: 16/15
c ---[ 879]---> Adder-cost: 248   maxlim: 16128   bits: 15/14
c ---[ 877]---> Adder-cost: 76   maxlim: 16128   bits: 15/14
c ---[ 875]---> Adder-cost: 276   maxlim: 17408   bits: 16/15
c ---[ 873]---> Adder-cost: 94   maxlim: 17408   bits: 16/15
c ---[ 871]---> Adder-cost: 158   maxlim: 9856   bits: 15/14
c ---[ 869]---> Adder-cost: 60   maxlim: 9856   bits: 15/14
c ---[ 867]---> Adder-cost: 96   maxlim: 6272   bits: 14/13
c ---[ 865]---> Adder-cost: 262   maxlim: 21376   bits: 16/15
c ---[ 863]---> Adder-cost: 280   maxlim: 31744   bits: 16/15
c ---[ 861]---> Adder-cost: 248   maxlim: 32000   bits: 16/15
c ---[ 859]---> Adder-cost: 468   maxlim: 32128   bits: 16/15
c ---[ 857]---> Adder-cost: 592   maxlim: 44672   bits: 17/16
c ---[ 855]---> Adder-cost: 454   maxlim: 39680   bits: 17/16
c ---[ 853]---> Adder-cost: 606   maxlim: 42496   bits: 17/16
c ---[ 851]---> Adder-cost: 632   maxlim: 43520   bits: 17/16
c ---[ 849]---> Adder-cost: 660   maxlim: 50944   bits: 17/16
c ---[ 847]---> Adder-cost: 392   maxlim: 30208   bits: 16/15
c ---[ 845]---> Adder-cost: 358   maxlim: 27776   bits: 16/15
c ---[ 843]---> Adder-cost: 322   maxlim: 22144   bits: 16/15
c ---[ 841]---> Adder-cost: 310   maxlim: 28288   bits: 16/15
c ---[ 839]---> Adder-cost: 400   maxlim: 30720   bits: 16/15
c ---[ 837]---> Adder-cost: 348   maxlim: 28928   bits: 16/15
c ---[ 835]---> Adder-cost: 464   maxlim: 31488   bits: 16/15
c ---[ 833]---> Adder-cost: 384   maxlim: 28160   bits: 16/15
c ---[ 831]---> Adder-cost: 282   maxlim: 20224   bits: 16/15
c ---[ 829]---> Adder-cost: 264   maxlim: 18816   bits: 16/15
c ---[ 827]---> Adder-cost: 410   maxlim: 27520   bits: 16/15
c ---[ 825]---> Adder-cost: 394   maxlim: 28928   bits: 16/15
c ---[ 823]---> Adder-cost: 331   maxlim: 24320   bits: 16/15
c ---[ 821]---> Adder-cost: 334   maxlim: 23808   bits: 16/15
c ---[ 819]---> Adder-cost: 538   maxlim: 38144   bits: 17/16
c ---[ 817]---> Adder-cost: 368   maxlim: 31488   bits: 16/15
c ---[ 815]---> Adder-cost: 236   maxlim: 18560   bits: 16/15
c ---[ 813]---> Adder-cost: 166   maxlim: 13952   bits: 15/14
c ---[ 811]---> Adder-cost: 276   maxlim: 20608   bits: 16/15
c ---[ 809]---> Adder-cost: 196   maxlim: 13824   bits: 15/14
c ---[ 807]---> Adder-cost: 160   maxlim: 12672   bits: 15/14
c ---[ 805]---> Adder-cost: 82   maxlim: 5760   bits: 14/13
c ---[ 803]---> Adder-cost: 128   maxlim: 8960   bits: 15/14
c ---[ 801]---> Adder-cost: 168   maxlim: 10752   bits: 15/14
c ---[ 799]---> Adder-cost: 120   maxlim: 11264   bits: 15/14
c ---[ 797]---> Adder-cost: 398   maxlim: 33536   bits: 17/16
c ---[ 795]---> Adder-cost: 668   maxlim: 56320   bits: 17/16
c ---[ 793]---> Adder-cost: 182   maxlim: 56320   bits: 17/16
c ---[ 791]---> Adder-cost: 360   maxlim: 23424   bits: 16/15
c ---[ 789]---> Adder-cost: 296   maxlim: 25984   bits: 16/15
c ---[ 787]---> Adder-cost: 374   maxlim: 24576   bits: 16/15
c ---[ 785]---> Adder-cost: 114   maxlim: 24576   bits: 16/15
c ---[ 783]---> Adder-cost: 440   maxlim: 31104   bits: 16/15
c ---[ 781]---> Adder-cost: 342   maxlim: 25600   bits: 16/15
c ---[ 779]---> Adder-cost: 248   maxlim: 16384   bits: 16/15
c ---[ 777]---> Adder-cost: 90   maxlim: 16384   bits: 16/15
c ---[ 775]---> Adder-cost: 260   maxlim: 16640   bits: 16/15
c ---[ 773]---> Adder-cost: 186   maxlim: 13056   bits: 15/14
c ---[ 771]---> Adder-cost: 194   maxlim: 14592   bits: 15/14
c ---[ 769]---> Adder-cost: 78   maxlim: 14592   bits: 15/14
c ---[ 767]---> Adder-cost: 746   maxlim: 51840   bits: 17/16
c ---[ 765]---> Adder-cost: 702   maxlim: 49792   bits: 17/16
c ---[ 763]---> Adder-cost: 430   maxlim: 29824   bits: 16/15
c ---[ 761]---> Adder-cost: 120   maxlim: 29824   bits: 16/15
c ---[ 759]---> Adder-cost: 448   maxlim: 30464   bits: 16/15
c ---[ 757]---> Adder-cost: 340   maxlim: 24192   bits: 16/15
c ---[ 755]---> Adder-cost: 258   maxlim: 16768   bits: 16/15
c ---[ 753]---> Adder-cost: 84   maxlim: 16768   bits: 16/15
c ---[ 751]---> Adder-cost: 244   maxlim: 16000   bits: 15/14
c ---[ 749]---> Adder-cost: 170   maxlim: 12416   bits: 15/14
c ---[ 747]---> Adder-cost: 112   maxlim: 7552   bits: 14/13
c ---[ 745]---> Adder-cost: 48   maxlim: 7552   bits: 14/13
c ---[ 743]---> Adder-cost: 78   maxlim: 6016   bits: 14/13
c ---[ 741]---> Adder-cost: 258   maxlim: 17152   bits: 16/15
c ---[ 739]---> Adder-cost: 210   maxlim: 19456   bits: 16/15
c ---[ 737]---> Adder-cost: 96   maxlim: 19456   bits: 16/15
c ---[ 735]---> Adder-cost: 352   maxlim: 22784   bits: 16/15
c ---[ 733]---> Adder-cost: 106   maxlim: 22784   bits: 16/15
c ---[ 731]---> Adder-cost: 460   maxlim: 31872   bits: 16/15
c ---[ 729]---> Adder-cost: 132   maxlim: 31872   bits: 16/15
c ---[ 727]---> Adder-cost: 314   maxlim: 20352   bits: 16/15
c ---[ 725]---> Adder-cost: 92   maxlim: 20352   bits: 16/15
c ---[ 723]---> Adder-cost: 558   maxlim: 36224   bits: 17/16
c ---[ 721]---> Adder-cost: 142   maxlim: 36224   bits: 17/16
c ---[ 719]---> Adder-cost: 530   maxlim: 35328   bits: 17/16
c ---[ 717]---> Adder-cost: 140   maxlim: 35328   bits: 17/16
c ---[ 715]---> Adder-cost: 470   maxlim: 30720   bits: 16/15
c ---[ 713]---> Adder-cost: 458   maxlim: 30848   bits: 16/15
c ---[ 711]---> Adder-cost: 657   maxlim: 46080   bits: 17/16
c ---[ 709]---> Adder-cost: 160   maxlim: 46080   bits: 17/16
c ---[ 707]---> Adder-cost: 358   maxlim: 22784   bits: 16/15
c ---[ 705]---> Adder-cost: 106   maxlim: 22784   bits: 16/15
c ---[ 703]---> Adder-cost: 326   maxlim: 22016   bits: 16/15
c ---[ 701]---> Adder-cost: 288   maxlim: 21888   bits: 16/15
c ---[ 699]---> Adder-cost: 288   maxlim: 19072   bits: 16/15
c ---[ 697]---> Adder-cost: 94   maxlim: 19072   bits: 16/15
c ---[ 695]---> Adder-cost: 474   maxlim: 30208   bits: 16/15
c ---[ 693]---> Adder-cost: 126   maxlim: 30208   bits: 16/15
c ---[ 691]---> Adder-cost: 420   maxlim: 28928   bits: 16/15
c ---[ 689]---> Adder-cost: 128   maxlim: 28928   bits: 16/15
c ---[ 687]---> Adder-cost: 240   maxlim: 15872   bits: 15/14
c ---[ 685]---> Adder-cost: 78   maxlim: 15872   bits: 15/14
c ---[ 683]---> Adder-cost: 192   maxlim: 12800   bits: 15/14
c ---[ 681]---> Adder-cost: 156   maxlim: 12416   bits: 15/14
c ---[ 679]---> Adder-cost: 176   maxlim: 11904   bits: 15/14
c ---[ 677]---> Adder-cost: 70   maxlim: 11904   bits: 15/14
c ---[ 675]---> Adder-cost: 192   maxlim: 12288   bits: 15/14
c ---[ 673]---> Adder-cost: 110   maxlim: 12160   bits: 15/14
c ---[ 671]---> Adder-cost: 186   maxlim: 12672   bits: 15/14
c ---[ 669]---> Adder-cost: 72   maxlim: 12672   bits: 15/14
c ---[ 667]---> Adder-cost: 156   maxlim: 9856   bits: 15/14
c ---[ 665]---> Adder-cost: 60   maxlim: 9856   bits: 15/14
c ---[ 663]---> Adder-cost: 114   maxlim: 7680   bits: 14/13
c ---[ 661]---> Adder-cost: 66   maxlim: 5760   bits: 14/13
c ---[ 659]---> Adder-cost: 542   maxlim: 40064   bits: 17/16
c ---[ 657]---> Adder-cost: 148   maxlim: 40064   bits: 17/16
c ---[ 655]---> Adder-cost: 682   maxlim: 55424   bits: 17/16
c ---[ 653]---> Adder-cost: 1361   maxlim: 108800   bits: 18/17
c ---[ 651]---> Adder-cost: 284   maxlim: 108800   bits: 18/17
c ---[ 649]---> Adder-cost: 1454   maxlim: 109952   bits: 18/17
c ---[ 647]---> Adder-cost: 286   maxlim: 109952   bits: 18/17
c ---[ 645]---> Adder-cost: 1828   maxlim: 146432   bits: 19/18
c ---[ 643]---> Adder-cost: 334   maxlim: 146432   bits: 19/18
c ---[ 641]---> Adder-cost: 1550   maxlim: 132480   bits: 19/18
c ---[ 639]---> Adder-cost: 322   maxlim: 132480   bits: 19/18
c ---[ 637]---> Adder-cost: 1282   maxlim: 92032   bits: 18/17
c ---[ 635]---> Adder-cost: 248   maxlim: 92032   bits: 18/17
c ---[ 633]---> Adder-cost: 1812   maxlim: 145408   bits: 19/18
c ---[ 631]---> Adder-cost: 1302   maxlim: 125440   bits: 18/17
c ---[ 629]---> Adder-cost: 2158   maxlim: 159104   bits: 19/18
c ---[ 627]---> Adder-cost: 1870   maxlim: 131584   bits: 19/18
c ---[ 625]---> Adder-cost: 1318   maxlim: 97408   bits: 18/17
c ---[ 623]---> Adder-cost: 1530   maxlim: 112128   bits: 18/17
c ---[ 621]---> Adder-cost: 1120   maxlim: 90112   bits: 18/17
c ---[ 619]---> Adder-cost: 1138   maxlim: 84992   bits: 18/17
c ---[ 617]---> Adder-cost: 1032   maxlim: 73728   bits: 18/17
c ---[ 615]---> Adder-cost: 1056   maxlim: 78592   bits: 18/17
c ---[ 613]---> Adder-cost: 1026   maxlim: 78848   bits: 18/17
c ---[ 611]---> Adder-cost: 232   maxlim: 78848   bits: 18/17
c ---[ 609]---> Adder-cost: 1101   maxlim: 87808   bits: 18/17
c ---[ 607]---> Adder-cost: 248   maxlim: 87808   bits: 18/17
c ---[ 605]---> Adder-cost: 926   maxlim: 68736   bits: 18/17
c ---[ 603]---> Adder-cost: 216   maxlim: 68736   bits: 18/17
c ---[ 601]---> Adder-cost: 844   maxlim: 62848   bits: 17/16
c ---[ 599]---> Adder-cost: 194   maxlim: 62848   bits: 17/16
c ---[ 597]---> Adder-cost: 755   maxlim: 56448   bits: 17/16
c ---[ 595]---> Adder-cost: 182   maxlim: 56448   bits: 17/16
c ---[ 593]---> Adder-cost: 182   maxlim: 56448   bits: 17/16
c ---[ 591]---> Adder-cost: 182   maxlim: 56448   bits: 17/16
c ---[ 589]---> Adder-cost: 868   maxlim: 64256   bits: 17/16
c ---[ 587]---> Adder-cost: 198   maxlim: 64256   bits: 17/16
c ---[ 585]---> Adder-cost: 704   maxlim: 52736   bits: 17/16
c ---[ 583]---> Adder-cost: 178   maxlim: 52736   bits: 17/16
c ---[ 581]---> Adder-cost: 178   maxlim: 52736   bits: 17/16
c ---[ 579]---> Adder-cost: 178   maxlim: 52736   bits: 17/16
c ---[ 577]---> Adder-cost: 556   maxlim: 43264   bits: 17/16
c ---[ 575]---> Adder-cost: 156   maxlim: 43264   bits: 17/16
c ---[ 573]---> Adder-cost: 156   maxlim: 43264   bits: 17/16
c ---[ 571]---> Adder-cost: 156   maxlim: 43264   bits: 17/16
c ---[ 569]---> Adder-cost: 412   maxlim: 32640   bits: 16/15
c ---[ 567]---> Adder-cost: 128   maxlim: 32640   bits: 16/15
c ---[ 565]---> Adder-cost: 128   maxlim: 32640   bits: 16/15
c ---[ 563]---> Adder-cost: 128   maxlim: 32640   bits: 16/15
c ---[ 561]---> Adder-cost: 302   maxlim: 19712   bits: 16/15
c ---[ 559]---> Adder-cost: 92   maxlim: 19712   bits: 16/15
c ---[ 557]---> Adder-cost: 172   maxlim: 11904   bits: 15/14
c ---[ 555]---> Adder-cost: 70   maxlim: 11904   bits: 15/14
c ---[ 553]---> Adder-cost: 114   maxlim: 7424   bits: 14/13
c ---[ 551]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[ 549]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[ 547]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[ 545]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[ 543]---> Adder-cost: 331   maxlim: 22912   bits: 16/15
c ---[ 541]---> Adder-cost: 352   maxlim: 24960   bits: 16/15
c ---[ 539]---> Adder-cost: 230   maxlim: 16256   bits: 15/14
c ---[ 537]---> Adder-cost: 74   maxlim: 16256   bits: 15/14
c ---[ 535]---> Adder-cost: 240   maxlim: 15616   bits: 15/14
c ---[ 533]---> Adder-cost: 216   maxlim: 16256   bits: 15/14
c ---[ 531]---> Adder-cost: 374   maxlim: 24448   bits: 16/15
c ---[ 529]---> Adder-cost: 108   maxlim: 24448   bits: 16/15
c ---[ 527]---> Adder-cost: 412   maxlim: 26752   bits: 16/15
c ---[ 525]---> Adder-cost: 374   maxlim: 25472   bits: 16/15
c ---[ 523]---> Adder-cost: 220   maxlim: 15744   bits: 15/14
c ---[ 521]---> Adder-cost: 78   maxlim: 15744   bits: 15/14
c ---[ 519]---> Adder-cost: 322   maxlim: 23680   bits: 16/15
c ---[ 517]---> Adder-cost: 278   maxlim: 19968   bits: 16/15
c ---[ 515]---> Adder-cost: 472   maxlim: 32512   bits: 16/15
c ---[ 513]---> Adder-cost: 128   maxlim: 32512   bits: 16/15
c ---[ 511]---> Adder-cost: 516   maxlim: 37248   bits: 17/16
c ---[ 509]---> Adder-cost: 464   maxlim: 33280   bits: 17/16
c ---[ 507]---> Adder-cost: 388   maxlim: 25856   bits: 16/15
c ---[ 505]---> Adder-cost: 114   maxlim: 25856   bits: 16/15
c ---[ 503]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[ 501]---> Adder-cost: 112   maxlim: 7552   bits: 14/13
c ---[ 499]---> Adder-cost: 48   maxlim: 7552   bits: 14/13
c ---[ 497]---> Adder-cost: 274   maxlim: 18944   bits: 16/15
c ---[ 495]---> Adder-cost: 198   maxlim: 13056   bits: 15/14
c ---[ 493]---> Adder-cost: 196   maxlim: 12416   bits: 15/14
c ---[ 491]---> Adder-cost: 70   maxlim: 12416   bits: 15/14
c ---[ 489]---> Adder-cost: 178   maxlim: 12544   bits: 15/14
c ---[ 487]---> Adder-cost: 154   maxlim: 10752   bits: 15/14
c ---[ 485]---> Adder-cost: 356   maxlim: 27392   bits: 16/15
c ---[ 483]---> Adder-cost: 114   maxlim: 27392   bits: 16/15
c ---[ 481]---> Adder-cost: 466   maxlim: 35712   bits: 17/16
c ---[ 479]---> Adder-cost: 140   maxlim: 35712   bits: 17/16
c ---[ 477]---> Adder-cost: 442   maxlim: 29440   bits: 16/15
c ---[ 475]---> Adder-cost: 126   maxlim: 29440   bits: 16/15
c ---[ 473]---> Adder-cost: 442   maxlim: 29312   bits: 16/15
c ---[ 471]---> Adder-cost: 120   maxlim: 29312   bits: 16/15
c ---[ 469]---> Adder-cost: 594   maxlim: 38016   bits: 17/16
c ---[ 467]---> Adder-cost: 148   maxlim: 38016   bits: 17/16
c ---[ 465]---> Adder-cost: 578   maxlim: 37888   bits: 17/16
c ---[ 463]---> Adder-cost: 324   maxlim: 38016   bits: 17/16
c ---[ 461]---> Adder-cost: 462   maxlim: 30720   bits: 16/15
c ---[ 459]---> Adder-cost: 128   maxlim: 30720   bits: 16/15
c ---[ 457]---> Adder-cost: 500   maxlim: 33664   bits: 17/16
c ---[ 455]---> Adder-cost: 144   maxlim: 33664   bits: 17/16
c ---[ 453]---> Adder-cost: 466   maxlim: 30848   bits: 16/15
c ---[ 451]---> Adder-cost: 128   maxlim: 30848   bits: 16/15
c ---[ 449]---> Adder-cost: 488   maxlim: 33536   bits: 17/16
c ---[ 447]---> Adder-cost: 144   maxlim: 33536   bits: 17/16
c ---[ 445]---> Adder-cost: 536   maxlim: 35200   bits: 17/16
c ---[ 443]---> Adder-cost: 136   maxlim: 35200   bits: 17/16
c ---[ 441]---> Adder-cost: 746   maxlim: 51584   bits: 17/16
c ---[ 439]---> Adder-cost: 168   maxlim: 51584   bits: 17/16
c ---[ 437]---> Adder-cost: 442   maxlim: 30464   bits: 16/15
c ---[ 435]---> Adder-cost: 124   maxlim: 30464   bits: 16/15
c ---[ 433]---> Adder-cost: 536   maxlim: 35456   bits: 17/16
c ---[ 431]---> Adder-cost: 468   maxlim: 33408   bits: 17/16
c ---[ 429]---> Adder-cost: 258   maxlim: 17280   bits: 16/15
c ---[ 427]---> Adder-cost: 88   maxlim: 17280   bits: 16/15
c ---[ 425]---> Adder-cost: 186   maxlim: 11904   bits: 15/14
c ---[ 423]---> Adder-cost: 70   maxlim: 11904   bits: 15/14
c ---[ 421]---> Adder-cost: 212   maxlim: 13952   bits: 15/14
c ---[ 419]---> Adder-cost: 72   maxlim: 13952   bits: 15/14
c ---[ 417]---> Adder-cost: 256   maxlim: 16384   bits: 16/15
c ---[ 415]---> Adder-cost: 90   maxlim: 16384   bits: 16/15
c ---[ 413]---> Adder-cost: 168   maxlim: 11264   bits: 15/14
c ---[ 411]---> Adder-cost: 72   maxlim: 11264   bits: 15/14
c ---[ 409]---> Adder-cost: 158   maxlim: 10368   bits: 15/14
c ---[ 407]---> Adder-cost: 148   maxlim: 9728   bits: 15/14
c ---[ 405]---> Adder-cost: 262   maxlim: 17408   bits: 16/15
c ---[ 403]---> Adder-cost: 246   maxlim: 20992   bits: 16/15
c ---[ 401]---> Adder-cost: 104   maxlim: 20992   bits: 16/15
c ---[ 399]---> Adder-cost: 166   maxlim: 10496   bits: 15/14
c ---[ 397]---> Adder-cost: 68   maxlim: 10496   bits: 15/14
c ---[ 395]---> Adder-cost: 202   maxlim: 14080   bits: 15/14
c ---[ 393]---> Adder-cost: 74   maxlim: 14080   bits: 15/14
c ---[ 391]---> Adder-cost: 394   maxlim: 24576   bits: 16/15
c ---[ 389]---> Adder-cost: 114   maxlim: 24576   bits: 16/15
c ---[ 387]---> Adder-cost: 406   maxlim: 26112   bits: 16/15
c ---[ 385]---> Adder-cost: 114   maxlim: 26112   bits: 16/15
c ---[ 383]---> Adder-cost: 412   maxlim: 27008   bits: 16/15
c ---[ 381]---> Adder-cost: 116   maxlim: 27008   bits: 16/15
c ---[ 379]---> Adder-cost: 437   maxlim: 28672   bits: 16/15
c ---[ 377]---> Adder-cost: 126   maxlim: 28672   bits: 16/15
c ---[ 375]---> Adder-cost: 432   maxlim: 30336   bits: 16/15
c ---[ 373]---> Adder-cost: 124   maxlim: 30336   bits: 16/15
c ---[ 371]---> Adder-cost: 146   maxlim: 9472   bits: 15/14
c ---[ 369]---> Adder-cost: 64   maxlim: 9472   bits: 15/14
c ---[ 367]---> Adder-cost: 78   maxlim: 5248   bits: 14/13
c ---[ 365]---> Adder-cost: 448   maxlim: 35072   bits: 17/16
c ---[ 363]---> Adder-cost: 136   maxlim: 35072   bits: 17/16
c ---[ 361]---> Adder-cost: 576   maxlim: 45824   bits: 17/16
c ---[ 359]---> Adder-cost: 168   maxlim: 45824   bits: 17/16
c ---[ 357]---> Adder-cost: 538   maxlim: 39040   bits: 17/16
c ---[ 355]---> Adder-cost: 154   maxlim: 39040   bits: 17/16
c ---[ 353]---> Adder-cost: 404   maxlim: 26880   bits: 16/15
c ---[ 351]---> Adder-cost: 118   maxlim: 26880   bits: 16/15
c ---[ 349]---> Adder-cost: 410   maxlim: 27904   bits: 16/15
c ---[ 347]---> Adder-cost: 118   maxlim: 27904   bits: 16/15
c ---[ 345]---> Adder-cost: 550   maxlim: 35840   bits: 17/16
c ---[ 343]---> Adder-cost: 150   maxlim: 35840   bits: 17/16
c ---[ 341]---> Adder-cost: 518   maxlim: 34432   bits: 17/16
c ---[ 339]---> Adder-cost: 498   maxlim: 34688   bits: 17/16
c ---[ 337]---> Adder-cost: 582   maxlim: 39552   bits: 17/16
c ---[ 335]---> Adder-cost: 154   maxlim: 39552   bits: 17/16
c ---[ 333]---> Adder-cost: 326   maxlim: 21760   bits: 16/15
c ---[ 331]---> Adder-cost: 106   maxlim: 21760   bits: 16/15
c ---[ 329]---> Adder-cost: 526   maxlim: 34688   bits: 17/16
c ---[ 327]---> Adder-cost: 511   maxlim: 34432   bits: 17/16
c ---[ 325]---> Adder-cost: 362   maxlim: 25984   bits: 16/15
c ---[ 323]---> Adder-cost: 108   maxlim: 25984   bits: 16/15
c ---[ 321]---> Adder-cost: 306   maxlim: 20096   bits: 16/15
c ---[ 319]---> Adder-cost: 94   maxlim: 20096   bits: 16/15
c ---[ 317]---> Adder-cost: 296   maxlim: 19328   bits: 16/15
c ---[ 315]---> Adder-cost: 92   maxlim: 19328   bits: 16/15
c ---[ 313]---> Adder-cost: 328   maxlim: 20864   bits: 16/15
c ---[ 311]---> Adder-cost: 100   maxlim: 20864   bits: 16/15
c ---[ 309]---> Adder-cost: 238   maxlim: 15872   bits: 15/14
c ---[ 307]---> Adder-cost: 176   maxlim: 14336   bits: 15/14
c ---[ 305]---> Adder-cost: 332   maxlim: 21760   bits: 16/15
c ---[ 303]---> Adder-cost: 106   maxlim: 21760   bits: 16/15
c ---[ 301]---> Adder-cost: 322   maxlim: 21888   bits: 16/15
c ---[ 299]---> Adder-cost: 102   maxlim: 21888   bits: 16/15
c ---[ 297]---> Adder-cost: 268   maxlim: 18944   bits: 16/15
c ---[ 295]---> Adder-cost: 96   maxlim: 18944   bits: 16/15
c ---[ 293]---> Adder-cost: 198   maxlim: 14080   bits: 15/14
c ---[ 291]---> Adder-cost: 74   maxlim: 14080   bits: 15/14
c ---[ 289]---> Adder-cost: 188   maxlim: 13056   bits: 15/14
c ---[ 287]---> Adder-cost: 142   maxlim: 9856   bits: 15/14
c ---[ 285]---> Adder-cost: 400   maxlim: 26240   bits: 16/15
c ---[ 283]---> Adder-cost: 346   maxlim: 30208   bits: 16/15
c ---[ 281]---> Adder-cost: 126   maxlim: 30208   bits: 16/15
c ---[ 279]---> Adder-cost: 344   maxlim: 23808   bits: 16/15
c ---[ 277]---> Adder-cost: 106   maxlim: 23808   bits: 16/15
c ---[ 275]---> Adder-cost: 480   maxlim: 32384   bits: 16/15
c ---[ 273]---> Adder-cost: 124   maxlim: 32384   bits: 16/15
c ---[ 271]---> Adder-cost: 432   maxlim: 27776   bits: 16/15
c ---[ 269]---> Adder-cost: 114   maxlim: 27776   bits: 16/15
c ---[ 267]---> Adder-cost: 438   maxlim: 28416   bits: 16/15
c ---[ 265]---> Adder-cost: 118   maxlim: 28416   bits: 16/15
c ---[ 263]---> Adder-cost: 346   maxlim: 22784   bits: 16/15
c ---[ 261]---> Adder-cost: 106   maxlim: 22784   bits: 16/15
c ---[ 259]---> Adder-cost: 290   maxlim: 19840   bits: 16/15
c ---[ 257]---> Adder-cost: 92   maxlim: 19840   bits: 16/15
c ---[ 255]---> Adder-cost: 334   maxlim: 21504   bits: 16/15
c ---[ 253]---> Adder-cost: 102   maxlim: 21504   bits: 16/15
c ---[ 251]---> Adder-cost: 160   maxlim: 10752   bits: 15/14
c ---[ 249]---> Adder-cost: 284   maxlim: 19328   bits: 16/15
c ---[ 247]---> Adder-cost: 92   maxlim: 19328   bits: 16/15
c ---[ 245]---> Adder-cost: 286   maxlim: 19840   bits: 16/15
c ---[ 243]---> Adder-cost: 310   maxlim: 23552   bits: 16/15
c ---[ 241]---> Adder-cost: 278   maxlim: 20352   bits: 16/15
c ---[ 239]---> Adder-cost: 92   maxlim: 20352   bits: 16/15
c ---[ 237]---> Adder-cost: 354   maxlim: 23296   bits: 16/15
c ---[ 235]---> Adder-cost: 382   maxlim: 28416   bits: 16/15
c ---[ 233]---> Adder-cost: 506   maxlim: 34432   bits: 17/16
c ---[ 231]---> Adder-cost: 148   maxlim: 34432   bits: 17/16
c ---[ 229]---> Adder-cost: 448   maxlim: 29824   bits: 16/15
c ---[ 227]---> Adder-cost: 298   maxlim: 26368   bits: 16/15
c ---[ 225]---> Adder-cost: 368   maxlim: 24320   bits: 16/15
c ---[ 223]---> Adder-cost: 110   maxlim: 24320   bits: 16/15
c ---[ 221]---> Adder-cost: 440   maxlim: 30336   bits: 16/15
c ---[ 219]---> Adder-cost: 324   maxlim: 25344   bits: 16/15
c ---[ 217]---> Adder-cost: 296   maxlim: 21120   bits: 16/15
c ---[ 215]---> Adder-cost: 100   maxlim: 21120   bits: 16/15
c ---[ 213]---> Adder-cost: 468   maxlim: 30976   bits: 16/15
c ---[ 211]---> Adder-cost: 410   maxlim: 31360   bits: 16/15
c ---[ 209]---> Adder-cost: 350   maxlim: 24064   bits: 16/15
c ---[ 207]---> Adder-cost: 110   maxlim: 24064   bits: 16/15
c ---[ 205]---> Adder-cost: 326   maxlim: 20992   bits: 16/15
c ---[ 203]---> Adder-cost: 186   maxlim: 13568   bits: 15/14
c ---[ 201]---> Adder-cost: 170   maxlim: 11264   bits: 15/14
c ---[ 199]---> Adder-cost: 72   maxlim: 11264   bits: 15/14
c ---[ 197]---> Adder-cost: 266   maxlim: 17152   bits: 16/15
c ---[ 195]---> Adder-cost: 170   maxlim: 14848   bits: 15/14
c ---[ 193]---> Adder-cost: 148   maxlim: 11392   bits: 15/14
c ---[ 191]---> Adder-cost: 150   maxlim: 11264   bits: 15/14
c ---[ 189]---> Adder-cost: 254   maxlim: 18816   bits: 16/15
c ---[ 187]---> Adder-cost: 290   maxlim: 22912   bits: 16/15
c ---[ 185]---> Adder-cost: 104   maxlim: 22912   bits: 16/15
c ---[ 183]---> Adder-cost: 430   maxlim: 29952   bits: 16/15
c ---[ 181]---> Adder-cost: 546   maxlim: 43136   bits: 17/16
c ---[ 179]---> Adder-cost: 404   maxlim: 29312   bits: 16/15
c ---[ 177]---> Adder-cost: 120   maxlim: 29312   bits: 16/15
c ---[ 175]---> Adder-cost: 260   maxlim: 17664   bits: 16/15
c ---[ 173]---> Adder-cost: 184   maxlim: 16896   bits: 16/15
c ---[ 171]---> Adder-cost: 296   maxlim: 19712   bits: 16/15
c ---[ 169]---> Adder-cost: 92   maxlim: 19712   bits: 16/15
c ---[ 167]---> Adder-cost: 322   maxlim: 22400   bits: 16/15
c ---[ 165]---> Adder-cost: 344   maxlim: 24064   bits: 16/15
c ---[ 163]---> Adder-cost: 538   maxlim: 36608   bits: 17/16
c ---[ 161]---> Adder-cost: 136   maxlim: 36608   bits: 17/16
c ---[ 159]---> Adder-cost: 414   maxlim: 29440   bits: 16/15
c ---[ 157]---> Adder-cost: 338   maxlim: 29184   bits: 16/15
c ---[ 155]---> Adder-cost: 562   maxlim: 38784   bits: 17/16
c ---[ 153]---> Adder-cost: 148   maxlim: 38784   bits: 17/16
c ---[ 151]---> Adder-cost: 568   maxlim: 38784   bits: 17/16
c ---[ 149]---> Adder-cost: 260   maxlim: 31872   bits: 16/15
c ---[ 147]---> Adder-cost: 242   maxlim: 16000   bits: 15/14
c ---[ 145]---> Adder-cost: 78   maxlim: 16000   bits: 15/14
c ---[ 143]---> Adder-cost: 342   maxlim: 23296   bits: 16/15
c ---[ 141]---> Adder-cost: 202   maxlim: 14208   bits: 15/14
c ---[ 139]---> Adder-cost: 138   maxlim: 9984   bits: 15/14
c ---[ 137]---> Adder-cost: 62   maxlim: 9984   bits: 15/14
c ---[ 135]---> Adder-cost: 156   maxlim: 9856   bits: 15/14
c ---[ 133]---> Adder-cost: 114   maxlim: 8064   bits: 14/13
c ---[ 131]---> Adder-cost: 84   maxlim: 6528   bits: 14/13
c ---[ 129]---> Adder-cost: 116   maxlim: 7552   bits: 14/13
c ---[ 127]---> Adder-cost: 94   maxlim: 8320   bits: 15/14
c ---[ 125]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[ 123]---> Adder-cost: 180   maxlim: 11904   bits: 15/14
c ---[ 121]---> Adder-cost: 70   maxlim: 11904   bits: 15/14
c ---[ 119]---> Adder-cost: 284   maxlim: 18816   bits: 16/15
c ---[ 117]---> Adder-cost: 256   maxlim: 18944   bits: 16/15
c ---[ 115]---> Adder-cost: 268   maxlim: 17024   bits: 16/15
c ---[ 113]---> Adder-cost: 88   maxlim: 17024   bits: 16/15
c ---[ 111]---> Adder-cost: 330   maxlim: 21760   bits: 16/15
c ---[ 109]---> Adder-cost: 106   maxlim: 21760   bits: 16/15
c ---[ 107]---> Adder-cost: 351   maxlim: 22784   bits: 16/15
c ---[ 105]---> Adder-cost: 106   maxlim: 22784   bits: 16/15
c ---[ 103]---> Adder-cost: 206   maxlim: 13568   bits: 15/14
c ---[ 101]---> Adder-cost: 78   maxlim: 13568   bits: 15/14
c ---[  99]---> Adder-cost: 266   maxlim: 16512   bits: 16/15
c ---[  97]---> Adder-cost: 90   maxlim: 16512   bits: 16/15
c ---[  95]---> Adder-cost: 274   maxlim: 17280   bits: 16/15
c ---[  93]---> Adder-cost: 88   maxlim: 17280   bits: 16/15
c ---[  91]---> Adder-cost: 88   maxlim: 17280   bits: 16/15
c ---[  89]---> Adder-cost: 170   maxlim: 11136   bits: 15/14
c ---[  87]---> Adder-cost: 68   maxlim: 11136   bits: 15/14
c ---[  85]---> Adder-cost: 104   maxlim: 6400   bits: 14/13
c ---[  83]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[  81]---> Adder-cost: 62   maxlim: 4480   bits: 14/13
c ---[  79]---> Adder-cost: 394   maxlim: 28800   bits: 16/15
c ---[  77]---> Adder-cost: 124   maxlim: 28800   bits: 16/15
c ---[  75]---> Adder-cost: 262   maxlim: 19712   bits: 16/15
c ---[  73]---> Adder-cost: 92   maxlim: 19712   bits: 16/15
c ---[  71]---> Adder-cost: 308   maxlim: 19840   bits: 16/15
c ---[  69]---> Adder-cost: 92   maxlim: 19840   bits: 16/15
c ---[  67]---> Adder-cost: 294   maxlim: 18944   bits: 16/15
c ---[  65]---> Adder-cost: 96   maxlim: 18944   bits: 16/15
c ---[  63]---> Adder-cost: 100   maxlim: 6144   bits: 14/13
c ---[  61]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[  59]---> Adder-cost: 164   maxlim: 10368   bits: 15/14
c ---[  57]---> Adder-cost: 68   maxlim: 10368   bits: 15/14
c ---[  55]---> Adder-cost: 314   maxlim: 20608   bits: 16/15
c ---[  53]---> Adder-cost: 288   maxlim: 20480   bits: 16/15
c ---[  51]---> Adder-cost: 298   maxlim: 19968   bits: 16/15
c ---[  49]---> Adder-cost: 94   maxlim: 19968   bits: 16/15
c ---[  47]---> Adder-cost: 214   maxlim: 13696   bits: 15/14
c ---[  45]---> Adder-cost: 78   maxlim: 13696   bits: 15/14
c ---[  43]---> Adder-cost: 244   maxlim: 15488   bits: 15/14
c ---[  41]---> Adder-cost: 78   maxlim: 15488   bits: 15/14
c ---[  39]---> Adder-cost: 224   maxlim: 14592   bits: 15/14
c ---[  37]---> Adder-cost: 78   maxlim: 14592   bits: 15/14
c ---[  35]---> Adder-cost: 154   maxlim: 11392   bits: 15/14
c ---[  33]---> Adder-cost: 72   maxlim: 11392   bits: 15/14
c ---[  31]---> Adder-cost: 328   maxlim: 23424   bits: 16/15
c ---[  29]---> Adder-cost: 320   maxlim: 25344   bits: 16/15
c ---[  27]---> Adder-cost: 112   maxlim: 25344   bits: 16/15
c ---[  25]---> Adder-cost: 170   maxlim: 11392   bits: 15/14
c ---[  23]---> Adder-cost: 72   maxlim: 11392   bits: 15/14
c ---[  21]---> Adder-cost: 298   maxlim: 18944   bits: 16/15
c ---[  19]---> Adder-cost: 96   maxlim: 18944   bits: 16/15
c ---[  17]---> Adder-cost: 328   maxlim: 21760   bits: 16/15
c ---[  15]---> Adder-cost: 106   maxlim: 21760   bits: 16/15
c ---[  13]---> Adder-cost: 580   maxlim: 39040   bits: 17/16
c ---[  11]---> Adder-cost: 154   maxlim: 39040   bits: 17/16
c ---[   9]---> Adder-cost: 278   maxlim: 18944   bits: 16/15
c ---[   7]---> Adder-cost: 190   maxlim: 18176   bits: 16/15
c ---[   5]---> Adder-cost: 278   maxlim: 17408   bits: 16/15
c ---[   3]---> Adder-cost: 94   maxlim: 17408   bits: 16/15
c ---[   2]---> Adder-cost: 528   maxlim: 30847   bits: 16/15
c ---[   1]---> Adder-cost: 398   maxlim: 16127   bits: 15/14
c ---[   0]---> Adder-cost: 256   maxlim: 14719   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 5696633 20262398 | 1898877       0        0     nan |  0.000 % |
c |       100 | 5696633 20262398 | 2088764     100      304     3.0 |  6.357 % |
c |       250 | 5696633 20262398 | 2297641     250      856     3.4 |  6.357 % |
c |       476 | 5696633 20262398 | 2527405     476     1665     3.5 |  6.357 % |
c |       813 | 5696633 20262398 | 2780145     813     3073     3.8 |  6.357 % |
c |      1319 | 5696633 20262398 | 3058160    1319     5750     4.4 |  6.357 % |
c |      2078 | 5696633 20262398 | 3363976    2078     8883     4.3 |  6.357 % |
c |      3218 | 5696633 20262398 | 3700374    3218    14982     4.7 |  6.357 % |
c |      4926 | 5696633 20262398 | 4070411    4926    23077     4.7 |  6.357 % |
c |      7488 | 5696633 20262398 | 4477452    7488    35500     4.7 |  6.357 % |
c |     11332 | 5696633 20262398 | 4925197   11332    54951     4.8 |  6.357 % |
c |     17098 | 5696633 20262398 | 5417717   17098    95119     5.6 |  6.357 % |
c |     25748 | 5696633 20262398 | 5959489   25748   149996     5.8 |  6.357 % |
c |     38722 | 5696633 20262398 | 6555438   38722   227995     5.9 |  6.357 % |
c |     58183 | 5696551 20262210 | 7210982   58179   368159     6.3 |  6.360 % |
c |     87375 | 5696467 20262014 | 7932080   87352   584444     6.7 |  6.362 % |
/oldhome/oroussel/solvers/minisat+_script: line 16: 13765 CPU time limit exceeded $XDIR/minisat+_bignum_static* "$@"
#### 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.86 0.95 0.90 2/54 13760
Raw data (stat): 13760 (runsolver) R 13759 23514 23513 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784907718 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0017 s]
Raw data (loadavg): 0.88 0.96 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+20.0026 s]
Raw data (loadavg): 0.90 0.96 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+30.002 s]
Raw data (loadavg): 0.91 0.96 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+40.003 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+50.0042 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+60.0046 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+70.0108 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+80.1124 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+90.1134 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+100.113 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+110.114 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+120.115 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+130.115 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+140.115 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+150.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+160.116 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+170.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+180.117 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+190.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+200.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+210.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+220.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+230.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+240.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+250.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+260.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+270.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+280.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+290.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+300.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+310.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+320.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+330.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+340.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+350.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+360.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+370.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+380.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+390.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+400.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+410.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+420.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+430.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+440.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+450.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+460.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+470.143 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+480.143 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+490.143 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+500.144 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+510.145 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+520.145 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+530.145 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+540.146 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+550.146 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+560.252 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+570.253 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+580.253 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+590.253 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+600.253 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+610.254 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+620.254 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+630.254 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+640.255 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+650.255 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+660.255 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+670.255 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+680.256 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+690.257 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+700.257 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+710.258 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+720.257 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+730.258 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+740.258 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+750.26 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+760.259 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+770.26 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+780.26 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+790.261 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+800.26 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+810.261 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+820.261 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+830.261 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+840.261 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+850.262 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+860.262 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+870.262 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+880.262 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+890.262 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+900.262 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+910.262 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+920.263 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+930.264 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+940.264 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+950.264 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+960.264 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+970.265 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+980.265 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+990.266 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1000.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1010.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1020.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1030.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1040.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1050.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1060.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1070.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1080.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1090.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1100.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1110.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1120.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1130.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1140.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1150.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1160.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1170.28 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1180.28 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1190.28 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1200.28 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1210.28 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1220.28 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1230.28 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1230.32 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 13765
Raw data (stat): 13760 (minisat+_script) S 13759 23514 23513 0 -1 0 300 1682 0 0 0 0 28 4 18 0 1 0 784907718 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 0

Child status: 152
Real time (s): 1230.32
CPU time (s): 1230.44
CPU user time (s): 1225.9
CPU system time (s): 4.53531
CPU usage (%): 100.009
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####