PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-dc1l.opb
MD5SUM	4d1c8086316d85cb5ef2a3148b52a8a1
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	85408
Biggest coefficient in the objective function	536870912000000000000
Number of bits for the biggest coefficient in the objective function	69
Sum of the numbers in the objective function	6807849934732110331904
Number of bits of the sum of numbers in the objective function	73
Biggest number in a constraint	536870912000000000000
Number of bits of the biggest number in a constraint	69
Biggest sum of numbers in a constraint	6807849934732110331904
Number of bits of the biggest sum of numbers	73
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.91486
Number of variables	85198
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	35129
Trace number 30961

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-05-25 21:06:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22345 boxname=wulflinc10 idbench=1161 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  4d1c8086316d85cb5ef2a3148b52a8a1  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-dc1l.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-dc1l.opb
IDLAUNCH: 22345
/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:        561840 kB
Buffers:         35540 kB
Cached:         414732 kB
SwapCached:         92 kB
Active:          79284 kB
Inactive:       373620 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        561588 kB
SwapTotal:     2097136 kB
SwapFree:      2096752 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6392 kB
Slab:            14268 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 21:26:53 (client local time) WITH STATUS 152 IN 1230.02 SECONDS
stats: 22345 7 1230.02 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): ssssssssssss
c ---[3296]---> Adder-cost: 204   maxlim: 100352   bits: 18/17
c ---[3294]---> Adder-cost: 72   maxlim: 100352   bits: 18/17
c ---[3292]---> Adder-cost: 196   maxlim: 98304   bits: 18/17
c ---[3290]---> Adder-cost: 70   maxlim: 98304   bits: 18/17
c ---[3288]---> Adder-cost: 120   maxlim: 59392   bits: 17/16
c ---[3286]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[3284]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3282]---> Adder-cost: 162   maxlim: 80896   bits: 18/17
c ---[3280]---> Adder-cost: 366   maxlim: 228352   bits: 19/18
c ---[3278]---> Adder-cost: 280   maxlim: 238592   bits: 19/18
c ---[3276]---> Adder-cost: 1036   maxlim: 534528   bits: 21/20
c ---[3274]---> Adder-cost: 1074   maxlim: 663552   bits: 21/20
c ---[3272]---> Adder-cost: 1174   maxlim: 603136   bits: 21/20
c ---[3270]---> Adder-cost: 686   maxlim: 395264   bits: 20/19
c ---[3268]---> Adder-cost: 508   maxlim: 261120   bits: 19/18
c ---[3266]---> Adder-cost: 490   maxlim: 277504   bits: 20/19
c ---[3264]---> Adder-cost: 306   maxlim: 159744   bits: 19/18
c ---[3262]---> Adder-cost: 222   maxlim: 159744   bits: 19/18
c ---[3260]---> Adder-cost: 238   maxlim: 119808   bits: 18/17
c ---[3258]---> Adder-cost: 170   maxlim: 116736   bits: 18/17
c ---[3256]---> Adder-cost: 292   maxlim: 159744   bits: 19/18
c ---[3254]---> Adder-cost: 300   maxlim: 181248   bits: 19/18
c ---[3252]---> Adder-cost: 532   maxlim: 292864   bits: 20/19
c ---[3250]---> Adder-cost: 498   maxlim: 293888   bits: 20/19
c ---[3248]---> Adder-cost: 356   maxlim: 199680   bits: 19/18
c ---[3246]---> Adder-cost: 300   maxlim: 176128   bits: 19/18
c ---[3244]---> Adder-cost: 560   maxlim: 284672   bits: 20/19
c ---[3242]---> Adder-cost: 398   maxlim: 233472   bits: 19/18
c ---[3240]---> Adder-cost: 222   maxlim: 117760   bits: 18/17
c ---[3238]---> Adder-cost: 208   maxlim: 108544   bits: 18/17
c ---[3236]---> Adder-cost: 322   maxlim: 166912   bits: 19/18
c ---[3234]---> Adder-cost: 224   maxlim: 125952   bits: 18/17
c ---[3232]---> Adder-cost: 240   maxlim: 123904   bits: 18/17
c ---[3230]---> Adder-cost: 182   maxlim: 98304   bits: 18/17
c ---[3228]---> Adder-cost: 406   maxlim: 205824   bits: 19/18
c ---[3226]---> Adder-cost: 242   maxlim: 162816   bits: 19/18
c ---[3224]---> Adder-cost: 184   maxlim: 101376   bits: 18/17
c ---[3222]---> Adder-cost: 160   maxlim: 94208   bits: 18/17
c ---[3220]---> Sorter-cost: 1250     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3218]---> Adder-cost: 178   maxlim: 88064   bits: 18/17
c ---[3216]---> Adder-cost: 164   maxlim: 104448   bits: 18/17
c ---[3214]---> Adder-cost: 202   maxlim: 112640   bits: 18/17
c ---[3212]---> Adder-cost: 316   maxlim: 158720   bits: 19/18
c ---[3210]---> Adder-cost: 92   maxlim: 158720   bits: 19/18
c ---[3208]---> Adder-cost: 308   maxlim: 157696   bits: 19/18
c ---[3206]---> Adder-cost: 414   maxlim: 229376   bits: 19/18
c ---[3204]---> Adder-cost: 410   maxlim: 240640   bits: 19/18
c ---[3202]---> Adder-cost: 120   maxlim: 240640   bits: 19/18
c ---[3200]---> Adder-cost: 430   maxlim: 224256   bits: 19/18
c ---[3198]---> Adder-cost: 334   maxlim: 192512   bits: 19/18
c ---[3196]---> Adder-cost: 268   maxlim: 132096   bits: 19/18
c ---[3194]---> Adder-cost: 90   maxlim: 132096   bits: 19/18
c ---[3192]---> Adder-cost: 274   maxlim: 139264   bits: 19/18
c ---[3190]---> Adder-cost: 152   maxlim: 139264   bits: 19/18
c ---[3188]---> Adder-cost: 292   maxlim: 153600   bits: 19/18
c ---[3186]---> Adder-cost: 92   maxlim: 153600   bits: 19/18
c ---[3184]---> Adder-cost: 362   maxlim: 187392   bits: 19/18
c ---[3182]---> Adder-cost: 346   maxlim: 185344   bits: 19/18
c ---[3180]---> Adder-cost: 382   maxlim: 201728   bits: 19/18
c ---[3178]---> Adder-cost: 114   maxlim: 201728   bits: 19/18
c ---[3176]---> Adder-cost: 254   maxlim: 129024   bits: 18/17
c ---[3174]---> Adder-cost: 184   maxlim: 100352   bits: 18/17
c ---[3172]---> Adder-cost: 222   maxlim: 133120   bits: 19/18
c ---[3170]---> Adder-cost: 272   maxlim: 134144   bits: 19/18
c ---[3168]---> Adder-cost: 84   maxlim: 134144   bits: 19/18
c ---[3166]---> Adder-cost: 206   maxlim: 107520   bits: 18/17
c ---[3164]---> Adder-cost: 202   maxlim: 106496   bits: 18/17
c ---[3162]---> Adder-cost: 118   maxlim: 71680   bits: 18/17
c ---[3160]---> Adder-cost: 182   maxlim: 90112   bits: 18/17
c ---[3158]---> Adder-cost: 72   maxlim: 90112   bits: 18/17
c ---[3156]---> Sorter-cost: 1185     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3154]---> Adder-cost: 412   maxlim: 206848   bits: 19/18
c ---[3152]---> Adder-cost: 114   maxlim: 206848   bits: 19/18
c ---[3150]---> Adder-cost: 166   maxlim: 86016   bits: 18/17
c ---[3148]---> Adder-cost: 66   maxlim: 86016   bits: 18/17
c ---[3146]---> Adder-cost: 204   maxlim: 101376   bits: 18/17
c ---[3144]---> Adder-cost: 72   maxlim: 101376   bits: 18/17
c ---[3142]---> Adder-cost: 290   maxlim: 143360   bits: 19/18
c ---[3140]---> Adder-cost: 90   maxlim: 143360   bits: 19/18
c ---[3138]---> Adder-cost: 492   maxlim: 252928   bits: 19/18
c ---[3136]---> Adder-cost: 360   maxlim: 181248   bits: 19/18
c ---[3134]---> Adder-cost: 126   maxlim: 252928   bits: 19/18
c ---[3132]---> Adder-cost: 338   maxlim: 167936   bits: 19/18
c ---[3130]---> Adder-cost: 104   maxlim: 167936   bits: 19/18
c ---[3128]---> Adder-cost: 306   maxlim: 169984   bits: 19/18
c ---[3126]---> Adder-cost: 102   maxlim: 169984   bits: 19/18
c ---[3124]---> Adder-cost: 276   maxlim: 135168   bits: 19/18
c ---[3122]---> Adder-cost: 88   maxlim: 135168   bits: 19/18
c ---[3120]---> Adder-cost: 222   maxlim: 111616   bits: 18/17
c ---[3118]---> Adder-cost: 72   maxlim: 111616   bits: 18/17
c ---[3116]---> Adder-cost: 202   maxlim: 98304   bits: 18/17
c ---[3114]---> Adder-cost: 430   maxlim: 221184   bits: 19/18
c ---[3112]---> Adder-cost: 70   maxlim: 98304   bits: 18/17
c ---[3110]---> Adder-cost: 162   maxlim: 79872   bits: 18/17
c ---[3108]---> Adder-cost: 62   maxlim: 79872   bits: 18/17
c ---[3106]---> Adder-cost: 110   maxlim: 60416   bits: 17/16
c ---[3104]---> Adder-cost: 48   maxlim: 60416   bits: 17/16
c ---[3102]---> Adder-cost: 380   maxlim: 193536   bits: 19/18
c ---[3100]---> Adder-cost: 108   maxlim: 193536   bits: 19/18
c ---[3098]---> Adder-cost: 492   maxlim: 273408   bits: 20/19
c ---[3096]---> Adder-cost: 142   maxlim: 273408   bits: 20/19
c ---[3094]---> Adder-cost: 542   maxlim: 271360   bits: 20/19
c ---[3092]---> Adder-cost: 116   maxlim: 221184   bits: 19/18
c ---[3090]---> Adder-cost: 140   maxlim: 271360   bits: 20/19
c ---[3088]---> Adder-cost: 626   maxlim: 318464   bits: 20/19
c ---[3086]---> Adder-cost: 152   maxlim: 318464   bits: 20/19
c ---[3084]---> Adder-cost: 428   maxlim: 220160   bits: 19/18
c ---[3082]---> Adder-cost: 110   maxlim: 220160   bits: 19/18
c ---[3080]---> Adder-cost: 400   maxlim: 204800   bits: 19/18
c ---[3078]---> Adder-cost: 118   maxlim: 204800   bits: 19/18
c ---[3076]---> Adder-cost: 358   maxlim: 190464   bits: 19/18
c ---[3074]---> Adder-cost: 106   maxlim: 190464   bits: 19/18
c ---[3072]---> Adder-cost: 314   maxlim: 160768   bits: 19/18
c ---[3070]---> Adder-cost: 284   maxlim: 142336   bits: 19/18
c ---[3068]---> Adder-cost: 94   maxlim: 160768   bits: 19/18
c ---[3066]---> Adder-cost: 256   maxlim: 134144   bits: 19/18
c ---[3064]---> Adder-cost: 178   maxlim: 131072   bits: 19/18
c ---[3062]---> Adder-cost: 276   maxlim: 135168   bits: 19/18
c ---[3060]---> Adder-cost: 360   maxlim: 184320   bits: 19/18
c ---[3058]---> Adder-cost: 104   maxlim: 184320   bits: 19/18
c ---[3056]---> Adder-cost: 932   maxlim: 478208   bits: 20/19
c ---[3054]---> Adder-cost: 184   maxlim: 478208   bits: 20/19
c ---[3052]---> Adder-cost: 396   maxlim: 219136   bits: 19/18
c ---[3050]---> Adder-cost: 114   maxlim: 219136   bits: 19/18
c ---[3048]---> Adder-cost: 92   maxlim: 142336   bits: 19/18
c ---[3046]---> Adder-cost: 336   maxlim: 173056   bits: 19/18
c ---[3044]---> Adder-cost: 100   maxlim: 173056   bits: 19/18
c ---[3042]---> Adder-cost: 342   maxlim: 173056   bits: 19/18
c ---[3040]---> Adder-cost: 250   maxlim: 176128   bits: 19/18
c ---[3038]---> Adder-cost: 422   maxlim: 215040   bits: 19/18
c ---[3036]---> Adder-cost: 118   maxlim: 215040   bits: 19/18
c ---[3034]---> Adder-cost: 302   maxlim: 151552   bits: 19/18
c ---[3032]---> Adder-cost: 96   maxlim: 151552   bits: 19/18
c ---[3030]---> Adder-cost: 366   maxlim: 187392   bits: 19/18
c ---[3028]---> Adder-cost: 102   maxlim: 187392   bits: 19/18
c ---[3026]---> Adder-cost: 282   maxlim: 142336   bits: 19/18
c ---[3024]---> Adder-cost: 560   maxlim: 282624   bits: 20/19
c ---[3022]---> Adder-cost: 140   maxlim: 282624   bits: 20/19
c ---[3020]---> Adder-cost: 396   maxlim: 206848   bits: 19/18
c ---[3018]---> Adder-cost: 374   maxlim: 201728   bits: 19/18
c ---[3016]---> Adder-cost: 438   maxlim: 240640   bits: 19/18
c ---[3014]---> Adder-cost: 120   maxlim: 240640   bits: 19/18
c ---[3012]---> Adder-cost: 362   maxlim: 194560   bits: 19/18
c ---[3010]---> Adder-cost: 110   maxlim: 194560   bits: 19/18
c ---[3008]---> Adder-cost: 312   maxlim: 156672   bits: 19/18
c ---[3006]---> Adder-cost: 264   maxlim: 155648   bits: 19/18
c ---[3004]---> Adder-cost: 92   maxlim: 142336   bits: 19/18
c ---[3002]---> Adder-cost: 336   maxlim: 168960   bits: 19/18
c ---[3000]---> Adder-cost: 100   maxlim: 168960   bits: 19/18
c ---[2998]---> Adder-cost: 364   maxlim: 184320   bits: 19/18
c ---[2996]---> Adder-cost: 104   maxlim: 184320   bits: 19/18
c ---[2994]---> Adder-cost: 240   maxlim: 126976   bits: 18/17
c ---[2992]---> Adder-cost: 78   maxlim: 126976   bits: 18/17
c ---[2990]---> Sorter-cost: 1223     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2988]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2986]---> Adder-cost: 140   maxlim: 66560   bits: 18/17
c ---[2984]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[2982]---> Adder-cost: 252   maxlim: 154624   bits: 19/18
c ---[2980]---> Adder-cost: 154   maxlim: 73728   bits: 18/17
c ---[2978]---> Adder-cost: 62   maxlim: 73728   bits: 18/17
c ---[2976]---> Sorter-cost:  642     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2974]---> Adder-cost: 404   maxlim: 202752   bits: 19/18
c ---[2972]---> Adder-cost: 112   maxlim: 202752   bits: 19/18
c ---[2970]---> Adder-cost: 332   maxlim: 251904   bits: 19/18
c ---[2968]---> Adder-cost: 466   maxlim: 240640   bits: 19/18
c ---[2966]---> Adder-cost: 126   maxlim: 251904   bits: 19/18
c ---[2964]---> Adder-cost: 874   maxlim: 477184   bits: 20/19
c ---[2962]---> Adder-cost: 184   maxlim: 477184   bits: 20/19
c ---[2960]---> Adder-cost: 876   maxlim: 472064   bits: 20/19
c ---[2958]---> Adder-cost: 190   maxlim: 472064   bits: 20/19
c ---[2956]---> Adder-cost: 404   maxlim: 239616   bits: 19/18
c ---[2954]---> Adder-cost: 1208   maxlim: 663552   bits: 21/20
c ---[2952]---> Adder-cost: 234   maxlim: 663552   bits: 21/20
c ---[2950]---> Adder-cost: 1068   maxlim: 607232   bits: 21/20
c ---[2948]---> Adder-cost: 230   maxlim: 607232   bits: 21/20
c ---[2946]---> Adder-cost: 1664   maxlim: 906240   bits: 21/20
c ---[2944]---> Adder-cost: 288   maxlim: 178176   bits: 19/18
c ---[2942]---> Adder-cost: 282   maxlim: 906240   bits: 21/20
c ---[2940]---> Adder-cost: 1996   maxlim: 1088512   bits: 22/21
c ---[2938]---> Adder-cost: 1880   maxlim: 1071104   bits: 22/21
c ---[2936]---> Adder-cost: 1680   maxlim: 934912   bits: 21/20
c ---[2934]---> Adder-cost: 1552   maxlim: 850944   bits: 21/20
c ---[2932]---> Adder-cost: 102   maxlim: 178176   bits: 19/18
c ---[2930]---> Adder-cost: 1408   maxlim: 828416   bits: 21/20
c ---[2928]---> Adder-cost: 1240   maxlim: 706560   bits: 21/20
c ---[2926]---> Adder-cost: 964   maxlim: 532480   bits: 21/20
c ---[2924]---> Adder-cost: 1018   maxlim: 555008   bits: 21/20
c ---[2922]---> Adder-cost: 210   maxlim: 555008   bits: 21/20
c ---[2920]---> Adder-cost: 886   maxlim: 499712   bits: 20/19
c ---[2918]---> Adder-cost: 424   maxlim: 212992   bits: 19/18
c ---[2916]---> Adder-cost: 198   maxlim: 499712   bits: 20/19
c ---[2914]---> Adder-cost: 1086   maxlim: 600064   bits: 21/20
c ---[2912]---> Adder-cost: 230   maxlim: 600064   bits: 21/20
c ---[2910]---> Adder-cost: 1218   maxlim: 658432   bits: 21/20
c ---[2908]---> Adder-cost: 240   maxlim: 658432   bits: 21/20
c ---[2906]---> Adder-cost: 1304   maxlim: 707584   bits: 21/20
c ---[2904]---> Adder-cost: 1014   maxlim: 555008   bits: 21/20
c ---[2902]---> Adder-cost: 210   maxlim: 555008   bits: 21/20
c ---[2900]---> Adder-cost: 122   maxlim: 212992   bits: 19/18
c ---[2898]---> Adder-cost: 698   maxlim: 368640   bits: 20/19
c ---[2896]---> Adder-cost: 160   maxlim: 368640   bits: 20/19
c ---[2894]---> Adder-cost: 718   maxlim: 408576   bits: 20/19
c ---[2892]---> Adder-cost: 170   maxlim: 408576   bits: 20/19
c ---[2890]---> Adder-cost: 636   maxlim: 340992   bits: 20/19
c ---[2888]---> Adder-cost: 350   maxlim: 184320   bits: 19/18
c ---[2886]---> Adder-cost: 152   maxlim: 340992   bits: 20/19
c ---[2884]---> Adder-cost: 716   maxlim: 394240   bits: 20/19
c ---[2882]---> Adder-cost: 166   maxlim: 394240   bits: 20/19
c ---[2880]---> Adder-cost: 612   maxlim: 339968   bits: 20/19
c ---[2878]---> Adder-cost: 154   maxlim: 339968   bits: 20/19
c ---[2876]---> Adder-cost: 264   maxlim: 154624   bits: 19/18
c ---[2874]---> Adder-cost: 104   maxlim: 184320   bits: 19/18
c ---[2872]---> Adder-cost: 92   maxlim: 154624   bits: 19/18
c ---[2870]---> Adder-cost: 190   maxlim: 105472   bits: 18/17
c ---[2868]---> Adder-cost: 74   maxlim: 105472   bits: 18/17
c ---[2866]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2864]---> Adder-cost: 348   maxlim: 174080   bits: 19/18
c ---[2862]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2860]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2858]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2856]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2854]---> Adder-cost: 844   maxlim: 436224   bits: 20/19
c ---[2852]---> Adder-cost: 770   maxlim: 447488   bits: 20/19
c ---[2850]---> Adder-cost: 546   maxlim: 302080   bits: 20/19
c ---[2848]---> Adder-cost: 304   maxlim: 206848   bits: 19/18
c ---[2846]---> Adder-cost: 106   maxlim: 174080   bits: 19/18
c ---[2844]---> Adder-cost: 472   maxlim: 250880   bits: 19/18
c ---[2842]---> Adder-cost: 466   maxlim: 273408   bits: 20/19
c ---[2840]---> Adder-cost: 520   maxlim: 285696   bits: 20/19
c ---[2838]---> Adder-cost: 568   maxlim: 312320   bits: 20/19
c ---[2836]---> Adder-cost: 562   maxlim: 290816   bits: 20/19
c ---[2834]---> Adder-cost: 436   maxlim: 281600   bits: 20/19
c ---[2832]---> Adder-cost: 278   maxlim: 142336   bits: 19/18
c ---[2830]---> Adder-cost: 220   maxlim: 119808   bits: 18/17
c ---[2828]---> Adder-cost: 284   maxlim: 141312   bits: 19/18
c ---[2826]---> Adder-cost: 284   maxlim: 157696   bits: 19/18
c ---[2824]---> Adder-cost: 388   maxlim: 200704   bits: 19/18
c ---[2822]---> Adder-cost: 408   maxlim: 227328   bits: 19/18
c ---[2820]---> Adder-cost: 414   maxlim: 223232   bits: 19/18
c ---[2818]---> Adder-cost: 614   maxlim: 324608   bits: 20/19
c ---[2816]---> Adder-cost: 750   maxlim: 453632   bits: 20/19
c ---[2814]---> Adder-cost: 676   maxlim: 376832   bits: 20/19
c ---[2812]---> Adder-cost: 394   maxlim: 246784   bits: 19/18
c ---[2810]---> Adder-cost: 526   maxlim: 262144   bits: 20/19
c ---[2808]---> Adder-cost: 434   maxlim: 241664   bits: 19/18
c ---[2806]---> Adder-cost: 396   maxlim: 205824   bits: 19/18
c ---[2804]---> Adder-cost: 414   maxlim: 222208   bits: 19/18
c ---[2802]---> Adder-cost: 116   maxlim: 200704   bits: 19/18
c ---[2800]---> Adder-cost: 340   maxlim: 178176   bits: 19/18
c ---[2798]---> Adder-cost: 252   maxlim: 145408   bits: 19/18
c ---[2796]---> Adder-cost: 216   maxlim: 109568   bits: 18/17
c ---[2794]---> Adder-cost: 204   maxlim: 120832   bits: 18/17
c ---[2792]---> Adder-cost: 278   maxlim: 147456   bits: 19/18
c ---[2790]---> Adder-cost: 94   maxlim: 92160   bits: 18/17
c ---[2788]---> Adder-cost: 396   maxlim: 199680   bits: 19/18
c ---[2786]---> Adder-cost: 114   maxlim: 199680   bits: 19/18
c ---[2784]---> Adder-cost: 516   maxlim: 264192   bits: 20/19
c ---[2782]---> Adder-cost: 138   maxlim: 264192   bits: 20/19
c ---[2780]---> Adder-cost: 362   maxlim: 182272   bits: 19/18
c ---[2778]---> Adder-cost: 376   maxlim: 198656   bits: 19/18
c ---[2776]---> Adder-cost: 116   maxlim: 198656   bits: 19/18
c ---[2774]---> Adder-cost: 334   maxlim: 171008   bits: 19/18
c ---[2772]---> Adder-cost: 100   maxlim: 171008   bits: 19/18
c ---[2770]---> Adder-cost: 396   maxlim: 203776   bits: 19/18
c ---[2768]---> Adder-cost: 110   maxlim: 203776   bits: 19/18
c ---[2766]---> Adder-cost: 402   maxlim: 203776   bits: 19/18
c ---[2764]---> Adder-cost: 354   maxlim: 207872   bits: 19/18
c ---[2762]---> Adder-cost: 372   maxlim: 190464   bits: 19/18
c ---[2760]---> Adder-cost: 106   maxlim: 190464   bits: 19/18
c ---[2758]---> Adder-cost: 106   maxlim: 182272   bits: 19/18
c ---[2756]---> Adder-cost: 330   maxlim: 167936   bits: 19/18
c ---[2754]---> Adder-cost: 104   maxlim: 167936   bits: 19/18
c ---[2752]---> Adder-cost: 280   maxlim: 141312   bits: 19/18
c ---[2750]---> Adder-cost: 264   maxlim: 139264   bits: 19/18
c ---[2748]---> Adder-cost: 344   maxlim: 180224   bits: 19/18
c ---[2746]---> Adder-cost: 110   maxlim: 180224   bits: 19/18
c ---[2744]---> Adder-cost: 262   maxlim: 132096   bits: 19/18
c ---[2742]---> Adder-cost: 90   maxlim: 132096   bits: 19/18
c ---[2740]---> Adder-cost: 226   maxlim: 121856   bits: 18/17
c ---[2738]---> Adder-cost: 80   maxlim: 121856   bits: 18/17
c ---[2736]---> Adder-cost: 330   maxlim: 167936   bits: 19/18
c ---[2734]---> Adder-cost: 466   maxlim: 235520   bits: 19/18
c ---[2732]---> Adder-cost: 126   maxlim: 235520   bits: 19/18
c ---[2730]---> Adder-cost: 332   maxlim: 165888   bits: 19/18
c ---[2728]---> Adder-cost: 188   maxlim: 156672   bits: 19/18
c ---[2726]---> Adder-cost: 184   maxlim: 90112   bits: 18/17
c ---[2724]---> Adder-cost: 72   maxlim: 90112   bits: 18/17
c ---[2722]---> Adder-cost: 192   maxlim: 96256   bits: 18/17
c ---[2720]---> Adder-cost: 68   maxlim: 96256   bits: 18/17
c ---[2718]---> Adder-cost: 208   maxlim: 105472   bits: 18/17
c ---[2716]---> Adder-cost: 74   maxlim: 105472   bits: 18/17
c ---[2714]---> Adder-cost: 104   maxlim: 167936   bits: 19/18
c ---[2712]---> Adder-cost: 228   maxlim: 120832   bits: 18/17
c ---[2710]---> Adder-cost: 80   maxlim: 120832   bits: 18/17
c ---[2708]---> Adder-cost: 124   maxlim: 64512   bits: 17/16
c ---[2706]---> Adder-cost: 50   maxlim: 64512   bits: 17/16
c ---[2704]---> Sorter-cost: 1287     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2702]---> Sorter-cost: 1176     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2700]---> Adder-cost: 214   maxlim: 110592   bits: 18/17
c ---[2698]---> Adder-cost: 236   maxlim: 129024   bits: 18/17
c ---[2696]---> Adder-cost: 76   maxlim: 129024   bits: 18/17
c ---[2694]---> Adder-cost: 172   maxlim: 83968   bits: 18/17
c ---[2692]---> Adder-cost: 262   maxlim: 144384   bits: 19/18
c ---[2690]---> Adder-cost: 68   maxlim: 83968   bits: 18/17
c ---[2688]---> Adder-cost: 224   maxlim: 115712   bits: 18/17
c ---[2686]---> Adder-cost: 76   maxlim: 115712   bits: 18/17
c ---[2684]---> Adder-cost: 434   maxlim: 224256   bits: 19/18
c ---[2682]---> Adder-cost: 114   maxlim: 224256   bits: 19/18
c ---[2680]---> Adder-cost: 358   maxlim: 186368   bits: 19/18
c ---[2678]---> Adder-cost: 106   maxlim: 186368   bits: 19/18
c ---[2676]---> Adder-cost: 310   maxlim: 157696   bits: 19/18
c ---[2674]---> Adder-cost: 92   maxlim: 157696   bits: 19/18
c ---[2672]---> Adder-cost: 340   maxlim: 173056   bits: 19/18
c ---[2670]---> Adder-cost: 90   maxlim: 144384   bits: 19/18
c ---[2668]---> Adder-cost: 100   maxlim: 173056   bits: 19/18
c ---[2666]---> Adder-cost: 150   maxlim: 75776   bits: 18/17
c ---[2664]---> Adder-cost: 136   maxlim: 74752   bits: 18/17
c ---[2662]---> Adder-cost: 156   maxlim: 75776   bits: 18/17
c ---[2660]---> Adder-cost: 64   maxlim: 75776   bits: 18/17
c ---[2658]---> Sorter-cost: 1084     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2656]---> Adder-cost: 272   maxlim: 133120   bits: 19/18
c ---[2654]---> Adder-cost: 244   maxlim: 169984   bits: 19/18
c ---[2652]---> Adder-cost: 102   maxlim: 169984   bits: 19/18
c ---[2650]---> Adder-cost: 372   maxlim: 191488   bits: 19/18
c ---[2648]---> Adder-cost: 204   maxlim: 104448   bits: 18/17
c ---[2646]---> Adder-cost: 104   maxlim: 191488   bits: 19/18
c ---[2644]---> Adder-cost: 312   maxlim: 160768   bits: 19/18
c ---[2642]---> Adder-cost: 94   maxlim: 160768   bits: 19/18
c ---[2640]---> Adder-cost: 610   maxlim: 316416   bits: 20/19
c ---[2638]---> Adder-cost: 154   maxlim: 316416   bits: 20/19
c ---[2636]---> Adder-cost: 516   maxlim: 263168   bits: 20/19
c ---[2634]---> Adder-cost: 138   maxlim: 263168   bits: 20/19
c ---[2632]---> Adder-cost: 382   maxlim: 198656   bits: 19/18
c ---[2630]---> Adder-cost: 116   maxlim: 198656   bits: 19/18
c ---[2628]---> Adder-cost: 270   maxlim: 142336   bits: 19/18
c ---[2626]---> Adder-cost: 124   maxlim: 71680   bits: 18/17
c ---[2624]---> Adder-cost: 92   maxlim: 142336   bits: 19/18
c ---[2622]---> Adder-cost: 360   maxlim: 181248   bits: 19/18
c ---[2620]---> Adder-cost: 106   maxlim: 181248   bits: 19/18
c ---[2618]---> Adder-cost: 532   maxlim: 280576   bits: 20/19
c ---[2616]---> Adder-cost: 136   maxlim: 280576   bits: 20/19
c ---[2614]---> Adder-cost: 374   maxlim: 196608   bits: 19/18
c ---[2612]---> Adder-cost: 114   maxlim: 196608   bits: 19/18
c ---[2610]---> Adder-cost: 384   maxlim: 194560   bits: 19/18
c ---[2608]---> Adder-cost: 110   maxlim: 194560   bits: 19/18
c ---[2606]---> Adder-cost: 222   maxlim: 113664   bits: 18/17
c ---[2604]---> Adder-cost: 364   maxlim: 185344   bits: 19/18
c ---[2602]---> Adder-cost: 72   maxlim: 113664   bits: 18/17
c ---[2600]---> Adder-cost: 174   maxlim: 87040   bits: 18/17
c ---[2598]---> Adder-cost: 66   maxlim: 87040   bits: 18/17
c ---[2596]---> Adder-cost: 290   maxlim: 145408   bits: 19/18
c ---[2594]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[2592]---> Adder-cost: 144   maxlim: 74752   bits: 18/17
c ---[2590]---> Adder-cost: 60   maxlim: 74752   bits: 18/17
c ---[2588]---> Adder-cost: 240   maxlim: 120832   bits: 18/17
c ---[2586]---> Adder-cost: 200   maxlim: 119808   bits: 18/17
c ---[2584]---> Adder-cost: 160   maxlim: 84992   bits: 18/17
c ---[2582]---> Adder-cost: 394   maxlim: 198656   bits: 19/18
c ---[2580]---> Adder-cost: 256   maxlim: 224256   bits: 19/18
c ---[2578]---> Adder-cost: 114   maxlim: 224256   bits: 19/18
c ---[2576]---> Adder-cost: 286   maxlim: 149504   bits: 19/18
c ---[2574]---> Adder-cost: 290   maxlim: 168960   bits: 19/18
c ---[2572]---> Adder-cost: 340   maxlim: 172032   bits: 19/18
c ---[2570]---> Adder-cost: 102   maxlim: 172032   bits: 19/18
c ---[2568]---> Adder-cost: 352   maxlim: 185344   bits: 19/18
c ---[2566]---> Adder-cost: 248   maxlim: 154624   bits: 19/18
c ---[2564]---> Adder-cost: 208   maxlim: 103424   bits: 18/17
c ---[2562]---> Adder-cost: 76   maxlim: 103424   bits: 18/17
c ---[2560]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2558]---> Adder-cost: 558   maxlim: 281600   bits: 20/19
c ---[2556]---> Adder-cost: 384   maxlim: 265216   bits: 20/19
c ---[2554]---> Adder-cost: 426   maxlim: 232448   bits: 19/18
c ---[2552]---> Adder-cost: 124   maxlim: 232448   bits: 19/18
c ---[2550]---> Adder-cost: 236   maxlim: 121856   bits: 18/17
c ---[2548]---> Adder-cost: 180   maxlim: 94208   bits: 18/17
c ---[2546]---> Adder-cost: 250   maxlim: 128000   bits: 18/17
c ---[2544]---> Adder-cost: 78   maxlim: 128000   bits: 18/17
c ---[2542]---> Adder-cost: 274   maxlim: 138240   bits: 19/18
c ---[2540]---> Adder-cost: 134   maxlim: 89088   bits: 18/17
c ---[2538]---> Adder-cost: 172   maxlim: 86016   bits: 18/17
c ---[2536]---> Adder-cost: 66   maxlim: 86016   bits: 18/17
c ---[2534]---> Adder-cost: 120   maxlim: 62464   bits: 17/16
c ---[2532]---> Sorter-cost: 1061     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2530]---> Sorter-cost:  597     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2528]---> Adder-cost: 102   maxlim: 185344   bits: 19/18
c ---[2526]---> Adder-cost: 228   maxlim: 115712   bits: 18/17
c ---[2524]---> Adder-cost: 160   maxlim: 118784   bits: 18/17
c ---[2522]---> Adder-cost: 80   maxlim: 118784   bits: 18/17
c ---[2520]---> Adder-cost: 136   maxlim: 65536   bits: 18/17
c ---[2518]---> Adder-cost: 62   maxlim: 65536   bits: 18/17
c ---[2516]---> Adder-cost: 288   maxlim: 145408   bits: 19/18
c ---[2514]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[2512]---> Adder-cost: 312   maxlim: 156672   bits: 19/18
c ---[2510]---> Adder-cost: 96   maxlim: 156672   bits: 19/18
c ---[2508]---> Adder-cost: 288   maxlim: 151552   bits: 19/18
c ---[2506]---> Adder-cost: 214   maxlim: 107520   bits: 18/17
c ---[2504]---> Adder-cost: 78   maxlim: 107520   bits: 18/17
c ---[2502]---> Adder-cost: 208   maxlim: 104448   bits: 18/17
c ---[2500]---> Adder-cost: 74   maxlim: 104448   bits: 18/17
c ---[2498]---> Adder-cost: 234   maxlim: 117760   bits: 18/17
c ---[2496]---> Adder-cost: 76   maxlim: 117760   bits: 18/17
c ---[2494]---> Adder-cost: 222   maxlim: 111616   bits: 18/17
c ---[2492]---> Adder-cost: 72   maxlim: 111616   bits: 18/17
c ---[2490]---> Adder-cost: 248   maxlim: 126976   bits: 18/17
c ---[2488]---> Adder-cost: 78   maxlim: 126976   bits: 18/17
c ---[2486]---> Adder-cost: 242   maxlim: 168960   bits: 19/18
c ---[2484]---> Adder-cost: 170   maxlim: 81920   bits: 18/17
c ---[2482]---> Adder-cost: 68   maxlim: 81920   bits: 18/17
c ---[2480]---> Adder-cost: 136   maxlim: 66560   bits: 18/17
c ---[2478]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[2476]---> Adder-cost: 244   maxlim: 122880   bits: 18/17
c ---[2474]---> Adder-cost: 286   maxlim: 169984   bits: 19/18
c ---[2472]---> Adder-cost: 102   maxlim: 169984   bits: 19/18
c ---[2470]---> Adder-cost: 604   maxlim: 318464   bits: 20/19
c ---[2468]---> Adder-cost: 152   maxlim: 318464   bits: 20/19
c ---[2466]---> Adder-cost: 222   maxlim: 110592   bits: 18/17
c ---[2464]---> Adder-cost: 74   maxlim: 110592   bits: 18/17
c ---[2462]---> Adder-cost: 328   maxlim: 163840   bits: 19/18
c ---[2460]---> Adder-cost: 102   maxlim: 163840   bits: 19/18
c ---[2458]---> Adder-cost: 246   maxlim: 122880   bits: 18/17
c ---[2456]---> Adder-cost: 80   maxlim: 122880   bits: 18/17
c ---[2454]---> Adder-cost: 262   maxlim: 140288   bits: 19/18
c ---[2452]---> Adder-cost: 94   maxlim: 140288   bits: 19/18
c ---[2450]---> Adder-cost: 224   maxlim: 112640   bits: 18/17
c ---[2448]---> Adder-cost: 74   maxlim: 112640   bits: 18/17
c ---[2446]---> Adder-cost: 252   maxlim: 126976   bits: 18/17
c ---[2444]---> Adder-cost: 78   maxlim: 126976   bits: 18/17
c ---[2442]---> Adder-cost: 146   maxlim: 71680   bits: 18/17
c ---[2440]---> Adder-cost: 60   maxlim: 71680   bits: 18/17
c ---[2438]---> Adder-cost: 118   maxlim: 59392   bits: 17/16
c ---[2436]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[2434]---> Adder-cost: 218   maxlim: 108544   bits: 18/17
c ---[2432]---> Adder-cost: 412   maxlim: 251904   bits: 19/18
c ---[2430]---> Adder-cost: 126   maxlim: 251904   bits: 19/18
c ---[2428]---> Adder-cost: 642   maxlim: 325632   bits: 20/19
c ---[2426]---> Adder-cost: 654   maxlim: 352256   bits: 20/19
c ---[2424]---> Adder-cost: 508   maxlim: 284672   bits: 20/19
c ---[2422]---> Adder-cost: 672   maxlim: 380928   bits: 20/19
c ---[2420]---> Adder-cost: 552   maxlim: 278528   bits: 20/19
c ---[2418]---> Adder-cost: 326   maxlim: 272384   bits: 20/19
c ---[2416]---> Adder-cost: 418   maxlim: 221184   bits: 19/18
c ---[2414]---> Adder-cost: 312   maxlim: 178176   bits: 19/18
c ---[2412]---> Adder-cost: 288   maxlim: 154624   bits: 19/18
c ---[2410]---> Adder-cost: 306   maxlim: 166912   bits: 19/18
c ---[2408]---> Adder-cost: 100   maxlim: 168960   bits: 19/18
c ---[2406]---> Adder-cost: 864   maxlim: 442368   bits: 20/19
c ---[2404]---> Adder-cost: 610   maxlim: 482304   bits: 20/19
c ---[2402]---> Adder-cost: 820   maxlim: 462848   bits: 20/19
c ---[2400]---> Adder-cost: 846   maxlim: 458752   bits: 20/19
c ---[2398]---> Adder-cost: 490   maxlim: 269312   bits: 20/19
c ---[2396]---> Adder-cost: 312   maxlim: 165888   bits: 19/18
c ---[2394]---> Adder-cost: 654   maxlim: 342016   bits: 20/19
c ---[2392]---> Adder-cost: 664   maxlim: 344064   bits: 20/19
c ---[2390]---> Adder-cost: 566   maxlim: 294912   bits: 20/19
c ---[2388]---> Adder-cost: 482   maxlim: 288768   bits: 20/19
c ---[2386]---> Adder-cost: 1092   maxlim: 576512   bits: 21/20
c ---[2384]---> Adder-cost: 408   maxlim: 215040   bits: 19/18
c ---[2382]---> Adder-cost: 330   maxlim: 180224   bits: 19/18
c ---[2380]---> Adder-cost: 322   maxlim: 181248   bits: 19/18
c ---[2378]---> Adder-cost: 234   maxlim: 133120   bits: 19/18
c ---[2376]---> Adder-cost: 356   maxlim: 186368   bits: 19/18
c ---[2374]---> Adder-cost: 236   maxlim: 133120   bits: 19/18
c ---[2372]---> Sorter-cost:  642     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2370]---> Sorter-cost:  570     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2368]---> Adder-cost: 104   maxlim: 52224   bits: 17/16
c ---[2366]---> Adder-cost: 210   maxlim: 105472   bits: 18/17
c ---[2364]---> Adder-cost: 634   maxlim: 577536   bits: 21/20
c ---[2362]---> Adder-cost: 270   maxlim: 146432   bits: 19/18
c ---[2360]---> Adder-cost: 252   maxlim: 167936   bits: 19/18
c ---[2358]---> Adder-cost: 276   maxlim: 138240   bits: 19/18
c ---[2356]---> Adder-cost: 88   maxlim: 138240   bits: 19/18
c ---[2354]---> Adder-cost: 412   maxlim: 207872   bits: 19/18
c ---[2352]---> Adder-cost: 464   maxlim: 245760   bits: 19/18
c ---[2350]---> Adder-cost: 372   maxlim: 197632   bits: 19/18
c ---[2348]---> Adder-cost: 112   maxlim: 197632   bits: 19/18
c ---[2346]---> Adder-cost: 378   maxlim: 195584   bits: 19/18
c ---[2344]---> Adder-cost: 338   maxlim: 197632   bits: 19/18
c ---[2342]---> Adder-cost: 262   maxlim: 136192   bits: 19/18
c ---[2340]---> Adder-cost: 88   maxlim: 136192   bits: 19/18
c ---[2338]---> Adder-cost: 284   maxlim: 144384   bits: 19/18
c ---[2336]---> Adder-cost: 100   maxlim: 116736   bits: 18/17
c ---[2334]---> Adder-cost: 118   maxlim: 57344   bits: 17/16
c ---[2332]---> Adder-cost: 52   maxlim: 57344   bits: 17/16
c ---[2330]---> Adder-cost: 240   maxlim: 120832   bits: 18/17
c ---[2328]---> Adder-cost: 304   maxlim: 153600   bits: 19/18
c ---[2326]---> Adder-cost: 282   maxlim: 142336   bits: 19/18
c ---[2324]---> Adder-cost: 92   maxlim: 142336   bits: 19/18
c ---[2322]---> Adder-cost: 358   maxlim: 181248   bits: 19/18
c ---[2320]---> Adder-cost: 224   maxlim: 123904   bits: 18/17
c ---[2318]---> Adder-cost: 188   maxlim: 97280   bits: 18/17
c ---[2316]---> Adder-cost: 64   maxlim: 97280   bits: 18/17
c ---[2314]---> Adder-cost: 270   maxlim: 134144   bits: 19/18
c ---[2312]---> Adder-cost: 222   maxlim: 117760   bits: 18/17
c ---[2310]---> Adder-cost: 154   maxlim: 83968   bits: 18/17
c ---[2308]---> Adder-cost: 134   maxlim: 82944   bits: 18/17
c ---[2306]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[2304]---> Adder-cost: 252   maxlim: 126976   bits: 18/17
c ---[2302]---> Adder-cost: 148   maxlim: 136192   bits: 19/18
c ---[2300]---> Adder-cost: 300   maxlim: 171008   bits: 19/18
c ---[2298]---> Adder-cost: 308   maxlim: 166912   bits: 19/18
c ---[2296]---> Adder-cost: 376   maxlim: 194560   bits: 19/18
c ---[2294]---> Adder-cost: 406   maxlim: 224256   bits: 19/18
c ---[2292]---> Adder-cost: 418   maxlim: 218112   bits: 19/18
c ---[2290]---> Adder-cost: 506   maxlim: 284672   bits: 20/19
c ---[2288]---> Adder-cost: 376   maxlim: 190464   bits: 19/18
c ---[2286]---> Adder-cost: 346   maxlim: 215040   bits: 19/18
c ---[2284]---> Adder-cost: 290   maxlim: 146432   bits: 19/18
c ---[2282]---> Adder-cost: 218   maxlim: 577536   bits: 21/20
c ---[2280]---> Adder-cost: 268   maxlim: 135168   bits: 19/18
c ---[2278]---> Adder-cost: 456   maxlim: 231424   bits: 19/18
c ---[2276]---> Adder-cost: 412   maxlim: 215040   bits: 19/18
c ---[2274]---> Adder-cost: 454   maxlim: 259072   bits: 19/18
c ---[2272]---> Adder-cost: 480   maxlim: 281600   bits: 20/19
c ---[2270]---> Adder-cost: 410   maxlim: 210944   bits: 19/18
c ---[2268]---> Adder-cost: 302   maxlim: 203776   bits: 19/18
c ---[2266]---> Adder-cost: 302   maxlim: 171008   bits: 19/18
c ---[2264]---> Adder-cost: 208   maxlim: 116736   bits: 18/17
c ---[2262]---> Adder-cost: 1136   maxlim: 701440   bits: 21/20
c ---[2260]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2258]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2256]---> Adder-cost: 124   maxlim: 62464   bits: 17/16
c ---[2254]---> Adder-cost: 168   maxlim: 88064   bits: 18/17
c ---[2252]---> Adder-cost: 366   maxlim: 194560   bits: 19/18
c ---[2250]---> Adder-cost: 284   maxlim: 156672   bits: 19/18
c ---[2248]---> Adder-cost: 194   maxlim: 112640   bits: 18/17
c ---[2246]---> Adder-cost: 194   maxlim: 109568   bits: 18/17
c ---[2244]---> Adder-cost: 204   maxlim: 111616   bits: 18/17
c ---[2242]---> Adder-cost: 106   maxlim: 71680   bits: 18/17
c ---[2240]---> Adder-cost: 242   maxlim: 701440   bits: 21/20
c ---[2238]---> Adder-cost: 216   maxlim: 107520   bits: 18/17
c ---[2236]---> Adder-cost: 78   maxlim: 107520   bits: 18/17
c ---[2234]---> Adder-cost: 220   maxlim: 119808   bits: 18/17
c ---[2232]---> Adder-cost: 80   maxlim: 119808   bits: 18/17
c ---[2230]---> Adder-cost: 288   maxlim: 144384   bits: 19/18
c ---[2228]---> Adder-cost: 90   maxlim: 144384   bits: 19/18
c ---[2226]---> Adder-cost: 348   maxlim: 183296   bits: 19/18
c ---[2224]---> Adder-cost: 104   maxlim: 183296   bits: 19/18
c ---[2222]---> Adder-cost: 428   maxlim: 219136   bits: 19/18
c ---[2220]---> Adder-cost: 114   maxlim: 219136   bits: 19/18
c ---[2218]---> Adder-cost: 242   maxlim: 701440   bits: 21/20
c ---[2216]---> Adder-cost: 420   maxlim: 218112   bits: 19/18
c ---[2214]---> Adder-cost: 396   maxlim: 222208   bits: 19/18
c ---[2212]---> Adder-cost: 492   maxlim: 257024   bits: 19/18
c ---[2210]---> Adder-cost: 132   maxlim: 257024   bits: 19/18
c ---[2208]---> Adder-cost: 362   maxlim: 190464   bits: 19/18
c ---[2206]---> Adder-cost: 106   maxlim: 190464   bits: 19/18
c ---[2204]---> Adder-cost: 954   maxlim: 504832   bits: 20/19
c ---[2202]---> Adder-cost: 190   maxlim: 504832   bits: 20/19
c ---[2200]---> Adder-cost: 536   maxlim: 277504   bits: 20/19
c ---[2198]---> Adder-cost: 136   maxlim: 277504   bits: 20/19
c ---[2196]---> Adder-cost: 242   maxlim: 701440   bits: 21/20
c ---[2194]---> Adder-cost: 694   maxlim: 356352   bits: 20/19
c ---[2192]---> Adder-cost: 156   maxlim: 356352   bits: 20/19
c ---[2190]---> Adder-cost: 668   maxlim: 342016   bits: 20/19
c ---[2188]---> Adder-cost: 152   maxlim: 342016   bits: 20/19
c ---[2186]---> Adder-cost: 544   maxlim: 274432   bits: 20/19
c ---[2184]---> Adder-cost: 148   maxlim: 274432   bits: 20/19
c ---[2182]---> Adder-cost: 376   maxlim: 194560   bits: 19/18
c ---[2180]---> Adder-cost: 282   maxlim: 173056   bits: 19/18
c ---[2178]---> Adder-cost: 292   maxlim: 152576   bits: 19/18
c ---[2176]---> Adder-cost: 94   maxlim: 152576   bits: 19/18
c ---[2174]---> Adder-cost: 242   maxlim: 701440   bits: 21/20
c ---[2172]---> Adder-cost: 118   maxlim: 62464   bits: 17/16
c ---[2170]---> Adder-cost: 48   maxlim: 62464   bits: 17/16
c ---[2168]---> Sorter-cost:  733     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2166]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2164]---> Adder-cost: 206   maxlim: 102400   bits: 18/17
c ---[2162]---> Adder-cost: 76   maxlim: 102400   bits: 18/17
c ---[2160]---> Adder-cost: 144   maxlim: 86016   bits: 18/17
c ---[2158]---> Adder-cost: 66   maxlim: 86016   bits: 18/17
c ---[2156]---> Adder-cost: 154   maxlim: 74752   bits: 18/17
c ---[2154]---> Adder-cost: 182   maxlim: 102400   bits: 18/17
c ---[2152]---> Adder-cost: 242   maxlim: 701440   bits: 21/20
c ---[2150]---> Adder-cost: 76   maxlim: 102400   bits: 18/17
c ---[2148]---> Adder-cost: 214   maxlim: 117760   bits: 18/17
c ---[2146]---> Adder-cost: 76   maxlim: 117760   bits: 18/17
c ---[2144]---> Adder-cost: 310   maxlim: 159744   bits: 19/18
c ---[2142]---> Adder-cost: 94   maxlim: 159744   bits: 19/18
c ---[2140]---> Adder-cost: 442   maxlim: 234496   bits: 19/18
c ---[2138]---> Adder-cost: 120   maxlim: 234496   bits: 19/18
c ---[2136]---> Adder-cost: 344   maxlim: 179200   bits: 19/18
c ---[2134]---> Adder-cost: 100   maxlim: 179200   bits: 19/18
c ---[2132]---> Adder-cost: 418   maxlim: 218112   bits: 19/18
c ---[2130]---> Adder-cost: 502   maxlim: 269312   bits: 20/19
c ---[2128]---> Adder-cost: 116   maxlim: 218112   bits: 19/18
c ---[2126]---> Adder-cost: 500   maxlim: 258048   bits: 19/18
c ---[2124]---> Adder-cost: 126   maxlim: 258048   bits: 19/18
c ---[2122]---> Adder-cost: 322   maxlim: 195584   bits: 19/18
c ---[2120]---> Adder-cost: 108   maxlim: 195584   bits: 19/18
c ---[2118]---> Adder-cost: 168   maxlim: 81920   bits: 18/17
c ---[2116]---> Adder-cost: 110   maxlim: 84992   bits: 18/17
c ---[2114]---> Adder-cost: 68   maxlim: 84992   bits: 18/17
c ---[2112]---> Adder-cost: 200   maxlim: 98304   bits: 18/17
c ---[2110]---> Adder-cost: 70   maxlim: 98304   bits: 18/17
c ---[2108]---> Adder-cost: 144   maxlim: 269312   bits: 20/19
c ---[2106]---> Adder-cost: 250   maxlim: 129024   bits: 18/17
c ---[2104]---> Adder-cost: 76   maxlim: 129024   bits: 18/17
c ---[2102]---> Adder-cost: 332   maxlim: 164864   bits: 19/18
c ---[2100]---> Adder-cost: 100   maxlim: 164864   bits: 19/18
c ---[2098]---> Adder-cost: 566   maxlim: 291840   bits: 20/19
c ---[2096]---> Adder-cost: 146   maxlim: 291840   bits: 20/19
c ---[2094]---> Adder-cost: 396   maxlim: 210944   bits: 19/18
c ---[2092]---> Adder-cost: 262   maxlim: 204800   bits: 19/18
c ---[2090]---> Adder-cost: 432   maxlim: 220160   bits: 19/18
c ---[2088]---> Adder-cost: 110   maxlim: 220160   bits: 19/18
c ---[2086]---> Adder-cost: 144   maxlim: 269312   bits: 20/19
c ---[2084]---> Adder-cost: 206   maxlim: 103424   bits: 18/17
c ---[2082]---> Adder-cost: 76   maxlim: 103424   bits: 18/17
c ---[2080]---> Adder-cost: 272   maxlim: 135168   bits: 19/18
c ---[2078]---> Adder-cost: 88   maxlim: 135168   bits: 19/18
c ---[2076]---> Adder-cost: 180   maxlim: 90112   bits: 18/17
c ---[2074]---> Adder-cost: 72   maxlim: 90112   bits: 18/17
c ---[2072]---> Adder-cost: 184   maxlim: 91136   bits: 18/17
c ---[2070]---> Adder-cost: 116   maxlim: 84992   bits: 18/17
c ---[2068]---> Adder-cost: 300   maxlim: 152576   bits: 19/18
c ---[2066]---> Adder-cost: 194   maxlim: 171008   bits: 19/18
c ---[2064]---> Adder-cost: 144   maxlim: 269312   bits: 20/19
c ---[2062]---> Adder-cost: 100   maxlim: 171008   bits: 19/18
c ---[2060]---> Adder-cost: 274   maxlim: 136192   bits: 19/18
c ---[2058]---> Adder-cost: 88   maxlim: 136192   bits: 19/18
c ---[2056]---> Adder-cost: 182   maxlim: 93184   bits: 18/17
c ---[2054]---> Adder-cost: 64   maxlim: 93184   bits: 18/17
c ---[2052]---> Adder-cost: 412   maxlim: 209920   bits: 19/18
c ---[2050]---> Adder-cost: 112   maxlim: 209920   bits: 19/18
c ---[2048]---> Adder-cost: 396   maxlim: 201728   bits: 19/18
c ---[2046]---> Adder-cost: 114   maxlim: 201728   bits: 19/18
c ---[2044]---> Adder-cost: 628   maxlim: 338944   bits: 20/19
c ---[2042]---> Adder-cost: 144   maxlim: 269312   bits: 20/19
c ---[2040]---> Adder-cost: 156   maxlim: 338944   bits: 20/19
c ---[2038]---> Adder-cost: 268   maxlim: 131072   bits: 19/18
c ---[2036]---> Adder-cost: 90   maxlim: 131072   bits: 19/18
c ---[2034]---> Adder-cost: 302   maxlim: 151552   bits: 19/18
c ---[2032]---> Adder-cost: 96   maxlim: 151552   bits: 19/18
c ---[2030]---> Adder-cost: 300   maxlim: 158720   bits: 19/18
c ---[2028]---> Adder-cost: 92   maxlim: 158720   bits: 19/18
c ---[2026]---> Adder-cost: 236   maxlim: 120832   bits: 18/17
c ---[2024]---> Adder-cost: 80   maxlim: 120832   bits: 18/17
c ---[2022]---> Adder-cost: 192   maxlim: 96256   bits: 18/17
c ---[2020]---> Adder-cost: 144   maxlim: 269312   bits: 20/19
c ---[2018]---> Adder-cost: 158   maxlim: 91136   bits: 18/17
c ---[2016]---> Adder-cost: 146   maxlim: 69632   bits: 18/17
c ---[2014]---> Adder-cost: 156   maxlim: 92160   bits: 18/17
c ---[2012]---> Adder-cost: 66   maxlim: 92160   bits: 18/17
c ---[2010]---> Adder-cost: 524   maxlim: 296960   bits: 20/19
c ---[2008]---> Adder-cost: 790   maxlim: 508928   bits: 20/19
c ---[2006]---> Adder-cost: 896   maxlim: 475136   bits: 20/19
c ---[2004]---> Adder-cost: 610   maxlim: 342016   bits: 20/19
c ---[2002]---> Adder-cost: 432   maxlim: 238592   bits: 19/18
c ---[2000]---> Adder-cost: 474   maxlim: 262144   bits: 20/19
c ---[1998]---> Adder-cost: 504   maxlim: 262144   bits: 20/19
c ---[1996]---> Adder-cost: 250   maxlim: 129024   bits: 18/17
c ---[1994]---> Adder-cost: 162   maxlim: 80896   bits: 18/17
c ---[1992]---> Adder-cost: 218   maxlim: 131072   bits: 19/18
c ---[1990]---> Adder-cost: 564   maxlim: 283648   bits: 20/19
c ---[1988]---> Adder-cost: 544   maxlim: 278528   bits: 20/19
c ---[1986]---> Adder-cost: 430   maxlim: 248832   bits: 19/18
c ---[1984]---> Adder-cost: 356   maxlim: 224256   bits: 19/18
c ---[1982]---> Adder-cost: 140   maxlim: 262144   bits: 20/19
c ---[1980]---> Adder-cost: 626   maxlim: 322560   bits: 20/19
c ---[1978]---> Adder-cost: 600   maxlim: 359424   bits: 20/19
c ---[1976]---> Adder-cost: 526   maxlim: 305152   bits: 20/19
c ---[1974]---> Adder-cost: 320   maxlim: 188416   bits: 19/18
c ---[1972]---> Adder-cost: 526   maxlim: 272384   bits: 20/19
c ---[1970]---> Adder-cost: 446   maxlim: 243712   bits: 19/18
c ---[1968]---> Adder-cost: 350   maxlim: 202752   bits: 19/18
c ---[1966]---> Adder-cost: 208   maxlim: 120832   bits: 18/17
c ---[1964]---> Adder-cost: 266   maxlim: 144384   bits: 19/18
c ---[1962]---> Adder-cost: 126   maxlim: 98304   bits: 18/17
c ---[1960]---> Adder-cost: 140   maxlim: 262144   bits: 20/19
c ---[1958]---> Adder-cost: 190   maxlim: 94208   bits: 18/17
c ---[1956]---> Adder-cost: 186   maxlim: 104448   bits: 18/17
c ---[1954]---> Adder-cost: 286   maxlim: 181248   bits: 19/18
c ---[1952]---> Adder-cost: 272   maxlim: 179200   bits: 19/18
c ---[1950]---> Adder-cost: 310   maxlim: 161792   bits: 19/18
c ---[1948]---> Adder-cost: 376   maxlim: 215040   bits: 19/18
c ---[1946]---> Adder-cost: 254   maxlim: 144384   bits: 19/18
c ---[1944]---> Adder-cost: 200   maxlim: 131072   bits: 19/18
c ---[1942]---> Adder-cost: 332   maxlim: 167936   bits: 19/18
c ---[1940]---> Adder-cost: 274   maxlim: 156672   bits: 19/18
c ---[1938]---> Adder-cost: 140   maxlim: 262144   bits: 20/19
c ---[1936]---> Adder-cost: 318   maxlim: 163840   bits: 19/18
c ---[1934]---> Adder-cost: 350   maxlim: 193536   bits: 19/18
c ---[1932]---> Adder-cost: 382   maxlim: 233472   bits: 19/18
c ---[1930]---> Adder-cost: 462   maxlim: 283648   bits: 20/19
c ---[1928]---> Adder-cost: 520   maxlim: 300032   bits: 20/19
c ---[1926]---> Adder-cost: 394   maxlim: 208896   bits: 19/18
c ---[1924]---> Adder-cost: 692   maxlim: 377856   bits: 20/19
c ---[1922]---> Adder-cost: 630   maxlim: 339968   bits: 20/19
c ---[1920]---> Adder-cost: 572   maxlim: 358400   bits: 20/19
c ---[1918]---> Adder-cost: 508   maxlim: 286720   bits: 20/19
c ---[1916]---> Adder-cost: 140   maxlim: 262144   bits: 20/19
c ---[1914]---> Adder-cost: 404   maxlim: 210944   bits: 19/18
c ---[1912]---> Adder-cost: 250   maxlim: 162816   bits: 19/18
c ---[1910]---> Adder-cost: 188   maxlim: 95232   bits: 18/17
c ---[1908]---> Adder-cost: 194   maxlim: 107520   bits: 18/17
c ---[1906]---> Adder-cost: 368   maxlim: 192512   bits: 19/18
c ---[1904]---> Adder-cost: 236   maxlim: 130048   bits: 18/17
c ---[1902]---> Adder-cost: 150   maxlim: 82944   bits: 18/17
c ---[1900]---> Adder-cost: 156   maxlim: 80896   bits: 18/17
c ---[1898]---> Adder-cost: 184   maxlim: 92160   bits: 18/17
c ---[1896]---> Sorter-cost: 1185     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1894]---> Adder-cost: 140   maxlim: 262144   bits: 20/19
c ---[1892]---> Adder-cost: 284   maxlim: 140288   bits: 19/18
c ---[1890]---> Adder-cost: 94   maxlim: 140288   bits: 19/18
c ---[1888]---> Adder-cost: 344   maxlim: 178176   bits: 19/18
c ---[1886]---> Adder-cost: 102   maxlim: 178176   bits: 19/18
c ---[1884]---> Adder-cost: 288   maxlim: 143360   bits: 19/18
c ---[1882]---> Adder-cost: 90   maxlim: 143360   bits: 19/18
c ---[1880]---> Adder-cost: 90   maxlim: 143360   bits: 19/18
c ---[1878]---> Adder-cost: 90   maxlim: 143360   bits: 19/18
c ---[1876]---> Adder-cost: 240   maxlim: 122880   bits: 18/17
c ---[1874]---> Adder-cost: 80   maxlim: 122880   bits: 18/17
c ---[1872]---> Adder-cost: 448   maxlim: 241664   bits: 19/18
c ---[1870]---> Adder-cost: 96   maxlim: 52224   bits: 17/16
c ---[1868]---> Adder-cost: 44   maxlim: 52224   bits: 17/16
c ---[1866]---> Adder-cost: 252   maxlim: 126976   bits: 18/17
c ---[1864]---> Adder-cost: 78   maxlim: 126976   bits: 18/17
c ---[1862]---> Adder-cost: 362   maxlim: 187392   bits: 19/18
c ---[1860]---> Adder-cost: 340   maxlim: 188416   bits: 19/18
c ---[1858]---> Adder-cost: 376   maxlim: 190464   bits: 19/18
c ---[1856]---> Adder-cost: 106   maxlim: 190464   bits: 19/18
c ---[1854]---> Adder-cost: 106   maxlim: 190464   bits: 19/18
c ---[1852]---> Adder-cost: 106   maxlim: 190464   bits: 19/18
c ---[1850]---> Adder-cost: 126   maxlim: 241664   bits: 19/18
c ---[1848]---> Adder-cost: 198   maxlim: 100352   bits: 18/17
c ---[1846]---> Adder-cost: 122   maxlim: 97280   bits: 18/17
c ---[1844]---> Adder-cost: 96   maxlim: 54272   bits: 17/16
c ---[1842]---> Adder-cost: 46   maxlim: 54272   bits: 17/16
c ---[1840]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1838]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1836]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1834]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1832]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1830]---> Adder-cost: 270   maxlim: 134144   bits: 19/18
c ---[1828]---> Adder-cost: 84   maxlim: 134144   bits: 19/18
c ---[1826]---> Adder-cost: 232   maxlim: 118784   bits: 18/17
c ---[1824]---> Adder-cost: 80   maxlim: 118784   bits: 18/17
c ---[1822]---> Adder-cost: 80   maxlim: 118784   bits: 18/17
c ---[1820]---> Adder-cost: 80   maxlim: 118784   bits: 18/17
c ---[1818]---> Adder-cost: 106   maxlim: 51200   bits: 17/16
c ---[1816]---> Adder-cost: 150   maxlim: 74752   bits: 18/17
c ---[1814]---> Adder-cost: 60   maxlim: 74752   bits: 18/17
c ---[1812]---> Adder-cost: 330   maxlim: 165888   bits: 19/18
c ---[1810]---> Adder-cost: 262   maxlim: 166912   bits: 19/18
c ---[1808]---> Adder-cost: 522   maxlim: 263168   bits: 20/19
c ---[1806]---> Adder-cost: 138   maxlim: 263168   bits: 20/19
c ---[1804]---> Adder-cost: 316   maxlim: 164864   bits: 19/18
c ---[1802]---> Adder-cost: 100   maxlim: 164864   bits: 19/18
c ---[1800]---> Adder-cost: 218   maxlim: 123904   bits: 18/17
c ---[1798]---> Adder-cost: 78   maxlim: 123904   bits: 18/17
c ---[1796]---> Adder-cost: 222   maxlim: 111616   bits: 18/17
c ---[1794]---> Adder-cost: 178   maxlim: 109568   bits: 18/17
c ---[1792]---> Adder-cost: 212   maxlim: 110592   bits: 18/17
c ---[1790]---> Adder-cost: 74   maxlim: 110592   bits: 18/17
c ---[1788]---> Adder-cost: 350   maxlim: 177152   bits: 19/18
c ---[1786]---> Adder-cost: 100   maxlim: 177152   bits: 19/18
c ---[1784]---> Adder-cost: 244   maxlim: 129024   bits: 18/17
c ---[1782]---> Adder-cost: 76   maxlim: 129024   bits: 18/17
c ---[1780]---> Adder-cost: 278   maxlim: 142336   bits: 19/18
c ---[1778]---> Adder-cost: 92   maxlim: 142336   bits: 19/18
c ---[1776]---> Adder-cost: 188   maxlim: 97280   bits: 18/17
c ---[1774]---> Adder-cost: 64   maxlim: 97280   bits: 18/17
c ---[1772]---> Adder-cost: 244   maxlim: 126976   bits: 18/17
c ---[1770]---> Adder-cost: 78   maxlim: 126976   bits: 18/17
c ---[1768]---> Adder-cost: 126   maxlim: 241664   bits: 19/18
c ---[1766]---> Adder-cost: 206   maxlim: 104448   bits: 18/17
c ---[1764]---> Adder-cost: 176   maxlim: 93184   bits: 18/17
c ---[1762]---> Adder-cost: 90   maxlim: 54272   bits: 17/16
c ---[1760]---> Adder-cost: 376   maxlim: 188416   bits: 19/18
c ---[1758]---> Adder-cost: 106   maxlim: 188416   bits: 19/18
c ---[1756]---> Adder-cost: 274   maxlim: 135168   bits: 19/18
c ---[1754]---> Adder-cost: 88   maxlim: 135168   bits: 19/18
c ---[1752]---> Adder-cost: 88   maxlim: 135168   bits: 19/18
c ---[1750]---> Adder-cost: 88   maxlim: 135168   bits: 19/18
c ---[1748]---> Adder-cost: 270   maxlim: 132096   bits: 19/18
c ---[1746]---> Adder-cost: 584   maxlim: 307200   bits: 20/19
c ---[1744]---> Adder-cost: 90   maxlim: 132096   bits: 19/18
c ---[1742]---> Adder-cost: 138   maxlim: 80896   bits: 18/17
c ---[1740]---> Adder-cost: 62   maxlim: 80896   bits: 18/17
c ---[1738]---> Adder-cost: 288   maxlim: 145408   bits: 19/18
c ---[1736]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[1734]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[1732]---> Adder-cost: 372   maxlim: 194560   bits: 19/18
c ---[1730]---> Adder-cost: 110   maxlim: 194560   bits: 19/18
c ---[1728]---> Adder-cost: 244   maxlim: 123904   bits: 18/17
c ---[1726]---> Adder-cost: 78   maxlim: 123904   bits: 18/17
c ---[1724]---> Adder-cost: 146   maxlim: 307200   bits: 20/19
c ---[1722]---> Adder-cost: 78   maxlim: 123904   bits: 18/17
c ---[1720]---> Adder-cost: 78   maxlim: 123904   bits: 18/17
c ---[1718]---> Adder-cost: 130   maxlim: 68608   bits: 18/17
c ---[1716]---> Adder-cost: 106   maxlim: 51200   bits: 17/16
c ---[1714]---> Adder-cost: 176   maxlim: 90112   bits: 18/17
c ---[1712]---> Adder-cost: 128   maxlim: 84992   bits: 18/17
c ---[1710]---> Adder-cost: 414   maxlim: 210944   bits: 19/18
c ---[1708]---> Adder-cost: 380   maxlim: 197632   bits: 19/18
c ---[1706]---> Adder-cost: 194   maxlim: 112640   bits: 18/17
c ---[1704]---> Adder-cost: 138   maxlim: 83968   bits: 18/17
c ---[1702]---> Adder-cost: 202   maxlim: 104448   bits: 18/17
c ---[1700]---> Adder-cost: 252   maxlim: 129024   bits: 18/17
c ---[1698]---> Adder-cost: 76   maxlim: 129024   bits: 18/17
c ---[1696]---> Adder-cost: 362   maxlim: 186368   bits: 19/18
c ---[1694]---> Adder-cost: 106   maxlim: 186368   bits: 19/18
c ---[1692]---> Adder-cost: 284   maxlim: 139264   bits: 19/18
c ---[1690]---> Adder-cost: 94   maxlim: 139264   bits: 19/18
c ---[1688]---> Adder-cost: 94   maxlim: 139264   bits: 19/18
c ---[1686]---> Adder-cost: 94   maxlim: 139264   bits: 19/18
c ---[1684]---> Adder-cost: 326   maxlim: 168960   bits: 19/18
c ---[1682]---> Adder-cost: 298   maxlim: 166912   bits: 19/18
c ---[1680]---> Sorter-cost: 1287     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1678]---> Adder-cost: 112   maxlim: 56320   bits: 17/16
c ---[1676]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[1674]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[1672]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[1670]---> Adder-cost: 234   maxlim: 117760   bits: 18/17
c ---[1668]---> Adder-cost: 76   maxlim: 117760   bits: 18/17
c ---[1666]---> Adder-cost: 136   maxlim: 66560   bits: 18/17
c ---[1664]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[1662]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[1660]---> Adder-cost: 144   maxlim: 70656   bits: 18/17
c ---[1658]---> Adder-cost: 60   maxlim: 70656   bits: 18/17
c ---[1656]---> Adder-cost: 60   maxlim: 70656   bits: 18/17
c ---[1654]---> Adder-cost: 244   maxlim: 125952   bits: 18/17
c ---[1652]---> Adder-cost: 78   maxlim: 125952   bits: 18/17
c ---[1650]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1648]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1646]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1644]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1642]---> Adder-cost: 146   maxlim: 307200   bits: 20/19
c ---[1640]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1638]---> Sorter-cost:  937     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1636]---> Adder-cost: 118   maxlim: 58368   bits: 17/16
c ---[1634]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[1632]---> Adder-cost: 570   maxlim: 287744   bits: 20/19
c ---[1630]---> Adder-cost: 150   maxlim: 287744   bits: 20/19
c ---[1628]---> Adder-cost: 818   maxlim: 435200   bits: 20/19
c ---[1626]---> Adder-cost: 182   maxlim: 435200   bits: 20/19
c ---[1624]---> Adder-cost: 796   maxlim: 408576   bits: 20/19
c ---[1622]---> Adder-cost: 170   maxlim: 408576   bits: 20/19
c ---[1620]---> Adder-cost: 1024   maxlim: 553984   bits: 21/20
c ---[1618]---> Adder-cost: 360   maxlim: 185344   bits: 19/18
c ---[1616]---> Adder-cost: 102   maxlim: 185344   bits: 19/18
c ---[1614]---> Adder-cost: 394   maxlim: 228352   bits: 19/18
c ---[1612]---> Adder-cost: 412   maxlim: 227328   bits: 19/18
c ---[1610]---> Adder-cost: 332   maxlim: 193536   bits: 19/18
c ---[1608]---> Adder-cost: 108   maxlim: 193536   bits: 19/18
c ---[1606]---> Adder-cost: 284   maxlim: 139264   bits: 19/18
c ---[1604]---> Adder-cost: 94   maxlim: 139264   bits: 19/18
c ---[1602]---> Adder-cost: 104   maxlim: 52224   bits: 17/16
c ---[1600]---> Adder-cost: 44   maxlim: 52224   bits: 17/16
c ---[1598]---> Adder-cost: 630   maxlim: 528384   bits: 21/20
c ---[1596]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1594]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1592]---> Adder-cost: 166   maxlim: 81920   bits: 18/17
c ---[1590]---> Adder-cost: 68   maxlim: 81920   bits: 18/17
c ---[1588]---> Adder-cost: 98   maxlim: 56320   bits: 17/16
c ---[1586]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[1584]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1582]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1580]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1578]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1576]---> Adder-cost: 208   maxlim: 528384   bits: 21/20
c ---[1574]---> Adder-cost: 156   maxlim: 75776   bits: 18/17
c ---[1572]---> Adder-cost: 186   maxlim: 108544   bits: 18/17
c ---[1570]---> Adder-cost: 494   maxlim: 250880   bits: 19/18
c ---[1568]---> Adder-cost: 440   maxlim: 258048   bits: 19/18
c ---[1566]---> Adder-cost: 224   maxlim: 116736   bits: 18/17
c ---[1564]---> Adder-cost: 182   maxlim: 106496   bits: 18/17
c ---[1562]---> Adder-cost: 172   maxlim: 88064   bits: 18/17
c ---[1560]---> Adder-cost: 222   maxlim: 110592   bits: 18/17
c ---[1558]---> Adder-cost: 74   maxlim: 110592   bits: 18/17
c ---[1556]---> Adder-cost: 252   maxlim: 130048   bits: 18/17
c ---[1554]---> Adder-cost: 208   maxlim: 528384   bits: 21/20
c ---[1552]---> Adder-cost: 74   maxlim: 130048   bits: 18/17
c ---[1550]---> Adder-cost: 536   maxlim: 271360   bits: 20/19
c ---[1548]---> Adder-cost: 140   maxlim: 271360   bits: 20/19
c ---[1546]---> Adder-cost: 140   maxlim: 271360   bits: 20/19
c ---[1544]---> Adder-cost: 140   maxlim: 271360   bits: 20/19
c ---[1542]---> Adder-cost: 132   maxlim: 75776   bits: 18/17
c ---[1540]---> Sorter-cost:  642     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1538]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1536]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1534]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1532]---> Adder-cost: 208   maxlim: 528384   bits: 21/20
c ---[1530]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1528]---> Adder-cost: 228   maxlim: 115712   bits: 18/17
c ---[1526]---> Adder-cost: 76   maxlim: 115712   bits: 18/17
c ---[1524]---> Adder-cost: 84   maxlim: 51200   bits: 17/16
c ---[1522]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[1520]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1518]---> Adder-cost: 154   maxlim: 75776   bits: 18/17
c ---[1516]---> Adder-cost: 64   maxlim: 75776   bits: 18/17
c ---[1514]---> Adder-cost: 666   maxlim: 344064   bits: 20/19
c ---[1512]---> Adder-cost: 552   maxlim: 326656   bits: 20/19
c ---[1510]---> Adder-cost: 208   maxlim: 528384   bits: 21/20
c ---[1508]---> Adder-cost: 510   maxlim: 290816   bits: 20/19
c ---[1506]---> Adder-cost: 146   maxlim: 290816   bits: 20/19
c ---[1504]---> Adder-cost: 488   maxlim: 254976   bits: 19/18
c ---[1502]---> Adder-cost: 276   maxlim: 193536   bits: 19/18
c ---[1500]---> Adder-cost: 240   maxlim: 136192   bits: 19/18
c ---[1498]---> Adder-cost: 88   maxlim: 136192   bits: 19/18
c ---[1496]---> Adder-cost: 112   maxlim: 55296   bits: 17/16
c ---[1494]---> Adder-cost: 230   maxlim: 116736   bits: 18/17
c ---[1492]---> Adder-cost: 78   maxlim: 116736   bits: 18/17
c ---[1490]---> Adder-cost: 220   maxlim: 110592   bits: 18/17
c ---[1488]---> Adder-cost: 560   maxlim: 349184   bits: 20/19
c ---[1486]---> Adder-cost: 74   maxlim: 110592   bits: 18/17
c ---[1484]---> Adder-cost: 172   maxlim: 83968   bits: 18/17
c ---[1482]---> Adder-cost: 68   maxlim: 83968   bits: 18/17
c ---[1480]---> Adder-cost: 488   maxlim: 253952   bits: 19/18
c ---[1478]---> Adder-cost: 132   maxlim: 253952   bits: 19/18
c ---[1476]---> Adder-cost: 156   maxlim: 78848   bits: 18/17
c ---[1474]---> Adder-cost: 196   maxlim: 100352   bits: 18/17
c ---[1472]---> Adder-cost: 72   maxlim: 100352   bits: 18/17
c ---[1470]---> Adder-cost: 466   maxlim: 237568   bits: 19/18
c ---[1468]---> Adder-cost: 384   maxlim: 214016   bits: 19/18
c ---[1466]---> Adder-cost: 426   maxlim: 237568   bits: 19/18
c ---[1464]---> Adder-cost: 128   maxlim: 237568   bits: 19/18
c ---[1462]---> Adder-cost: 470   maxlim: 250880   bits: 19/18
c ---[1460]---> Adder-cost: 460   maxlim: 250880   bits: 19/18
c ---[1458]---> Adder-cost: 484   maxlim: 264192   bits: 20/19
c ---[1456]---> Adder-cost: 138   maxlim: 264192   bits: 20/19
c ---[1454]---> Adder-cost: 160   maxlim: 90112   bits: 18/17
c ---[1452]---> Sorter-cost: 1185     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1450]---> Adder-cost: 118   maxlim: 57344   bits: 17/16
c ---[1448]---> Adder-cost: 52   maxlim: 57344   bits: 17/16
c ---[1446]---> Adder-cost: 306   maxlim: 151552   bits: 19/18
c ---[1444]---> Adder-cost: 96   maxlim: 151552   bits: 19/18
c ---[1442]---> Adder-cost: 276   maxlim: 157696   bits: 19/18
c ---[1440]---> Adder-cost: 92   maxlim: 157696   bits: 19/18
c ---[1438]---> Adder-cost: 570   maxlim: 286720   bits: 20/19
c ---[1436]---> Adder-cost: 496   maxlim: 285696   bits: 20/19
c ---[1434]---> Adder-cost: 454   maxlim: 271360   bits: 20/19
c ---[1432]---> Adder-cost: 140   maxlim: 271360   bits: 20/19
c ---[1430]---> Adder-cost: 544   maxlim: 278528   bits: 20/19
c ---[1428]---> Adder-cost: 148   maxlim: 278528   bits: 20/19
c ---[1426]---> Adder-cost: 672   maxlim: 351232   bits: 20/19
c ---[1424]---> Adder-cost: 152   maxlim: 351232   bits: 20/19
c ---[1422]---> Adder-cost: 400   maxlim: 200704   bits: 19/18
c ---[1420]---> Adder-cost: 116   maxlim: 200704   bits: 19/18
c ---[1418]---> Adder-cost: 454   maxlim: 234496   bits: 19/18
c ---[1416]---> Adder-cost: 348   maxlim: 193536   bits: 19/18
c ---[1414]---> Adder-cost: 108   maxlim: 193536   bits: 19/18
c ---[1412]---> Adder-cost: 288   maxlim: 146432   bits: 19/18
c ---[1410]---> Adder-cost: 88   maxlim: 146432   bits: 19/18
c ---[1408]---> Adder-cost: 238   maxlim: 122880   bits: 18/17
c ---[1406]---> Adder-cost: 80   maxlim: 122880   bits: 18/17
c ---[1404]---> Adder-cost: 204   maxlim: 102400   bits: 18/17
c ---[1402]---> Adder-cost: 132   maxlim: 99328   bits: 18/17
c ---[1400]---> Adder-cost: 140   maxlim: 75776   bits: 18/17
c ---[1398]---> Adder-cost: 426   maxlim: 212992   bits: 19/18
c ---[1396]---> Adder-cost: 122   maxlim: 212992   bits: 19/18
c ---[1394]---> Adder-cost: 548   maxlim: 293888   bits: 20/19
c ---[1392]---> Adder-cost: 376   maxlim: 306176   bits: 20/19
c ---[1390]---> Adder-cost: 146   maxlim: 306176   bits: 20/19
c ---[1388]---> Adder-cost: 722   maxlim: 386048   bits: 20/19
c ---[1386]---> Adder-cost: 562   maxlim: 387072   bits: 20/19
c ---[1384]---> Adder-cost: 160   maxlim: 387072   bits: 20/19
c ---[1382]---> Adder-cost: 736   maxlim: 398336   bits: 20/19
c ---[1380]---> Adder-cost: 178   maxlim: 398336   bits: 20/19
c ---[1378]---> Adder-cost: 178   maxlim: 398336   bits: 20/19
c ---[1376]---> Adder-cost: 496   maxlim: 275456   bits: 20/19
c ---[1374]---> Adder-cost: 148   maxlim: 275456   bits: 20/19
c ---[1372]---> Adder-cost: 148   maxlim: 275456   bits: 20/19
c ---[1370]---> Adder-cost: 890   maxlim: 506880   bits: 20/19
c ---[1368]---> Adder-cost: 192   maxlim: 506880   bits: 20/19
c ---[1363]---> Adder-cost: 7502   maxlim: 4320256   bits: 24/23
c ---[1356]---> Adder-cost: 156951   maxlim: 351637503   bits: 30/29
c ---[1354]---> Adder-cost: 90410   maxlim: 300771327   bits: 30/29
c ---[1350]---> Adder-cost: 192   maxlim: 506880   bits: 20/19
c ---[1348]---> Adder-cost: 724   maxlim: 423936   bits: 20/19
c ---[1346]---> Adder-cost: 172   maxlim: 423936   bits: 20/19
c ---[1344]---> Adder-cost: 172   maxlim: 423936   bits: 20/19
c ---[1342]---> Adder-cost: 448   maxlim: 246784   bits: 19/18
c ---[1340]---> Adder-cost: 128   maxlim: 246784   bits: 19/18
c ---[1338]---> Adder-cost: 128   maxlim: 246784   bits: 19/18
c ---[1336]---> Adder-cost: 318   maxlim: 165888   bits: 19/18
c ---[1334]---> Adder-cost: 182   maxlim: 162816   bits: 19/18
c ---[1332]---> Adder-cost: 92   maxlim: 162816   bits: 19/18
c ---[1330]---> Adder-cost: 88   maxlim: 70656   bits: 18/17
c ---[1328]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1326]---> Adder-cost: 152   maxlim: 75776   bits: 18/17
c ---[1324]---> Adder-cost: 64   maxlim: 75776   bits: 18/17
c ---[1322]---> Adder-cost: 587   maxlim: 312320   bits: 20/19
c ---[1320]---> Adder-cost: 386   maxlim: 242688   bits: 19/18
c ---[1318]---> Adder-cost: 354   maxlim: 197632   bits: 19/18
c ---[1316]---> Adder-cost: 112   maxlim: 197632   bits: 19/18
c ---[1314]---> Adder-cost: 478   maxlim: 256000   bits: 19/18
c ---[1312]---> Adder-cost: 416   maxlim: 227328   bits: 19/18
c ---[1310]---> Adder-cost: 250   maxlim: 142336   bits: 19/18
c ---[1308]---> Adder-cost: 92   maxlim: 142336   bits: 19/18
c ---[1306]---> Adder-cost: 134   maxlim: 68608   bits: 18/17
c ---[1304]---> Adder-cost: 192   maxlim: 97280   bits: 18/17
c ---[1302]---> Adder-cost: 196   maxlim: 114688   bits: 18/17
c ---[1300]---> Adder-cost: 76   maxlim: 114688   bits: 18/17
c ---[1298]---> Adder-cost: 338   maxlim: 171008   bits: 19/18
c ---[1296]---> Adder-cost: 100   maxlim: 171008   bits: 19/18
c ---[1294]---> Adder-cost: 272   maxlim: 142336   bits: 19/18
c ---[1292]---> Adder-cost: 92   maxlim: 142336   bits: 19/18
c ---[1290]---> Adder-cost: 302   maxlim: 151552   bits: 19/18
c ---[1288]---> Adder-cost: 96   maxlim: 151552   bits: 19/18
c ---[1286]---> Adder-cost: 234   maxlim: 123904   bits: 18/17
c ---[1284]---> Adder-cost: 78   maxlim: 123904   bits: 18/17
c ---[1282]---> Adder-cost: 362   maxlim: 184320   bits: 19/18
c ---[1280]---> Adder-cost: 104   maxlim: 184320   bits: 19/18
c ---[1278]---> Adder-cost: 354   maxlim: 185344   bits: 19/18
c ---[1276]---> Adder-cost: 102   maxlim: 185344   bits: 19/18
c ---[1274]---> Adder-cost: 262   maxlim: 131072   bits: 19/18
c ---[1272]---> Adder-cost: 90   maxlim: 131072   bits: 19/18
c ---[1270]---> Adder-cost: 218   maxlim: 122880   bits: 18/17
c ---[1268]---> Adder-cost: 180   maxlim: 121856   bits: 18/17
c ---[1266]---> Adder-cost: 162   maxlim: 88064   bits: 18/17
c ---[1264]---> Adder-cost: 68   maxlim: 88064   bits: 18/17
c ---[1262]---> Adder-cost: 144   maxlim: 77824   bits: 18/17
c ---[1260]---> Adder-cost: 64   maxlim: 77824   bits: 18/17
c ---[1258]---> Adder-cost: 138   maxlim: 71680   bits: 18/17
c ---[1256]---> Adder-cost: 96   maxlim: 68608   bits: 18/17
c ---[1254]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1252]---> Adder-cost: 592   maxlim: 312320   bits: 20/19
c ---[1250]---> Adder-cost: 518   maxlim: 347136   bits: 20/19
c ---[1248]---> Adder-cost: 650   maxlim: 351232   bits: 20/19
c ---[1246]---> Adder-cost: 152   maxlim: 351232   bits: 20/19
c ---[1244]---> Adder-cost: 580   maxlim: 315392   bits: 20/19
c ---[1242]---> Adder-cost: 558   maxlim: 299008   bits: 20/19
c ---[1240]---> Adder-cost: 260   maxlim: 139264   bits: 19/18
c ---[1238]---> Adder-cost: 94   maxlim: 139264   bits: 19/18
c ---[1236]---> Adder-cost: 158   maxlim: 91136   bits: 18/17
c ---[1234]---> Adder-cost: 410   maxlim: 216064   bits: 19/18
c ---[1232]---> Adder-cost: 116   maxlim: 216064   bits: 19/18
c ---[1230]---> Adder-cost: 590   maxlim: 326656   bits: 20/19
c ---[1228]---> Adder-cost: 448   maxlim: 333824   bits: 20/19
c ---[1226]---> Adder-cost: 154   maxlim: 333824   bits: 20/19
c ---[1224]---> Adder-cost: 534   maxlim: 297984   bits: 20/19
c ---[1222]---> Adder-cost: 142   maxlim: 297984   bits: 20/19
c ---[1220]---> Adder-cost: 142   maxlim: 297984   bits: 20/19
c ---[1218]---> Adder-cost: 682   maxlim: 390144   bits: 20/19
c ---[1216]---> Adder-cost: 162   maxlim: 390144   bits: 20/19
c ---[1214]---> Adder-cost: 162   maxlim: 390144   bits: 20/19
c ---[1212]---> Adder-cost: 714   maxlim: 390144   bits: 20/19
c ---[1210]---> Adder-cost: 162   maxlim: 390144   bits: 20/19
c ---[1208]---> Adder-cost: 162   maxlim: 390144   bits: 20/19
c ---[1206]---> Adder-cost: 720   maxlim: 389120   bits: 20/19
c ---[1204]---> Adder-cost: 164   maxlim: 389120   bits: 20/19
c ---[1202]---> Adder-cost: 164   maxlim: 389120   bits: 20/19
c ---[1200]---> Adder-cost: 164   maxlim: 389120   bits: 20/19
c ---[1198]---> Adder-cost: 164   maxlim: 389120   bits: 20/19
c ---[1196]---> Adder-cost: 164   maxlim: 389120   bits: 20/19
c ---[1194]---> Adder-cost: 530   maxlim: 306176   bits: 20/19
c ---[1192]---> Adder-cost: 146   maxlim: 306176   bits: 20/19
c ---[1190]---> Adder-cost: 146   maxlim: 306176   bits: 20/19
c ---[1188]---> Adder-cost: 146   maxlim: 306176   bits: 20/19
c ---[1186]---> Adder-cost: 146   maxlim: 306176   bits: 20/19
c ---[1184]---> Adder-cost: 146   maxlim: 306176   bits: 20/19
c ---[1182]---> Adder-cost: 482   maxlim: 266240   bits: 20/19
c ---[1180]---> Adder-cost: 332   maxlim: 263168   bits: 20/19
c ---[1178]---> Adder-cost: 138   maxlim: 263168   bits: 20/19
c ---[1176]---> Adder-cost: 138   maxlim: 263168   bits: 20/19
c ---[1174]---> Adder-cost: 138   maxlim: 263168   bits: 20/19
c ---[1172]---> Adder-cost: 138   maxlim: 263168   bits: 20/19
c ---[1170]---> Adder-cost: 238   maxlim: 123904   bits: 18/17
c ---[1168]---> Adder-cost: 150   maxlim: 101376   bits: 18/17
c ---[1166]---> Adder-cost: 72   maxlim: 101376   bits: 18/17
c ---[1164]---> Adder-cost: 106   maxlim: 66560   bits: 18/17
c ---[1162]---> Adder-cost: 212   maxlim: 107520   bits: 18/17
c ---[1160]---> Adder-cost: 242   maxlim: 146432   bits: 19/18
c ---[1158]---> Adder-cost: 88   maxlim: 146432   bits: 19/18
c ---[1156]---> Adder-cost: 616   maxlim: 335872   bits: 20/19
c ---[1154]---> Adder-cost: 578   maxlim: 310272   bits: 20/19
c ---[1152]---> Adder-cost: 438   maxlim: 239616   bits: 19/18
c ---[1150]---> Adder-cost: 122   maxlim: 239616   bits: 19/18
c ---[1148]---> Adder-cost: 508   maxlim: 266240   bits: 20/19
c ---[1146]---> Adder-cost: 234   maxlim: 247808   bits: 19/18
c ---[1144]---> Adder-cost: 329   maxlim: 176128   bits: 19/18
c ---[1142]---> Adder-cost: 102   maxlim: 176128   bits: 19/18
c ---[1140]---> Sorter-cost: 1250     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1138]---> Adder-cost: 112   maxlim: 55296   bits: 17/16
c ---[1136]---> Adder-cost: 122   maxlim: 63488   bits: 17/16
c ---[1134]---> Adder-cost: 52   maxlim: 63488   bits: 17/16
c ---[1132]---> Adder-cost: 246   maxlim: 130048   bits: 18/17
c ---[1130]---> Adder-cost: 74   maxlim: 130048   bits: 18/17
c ---[1128]---> Adder-cost: 262   maxlim: 137216   bits: 19/18
c ---[1126]---> Adder-cost: 88   maxlim: 137216   bits: 19/18
c ---[1124]---> Adder-cost: 410   maxlim: 207872   bits: 19/18
c ---[1122]---> Adder-cost: 352   maxlim: 203776   bits: 19/18
c ---[1120]---> Adder-cost: 352   maxlim: 203776   bits: 19/18
c ---[1118]---> Adder-cost: 110   maxlim: 203776   bits: 19/18
c ---[1116]---> Adder-cost: 272   maxlim: 136192   bits: 19/18
c ---[1114]---> Adder-cost: 88   maxlim: 136192   bits: 19/18
c ---[1112]---> Adder-cost: 380   maxlim: 194560   bits: 19/18
c ---[1110]---> Adder-cost: 110   maxlim: 194560   bits: 19/18
c ---[1108]---> Adder-cost: 218   maxlim: 108544   bits: 18/17
c ---[1106]---> Adder-cost: 78   maxlim: 108544   bits: 18/17
c ---[1104]---> Adder-cost: 184   maxlim: 93184   bits: 18/17
c ---[1102]---> Adder-cost: 64   maxlim: 93184   bits: 18/17
c ---[1100]---> Adder-cost: 210   maxlim: 105472   bits: 18/17
c ---[1098]---> Adder-cost: 74   maxlim: 105472   bits: 18/17
c ---[1096]---> Adder-cost: 176   maxlim: 93184   bits: 18/17
c ---[1094]---> Adder-cost: 64   maxlim: 93184   bits: 18/17
c ---[1092]---> Adder-cost: 134   maxlim: 69632   bits: 18/17
c ---[1090]---> Adder-cost: 98   maxlim: 61440   bits: 17/16
c ---[1088]---> Adder-cost: 114   maxlim: 59392   bits: 17/16
c ---[1086]---> Adder-cost: 106   maxlim: 65536   bits: 18/17
c ---[1084]---> Adder-cost: 62   maxlim: 65536   bits: 18/17
c ---[1082]---> Adder-cost: 336   maxlim: 175104   bits: 19/18
c ---[1080]---> Adder-cost: 264   maxlim: 168960   bits: 19/18
c ---[1078]---> Adder-cost: 312   maxlim: 176128   bits: 19/18
c ---[1076]---> Adder-cost: 102   maxlim: 176128   bits: 19/18
c ---[1074]---> Adder-cost: 394   maxlim: 200704   bits: 19/18
c ---[1072]---> Adder-cost: 308   maxlim: 174080   bits: 19/18
c ---[1070]---> Adder-cost: 290   maxlim: 173056   bits: 19/18
c ---[1068]---> Adder-cost: 100   maxlim: 173056   bits: 19/18
c ---[1066]---> Adder-cost: 296   maxlim: 149504   bits: 19/18
c ---[1064]---> Adder-cost: 214   maxlim: 180224   bits: 19/18
c ---[1062]---> Adder-cost: 110   maxlim: 180224   bits: 19/18
c ---[1060]---> Adder-cost: 390   maxlim: 201728   bits: 19/18
c ---[1058]---> Adder-cost: 114   maxlim: 201728   bits: 19/18
c ---[1056]---> Adder-cost: 432   maxlim: 248832   bits: 19/18
c ---[1054]---> Adder-cost: 128   maxlim: 248832   bits: 19/18
c ---[1052]---> Adder-cost: 516   maxlim: 266240   bits: 20/19
c ---[1050]---> Adder-cost: 142   maxlim: 266240   bits: 20/19
c ---[1048]---> Adder-cost: 466   maxlim: 248832   bits: 19/18
c ---[1046]---> Adder-cost: 128   maxlim: 248832   bits: 19/18
c ---[1044]---> Adder-cost: 524   maxlim: 272384   bits: 20/19
c ---[1042]---> Adder-cost: 142   maxlim: 272384   bits: 20/19
c ---[1040]---> Adder-cost: 322   maxlim: 176128   bits: 19/18
c ---[1038]---> Adder-cost: 102   maxlim: 176128   bits: 19/18
c ---[1036]---> Adder-cost: 504   maxlim: 282624   bits: 20/19
c ---[1034]---> Adder-cost: 140   maxlim: 282624   bits: 20/19
c ---[1032]---> Adder-cost: 336   maxlim: 176128   bits: 19/18
c ---[1030]---> Adder-cost: 102   maxlim: 176128   bits: 19/18
c ---[1028]---> Sorter-cost: 1024     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1026]---> Adder-cost: 252   maxlim: 131072   bits: 19/18
c ---[1024]---> Adder-cost: 90   maxlim: 131072   bits: 19/18
c ---[1022]---> Adder-cost: 90   maxlim: 131072   bits: 19/18
c ---[1020]---> Adder-cost: 342   maxlim: 178176   bits: 19/18
c ---[1018]---> Adder-cost: 392   maxlim: 198656   bits: 19/18
c ---[1016]---> Adder-cost: 472   maxlim: 264192   bits: 20/19
c ---[1014]---> Adder-cost: 138   maxlim: 264192   bits: 20/19
c ---[1012]---> Adder-cost: 598   maxlim: 320512   bits: 20/19
c ---[1010]---> Adder-cost: 612   maxlim: 336896   bits: 20/19
c ---[1008]---> Adder-cost: 302   maxlim: 158720   bits: 19/18
c ---[1006]---> Adder-cost: 92   maxlim: 158720   bits: 19/18
c ---[1004]---> Adder-cost: 446   maxlim: 234496   bits: 19/18
c ---[1002]---> Adder-cost: 344   maxlim: 231424   bits: 19/18
c ---[1000]---> Adder-cost: 224   maxlim: 116736   bits: 18/17
c ---[ 998]---> Adder-cost: 78   maxlim: 116736   bits: 18/17
c ---[ 996]---> Adder-cost: 348   maxlim: 202752   bits: 19/18
c ---[ 994]---> Adder-cost: 374   maxlim: 220160   bits: 19/18
c ---[ 992]---> Adder-cost: 402   maxlim: 210944   bits: 19/18
c ---[ 990]---> Adder-cost: 114   maxlim: 210944   bits: 19/18
c ---[ 988]---> Adder-cost: 360   maxlim: 184320   bits: 19/18
c ---[ 986]---> Adder-cost: 236   maxlim: 139264   bits: 19/18
c ---[ 984]---> Adder-cost: 278   maxlim: 140288   bits: 19/18
c ---[ 982]---> Adder-cost: 94   maxlim: 140288   bits: 19/18
c ---[ 980]---> Adder-cost: 392   maxlim: 210944   bits: 19/18
c ---[ 978]---> Adder-cost: 216   maxlim: 126976   bits: 18/17
c ---[ 976]---> Adder-cost: 94   maxlim: 53248   bits: 17/16
c ---[ 974]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[ 972]---> Adder-cost: 224   maxlim: 115712   bits: 18/17
c ---[ 970]---> Adder-cost: 164   maxlim: 90112   bits: 18/17
c ---[ 968]---> Adder-cost: 84   maxlim: 60416   bits: 17/16
c ---[ 966]---> Adder-cost: 154   maxlim: 75776   bits: 18/17
c ---[ 964]---> Adder-cost: 64   maxlim: 75776   bits: 18/17
c ---[ 962]---> Adder-cost: 272   maxlim: 139264   bits: 19/18
c ---[ 960]---> Adder-cost: 94   maxlim: 139264   bits: 19/18
c ---[ 958]---> Adder-cost: 774   maxlim: 406528   bits: 20/19
c ---[ 956]---> Adder-cost: 166   maxlim: 406528   bits: 20/19
c ---[ 954]---> Adder-cost: 716   maxlim: 397312   bits: 20/19
c ---[ 952]---> Adder-cost: 178   maxlim: 397312   bits: 20/19
c ---[ 950]---> Adder-cost: 254   maxlim: 130048   bits: 18/17
c ---[ 948]---> Adder-cost: 74   maxlim: 130048   bits: 18/17
c ---[ 946]---> Adder-cost: 482   maxlim: 256000   bits: 19/18
c ---[ 944]---> Adder-cost: 354   maxlim: 251904   bits: 19/18
c ---[ 942]---> Adder-cost: 524   maxlim: 305152   bits: 20/19
c ---[ 940]---> Adder-cost: 146   maxlim: 305152   bits: 20/19
c ---[ 938]---> Adder-cost: 332   maxlim: 173056   bits: 19/18
c ---[ 936]---> Adder-cost: 100   maxlim: 173056   bits: 19/18
c ---[ 934]---> Adder-cost: 194   maxlim: 101376   bits: 18/17
c ---[ 932]---> Adder-cost: 72   maxlim: 101376   bits: 18/17
c ---[ 930]---> Adder-cost: 288   maxlim: 147456   bits: 19/18
c ---[ 928]---> Adder-cost: 94   maxlim: 147456   bits: 19/18
c ---[ 926]---> Adder-cost: 138   maxlim: 68608   bits: 18/17
c ---[ 924]---> Adder-cost: 58   maxlim: 68608   bits: 18/17
c ---[ 922]---> Sorter-cost: 1082     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 920]---> Adder-cost: 358   maxlim: 188416   bits: 19/18
c ---[ 918]---> Adder-cost: 106   maxlim: 188416   bits: 19/18
c ---[ 916]---> Adder-cost: 280   maxlim: 145408   bits: 19/18
c ---[ 914]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[ 912]---> Adder-cost: 338   maxlim: 173056   bits: 19/18
c ---[ 910]---> Adder-cost: 100   maxlim: 173056   bits: 19/18
c ---[ 908]---> Adder-cost: 354   maxlim: 186368   bits: 19/18
c ---[ 906]---> Adder-cost: 106   maxlim: 186368   bits: 19/18
c ---[ 904]---> Adder-cost: 178   maxlim: 92160   bits: 18/17
c ---[ 902]---> Adder-cost: 66   maxlim: 92160   bits: 18/17
c ---[ 900]---> Adder-cost: 228   maxlim: 114688   bits: 18/17
c ---[ 898]---> Adder-cost: 216   maxlim: 113664   bits: 18/17
c ---[ 896]---> Adder-cost: 438   maxlim: 230400   bits: 19/18
c ---[ 894]---> Adder-cost: 124   maxlim: 230400   bits: 19/18
c ---[ 892]---> Adder-cost: 422   maxlim: 221184   bits: 19/18
c ---[ 890]---> Adder-cost: 116   maxlim: 221184   bits: 19/18
c ---[ 888]---> Adder-cost: 248   maxlim: 129024   bits: 18/17
c ---[ 886]---> Adder-cost: 76   maxlim: 129024   bits: 18/17
c ---[ 884]---> Adder-cost: 280   maxlim: 139264   bits: 19/18
c ---[ 882]---> Adder-cost: 94   maxlim: 139264   bits: 19/18
c ---[ 880]---> Adder-cost: 158   maxlim: 78848   bits: 18/17
c ---[ 878]---> Adder-cost: 60   maxlim: 78848   bits: 18/17
c ---[ 876]---> Sorter-cost: 1313     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 874]---> Adder-cost: 276   maxlim: 171008   bits: 19/18
c ---[ 872]---> Adder-cost: 288   maxlim: 253952   bits: 19/18
c ---[ 870]---> Adder-cost: 250   maxlim: 256000   bits: 19/18
c ---[ 868]---> Adder-cost: 472   maxlim: 257024   bits: 19/18
c ---[ 866]---> Adder-cost: 624   maxlim: 357376   bits: 20/19
c ---[ 864]---> Adder-cost: 456   maxlim: 317440   bits: 20/19
c ---[ 862]---> Adder-cost: 612   maxlim: 339968   bits: 20/19
c ---[ 860]---> Adder-cost: 638   maxlim: 348160   bits: 20/19
c ---[ 858]---> Adder-cost: 672   maxlim: 407552   bits: 20/19
c ---[ 856]---> Adder-cost: 402   maxlim: 241664   bits: 19/18
c ---[ 854]---> Adder-cost: 358   maxlim: 222208   bits: 19/18
c ---[ 852]---> Adder-cost: 332   maxlim: 177152   bits: 19/18
c ---[ 850]---> Adder-cost: 326   maxlim: 226304   bits: 19/18
c ---[ 848]---> Adder-cost: 412   maxlim: 245760   bits: 19/18
c ---[ 846]---> Adder-cost: 348   maxlim: 231424   bits: 19/18
c ---[ 844]---> Adder-cost: 478   maxlim: 251904   bits: 19/18
c ---[ 842]---> Adder-cost: 392   maxlim: 225280   bits: 19/18
c ---[ 840]---> Adder-cost: 282   maxlim: 161792   bits: 19/18
c ---[ 838]---> Adder-cost: 266   maxlim: 150528   bits: 19/18
c ---[ 836]---> Adder-cost: 426   maxlim: 220160   bits: 19/18
c ---[ 834]---> Adder-cost: 394   maxlim: 231424   bits: 19/18
c ---[ 832]---> Adder-cost: 335   maxlim: 194560   bits: 19/18
c ---[ 830]---> Adder-cost: 338   maxlim: 190464   bits: 19/18
c ---[ 828]---> Adder-cost: 564   maxlim: 305152   bits: 20/19
c ---[ 826]---> Adder-cost: 368   maxlim: 251904   bits: 19/18
c ---[ 824]---> Adder-cost: 238   maxlim: 148480   bits: 19/18
c ---[ 822]---> Adder-cost: 172   maxlim: 111616   bits: 18/17
c ---[ 820]---> Adder-cost: 284   maxlim: 164864   bits: 19/18
c ---[ 818]---> Adder-cost: 196   maxlim: 110592   bits: 18/17
c ---[ 816]---> Adder-cost: 160   maxlim: 101376   bits: 18/17
c ---[ 814]---> Sorter-cost: 1223     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 812]---> Adder-cost: 128   maxlim: 71680   bits: 18/17
c ---[ 810]---> Adder-cost: 168   maxlim: 86016   bits: 18/17
c ---[ 808]---> Adder-cost: 120   maxlim: 90112   bits: 18/17
c ---[ 806]---> Adder-cost: 430   maxlim: 268288   bits: 20/19
c ---[ 804]---> Adder-cost: 680   maxlim: 450560   bits: 20/19
c ---[ 802]---> Adder-cost: 182   maxlim: 450560   bits: 20/19
c ---[ 800]---> Adder-cost: 360   maxlim: 187392   bits: 19/18
c ---[ 798]---> Adder-cost: 296   maxlim: 207872   bits: 19/18
c ---[ 796]---> Adder-cost: 384   maxlim: 196608   bits: 19/18
c ---[ 794]---> Adder-cost: 114   maxlim: 196608   bits: 19/18
c ---[ 792]---> Adder-cost: 452   maxlim: 248832   bits: 19/18
c ---[ 790]---> Adder-cost: 346   maxlim: 204800   bits: 19/18
c ---[ 788]---> Adder-cost: 248   maxlim: 131072   bits: 19/18
c ---[ 786]---> Adder-cost: 90   maxlim: 131072   bits: 19/18
c ---[ 784]---> Adder-cost: 260   maxlim: 133120   bits: 19/18
c ---[ 782]---> Adder-cost: 186   maxlim: 104448   bits: 18/17
c ---[ 780]---> Adder-cost: 194   maxlim: 116736   bits: 18/17
c ---[ 778]---> Adder-cost: 78   maxlim: 116736   bits: 18/17
c ---[ 776]---> Adder-cost: 780   maxlim: 414720   bits: 20/19
c ---[ 774]---> Adder-cost: 727   maxlim: 398336   bits: 20/19
c ---[ 772]---> Adder-cost: 432   maxlim: 238592   bits: 19/18
c ---[ 770]---> Adder-cost: 120   maxlim: 238592   bits: 19/18
c ---[ 768]---> Adder-cost: 468   maxlim: 243712   bits: 19/18
c ---[ 766]---> Adder-cost: 350   maxlim: 193536   bits: 19/18
c ---[ 764]---> Adder-cost: 258   maxlim: 134144   bits: 19/18
c ---[ 762]---> Adder-cost: 84   maxlim: 134144   bits: 19/18
c ---[ 760]---> Adder-cost: 244   maxlim: 128000   bits: 18/17
c ---[ 758]---> Adder-cost: 172   maxlim: 99328   bits: 18/17
c ---[ 756]---> Adder-cost: 116   maxlim: 60416   bits: 17/16
c ---[ 754]---> Adder-cost: 48   maxlim: 60416   bits: 17/16
c ---[ 752]---> Sorter-cost: 1271     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 750]---> Adder-cost: 264   maxlim: 137216   bits: 19/18
c ---[ 748]---> Adder-cost: 210   maxlim: 155648   bits: 19/18
c ---[ 746]---> Adder-cost: 96   maxlim: 155648   bits: 19/18
c ---[ 744]---> Adder-cost: 358   maxlim: 182272   bits: 19/18
c ---[ 742]---> Adder-cost: 106   maxlim: 182272   bits: 19/18
c ---[ 740]---> Adder-cost: 464   maxlim: 254976   bits: 19/18
c ---[ 738]---> Adder-cost: 132   maxlim: 254976   bits: 19/18
c ---[ 736]---> Adder-cost: 314   maxlim: 162816   bits: 19/18
c ---[ 734]---> Adder-cost: 92   maxlim: 162816   bits: 19/18
c ---[ 732]---> Adder-cost: 564   maxlim: 289792   bits: 20/19
c ---[ 730]---> Adder-cost: 142   maxlim: 289792   bits: 20/19
c ---[ 728]---> Adder-cost: 548   maxlim: 282624   bits: 20/19
c ---[ 726]---> Adder-cost: 140   maxlim: 282624   bits: 20/19
c ---[ 724]---> Adder-cost: 478   maxlim: 245760   bits: 19/18
c ---[ 722]---> Adder-cost: 467   maxlim: 246784   bits: 19/18
c ---[ 720]---> Adder-cost: 673   maxlim: 368640   bits: 20/19
c ---[ 718]---> Adder-cost: 160   maxlim: 368640   bits: 20/19
c ---[ 716]---> Adder-cost: 358   maxlim: 182272   bits: 19/18
c ---[ 714]---> Adder-cost: 106   maxlim: 182272   bits: 19/18
c ---[ 712]---> Adder-cost: 326   maxlim: 176128   bits: 19/18
c ---[ 710]---> Adder-cost: 290   maxlim: 175104   bits: 19/18
c ---[ 708]---> Adder-cost: 288   maxlim: 152576   bits: 19/18
c ---[ 706]---> Adder-cost: 94   maxlim: 152576   bits: 19/18
c ---[ 704]---> Adder-cost: 474   maxlim: 241664   bits: 19/18
c ---[ 702]---> Adder-cost: 126   maxlim: 241664   bits: 19/18
c ---[ 700]---> Adder-cost: 424   maxlim: 231424   bits: 19/18
c ---[ 698]---> Adder-cost: 128   maxlim: 231424   bits: 19/18
c ---[ 696]---> Adder-cost: 244   maxlim: 126976   bits: 18/17
c ---[ 694]---> Adder-cost: 78   maxlim: 126976   bits: 18/17
c ---[ 692]---> Adder-cost: 196   maxlim: 102400   bits: 18/17
c ---[ 690]---> Adder-cost: 156   maxlim: 99328   bits: 18/17
c ---[ 688]---> Adder-cost: 180   maxlim: 95232   bits: 18/17
c ---[ 686]---> Adder-cost: 70   maxlim: 95232   bits: 18/17
c ---[ 684]---> Adder-cost: 196   maxlim: 98304   bits: 18/17
c ---[ 682]---> Adder-cost: 110   maxlim: 97280   bits: 18/17
c ---[ 680]---> Adder-cost: 196   maxlim: 101376   bits: 18/17
c ---[ 678]---> Adder-cost: 72   maxlim: 101376   bits: 18/17
c ---[ 676]---> Adder-cost: 156   maxlim: 78848   bits: 18/17
c ---[ 674]---> Adder-cost: 60   maxlim: 78848   bits: 18/17
c ---[ 672]---> Adder-cost: 118   maxlim: 61440   bits: 17/16
c ---[ 670]---> Sorter-cost: 1223     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 668]---> Adder-cost: 553   maxlim: 320512   bits: 20/19
c ---[ 666]---> Adder-cost: 148   maxlim: 320512   bits: 20/19
c ---[ 664]---> Adder-cost: 748   maxlim: 443392   bits: 20/19
c ---[ 662]---> Adder-cost: 1511   maxlim: 870400   bits: 21/20
c ---[ 660]---> Adder-cost: 284   maxlim: 870400   bits: 21/20
c ---[ 658]---> Adder-cost: 1484   maxlim: 879616   bits: 21/20
c ---[ 656]---> Adder-cost: 286   maxlim: 879616   bits: 21/20
c ---[ 654]---> Adder-cost: 1876   maxlim: 1171456   bits: 22/21
c ---[ 652]---> Adder-cost: 334   maxlim: 1171456   bits: 22/21
c ---[ 650]---> Adder-cost: 1556   maxlim: 1059840   bits: 22/21
c ---[ 648]---> Adder-cost: 322   maxlim: 1059840   bits: 22/21
c ---[ 646]---> Adder-cost: 1290   maxlim: 736256   bits: 21/20
c ---[ 644]---> Adder-cost: 248   maxlim: 736256   bits: 21/20
c ---[ 642]---> Adder-cost: 1838   maxlim: 1163264   bits: 22/21
c ---[ 640]---> Adder-cost: 1308   maxlim: 1003520   bits: 21/20
c ---[ 638]---> Adder-cost: 2224   maxlim: 1272832   bits: 22/21
c ---[ 636]---> Adder-cost: 1886   maxlim: 1052672   bits: 22/21
c ---[ 634]---> Adder-cost: 1330   maxlim: 779264   bits: 21/20
c ---[ 632]---> Adder-cost: 1542   maxlim: 897024   bits: 21/20
c ---[ 630]---> Adder-cost: 1122   maxlim: 720896   bits: 21/20
c ---[ 628]---> Adder-cost: 1138   maxlim: 679936   bits: 21/20
c ---[ 626]---> Adder-cost: 1044   maxlim: 589824   bits: 21/20
c ---[ 624]---> Adder-cost: 1058   maxlim: 628736   bits: 21/20
c ---[ 622]---> Adder-cost: 1046   maxlim: 630784   bits: 21/20
c ---[ 620]---> Adder-cost: 232   maxlim: 630784   bits: 21/20
c ---[ 618]---> Adder-cost: 1106   maxlim: 702464   bits: 21/20
c ---[ 616]---> Adder-cost: 248   maxlim: 702464   bits: 21/20
c ---[ 614]---> Adder-cost: 932   maxlim: 549888   bits: 21/20
c ---[ 612]---> Adder-cost: 216   maxlim: 549888   bits: 21/20
c ---[ 610]---> Adder-cost: 850   maxlim: 502784   bits: 20/19
c ---[ 608]---> Adder-cost: 194   maxlim: 502784   bits: 20/19
c ---[ 606]---> Adder-cost: 757   maxlim: 451584   bits: 20/19
c ---[ 604]---> Adder-cost: 182   maxlim: 451584   bits: 20/19
c ---[ 602]---> Adder-cost: 182   maxlim: 451584   bits: 20/19
c ---[ 600]---> Adder-cost: 182   maxlim: 451584   bits: 20/19
c ---[ 598]---> Adder-cost: 874   maxlim: 514048   bits: 20/19
c ---[ 596]---> Adder-cost: 198   maxlim: 514048   bits: 20/19
c ---[ 594]---> Adder-cost: 708   maxlim: 421888   bits: 20/19
c ---[ 592]---> Adder-cost: 178   maxlim: 421888   bits: 20/19
c ---[ 590]---> Adder-cost: 178   maxlim: 421888   bits: 20/19
c ---[ 588]---> Adder-cost: 178   maxlim: 421888   bits: 20/19
c ---[ 586]---> Adder-cost: 556   maxlim: 346112   bits: 20/19
c ---[ 584]---> Adder-cost: 156   maxlim: 346112   bits: 20/19
c ---[ 582]---> Adder-cost: 156   maxlim: 346112   bits: 20/19
c ---[ 580]---> Adder-cost: 156   maxlim: 346112   bits: 20/19
c ---[ 578]---> Adder-cost: 412   maxlim: 261120   bits: 19/18
c ---[ 576]---> Adder-cost: 128   maxlim: 261120   bits: 19/18
c ---[ 574]---> Adder-cost: 128   maxlim: 261120   bits: 19/18
c ---[ 572]---> Adder-cost: 128   maxlim: 261120   bits: 19/18
c ---[ 570]---> Adder-cost: 302   maxlim: 157696   bits: 19/18
c ---[ 568]---> Adder-cost: 92   maxlim: 157696   bits: 19/18
c ---[ 566]---> Adder-cost: 172   maxlim: 95232   bits: 18/17
c ---[ 564]---> Adder-cost: 70   maxlim: 95232   bits: 18/17
c ---[ 562]---> Adder-cost: 114   maxlim: 59392   bits: 17/16
c ---[ 560]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[ 558]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[ 556]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[ 554]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[ 552]---> Adder-cost: 355   maxlim: 183296   bits: 19/18
c ---[ 550]---> Adder-cost: 360   maxlim: 199680   bits: 19/18
c ---[ 548]---> Adder-cost: 246   maxlim: 130048   bits: 18/17
c ---[ 546]---> Adder-cost: 74   maxlim: 130048   bits: 18/17
c ---[ 544]---> Adder-cost: 240   maxlim: 124928   bits: 18/17
c ---[ 542]---> Adder-cost: 216   maxlim: 130048   bits: 18/17
c ---[ 540]---> Adder-cost: 374   maxlim: 195584   bits: 19/18
c ---[ 538]---> Adder-cost: 108   maxlim: 195584   bits: 19/18
c ---[ 536]---> Adder-cost: 412   maxlim: 214016   bits: 19/18
c ---[ 534]---> Adder-cost: 378   maxlim: 203776   bits: 19/18
c ---[ 532]---> Adder-cost: 222   maxlim: 125952   bits: 18/17
c ---[ 530]---> Adder-cost: 78   maxlim: 125952   bits: 18/17
c ---[ 528]---> Adder-cost: 344   maxlim: 189440   bits: 19/18
c ---[ 526]---> Adder-cost: 282   maxlim: 159744   bits: 19/18
c ---[ 524]---> Adder-cost: 480   maxlim: 260096   bits: 19/18
c ---[ 522]---> Adder-cost: 128   maxlim: 260096   bits: 19/18
c ---[ 520]---> Adder-cost: 538   maxlim: 297984   bits: 20/19
c ---[ 518]---> Adder-cost: 470   maxlim: 266240   bits: 20/19
c ---[ 516]---> Adder-cost: 396   maxlim: 206848   bits: 19/18
c ---[ 514]---> Adder-cost: 114   maxlim: 206848   bits: 19/18
c ---[ 512]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 510]---> Adder-cost: 116   maxlim: 60416   bits: 17/16
c ---[ 508]---> Adder-cost: 48   maxlim: 60416   bits: 17/16
c ---[ 506]---> Adder-cost: 292   maxlim: 151552   bits: 19/18
c ---[ 504]---> Adder-cost: 200   maxlim: 104448   bits: 18/17
c ---[ 502]---> Adder-cost: 198   maxlim: 99328   bits: 18/17
c ---[ 500]---> Adder-cost: 70   maxlim: 99328   bits: 18/17
c ---[ 498]---> Adder-cost: 180   maxlim: 100352   bits: 18/17
c ---[ 496]---> Adder-cost: 156   maxlim: 86016   bits: 18/17
c ---[ 494]---> Adder-cost: 376   maxlim: 219136   bits: 19/18
c ---[ 492]---> Adder-cost: 114   maxlim: 219136   bits: 19/18
c ---[ 490]---> Adder-cost: 484   maxlim: 285696   bits: 20/19
c ---[ 488]---> Adder-cost: 140   maxlim: 285696   bits: 20/19
c ---[ 486]---> Adder-cost: 444   maxlim: 235520   bits: 19/18
c ---[ 484]---> Adder-cost: 126   maxlim: 235520   bits: 19/18
c ---[ 482]---> Adder-cost: 444   maxlim: 234496   bits: 19/18
c ---[ 480]---> Adder-cost: 120   maxlim: 234496   bits: 19/18
c ---[ 478]---> Adder-cost: 596   maxlim: 304128   bits: 20/19
c ---[ 476]---> Adder-cost: 148   maxlim: 304128   bits: 20/19
c ---[ 474]---> Adder-cost: 584   maxlim: 303104   bits: 20/19
c ---[ 472]---> Adder-cost: 324   maxlim: 304128   bits: 20/19
c ---[ 470]---> Adder-cost: 468   maxlim: 245760   bits: 19/18
c ---[ 468]---> Adder-cost: 128   maxlim: 245760   bits: 19/18
c ---[ 466]---> Adder-cost: 506   maxlim: 269312   bits: 20/19
c ---[ 464]---> Adder-cost: 144   maxlim: 269312   bits: 20/19
c ---[ 462]---> Adder-cost: 472   maxlim: 246784   bits: 19/18
c ---[ 460]---> Adder-cost: 128   maxlim: 246784   bits: 19/18
c ---[ 458]---> Adder-cost: 494   maxlim: 268288   bits: 20/19
c ---[ 456]---> Adder-cost: 144   maxlim: 268288   bits: 20/19
c ---[ 454]---> Adder-cost: 542   maxlim: 281600   bits: 20/19
c ---[ 452]---> Adder-cost: 136   maxlim: 281600   bits: 20/19
c ---[ 450]---> Adder-cost: 758   maxlim: 412672   bits: 20/19
c ---[ 448]---> Adder-cost: 168   maxlim: 412672   bits: 20/19
c ---[ 446]---> Adder-cost: 450   maxlim: 243712   bits: 19/18
c ---[ 444]---> Adder-cost: 124   maxlim: 243712   bits: 19/18
c ---[ 442]---> Adder-cost: 550   maxlim: 283648   bits: 20/19
c ---[ 440]---> Adder-cost: 472   maxlim: 267264   bits: 20/19
c ---[ 438]---> Adder-cost: 258   maxlim: 138240   bits: 19/18
c ---[ 436]---> Adder-cost: 88   maxlim: 138240   bits: 19/18
c ---[ 434]---> Adder-cost: 186   maxlim: 95232   bits: 18/17
c ---[ 432]---> Adder-cost: 70   maxlim: 95232   bits: 18/17
c ---[ 430]---> Adder-cost: 212   maxlim: 111616   bits: 18/17
c ---[ 428]---> Adder-cost: 72   maxlim: 111616   bits: 18/17
c ---[ 426]---> Adder-cost: 258   maxlim: 131072   bits: 19/18
c ---[ 424]---> Adder-cost: 90   maxlim: 131072   bits: 19/18
c ---[ 422]---> Adder-cost: 170   maxlim: 90112   bits: 18/17
c ---[ 420]---> Adder-cost: 72   maxlim: 90112   bits: 18/17
c ---[ 418]---> Adder-cost: 162   maxlim: 82944   bits: 18/17
c ---[ 416]---> Adder-cost: 150   maxlim: 77824   bits: 18/17
c ---[ 414]---> Adder-cost: 270   maxlim: 139264   bits: 19/18
c ---[ 412]---> Adder-cost: 248   maxlim: 167936   bits: 19/18
c ---[ 410]---> Adder-cost: 104   maxlim: 167936   bits: 19/18
c ---[ 408]---> Adder-cost: 168   maxlim: 83968   bits: 18/17
c ---[ 406]---> Adder-cost: 68   maxlim: 83968   bits: 18/17
c ---[ 404]---> Adder-cost: 202   maxlim: 112640   bits: 18/17
c ---[ 402]---> Adder-cost: 74   maxlim: 112640   bits: 18/17
c ---[ 400]---> Adder-cost: 394   maxlim: 196608   bits: 19/18
c ---[ 398]---> Adder-cost: 114   maxlim: 196608   bits: 19/18
c ---[ 396]---> Adder-cost: 406   maxlim: 208896   bits: 19/18
c ---[ 394]---> Adder-cost: 114   maxlim: 208896   bits: 19/18
c ---[ 392]---> Adder-cost: 414   maxlim: 216064   bits: 19/18
c ---[ 390]---> Adder-cost: 116   maxlim: 216064   bits: 19/18
c ---[ 388]---> Adder-cost: 439   maxlim: 229376   bits: 19/18
c ---[ 386]---> Adder-cost: 126   maxlim: 229376   bits: 19/18
c ---[ 384]---> Adder-cost: 440   maxlim: 242688   bits: 19/18
c ---[ 382]---> Adder-cost: 124   maxlim: 242688   bits: 19/18
c ---[ 380]---> Adder-cost: 152   maxlim: 75776   bits: 18/17
c ---[ 378]---> Adder-cost: 64   maxlim: 75776   bits: 18/17
c ---[ 376]---> Sorter-cost: 1135     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 374]---> Adder-cost: 486   maxlim: 280576   bits: 20/19
c ---[ 372]---> Adder-cost: 136   maxlim: 280576   bits: 20/19
c ---[ 370]---> Adder-cost: 602   maxlim: 366592   bits: 20/19
c ---[ 368]---> Adder-cost: 168   maxlim: 366592   bits: 20/19
c ---[ 366]---> Adder-cost: 556   maxlim: 312320   bits: 20/19
c ---[ 364]---> Adder-cost: 154   maxlim: 312320   bits: 20/19
c ---[ 362]---> Adder-cost: 404   maxlim: 215040   bits: 19/18
c ---[ 360]---> Adder-cost: 118   maxlim: 215040   bits: 19/18
c ---[ 358]---> Adder-cost: 410   maxlim: 223232   bits: 19/18
c ---[ 356]---> Adder-cost: 118   maxlim: 223232   bits: 19/18
c ---[ 354]---> Adder-cost: 554   maxlim: 286720   bits: 20/19
c ---[ 352]---> Adder-cost: 150   maxlim: 286720   bits: 20/19
c ---[ 350]---> Adder-cost: 526   maxlim: 275456   bits: 20/19
c ---[ 348]---> Adder-cost: 500   maxlim: 277504   bits: 20/19
c ---[ 346]---> Adder-cost: 590   maxlim: 316416   bits: 20/19
c ---[ 344]---> Adder-cost: 154   maxlim: 316416   bits: 20/19
c ---[ 342]---> Adder-cost: 328   maxlim: 174080   bits: 19/18
c ---[ 340]---> Adder-cost: 106   maxlim: 174080   bits: 19/18
c ---[ 338]---> Adder-cost: 540   maxlim: 277504   bits: 20/19
c ---[ 336]---> Adder-cost: 515   maxlim: 275456   bits: 20/19
c ---[ 334]---> Adder-cost: 362   maxlim: 207872   bits: 19/18
c ---[ 332]---> Adder-cost: 108   maxlim: 207872   bits: 19/18
c ---[ 330]---> Adder-cost: 310   maxlim: 160768   bits: 19/18
c ---[ 328]---> Adder-cost: 94   maxlim: 160768   bits: 19/18
c ---[ 326]---> Adder-cost: 296   maxlim: 154624   bits: 19/18
c ---[ 324]---> Adder-cost: 92   maxlim: 154624   bits: 19/18
c ---[ 322]---> Adder-cost: 328   maxlim: 166912   bits: 19/18
c ---[ 320]---> Adder-cost: 100   maxlim: 166912   bits: 19/18
c ---[ 318]---> Adder-cost: 238   maxlim: 126976   bits: 18/17
c ---[ 316]---> Adder-cost: 176   maxlim: 114688   bits: 18/17
c ---[ 314]---> Adder-cost: 336   maxlim: 174080   bits: 19/18
c ---[ 312]---> Adder-cost: 106   maxlim: 174080   bits: 19/18
c ---[ 310]---> Adder-cost: 330   maxlim: 175104   bits: 19/18
c ---[ 308]---> Adder-cost: 102   maxlim: 175104   bits: 19/18
c ---[ 306]---> Adder-cost: 272   maxlim: 151552   bits: 19/18
c ---[ 304]---> Adder-cost: 96   maxlim: 151552   bits: 19/18
c ---[ 302]---> Adder-cost: 212   maxlim: 112640   bits: 18/17
c ---[ 300]---> Adder-cost: 74   maxlim: 112640   bits: 18/17
c ---[ 298]---> Adder-cost: 196   maxlim: 104448   bits: 18/17
c ---[ 296]---> Adder-cost: 148   maxlim: 78848   bits: 18/17
c ---[ 294]---> Adder-cost: 404   maxlim: 209920   bits: 19/18
c ---[ 292]---> Adder-cost: 346   maxlim: 241664   bits: 19/18
c ---[ 290]---> Adder-cost: 126   maxlim: 241664   bits: 19/18
c ---[ 288]---> Adder-cost: 350   maxlim: 190464   bits: 19/18
c ---[ 286]---> Adder-cost: 106   maxlim: 190464   bits: 19/18
c ---[ 284]---> Adder-cost: 490   maxlim: 259072   bits: 19/18
c ---[ 282]---> Adder-cost: 124   maxlim: 259072   bits: 19/18
c ---[ 280]---> Adder-cost: 432   maxlim: 222208   bits: 19/18
c ---[ 278]---> Adder-cost: 114   maxlim: 222208   bits: 19/18
c ---[ 276]---> Adder-cost: 440   maxlim: 227328   bits: 19/18
c ---[ 274]---> Adder-cost: 118   maxlim: 227328   bits: 19/18
c ---[ 272]---> Adder-cost: 348   maxlim: 182272   bits: 19/18
c ---[ 270]---> Adder-cost: 106   maxlim: 182272   bits: 19/18
c ---[ 268]---> Adder-cost: 290   maxlim: 158720   bits: 19/18
c ---[ 266]---> Adder-cost: 92   maxlim: 158720   bits: 19/18
c ---[ 264]---> Adder-cost: 342   maxlim: 172032   bits: 19/18
c ---[ 262]---> Adder-cost: 102   maxlim: 172032   bits: 19/18
c ---[ 260]---> Adder-cost: 160   maxlim: 86016   bits: 18/17
c ---[ 258]---> Adder-cost: 284   maxlim: 154624   bits: 19/18
c ---[ 256]---> Adder-cost: 92   maxlim: 154624   bits: 19/18
c ---[ 254]---> Adder-cost: 290   maxlim: 158720   bits: 19/18
c ---[ 252]---> Adder-cost: 318   maxlim: 188416   bits: 19/18
c ---[ 250]---> Adder-cost: 288   maxlim: 162816   bits: 19/18
c ---[ 248]---> Adder-cost: 92   maxlim: 162816   bits: 19/18
c ---[ 246]---> Adder-cost: 360   maxlim: 186368   bits: 19/18
c ---[ 244]---> Adder-cost: 386   maxlim: 227328   bits: 19/18
c ---[ 242]---> Adder-cost: 508   maxlim: 275456   bits: 20/19
c ---[ 240]---> Adder-cost: 148   maxlim: 275456   bits: 20/19
c ---[ 238]---> Adder-cost: 450   maxlim: 238592   bits: 19/18
c ---[ 236]---> Adder-cost: 300   maxlim: 210944   bits: 19/18
c ---[ 234]---> Adder-cost: 372   maxlim: 194560   bits: 19/18
c ---[ 232]---> Adder-cost: 110   maxlim: 194560   bits: 19/18
c ---[ 230]---> Adder-cost: 454   maxlim: 242688   bits: 19/18
c ---[ 228]---> Adder-cost: 324   maxlim: 202752   bits: 19/18
c ---[ 226]---> Adder-cost: 296   maxlim: 168960   bits: 19/18
c ---[ 224]---> Adder-cost: 100   maxlim: 168960   bits: 19/18
c ---[ 222]---> Adder-cost: 476   maxlim: 247808   bits: 19/18
c ---[ 220]---> Adder-cost: 416   maxlim: 250880   bits: 19/18
c ---[ 218]---> Adder-cost: 350   maxlim: 192512   bits: 19/18
c ---[ 216]---> Adder-cost: 110   maxlim: 192512   bits: 19/18
c ---[ 214]---> Adder-cost: 330   maxlim: 167936   bits: 19/18
c ---[ 212]---> Adder-cost: 188   maxlim: 108544   bits: 18/17
c ---[ 210]---> Adder-cost: 172   maxlim: 90112   bits: 18/17
c ---[ 208]---> Adder-cost: 72   maxlim: 90112   bits: 18/17
c ---[ 206]---> Adder-cost: 272   maxlim: 137216   bits: 19/18
c ---[ 204]---> Adder-cost: 170   maxlim: 118784   bits: 18/17
c ---[ 202]---> Adder-cost: 148   maxlim: 91136   bits: 18/17
c ---[ 200]---> Adder-cost: 150   maxlim: 90112   bits: 18/17
c ---[ 198]---> Adder-cost: 274   maxlim: 150528   bits: 19/18
c ---[ 196]---> Adder-cost: 308   maxlim: 183296   bits: 19/18
c ---[ 194]---> Adder-cost: 104   maxlim: 183296   bits: 19/18
c ---[ 192]---> Adder-cost: 452   maxlim: 239616   bits: 19/18
c ---[ 190]---> Adder-cost: 576   maxlim: 345088   bits: 20/19
c ---[ 188]---> Adder-cost: 414   maxlim: 234496   bits: 19/18
c ---[ 186]---> Adder-cost: 120   maxlim: 234496   bits: 19/18
c ---[ 184]---> Adder-cost: 266   maxlim: 141312   bits: 19/18
c ---[ 182]---> Adder-cost: 184   maxlim: 135168   bits: 19/18
c ---[ 180]---> Adder-cost: 298   maxlim: 157696   bits: 19/18
c ---[ 178]---> Adder-cost: 92   maxlim: 157696   bits: 19/18
c ---[ 176]---> Adder-cost: 324   maxlim: 179200   bits: 19/18
c ---[ 174]---> Adder-cost: 358   maxlim: 192512   bits: 19/18
c ---[ 172]---> Adder-cost: 540   maxlim: 292864   bits: 20/19
c ---[ 170]---> Adder-cost: 136   maxlim: 292864   bits: 20/19
c ---[ 168]---> Adder-cost: 414   maxlim: 235520   bits: 19/18
c ---[ 166]---> Adder-cost: 350   maxlim: 233472   bits: 19/18
c ---[ 164]---> Adder-cost: 568   maxlim: 310272   bits: 20/19
c ---[ 162]---> Adder-cost: 148   maxlim: 310272   bits: 20/19
c ---[ 160]---> Adder-cost: 574   maxlim: 310272   bits: 20/19
c ---[ 158]---> Adder-cost: 266   maxlim: 254976   bits: 19/18
c ---[ 156]---> Adder-cost: 244   maxlim: 128000   bits: 18/17
c ---[ 154]---> Adder-cost: 78   maxlim: 128000   bits: 18/17
c ---[ 152]---> Adder-cost: 364   maxlim: 186368   bits: 19/18
c ---[ 150]---> Adder-cost: 202   maxlim: 113664   bits: 18/17
c ---[ 148]---> Adder-cost: 138   maxlim: 79872   bits: 18/17
c ---[ 146]---> Adder-cost: 62   maxlim: 79872   bits: 18/17
c ---[ 144]---> Adder-cost: 160   maxlim: 78848   bits: 18/17
c ---[ 142]---> Adder-cost: 118   maxlim: 64512   bits: 17/16
c ---[ 140]---> Adder-cost: 84   maxlim: 52224   bits: 17/16
c ---[ 138]---> Adder-cost: 116   maxlim: 60416   bits: 17/16
c ---[ 136]---> Adder-cost: 94   maxlim: 66560   bits: 18/17
c ---[ 134]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[ 132]---> Adder-cost: 180   maxlim: 95232   bits: 18/17
c ---[ 130]---> Adder-cost: 70   maxlim: 95232   bits: 18/17
c ---[ 128]---> Adder-cost: 284   maxlim: 150528   bits: 19/18
c ---[ 126]---> Adder-cost: 256   maxlim: 151552   bits: 19/18
c ---[ 124]---> Adder-cost: 268   maxlim: 136192   bits: 19/18
c ---[ 122]---> Adder-cost: 88   maxlim: 136192   bits: 19/18
c ---[ 120]---> Adder-cost: 336   maxlim: 174080   bits: 19/18
c ---[ 118]---> Adder-cost: 106   maxlim: 174080   bits: 19/18
c ---[ 116]---> Adder-cost: 355   maxlim: 182272   bits: 19/18
c ---[ 114]---> Adder-cost: 106   maxlim: 182272   bits: 19/18
c ---[ 112]---> Adder-cost: 206   maxlim: 108544   bits: 18/17
c ---[ 110]---> Adder-cost: 78   maxlim: 108544   bits: 18/17
c ---[ 108]---> Adder-cost: 266   maxlim: 132096   bits: 19/18
c ---[ 106]---> Adder-cost: 90   maxlim: 132096   bits: 19/18
c ---[ 104]---> Adder-cost: 274   maxlim: 138240   bits: 19/18
c ---[ 102]---> Adder-cost: 88   maxlim: 138240   bits: 19/18
c ---[ 100]---> Adder-cost: 88   maxlim: 138240   bits: 19/18
c ---[  98]---> Adder-cost: 170   maxlim: 89088   bits: 18/17
c ---[  96]---> Adder-cost: 68   maxlim: 89088   bits: 18/17
c ---[  94]---> Adder-cost: 104   maxlim: 51200   bits: 17/16
c ---[  92]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[  90]---> Sorter-cost:  991     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  88]---> Adder-cost: 402   maxlim: 230400   bits: 19/18
c ---[  86]---> Adder/oldhome/oroussel/solvers/minisat+_script: line 16:  2178 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.93 0.98 0.93 2/54 2173
Raw data (stat): 2173 (runsolver) R 2172 15547 15546 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783780540 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.0008 s]
Raw data (loadavg): 0.94 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.0014 s]
Raw data (loadavg): 0.95 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.0007 s]
Raw data (loadavg): 0.95 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.0013 s]
Raw data (loadavg): 0.96 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.0019 s]
Raw data (loadavg): 0.97 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.0021 s]
Raw data (loadavg): 0.97 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.0016 s]
Raw data (loadavg): 0.97 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.0019 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.0021 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.001 s]
Raw data (loadavg): 0.98 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.002 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.004 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.003 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.011 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.016 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.015 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.013 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.014 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.124 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.124 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.128 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.128 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.127 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.128 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.128 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.127 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.128 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.128 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.128 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.128 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.127 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.127 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.126 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.127 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.126 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.126 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.127 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.126 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.128 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.127 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.126 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.127 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.127 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.127 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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.13 s]
Raw data (loadavg): 0.99 0.98 0.93 2/55 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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+1229.85 s]
Raw data (loadavg): 0.99 0.98 0.93 1/53 2178
Raw data (stat): 2173 (minisat+_script) S 2172 15547 15546 0 -1 0 300 361 0 0 0 0 4 2 18 0 1 0 783780540 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): 1229.85
CPU time (s): 1230.02
CPU user time (s): 1227.79
CPU system time (s): 2.23066
CPU usage (%): 100.014
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####