PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-dolom1.opb
MD5SUM	fe8b094f76209ea2b750f65d04b1eb0e
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	47560
Biggest coefficient in the objective function	524288000000000000
Number of bits for the biggest coefficient in the objective function	59
Sum of the numbers in the objective function	35144117773963558912
Number of bits of the sum of numbers in the objective function	65
Biggest number in a constraint	524288000000000000
Number of bits of the biggest number in a constraint	59
Biggest sum of numbers in a constraint	35156917773963558912
Number of bits of the biggest sum of numbers	65
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.444932
Number of variables	47560
Total number of constraints	11523
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9721
Number of constraints which are nor clauses,nor cardinality constraints	1802
Minimum length of a constraint	1
Maximum length of a constraint	47560
Trace number 31337

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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:        732620 kB
Buffers:         32364 kB
Cached:         244868 kB
SwapCached:        412 kB
Active:          39532 kB
Inactive:       240048 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        732368 kB
SwapTotal:     2097136 kB
SwapFree:      2096036 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            16764 kB
Committed_AS:    63724 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:38:04 (client local time) WITH STATUS 152 IN 1230.31 SECONDS
stats: 22732 7 1230.31 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c PARSE ERROR! [line 11616] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 3495 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[3556]---> Adder-cost: 192   maxlim: 12160   bits: 15/14
c ---[3554]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[3552]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[3550]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[3548]---> Adder-cost: 120   maxlim: 7424   bits: 14/13
c ---[3546]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[3544]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[3542]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[3540]---> Sorter-cost:  653     Base: 2 2 2 2 2 2 2 7
c ---[3538]---> Adder-cost: 94   maxlim: 5888   bits: 14/13
c ---[3536]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[3534]---> Adder-cost: 136   maxlim: 8576   bits: 15/14
c ---[3532]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[3530]---> Adder-cost: 102   maxlim: 6656   bits: 14/13
c ---[3528]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[3526]---> Adder-cost: 80   maxlim: 5120   bits: 14/13
c ---[3524]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[3522]---> Adder-cost: 82   maxlim: 5632   bits: 14/13
c ---[3520]---> Adder-cost: 132   maxlim: 8704   bits: 15/14
c ---[3518]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[3516]---> Adder-cost: 124   maxlim: 10880   bits: 15/14
c ---[3514]---> Adder-cost: 66   maxlim: 10880   bits: 15/14
c ---[3512]---> Adder-cost: 142   maxlim: 10240   bits: 15/14
c ---[3510]---> Adder-cost: 68   maxlim: 10240   bits: 15/14
c ---[3508]---> Adder-cost: 74   maxlim: 5632   bits: 14/13
c ---[3506]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[3504]---> Adder-cost: 108   maxlim: 6784   bits: 14/13
c ---[3502]---> Adder-cost: 102   maxlim: 6528   bits: 14/13
c ---[3500]---> Sorter-cost:  644     Base: 2 2 2 2 2 2 2 7
c ---[3498]---> Adder-cost: 124   maxlim: 7680   bits: 14/13
c ---[3496]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[3494]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[3492]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[3490]---> Adder-cost: 94   maxlim: 6144   bits: 14/13
c ---[3488]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[3486]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[3484]---> Adder-cost: 124   maxlim: 8832   bits: 15/14
c ---[3482]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[3480]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[3478]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[3476]---> Sorter-cost:  620     Base: 2 2 2 2 2 2 2 7
c ---[3474]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[3472]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[3470]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[3468]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[3466]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[3464]---> Adder-cost: 102   maxlim: 7040   bits: 14/13
c ---[3462]---> Sorter-cost:  932     Base: 2 2 2 2 2 2 2 7
c ---[3460]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[3458]---> Adder-cost: 154   maxlim: 9216   bits: 15/14
c ---[3456]---> Adder-cost: 252   maxlim: 15872   bits: 15/14
c ---[3454]---> Adder-cost: 340   maxlim: 21376   bits: 16/15
c ---[3452]---> Adder-cost: 324   maxlim: 22912   bits: 16/15
c ---[3450]---> Adder-cost: 158   maxlim: 9984   bits: 15/14
c ---[3448]---> Sorter-cost:  883     Base: 2 2 2 2 2 2 2 7
c ---[3446]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[3444]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[3442]---> Adder-cost: 232   maxlim: 14976   bits: 15/14
c ---[3440]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[3438]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[3436]---> Adder-cost: 90   maxlim: 5632   bits: 14/13
c ---[3434]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[3432]---> Adder-cost: 78   maxlim: 6400   bits: 14/13
c ---[3430]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[3428]---> Adder-cost: 112   maxlim: 14720   bits: 15/14
c ---[3426]---> Adder-cost: 82   maxlim: 5504   bits: 14/13
c ---[3424]---> Sorter-cost:  308     Base: 2 2 2 2 2 2 2 2
c ---[3422]---> Sorter-cost: 1015     Base: 2 2 2 2 2 2 2 7
c ---[3420]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[3418]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[3416]---> Adder-cost: 162   maxlim: 14464   bits: 15/14
c ---[3414]---> Adder-cost: 90   maxlim: 6656   bits: 14/13
c ---[3412]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[3410]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[3408]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[3406]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[3404]---> Adder-cost: 90   maxlim: 6016   bits: 14/13
c ---[3402]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[3400]---> Adder-cost: 216   maxlim: 15360   bits: 15/14
c ---[3398]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[3396]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[3394]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[3392]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[3390]---> Sorter-cost: 1051     Base: 2 2 2 2 2 2 2 7
c ---[3388]---> Adder-cost: 520   maxlim: 33024   bits: 17/16
c ---[3386]---> Adder-cost: 138   maxlim: 33024   bits: 17/16
c ---[3384]---> Adder-cost: 80   maxlim: 15360   bits: 15/14
c ---[3382]---> Adder-cost: 74   maxlim: 4480   bits: 14/13
c ---[3380]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[3378]---> Adder-cost: 194   maxlim: 12544   bits: 15/14
c ---[3376]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[3374]---> Sorter-cost:  597     Base: 2 2 2 2 2 2 2 7
c ---[3372]---> Adder-cost: 80   maxlim: 15360   bits: 15/14
c ---[3370]---> Adder-cost: 210   maxlim: 13184   bits: 15/14
c ---[3368]---> Adder-cost: 74   maxlim: 13184   bits: 15/14
c ---[3366]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[3364]---> Adder-cost: 176   maxlim: 10752   bits: 15/14
c ---[3362]---> Adder-cost: 184   maxlim: 11648   bits: 15/14
c ---[3360]---> Adder-cost: 118   maxlim: 7424   bits: 14/13
c ---[3358]---> Adder-cost: 134   maxlim: 8576   bits: 15/14
c ---[3356]---> Adder-cost: 142   maxlim: 9856   bits: 15/14
c ---[3354]---> Sorter-cost:  644     Base: 2 2 2 2 2 2 2 7
c ---[3352]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[3350]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[3348]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 7
c ---[3346]---> Adder-cost: 176   maxlim: 10752   bits: 15/14
c ---[3344]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[3342]---> Adder-cost: 140   maxlim: 8320   bits: 15/14
c ---[3340]---> Adder-cost: 68   maxlim: 7424   bits: 14/13
c ---[3338]---> Adder-cost: 86   maxlim: 5888   bits: 14/13
c ---[3336]---> Adder-cost: 144   maxlim: 9216   bits: 15/14
c ---[3334]---> Adder-cost: 62   maxlim: 9216   bits: 15/14
c ---[3332]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[3330]---> Adder-cost: 66   maxlim: 7424   bits: 14/13
c ---[3328]---> Adder-cost: 122   maxlim: 7808   bits: 14/13
c ---[3326]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[3324]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[3322]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[3320]---> Adder-cost: 146   maxlim: 8832   bits: 15/14
c ---[3318]---> Adder-cost: 124   maxlim: 8192   bits: 15/14
c ---[3316]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[3314]---> Adder-cost: 92   maxlim: 6784   bits: 14/13
c ---[3312]---> Adder-cost: 170   maxlim: 10496   bits: 15/14
c ---[3310]---> Adder-cost: 252   maxlim: 16000   bits: 15/14
c ---[3308]---> Adder-cost: 108   maxlim: 7552   bits: 14/13
c ---[3306]---> Adder-cost: 70   maxlim: 5760   bits: 14/13
c ---[3304]---> Adder-cost: 236   maxlim: 15616   bits: 15/14
c ---[3302]---> Adder-cost: 92   maxlim: 6528   bits: 14/13
c ---[3300]---> Adder-cost: 274   maxlim: 17024   bits: 16/15
c ---[3298]---> Adder-cost: 198   maxlim: 12800   bits: 15/14
c ---[3296]---> Adder-cost: 122   maxlim: 7936   bits: 14/13
c ---[3294]---> Adder-cost: 190   maxlim: 11776   bits: 15/14
c ---[3292]---> Adder-cost: 192   maxlim: 12032   bits: 15/14
c ---[3290]---> Adder-cost: 168   maxlim: 12160   bits: 15/14
c ---[3288]---> Adder-cost: 140   maxlim: 8192   bits: 15/14
c ---[3286]---> Adder-cost: 94   maxlim: 6784   bits: 14/13
c ---[3284]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[3282]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 7
c ---[3280]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[3278]---> Sorter-cost:  453     Base: 2 2 2 2 2 2 2 7
c ---[3276]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[3274]---> Adder-cost: 208   maxlim: 13184   bits: 15/14
c ---[3272]---> Adder-cost: 202   maxlim: 13568   bits: 15/14
c ---[3270]---> Adder-cost: 108   maxlim: 8448   bits: 15/14
c ---[3268]---> Adder-cost: 140   maxlim: 12928   bits: 15/14
c ---[3266]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[3264]---> Adder-cost: 84   maxlim: 5760   bits: 14/13
c ---[3262]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[3260]---> Sorter-cost:  608     Base: 2 2 2 2 2 2 2 7
c ---[3258]---> Adder-cost: 170   maxlim: 10240   bits: 15/14
c ---[3256]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[3254]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[3252]---> Adder-cost: 100   maxlim: 6144   bits: 14/13
c ---[3250]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[3248]---> Adder-cost: 78   maxlim: 4736   bits: 14/13
c ---[3246]---> Adder-cost: 60   maxlim: 4480   bits: 14/13
c ---[3244]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[3242]---> Adder-cost: 120   maxlim: 7680   bits: 14/13
c ---[3240]---> Adder-cost: 286   maxlim: 18048   bits: 16/15
c ---[3238]---> Adder-cost: 80   maxlim: 6656   bits: 14/13
c ---[3236]---> Adder-cost: 78   maxlim: 4992   bits: 14/13
c ---[3234]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[3232]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[3230]---> Sorter-cost:  722     Base: 2 2 2 2 2 2 2 7
c ---[3228]---> Sorter-cost:  561     Base: 2 2 2 2 2 2 2 7
c ---[3226]---> Sorter-cost:  699     Base: 2 2 2 2 2 2 2 7
c ---[3224]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 7
c ---[3222]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[3220]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[3218]---> Adder-cost: 86   maxlim: 5120   bits: 14/13
c ---[3216]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[3214]---> Adder-cost: 84   maxlim: 5248   bits: 14/13
c ---[3212]---> Adder-cost: 156   maxlim: 9472   bits: 15/14
c ---[3210]---> Adder-cost: 74   maxlim: 4480   bits: 14/13
c ---[3208]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[3206]---> Adder-cost: 270   maxlim: 16896   bits: 16/15
c ---[3204]---> Adder-cost: 120   maxlim: 7552   bits: 14/13
c ---[3202]---> Adder-cost: 174   maxlim: 10880   bits: 15/14
c ---[3200]---> Adder-cost: 110   maxlim: 6656   bits: 14/13
c ---[3198]---> Adder-cost: 90   maxlim: 6784   bits: 14/13
c ---[3196]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[3194]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[3192]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[3190]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[3188]---> Sorter-cost:  513     Base: 2 2 2 2 2 2 2 7
c ---[3186]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 7
c ---[3184]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[3182]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[3180]---> Adder-cost: 162   maxlim: 9984   bits: 15/14
c ---[3178]---> Adder-cost: 206   maxlim: 13056   bits: 15/14
c ---[3176]---> Adder-cost: 198   maxlim: 12416   bits: 15/14
c ---[3174]---> Adder-cost: 234   maxlim: 14592   bits: 15/14
c ---[3172]---> Adder-cost: 328   maxlim: 23936   bits: 16/15
c ---[3170]---> Adder-cost: 140   maxlim: 8448   bits: 15/14
c ---[3168]---> Adder-cost: 144   maxlim: 8704   bits: 15/14
c ---[3166]---> Adder-cost: 192   maxlim: 12416   bits: 15/14
c ---[3164]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[3162]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[3160]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[3158]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[3156]---> Adder-cost: 222   maxlim: 13952   bits: 15/14
c ---[3154]---> Adder-cost: 330   maxlim: 21760   bits: 16/15
c ---[3152]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[3150]---> Adder-cost: 112   maxlim: 7040   bits: 14/13
c ---[3148]---> Adder-cost: 92   maxlim: 6656   bits: 14/13
c ---[3146]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[3144]---> Adder-cost: 130   maxlim: 8320   bits: 15/14
c ---[3142]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[3140]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[3138]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[3136]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[3134]---> Adder-cost: 182   maxlim: 11648   bits: 15/14
c ---[3132]---> Adder-cost: 118   maxlim: 7552   bits: 14/13
c ---[3130]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[3128]---> Sorter-cost:  784     Base: 2 2 2 2 2 2 2 7
c ---[3126]---> Adder-cost: 124   maxlim: 7808   bits: 14/13
c ---[3124]---> Adder-cost: 190   maxlim: 12032   bits: 15/14
c ---[3122]---> Adder-cost: 224   maxlim: 15488   bits: 15/14
c ---[3120]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[3118]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[3116]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[3114]---> Adder-cost: 114   maxlim: 7552   bits: 14/13
c ---[3112]---> Adder-cost: 70   maxlim: 4480   bits: 14/13
c ---[3110]---> Adder-cost: 186   maxlim: 11520   bits: 15/14
c ---[3108]---> Adder-cost: 90   maxlim: 5632   bits: 14/13
c ---[3106]---> Adder-cost: 230   maxlim: 15232   bits: 15/14
c ---[3104]---> Sorter-cost:  600     Base: 2 2 2 2 2 2 2 7
c ---[3102]---> Adder-cost: 104   maxlim: 6144   bits: 14/13
c ---[3100]---> Adder-cost: 182   maxlim: 11520   bits: 15/14
c ---[3098]---> Adder-cost: 122   maxlim: 7680   bits: 14/13
c ---[3096]---> Adder-cost: 244   maxlim: 15616   bits: 15/14
c ---[3094]---> Adder-cost: 120   maxlim: 7808   bits: 14/13
c ---[3092]---> Adder-cost: 112   maxlim: 7552   bits: 14/13
c ---[3090]---> Adder-cost: 230   maxlim: 14592   bits: 15/14
c ---[3088]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[3086]---> Adder-cost: 424   maxlim: 27136   bits: 16/15
c ---[3084]---> Adder-cost: 118   maxlim: 27136   bits: 16/15
c ---[3082]---> Adder-cost: 120   maxlim: 7808   bits: 14/13
c ---[3080]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[3078]---> Adder-cost: 96   maxlim: 7680   bits: 14/13
c ---[3076]---> Adder-cost: 308   maxlim: 20352   bits: 16/15
c ---[3074]---> Adder-cost: 226   maxlim: 14848   bits: 15/14
c ---[3072]---> Adder-cost: 140   maxlim: 8704   bits: 15/14
c ---[3070]---> Adder-cost: 94   maxlim: 5888   bits: 14/13
c ---[3068]---> Adder-cost: 182   maxlim: 12928   bits: 15/14
c ---[3066]---> Adder-cost: 154   maxlim: 9984   bits: 15/14
c ---[3064]---> Adder-cost: 62   maxlim: 9984   bits: 15/14
c ---[3062]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[3060]---> Adder-cost: 202   maxlim: 12416   bits: 15/14
c ---[3058]---> Adder-cost: 122   maxlim: 7680   bits: 14/13
c ---[3056]---> Adder-cost: 218   maxlim: 13568   bits: 15/14
c ---[3054]---> Adder-cost: 140   maxlim: 8576   bits: 15/14
c ---[3052]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[3050]---> Adder-cost: 148   maxlim: 10368   bits: 15/14
c ---[3048]---> Adder-cost: 126   maxlim: 9088   bits: 15/14
c ---[3046]---> Adder-cost: 258   maxlim: 17280   bits: 16/15
c ---[3044]---> Adder-cost: 92   maxlim: 8320   bits: 15/14
c ---[3042]---> Sorter-cost:  958     Base: 2 2 2 2 2 2 2 7
c ---[3040]---> Adder-cost: 144   maxlim: 10496   bits: 15/14
c ---[3038]---> Adder-cost: 106   maxlim: 10112   bits: 15/14
c ---[3036]---> Adder-cost: 136   maxlim: 12288   bits: 15/14
c ---[3034]---> Adder-cost: 100   maxlim: 7552   bits: 14/13
c ---[3032]---> Sorter-cost:  905     Base: 2 2 2 2 2 2 2 7
c ---[3030]---> Adder-cost: 248   maxlim: 15872   bits: 15/14
c ---[3028]---> Adder-cost: 138   maxlim: 8576   bits: 15/14
c ---[3026]---> Adder-cost: 84   maxlim: 5504   bits: 14/13
c ---[3024]---> Adder-cost: 114   maxlim: 7424   bits: 14/13
c ---[3022]---> Sorter-cost: 1019     Base: 2 2 2 2 2 2 2 7
c ---[3020]---> Adder-cost: 126   maxlim: 8576   bits: 15/14
c ---[3018]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[3016]---> Adder-cost: 174   maxlim: 11136   bits: 15/14
c ---[3014]---> Adder-cost: 130   maxlim: 10880   bits: 15/14
c ---[3012]---> Adder-cost: 136   maxlim: 12160   bits: 15/14
c ---[3010]---> Adder-cost: 242   maxlim: 15360   bits: 15/14
c ---[3008]---> Adder-cost: 142   maxlim: 9088   bits: 15/14
c ---[3006]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[3004]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[3002]---> Adder-cost: 104   maxlim: 6400   bits: 14/13
c ---[3000]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[2998]---> Adder-cost: 94   maxlim: 5888   bits: 14/13
c ---[2996]---> Adder-cost: 104   maxlim: 6656   bits: 14/13
c ---[2994]---> Adder-cost: 186   maxlim: 12800   bits: 15/14
c ---[2992]---> Adder-cost: 202   maxlim: 12544   bits: 15/14
c ---[2990]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[2988]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[2986]---> Sorter-cost:  994     Base: 2 2 2 2 2 2 2 7
c ---[2984]---> Sorter-cost:  899     Base: 2 2 2 2 2 2 2 7
c ---[2982]---> Sorter-cost:  810     Base: 2 2 2 2 2 2 2 7
c ---[2980]---> Adder-cost: 90   maxlim: 5632   bits: 14/13
c ---[2978]---> Sorter-cost:  951     Base: 2 2 2 2 2 2 2 7
c ---[2976]---> Adder-cost: 138   maxlim: 8320   bits: 15/14
c ---[2974]---> Adder-cost: 84   maxlim: 6656   bits: 14/13
c ---[2972]---> Adder-cost: 182   maxlim: 12288   bits: 15/14
c ---[2970]---> Adder-cost: 188   maxlim: 12928   bits: 15/14
c ---[2968]---> Adder-cost: 184   maxlim: 13696   bits: 15/14
c ---[2966]---> Adder-cost: 110   maxlim: 6912   bits: 14/13
c ---[2964]---> Adder-cost: 48   maxlim: 6912   bits: 14/13
c ---[2962]---> Adder-cost: 78   maxlim: 6528   bits: 14/13
c ---[2960]---> Adder-cost: 98   maxlim: 8064   bits: 14/13
c ---[2958]---> Adder-cost: 98   maxlim: 7168   bits: 14/13
c ---[2956]---> Adder-cost: 70   maxlim: 6784   bits: 14/13
c ---[2954]---> Adder-cost: 100   maxlim: 7424   bits: 14/13
c ---[2952]---> Adder-cost: 106   maxlim: 6784   bits: 14/13
c ---[2950]---> Adder-cost: 98   maxlim: 7296   bits: 14/13
c ---[2948]---> Adder-cost: 284   maxlim: 19328   bits: 16/15
c ---[2946]---> Adder-cost: 280   maxlim: 20736   bits: 16/15
c ---[2944]---> Adder-cost: 268   maxlim: 20480   bits: 16/15
c ---[2942]---> Adder-cost: 88   maxlim: 5760   bits: 14/13
c ---[2940]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[2938]---> Adder-cost: 102   maxlim: 6400   bits: 14/13
c ---[2936]---> Adder-cost: 86   maxlim: 5632   bits: 14/13
c ---[2934]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[2932]---> Adder-cost: 98   maxlim: 6272   bits: 14/13
c ---[2930]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[2928]---> Adder-cost: 78   maxlim: 6528   bits: 14/13
c ---[2926]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2924]---> Adder-cost: 66   maxlim: 10880   bits: 15/14
c ---[2922]---> Adder-cost: 158   maxlim: 10624   bits: 15/14
c ---[2920]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[2918]---> Adder-cost: 184   maxlim: 11904   bits: 15/14
c ---[2916]---> Adder-cost: 132   maxlim: 8320   bits: 15/14
c ---[2914]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[2912]---> Adder-cost: 86   maxlim: 8448   bits: 15/14
c ---[2910]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[2908]---> Adder-cost: 142   maxlim: 8448   bits: 15/14
c ---[2906]---> Adder-cost: 112   maxlim: 6912   bits: 14/13
c ---[2904]---> Adder-cost: 48   maxlim: 6912   bits: 14/13
c ---[2902]---> Adder-cost: 248   maxlim: 16640   bits: 16/15
c ---[2900]---> Adder-cost: 234   maxlim: 15744   bits: 15/14
c ---[2898]---> Adder-cost: 86   maxlim: 5376   bits: 14/13
c ---[2896]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[2894]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[2892]---> Adder-cost: 78   maxlim: 4992   bits: 14/13
c ---[2890]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[2888]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[2886]---> Adder-cost: 68   maxlim: 4736   bits: 14/13
c ---[2884]---> Adder-cost: 54   maxlim: 4992   bits: 14/13
c ---[2882]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[2880]---> Adder-cost: 196   maxlim: 13056   bits: 15/14
c ---[2878]---> Adder-cost: 146   maxlim: 9216   bits: 15/14
c ---[2876]---> Adder-cost: 78   maxlim: 4736   bits: 14/13
c ---[2874]---> Adder-cost: 90   maxlim: 7680   bits: 14/13
c ---[2872]---> Adder-cost: 196   maxlim: 13440   bits: 15/14
c ---[2870]---> Adder-cost: 118   maxlim: 7424   bits: 14/13
c ---[2868]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[2866]---> Adder-cost: 82   maxlim: 5504   bits: 14/13
c ---[2864]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[2862]---> Sorter-cost:  431     Base: 2 2 2 2 2 2 2 7
c ---[2860]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[2858]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[2856]---> Adder-cost: 278   maxlim: 20480   bits: 16/15
c ---[2854]---> Adder-cost: 276   maxlim: 17920   bits: 16/15
c ---[2852]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[2850]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[2848]---> Adder-cost: 80   maxlim: 6784   bits: 14/13
c ---[2846]---> Adder-cost: 104   maxlim: 6784   bits: 14/13
c ---[2844]---> Adder-cost: 80   maxlim: 6400   bits: 14/13
c ---[2842]---> Adder-cost: 88   maxlim: 5632   bits: 14/13
c ---[2840]---> Adder-cost: 194   maxlim: 13184   bits: 15/14
c ---[2838]---> Adder-cost: 88   maxlim: 6784   bits: 14/13
c ---[2836]---> Adder-cost: 274   maxlim: 20096   bits: 16/15
c ---[2834]---> Adder-cost: 226   maxlim: 17024   bits: 16/15
c ---[2832]---> Adder-cost: 124   maxlim: 8064   bits: 14/13
c ---[2830]---> Adder-cost: 84   maxlim: 6144   bits: 14/13
c ---[2828]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 7
c ---[2826]---> Sorter-cost:  914     Base: 2 2 2 2 2 2 2 7
c ---[2824]---> Adder-cost: 156   maxlim: 10368   bits: 15/14
c ---[2822]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[2820]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[2818]---> Sorter-cost:  901     Base: 2 2 2 2 2 2 2 7
c ---[2816]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 7
c ---[2814]---> Sorter-cost:  986     Base: 2 2 2 2 2 2 2 7
c ---[2812]---> Sorter-cost: 1038     Base: 2 2 2 2 2 2 2 7
c ---[2810]---> Adder-cost: 68   maxlim: 10368   bits: 15/14
c ---[2808]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 7
c ---[2806]---> Sorter-cost:  696     Base: 2 2 2 2 2 2 2 7
c ---[2804]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[2802]---> Sorter-cost:  569     Base: 2 2 2 2 2 2 2 7
c ---[2800]---> Adder-cost: 170   maxlim: 11904   bits: 15/14
c ---[2798]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 7
c ---[2796]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[2794]---> Sorter-cost:  547     Base: 2 2 2 2 2 2 2 7
c ---[2792]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[2790]---> Adder-cost: 126   maxlim: 8064   bits: 14/13
c ---[2788]---> Adder-cost: 76   maxlim: 7680   bits: 14/13
c ---[2786]---> Adder-cost: 80   maxlim: 6016   bits: 14/13
c ---[2784]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[2782]---> Adder-cost: 102   maxlim: 6144   bits: 14/13
c ---[2780]---> Adder-cost: 238   maxlim: 15488   bits: 15/14
c ---[2778]---> Adder-cost: 108   maxlim: 6912   bits: 14/13
c ---[2776]---> Adder-cost: 158   maxlim: 10496   bits: 15/14
c ---[2774]---> Adder-cost: 68   maxlim: 10496   bits: 15/14
c ---[2772]---> Adder-cost: 172   maxlim: 10624   bits: 15/14
c ---[2770]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[2768]---> Adder-cost: 184   maxlim: 11776   bits: 15/14
c ---[2766]---> Adder-cost: 70   maxlim: 11776   bits: 15/14
c ---[2764]---> Adder-cost: 120   maxlim: 12160   bits: 15/14
c ---[2762]---> Adder-cost: 174   maxlim: 12032   bits: 15/14
c ---[2760]---> Adder-cost: 244   maxlim: 15360   bits: 15/14
c ---[2758]---> Adder-cost: 104   maxlim: 12416   bits: 15/14
c ---[2756]---> Adder-cost: 70   maxlim: 12416   bits: 15/14
c ---[2754]---> Adder-cost: 146   maxlim: 10880   bits: 15/14
c ---[2752]---> Adder-cost: 122   maxlim: 9856   bits: 15/14
c ---[2750]---> Adder-cost: 84   maxlim: 6272   bits: 14/13
c ---[2748]---> Adder-cost: 180   maxlim: 14976   bits: 15/14
c ---[2746]---> Adder-cost: 118   maxlim: 7808   bits: 14/13
c ---[2744]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[2742]---> Adder-cost: 108   maxlim: 7680   bits: 14/13
c ---[2740]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[2738]---> Adder-cost: 110   maxlim: 7808   bits: 14/13
c ---[2736]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[2734]---> Adder-cost: 104   maxlim: 7040   bits: 14/13
c ---[2732]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[2730]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[2728]---> Adder-cost: 218   maxlim: 14848   bits: 15/14
c ---[2726]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[2724]---> Sorter-cost:  360     Base: 2 2 2 2 2 2 2 7
c ---[2722]---> Adder-cost: 86   maxlim: 5120   bits: 14/13
c ---[2720]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2
c ---[2718]---> Adder-cost: 74   maxlim: 4992   bits: 14/13
c ---[2716]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[2714]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[2712]---> Adder-cost: 80   maxlim: 14848   bits: 15/14
c ---[2710]---> Sorter-cost:  734     Base: 2 2 2 2 2 2 2 7
c ---[2708]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2706]---> Sorter-cost:  298     Base: 2 2 2 2 2 2 2 2
c ---[2704]---> Sorter-cost:  992     Base: 2 2 2 2 2 2 2 7
c ---[2702]---> Adder-cost: 104   maxlim: 6784   bits: 14/13
c ---[2700]---> Adder-cost: 238   maxlim: 15104   bits: 15/14
c ---[2698]---> Sorter-cost:  650     Base: 2 2 2 2 2 2 2 7
c ---[2696]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[2694]---> Sorter-cost:  610     Base: 2 2 2 2 2 2 2 7
c ---[2692]---> Sorter-cost:  453     Base: 2 2 2 2 2 2 2 7
c ---[2690]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[2688]---> Sorter-cost:  292     Base: 2 2 2 2 2 2 2 2
c ---[2686]---> Adder-cost: 80   maxlim: 15104   bits: 15/14
c ---[2684]---> Adder-cost: 120   maxlim: 8064   bits: 14/13
c ---[2682]---> Adder-cost: 50   maxlim: 8064   bits: 14/13
c ---[2680]---> Adder-cost: 94   maxlim: 6528   bits: 14/13
c ---[2678]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[2676]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[2674]---> Adder-cost: 116   maxlim: 7552   bits: 14/13
c ---[2672]---> Adder-cost: 188   maxlim: 12288   bits: 15/14
c ---[2670]---> Adder-cost: 98   maxlim: 6656   bits: 14/13
c ---[2668]---> Adder-cost: 152   maxlim: 14720   bits: 15/14
c ---[2666]---> Sorter-cost: 1011     Base: 2 2 2 2 2 2 2 7
c ---[2664]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 7
c ---[2662]---> Sorter-cost:  968     Base: 2 2 2 2 2 2 2 7
c ---[2660]---> Sorter-cost:  832     Base: 2 2 2 2 2 2 2 7
c ---[2658]---> Adder-cost: 160   maxlim: 14464   bits: 15/14
c ---[2656]---> Adder-cost: 140   maxlim: 8832   bits: 15/14
c ---[2654]---> Adder-cost: 120   maxlim: 10240   bits: 15/14
c ---[2652]---> Adder-cost: 124   maxlim: 8192   bits: 15/14
c ---[2650]---> Adder-cost: 56   maxlim: 7040   bits: 14/13
c ---[2648]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[2646]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[2644]---> Adder-cost: 152   maxlim: 14336   bits: 15/14
c ---[2642]---> Adder-cost: 188   maxlim: 12288   bits: 15/14
c ---[2640]---> Adder-cost: 138   maxlim: 15744   bits: 15/14
c ---[2638]---> Adder-cost: 78   maxlim: 15744   bits: 15/14
c ---[2636]---> Adder-cost: 204   maxlim: 13568   bits: 15/14
c ---[2634]---> Adder-cost: 82   maxlim: 7552   bits: 14/13
c ---[2632]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 7
c ---[2630]---> Adder-cost: 156   maxlim: 13056   bits: 15/14
c ---[2628]---> Sorter-cost:  653     Base: 2 2 2 2 2 2 2 7
c ---[2626]---> Sorter-cost:  734     Base: 2 2 2 2 2 2 2 7
c ---[2624]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2622]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 7
c ---[2620]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 7
c ---[2618]---> Adder-cost: 128   maxlim: 8960   bits: 15/14
c ---[2616]---> Adder-cost: 80   maxlim: 4864   bits: 14/13
c ---[2614]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 7
c ---[2612]---> Sorter-cost:  580     Base: 2 2 2 2 2 2 2 7
c ---[2610]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[2608]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[2606]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[2604]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[2602]---> Sorter-cost:  565     Base: 2 2 2 2 2 2 2 7
c ---[2600]---> Adder-cost: 146   maxlim: 9728   bits: 15/14
c ---[2598]---> Adder-cost: 202   maxlim: 12928   bits: 15/14
c ---[2596]---> Adder-cost: 204   maxlim: 14464   bits: 15/14
c ---[2594]---> Adder-cost: 82   maxlim: 5120   bits: 14/13
c ---[2592]---> Adder-cost: 92   maxlim: 5888   bits: 14/13
c ---[2590]---> Adder-cost: 46   maxlim: 6784   bits: 14/13
c ---[2588]---> Adder-cost: 382   maxlim: 26368   bits: 16/15
c ---[2586]---> Adder-cost: 130   maxlim: 8320   bits: 15/14
c ---[2584]---> Adder-cost: 200   maxlim: 12544   bits: 15/14
c ---[2582]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[2580]---> Adder-cost: 140   maxlim: 10112   bits: 15/14
c ---[2578]---> Adder-cost: 298   maxlim: 20864   bits: 16/15
c ---[2576]---> Adder-cost: 214   maxlim: 15488   bits: 15/14
c ---[2574]---> Adder-cost: 182   maxlim: 17792   bits: 16/15
c ---[2572]---> Sorter-cost: 1074     Base: 2 2 2 2 2 2 2 7
c ---[2570]---> Sorter-cost: 1001     Base: 2 2 2 2 2 2 2 7
c ---[2568]---> Adder-cost: 190   maxlim: 12288   bits: 15/14
c ---[2566]---> Sorter-cost:  759     Base: 2 2 2 2 2 2 2 7
c ---[2564]---> Sorter-cost:  759     Base: 2 2 2 2 2 2 2 7
c ---[2562]---> Sorter-cost:  759     Base: 2 2 2 2 2 2 2 7
c ---[2560]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[2558]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[2556]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[2554]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[2552]---> Adder-cost: 70   maxlim: 12288   bits: 15/14
c ---[2550]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 7
c ---[2548]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[2546]---> Adder-cost: 130   maxlim: 8320   bits: 15/14
c ---[2544]---> Adder-cost: 88   maxlim: 5888   bits: 14/13
c ---[2542]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[2540]---> Adder-cost: 70   maxlim: 12288   bits: 15/14
c ---[2538]---> Sorter-cost:  256     Base: 2 2 2 2 2 2 2 2
c ---[2536]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[2534]---> Sorter-cost:  390     Base: 2 2 2 2 2 2 2 7
c ---[2532]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2
c ---[2530]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[2528]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 7
c ---[2526]---> Adder-cost: 108   maxlim: 7936   bits: 14/13
c ---[2524]---> Adder-cost: 188   maxlim: 13184   bits: 15/14
c ---[2522]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[2520]---> Adder-cost: 180   maxlim: 12032   bits: 15/14
c ---[2518]---> Adder-cost: 108   maxlim: 7296   bits: 14/13
c ---[2516]---> Adder-cost: 78   maxlim: 4992   bits: 14/13
c ---[2514]---> Adder-cost: 98   maxlim: 6784   bits: 14/13
c ---[2512]---> Sorter-cost:  952     Base: 2 2 2 2 2 2 2 7
c ---[2510]---> Adder-cost: 112   maxlim: 7040   bits: 14/13
c ---[2508]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[2506]---> Adder-cost: 192   maxlim: 12416   bits: 15/14
c ---[2504]---> Adder-cost: 222   maxlim: 14208   bits: 15/14
c ---[2502]---> Adder-cost: 72   maxlim: 14208   bits: 15/14
c ---[2500]---> Adder-cost: 72   maxlim: 14208   bits: 15/14
c ---[2498]---> Adder-cost: 164   maxlim: 10368   bits: 15/14
c ---[2496]---> Adder-cost: 192   maxlim: 13056   bits: 15/14
c ---[2494]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 7
c ---[2492]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[2490]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[2488]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[2486]---> Sorter-cost:  596     Base: 2 2 2 2 2 2 2 7
c ---[2484]---> Adder-cost: 86   maxlim: 5760   bits: 14/13
c ---[2482]---> Sorter-cost:  926     Base: 2 2 2 2 2 2 2 7
c ---[2480]---> Adder-cost: 170   maxlim: 11392   bits: 15/14
c ---[2478]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[2476]---> Adder-cost: 94   maxlim: 6016   bits: 14/13
c ---[2474]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[2472]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[2470]---> Adder-cost: 136   maxlim: 8192   bits: 15/14
c ---[2468]---> Sorter-cost:  782     Base: 2 2 2 2 2 2 2 7
c ---[2466]---> Adder-cost: 116   maxlim: 7424   bits: 14/13
c ---[2464]---> Adder-cost: 180   maxlim: 12544   bits: 15/14
c ---[2462]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[2460]---> Adder-cost: 78   maxlim: 6272   bits: 14/13
c ---[2458]---> Adder-cost: 170   maxlim: 12672   bits: 15/14
c ---[2456]---> Adder-cost: 84   maxlim: 5504   bits: 14/13
c ---[2454]---> Adder-cost: 212   maxlim: 14080   bits: 15/14
c ---[2452]---> Adder-cost: 186   maxlim: 12032   bits: 15/14
c ---[2450]---> Adder-cost: 118   maxlim: 12800   bits: 15/14
c ---[2448]---> Adder-cost: 98   maxlim: 6144   bits: 14/13
c ---[2446]---> Adder-cost: 112   maxlim: 7296   bits: 14/13
c ---[2444]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[2442]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[2440]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[2438]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[2436]---> Adder-cost: 78   maxlim: 5120   bits: 14/13
c ---[2434]---> Adder-cost: 166   maxlim: 10368   bits: 15/14
c ---[2432]---> Adder-cost: 144   maxlim: 8832   bits: 15/14
c ---[2430]---> Adder-cost: 288   maxlim: 21888   bits: 16/15
c ---[2428]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[2426]---> Adder-cost: 120   maxlim: 7808   bits: 14/13
c ---[2424]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[2422]---> Adder-cost: 78   maxlim: 4736   bits: 14/13
c ---[2420]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[2418]---> Adder-cost: 70   maxlim: 4480   bits: 14/13
c ---[2416]---> Adder-cost: 202   maxlim: 12288   bits: 15/14
c ---[2414]---> Adder-cost: 136   maxlim: 8960   bits: 15/14
c ---[2412]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[2410]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[2408]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2406]---> Sorter-cost:  732     Base: 2 2 2 2 2 2 2 7
c ---[2404]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2402]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2400]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[2398]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2396]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2394]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2392]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2390]---> Adder-cost: 162   maxlim: 9984   bits: 15/14
c ---[2388]---> Adder-cost: 214   maxlim: 13312   bits: 15/14
c ---[2386]---> Adder-cost: 78   maxlim: 13312   bits: 15/14
c ---[2384]---> Adder-cost: 270   maxlim: 16768   bits: 16/15
c ---[2382]---> Adder-cost: 52   maxlim: 4352   bits: 14/13
c ---[2380]---> Adder-cost: 232   maxlim: 14336   bits: 15/14
c ---[2378]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[2376]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[2374]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[2372]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[2370]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[2368]---> Adder-cost: 118   maxlim: 7424   bits: 14/13
c ---[2366]---> Adder-cost: 186   maxlim: 11520   bits: 15/14
c ---[2364]---> Adder-cost: 162   maxlim: 11776   bits: 15/14
c ---[2362]---> Adder-cost: 118   maxlim: 11648   bits: 15/14
c ---[2360]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[2358]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 7
c ---[2356]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[2354]---> Adder-cost: 114   maxlim: 9088   bits: 15/14
c ---[2352]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[2350]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[2348]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[2346]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[2344]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[2342]---> Sorter-cost:  559     Base: 2 2 2 2 2 2 2 7
c ---[2340]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 7
c ---[2338]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 7
c ---[2336]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 7
c ---[2334]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[2332]---> Sorter-cost:  944     Base: 2 2 2 2 2 2 2 7
c ---[2330]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[2328]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 7
c ---[2326]---> Adder-cost: 190   maxlim: 11776   bits: 15/14
c ---[2324]---> Adder-cost: 168   maxlim: 10624   bits: 15/14
c ---[2322]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[2320]---> Adder-cost: 272   maxlim: 18304   bits: 16/15
c ---[2318]---> Adder-cost: 234   maxlim: 15104   bits: 15/14
c ---[2316]---> Sorter-cost:  992     Base: 2 2 2 2 2 2 2 7
c ---[2314]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[2312]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[2310]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[2308]---> Adder-cost: 188   maxlim: 12672   bits: 15/14
c ---[2306]---> Adder-cost: 72   maxlim: 12672   bits: 15/14
c ---[2304]---> Adder-cost: 190   maxlim: 12544   bits: 15/14
c ---[2302]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[2300]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[2298]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[2296]---> Adder-cost: 136   maxlim: 9344   bits: 15/14
c ---[2294]---> Adder-cost: 172   maxlim: 10752   bits: 15/14
c ---[2292]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[2290]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[2288]---> Adder-cost: 154   maxlim: 10880   bits: 15/14
c ---[2286]---> Adder-cost: 160   maxlim: 9984   bits: 15/14
c ---[2284]---> Adder-cost: 62   maxlim: 9984   bits: 15/14
c ---[2282]---> Adder-cost: 62   maxlim: 9984   bits: 15/14
c ---[2280]---> Adder-cost: 110   maxlim: 9600   bits: 15/14
c ---[2278]---> Adder-cost: 62   maxlim: 9600   bits: 15/14
c ---[2276]---> Adder-cost: 60   maxlim: 9344   bits: 15/14
c ---[2274]---> Adder-cost: 62   maxlim: 9984   bits: 15/14
c ---[2272]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[2270]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[2268]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[2266]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[2264]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 7
c ---[2262]---> Adder-cost: 140   maxlim: 8576   bits: 15/14
c ---[2260]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[2258]---> Adder-cost: 140   maxlim: 9088   bits: 15/14
c ---[2256]---> Sorter-cost:  905     Base: 2 2 2 2 2 2 2 7
c ---[2254]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[2252]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[2250]---> Adder-cost: 160   maxlim: 9728   bits: 15/14
c ---[2248]---> Adder-cost: 92   maxlim: 6656   bits: 14/13
c ---[2246]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 7
c ---[2244]---> Adder-cost: 334   maxlim: 21120   bits: 16/15
c ---[2242]---> Adder-cost: 56   maxlim: 9088   bits: 15/14
c ---[2240]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[2238]---> Sorter-cost:  463     Base: 2 2 2 2 2 2 2 7
c ---[2236]---> Adder-cost: 168   maxlim: 10752   bits: 15/14
c ---[2234]---> Adder-cost: 108   maxlim: 6912   bits: 14/13
c ---[2232]---> Adder-cost: 72   maxlim: 6016   bits: 14/13
c ---[2230]---> Sorter-cost:  722     Base: 2 2 2 2 2 2 2 7
c ---[2228]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2226]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 7
c ---[2224]---> Sorter-cost:  549     Base: 2 2 2 2 2 2 2 7
c ---[2222]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 7
c ---[2220]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[2218]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 7
c ---[2216]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 7
c ---[2214]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[2212]---> Sorter-cost:  272     Base: 2 2 2 2 2 2 2 2
c ---[2210]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[2208]---> Sorter-cost:  504     Base: 2 2 2 2 2 2 2 7
c ---[2206]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[2204]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 7
c ---[2202]---> Sorter-cost:  356     Base: 2 2 2 2 2 2 2 7
c ---[2200]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[2198]---> Sorter-cost:  322     Base: 2 2 2 2 2 2 2 7
c ---[2196]---> Adder-cost: 244   maxlim: 15872   bits: 15/14
c ---[2194]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[2192]---> Adder-cost: 154   maxlim: 9216   bits: 15/14
c ---[2190]---> Adder-cost: 62   maxlim: 9216   bits: 15/14
c ---[2188]---> Adder-cost: 94   maxlim: 6272   bits: 14/13
c ---[2186]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[2184]---> Adder-cost: 182   maxlim: 11264   bits: 15/14
c ---[2182]---> Adder-cost: 108   maxlim: 8320   bits: 15/14
c ---[2180]---> Adder-cost: 166   maxlim: 14336   bits: 15/14
c ---[2178]---> Adder-cost: 122   maxlim: 7808   bits: 14/13
c ---[2176]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[2174]---> Adder-cost: 148   maxlim: 9088   bits: 15/14
c ---[2172]---> Adder-cost: 56   maxlim: 9088   bits: 15/14
c ---[2170]---> Adder-cost: 112   maxlim: 6912   bits: 14/13
c ---[2168]---> Adder-cost: 108   maxlim: 7168   bits: 14/13
c ---[2166]---> Adder-cost: 218   maxlim: 14464   bits: 15/14
c ---[2164]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[2162]---> Adder-cost: 162   maxlim: 10112   bits: 15/14
c ---[2160]---> Adder-cost: 154   maxlim: 9856   bits: 15/14
c ---[2158]---> Adder-cost: 60   maxlim: 9856   bits: 15/14
c ---[2156]---> Adder-cost: 190   maxlim: 14336   bits: 15/14
c ---[2154]---> Adder-cost: 76   maxlim: 14336   bits: 15/14
c ---[2152]---> Adder-cost: 176   maxlim: 14080   bits: 15/14
c ---[2150]---> Adder-cost: 74   maxlim: 14080   bits: 15/14
c ---[2148]---> Adder-cost: 76   maxlim: 14464   bits: 15/14
c ---[2146]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[2144]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[2142]---> Adder-cost: 168   maxlim: 10368   bits: 15/14
c ---[2140]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[2138]---> Adder-cost: 138   maxlim: 9472   bits: 15/14
c ---[2136]---> Adder-cost: 122   maxlim: 9216   bits: 15/14
c ---[2134]---> Adder-cost: 76   maxlim: 14464   bits: 15/14
c ---[2132]---> Adder-cost: 62   maxlim: 9216   bits: 15/14
c ---[2130]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[2128]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[2126]---> Adder-cost: 196   maxlim: 12672   bits: 15/14
c ---[2124]---> Adder-cost: 164   maxlim: 11008   bits: 15/14
c ---[2122]---> Adder-cost: 112   maxlim: 13568   bits: 15/14
c ---[2120]---> Adder-cost: 224   maxlim: 15104   bits: 15/14
c ---[2118]---> Adder-cost: 80   maxlim: 15104   bits: 15/14
c ---[2116]---> Adder-cost: 194   maxlim: 14336   bits: 15/14
c ---[2114]---> Adder-cost: 76   maxlim: 14336   bits: 15/14
c ---[2112]---> Adder-cost: 164   maxlim: 11392   bits: 15/14
c ---[2110]---> Adder-cost: 152   maxlim: 11904   bits: 15/14
c ---[2108]---> Adder-cost: 70   maxlim: 11904   bits: 15/14
c ---[2106]---> Adder-cost: 126   maxlim: 8192   bits: 15/14
c ---[2104]---> Adder-cost: 62   maxlim: 8192   bits: 15/14
c ---[2102]---> Adder-cost: 170   maxlim: 10752   bits: 15/14
c ---[2100]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[2098]---> Adder-cost: 138   maxlim: 10368   bits: 15/14
c ---[2096]---> Adder-cost: 68   maxlim: 10368   bits: 15/14
c ---[2094]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[2092]---> Adder-cost: 304   maxlim: 20096   bits: 16/15
c ---[2090]---> Adder-cost: 94   maxlim: 6016   bits: 14/13
c ---[2088]---> Adder-cost: 86   maxlim: 6528   bits: 14/13
c ---[2086]---> Adder-cost: 88   maxlim: 6016   bits: 14/13
c ---[2084]---> Sorter-cost:  612     Base: 2 2 2 2 2 2 2 7
c ---[2082]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[2080]---> Sorter-cost:  549     Base: 2 2 2 2 2 2 2 7
c ---[2078]---> Adder-cost: 80   maxlim: 4864   bits: 14/13
c ---[2076]---> Sorter-cost:  608     Base: 2 2 2 2 2 2 2 7
c ---[2074]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[2072]---> Adder-cost: 66   maxlim: 6528   bits: 14/13
c ---[2070]---> Adder-cost: 156   maxlim: 9984   bits: 15/14
c ---[2068]---> Adder-cost: 62   maxlim: 9984   bits: 15/14
c ---[2066]---> Adder-cost: 112   maxlim: 8704   bits: 15/14
c ---[2064]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[2062]---> Adder-cost: 110   maxlim: 8704   bits: 15/14
c ---[2060]---> Sorter-cost:  461     Base: 2 2 2 2 2 2 2 7
c ---[2058]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[2056]---> Sorter-cost:  559     Base: 2 2 2 2 2 2 2 7
c ---[2054]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[2052]---> Sorter-cost:  641     Base: 2 2 2 2 2 2 2 7
c ---[2050]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[2048]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[2046]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[2044]---> Adder-cost: 100   maxlim: 7040   bits: 14/13
c ---[2042]---> Adder-cost: 86   maxlim: 5248   bits: 14/13
c ---[2040]---> Adder-cost: 56   maxlim: 5120   bits: 14/13
c ---[2038]---> Adder-cost: 306   maxlim: 23808   bits: 16/15
c ---[2036]---> Adder-cost: 98   maxlim: 6656   bits: 14/13
c ---[2034]---> Adder-cost: 92   maxlim: 6656   bits: 14/13
c ---[2032]---> Adder-cost: 90   maxlim: 6016   bits: 14/13
c ---[2030]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[2028]---> Adder-cost: 176   maxlim: 11264   bits: 15/14
c ---[2026]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[2024]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[2022]---> Adder-cost: 102   maxlim: 6272   bits: 14/13
c ---[2020]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[2018]---> Sorter-cost:  571     Base: 2 2 2 2 2 2 2 7
c ---[2016]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[2014]---> Sorter-cost:  434     Base: 2 2 2 2 2 2 2 7
c ---[2012]---> Sorter-cost:  308     Base: 2 2 2 2 2 2 2 2
c ---[2010]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[2008]---> Sorter-cost:  264     Base: 2 2 2 2 2 2 2 2
c ---[2006]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2 7
c ---[2004]---> Adder-cost: 122   maxlim: 7808   bits: 14/13
c ---[2002]---> Sorter-cost:  392     Base: 2 2 2 2 2 2 2 7
c ---[2000]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[1998]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 7
c ---[1996]---> Sorter-cost:  728     Base: 2 2 2 2 2 2 2 7
c ---[1994]---> Sorter-cost:  950     Base: 2 2 2 2 2 2 2 7
c ---[1992]---> Adder-cost: 214   maxlim: 13568   bits: 15/14
c ---[1990]---> Adder-cost: 158   maxlim: 11392   bits: 15/14
c ---[1988]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 7
c ---[1986]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 7
c ---[1984]---> Adder-cost: 166   maxlim: 10624   bits: 15/14
c ---[1982]---> Adder-cost: 80   maxlim: 4864   bits: 14/13
c ---[1980]---> Adder-cost: 102   maxlim: 6400   bits: 14/13
c ---[1978]---> Adder-cost: 308   maxlim: 19968   bits: 16/15
c ---[1976]---> Adder-cost: 272   maxlim: 17536   bits: 16/15
c ---[1974]---> Adder-cost: 200   maxlim: 12672   bits: 15/14
c ---[1972]---> Adder-cost: 208   maxlim: 13440   bits: 15/14
c ---[1970]---> Adder-cost: 168   maxlim: 13312   bits: 15/14
c ---[1968]---> Adder-cost: 142   maxlim: 14080   bits: 15/14
c ---[1966]---> Sorter-cost:  641     Base: 2 2 2 2 2 2 2 7
c ---[1964]---> Adder-cost: 134   maxlim: 9600   bits: 15/14
c ---[1962]---> Adder-cost: 120   maxlim: 8448   bits: 15/14
c ---[1960]---> Adder-cost: 90   maxlim: 5888   bits: 14/13
c ---[1958]---> Adder-cost: 106   maxlim: 6912   bits: 14/13
c ---[1956]---> Adder-cost: 218   maxlim: 14720   bits: 15/14
c ---[1954]---> Adder-cost: 162   maxlim: 12160   bits: 15/14
c ---[1952]---> Adder-cost: 168   maxlim: 10624   bits: 15/14
c ---[1950]---> Adder-cost: 174   maxlim: 11264   bits: 15/14
c ---[1948]---> Adder-cost: 112   maxlim: 7552   bits: 14/13
c ---[1946]---> Adder-cost: 220   maxlim: 17408   bits: 16/15
c ---[1944]---> Adder-cost: 94   maxlim: 17408   bits: 16/15
c ---[1942]---> Adder-cost: 94   maxlim: 17408   bits: 16/15
c ---[1940]---> Adder-cost: 90   maxlim: 7552   bits: 14/13
c ---[1938]---> Adder-cost: 216   maxlim: 14464   bits: 15/14
c ---[1936]---> Adder-cost: 76   maxlim: 14464   bits: 15/14
c ---[1934]---> Adder-cost: 148   maxlim: 10624   bits: 15/14
c ---[1932]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[1930]---> Adder-cost: 120   maxlim: 7680   bits: 14/13
c ---[1928]---> Adder-cost: 84   maxlim: 5760   bits: 14/13
c ---[1926]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[1924]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[1922]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 7
c ---[1920]---> Adder-cost: 176   maxlim: 11648   bits: 15/14
c ---[1918]---> Adder-cost: 88   maxlim: 5760   bits: 14/13
c ---[1916]---> Adder-cost: 74   maxlim: 5504   bits: 14/13
c ---[1914]---> Adder-cost: 122   maxlim: 10752   bits: 15/14
c ---[1912]---> Adder-cost: 208   maxlim: 14336   bits: 15/14
c ---[1910]---> Adder-cost: 76   maxlim: 14336   bits: 15/14
c ---[1908]---> Adder-cost: 76   maxlim: 4736   bits: 14/13
c ---[1906]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[1904]---> Adder-cost: 186   maxlim: 12288   bits: 15/14
c ---[1902]---> Sorter-cost:  646     Base: 2 2 2 2 2 2 2 7
c ---[1900]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1898]---> Sorter-cost: 1038     Base: 2 2 2 2 2 2 2 7
c ---[1896]---> Adder-cost: 236   maxlim: 15616   bits: 15/14
c ---[1894]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 7
c ---[1892]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 7
c ---[1890]---> Sorter-cost:  759     Base: 2 2 2 2 2 2 2 7
c ---[1888]---> Sorter-cost:  936     Base: 2 2 2 2 2 2 2 7
c ---[1886]---> Adder-cost: 140   maxlim: 9088   bits: 15/14
c ---[1884]---> Adder-cost: 56   maxlim: 9088   bits: 15/14
c ---[1882]---> Adder-cost: 102   maxlim: 6400   bits: 14/13
c ---[1880]---> Adder-cost: 154   maxlim: 15488   bits: 15/14
c ---[1878]---> Adder-cost: 96   maxlim: 6272   bits: 14/13
c ---[1876]---> Adder-cost: 270   maxlim: 18944   bits: 16/15
c ---[1874]---> Adder-cost: 160   maxlim: 11904   bits: 15/14
c ---[1872]---> Adder-cost: 312   maxlim: 22912   bits: 16/15
c ---[1870]---> Adder-cost: 168   maxlim: 12544   bits: 15/14
c ---[1868]---> Adder-cost: 96   maxlim: 6144   bits: 14/13
c ---[1866]---> Adder-cost: 172   maxlim: 14720   bits: 15/14
c ---[1864]---> Sorter-cost:  954     Base: 2 2 2 2 2 2 2 7
c ---[1862]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[1860]---> Sorter-cost:  730     Base: 2 2 2 2 2 2 2 7
c ---[1858]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[1856]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[1854]---> Sorter-cost:  710     Base: 2 2 2 2 2 2 2 7
c ---[1852]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[1850]---> Adder-cost: 124   maxlim: 8320   bits: 15/14
c ---[1848]---> Adder-cost: 138   maxlim: 14848   bits: 15/14
c ---[1846]---> Adder-cost: 136   maxlim: 8576   bits: 15/14
c ---[1844]---> Adder-cost: 138   maxlim: 8832   bits: 15/14
c ---[1842]---> Sorter-cost:  685     Base: 2 2 2 2 2 2 2 7
c ---[1840]---> Adder-cost: 108   maxlim: 7296   bits: 14/13
c ---[1838]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 7
c ---[1836]---> Adder-cost: 186   maxlim: 13056   bits: 15/14
c ---[1834]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[1832]---> Adder-cost: 122   maxlim: 7808   bits: 14/13
c ---[1830]---> Adder-cost: 100   maxlim: 6272   bits: 14/13
c ---[1828]---> Adder-cost: 104   maxlim: 6656   bits: 14/13
c ---[1826]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1825]---> Adder-cost: 2746   maxlim: 175871   bits: 19/18
c ---[1823]---> Adder-cost: 277   maxlim: 19839   bits: 16/15
c ---[1821]---> Adder-cost: 486   maxlim: 31487   bits: 16/15
c ---[1819]---> Adder-cost: 589   maxlim: 43135   bits: 17/16
c ---[1818]---> Adder-cost: 587   maxlim: 42367   bits: 17/16
c ---[1816]---> Adder-cost: 727   maxlim: 45311   bits: 17/16
c ---[1814]---> Adder-cost: 241   maxlim: 17023   bits: 16/15
c ---[1809]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 7
c ---[1806]---> Adder-cost: 1742   maxlim: 116479   bits: 18/17
c ---[1804]---> Adder-cost: 755   maxlim: 59647   bits: 17/16
c ---[1803]---> Adder-cost: 3252   maxlim: 215551   bits: 19/18
c ---[1802]---> Adder-cost: 911   maxlim: 62207   bits: 17/16
c ---[1801]---> Adder-cost: 374   maxlim: 23679   bits: 16/15
c ---[1799]---> Adder-cost: 2092   maxlim: 144255   bits: 19/18
c ---[1797]---> Sorter-cost:  612     Base: 2 2 2 2 2 2 2 7
c ---[1796]---> Adder-cost: 410   maxlim: 25727   bits: 16/15
c ---[1794]---> Adder-cost: 398   maxlim: 29951   bits: 16/15
c ---[1789]---> Adder-cost: 829   maxlim: 51711   bits: 17/16
c ---[1788]---> Adder-cost: 5332   maxlim: 182783   bits: 19/18
c ---[1786]---> Sorter-cost:  256     Base: 2 2 2 2 2 2 2 2
c ---[1785]---> Adder-cost: 13948   maxlim: 822783   bits: 21/20
c ---[1784]---> Adder-cost: 750   maxlim: 50559   bits: 17/16
c ---[1782]---> Adder-cost: 75   maxlim: 4735   bits: 14/13
c ---[1780]---> Adder-cost: 180   maxlim: 3455   bits: 13/12
c ---[1778]---> Adder-cost: 148   maxlim: 4735   bits: 14/13
c ---[1777]---> Adder-cost: 245   maxlim: 15231   bits: 15/14
c ---[1775]---> Adder-cost: 141   maxlim: 3711   bits: 13/12
c ---[1774]---> Adder-cost: 126   maxlim: 6399   bits: 14/13
c ---[1773]---> Adder-cost: 107   maxlim: 4863   bits: 14/13
c ---[1770]---> Adder-cost: 341   maxlim: 9727   bits: 15/14
c ---[1768]---> Adder-cost: 1024   maxlim: 36607   bits: 17/16
c ---[1767]---> Adder-cost: 203   maxlim: 3839   bits: 13/12
c ---[1765]---> Adder-cost: 122   maxlim: 9344   bits: 15/14
c ---[1764]---> Adder-cost: 359   maxlim: 2815   bits: 13/12
c ---[1763]---> Adder-cost: 235   maxlim: 13823   bits: 15/14
c ---[1762]---> Adder-cost: 188   maxlim: 11135   bits: 15/14
c ---[1760]---> Adder-cost: 302   maxlim: 18815   bits: 16/15
c ---[1759]---> Adder-cost: 9086   maxlim: 459263   bits: 20/19
c ---[1758]---> Adder-cost: 2762   maxlim: 206335   bits: 19/18
c ---[1757]---> Adder-cost: 15274   maxlim: 1224063   bits: 21/21
c ---[1756]---> Adder-cost: 1631   maxlim: 161023   bits: 19/18
c ---[1743]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 7
c ---[1735]---> Adder-cost: 2225   maxlim: 149119   bits: 19/18
c ---[1718]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 7
c ---[1712]---> Adder-cost: 482   maxlim: 37888   bits: 17/16
c ---[1707]---> Adder-cost: 378   maxlim: 34432   bits: 17/16
c ---[1702]---> Adder-cost: 434   maxlim: 38016   bits: 17/16
c ---[1700]---> Adder-cost: 82   maxlim: 5120   bits: 14/13
c ---[1698]---> Adder-cost: 86   maxlim: 6016   bits: 14/13
c ---[1697]---> Adder-cost: 53810   maxlim: 40062207   bits: 27/26
c ---[1695]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[1693]---> Adder-cost: 76   maxlim: 5376   bits: 14/13
c ---[1692]---> Adder-cost: 8142   maxlim: 441599   bits: 20/19
c ---[1690]---> Adder-cost: 56   maxlim: 4352   bits: 14/13
c ---[1688]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[1686]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[1684]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1682]---> Adder-cost: 466   maxlim: 31232   bits: 16/15
c ---[1680]---> Adder-cost: 286   maxlim: 31488   bits: 16/15
c ---[1678]---> Adder-cost: 74   maxlim: 4736   bits: 14/13
c ---[1676]---> Adder-cost: 76   maxlim: 4736   bits: 14/13
c ---[1674]---> Adder-cost: 46   maxlim: 4736   bits: 14/13
c ---[1672]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[1670]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[1668]---> Adder-cost: 174   maxlim: 11008   bits: 15/14
c ---[1666]---> Adder-cost: 202   maxlim: 12800   bits: 15/14
c ---[1664]---> Adder-cost: 212   maxlim: 13696   bits: 15/14
c ---[1662]---> Adder-cost: 212   maxlim: 16640   bits: 16/15
c ---[1660]---> Adder-cost: 88   maxlim: 16640   bits: 16/15
c ---[1658]---> Adder-cost: 450   maxlim: 32384   bits: 16/15
c ---[1656]---> Adder-cost: 124   maxlim: 32384   bits: 16/15
c ---[1654]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1652]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[1650]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1648]---> Adder-cost: 104   maxlim: 6912   bits: 14/13
c ---[1646]---> Adder-cost: 132   maxlim: 11136   bits: 15/14
c ---[1644]---> Adder-cost: 256   maxlim: 19072   bits: 16/15
c ---[1642]---> Adder-cost: 134   maxlim: 8960   bits: 15/14
c ---[1640]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1638]---> Adder-cost: 290   maxlim: 24576   bits: 16/15
c ---[1636]---> Adder-cost: 532   maxlim: 40192   bits: 17/16
c ---[1634]---> Adder-cost: 560   maxlim: 40320   bits: 17/16
c ---[1632]---> Adder-cost: 566   maxlim: 40448   bits: 17/16
c ---[1630]---> Adder-cost: 434   maxlim: 29824   bits: 16/15
c ---[1628]---> Adder-cost: 362   maxlim: 30592   bits: 16/15
c ---[1626]---> Adder-cost: 142   maxlim: 8960   bits: 15/14
c ---[1624]---> Adder-cost: 60   maxlim: 8960   bits: 15/14
c ---[1622]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 7
c ---[1620]---> Adder-cost: 718   maxlim: 52352   bits: 17/16
c ---[1618]---> Adder-cost: 174   maxlim: 52352   bits: 17/16
c ---[1616]---> Adder-cost: 554   maxlim: 39936   bits: 17/16
c ---[1614]---> Adder-cost: 148   maxlim: 39936   bits: 17/16
c ---[1612]---> Adder-cost: 216   maxlim: 14336   bits: 15/14
c ---[1610]---> Adder-cost: 76   maxlim: 14336   bits: 15/14
c ---[1608]---> Adder-cost: 334   maxlim: 22528   bits: 16/15
c ---[1606]---> Adder-cost: 244   maxlim: 20480   bits: 16/15
c ---[1604]---> Adder-cost: 530   maxlim: 39040   bits: 17/16
c ---[1602]---> Sorter-cost:  759     Base: 2 2 2 2 2 2 2 7
c ---[1600]---> Adder-cost: 154   maxlim: 39040   bits: 17/16
c ---[1598]---> Adder-cost: 158   maxlim: 10752   bits: 15/14
c ---[1596]---> Adder-cost: 110   maxlim: 7424   bits: 14/13
c ---[1594]---> Adder-cost: 528   maxlim: 48128   bits: 17/16
c ---[1592]---> Adder-cost: 164   maxlim: 48128   bits: 17/16
c ---[1590]---> Adder-cost: 234   maxlim: 16512   bits: 16/15
c ---[1588]---> Adder-cost: 90   maxlim: 16512   bits: 16/15
c ---[1586]---> Adder-cost: 226   maxlim: 19072   bits: 16/15
c ---[1584]---> Adder-cost: 94   maxlim: 19072   bits: 16/15
c ---[1582]---> Sorter-cost:  759     Base: 2 2 2 2 2 2 2 7
c ---[1580]---> Adder-cost: 168   maxlim: 15488   bits: 15/14
c ---[1578]---> Adder-cost: 78   maxlim: 15488   bits: 15/14
c ---[1576]---> Adder-cost: 164   maxlim: 14208   bits: 15/14
c ---[1574]---> Adder-cost: 216   maxlim: 17792   bits: 16/15
c ---[1572]---> Adder-cost: 172   maxlim: 16256   bits: 15/14
c ---[1570]---> Adder-cost: 74   maxlim: 16256   bits: 15/14
c ---[1568]---> Adder-cost: 100   maxlim: 7424   bits: 14/13
c ---[1566]---> Adder-cost: 68   maxlim: 6656   bits: 14/13
c ---[1564]---> Adder-cost: 234   maxlim: 16256   bits: 15/14
c ---[1562]---> Adder-cost: 172   maxlim: 14720   bits: 15/14
c ---[1560]---> Adder-cost: 96   maxlim: 6656   bits: 14/13
c ---[1558]---> Adder-cost: 226   maxlim: 14848   bits: 15/14
c ---[1556]---> Adder-cost: 172   maxlim: 12800   bits: 15/14
c ---[1554]---> Adder-cost: 214   maxlim: 14976   bits: 15/14
c ---[1552]---> Adder-cost: 376   maxlim: 27392   bits: 16/15
c ---[1550]---> Adder-cost: 94   maxlim: 5888   bits: 14/13
c ---[1548]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[1546]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[1544]---> Adder-cost: 74   maxlim: 16256   bits: 15/14
c ---[1542]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[1540]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[1538]---> Adder-cost: 234   maxlim: 16768   bits: 16/15
c ---[1536]---> Adder-cost: 230   maxlim: 16000   bits: 15/14
c ---[1534]---> Adder-cost: 96   maxlim: 7936   bits: 14/13
c ---[1532]---> Adder-cost: 108   maxlim: 9856   bits: 15/14
c ---[1530]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 7
c ---[1528]---> Sorter-cost:  300     Base: 2 2 2 2 2 2 2 2
c ---[1526]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1524]---> Adder-cost: 464   maxlim: 33024   bits: 17/16
c ---[1522]---> Adder-cost: 138   maxlim: 33024   bits: 17/16
c ---[1520]---> Adder-cost: 338   maxlim: 26624   bits: 16/15
c ---[1518]---> Adder-cost: 270   maxlim: 21504   bits: 16/15
c ---[1516]---> Adder-cost: 248   maxlim: 22400   bits: 16/15
c ---[1514]---> Adder-cost: 288   maxlim: 27392   bits: 16/15
c ---[1512]---> Adder-cost: 94   maxlim: 7296   bits: 14/13
c ---[1510]---> Adder-cost: 146   maxlim: 12288   bits: 15/14
c ---[1508]---> Adder-cost: 130   maxlim: 9216   bits: 15/14
c ---[1506]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1504]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 7
c ---[1502]---> Sorter-cost:  451     Base: 2 2 2 2 2 2 2 7
c ---[1500]---> Sorter-cost:  274     Base: 2 2 2 2 2 2 2 2
c ---[1498]---> Sorter-cost:  576     Base: 2 2 2 2 2 2 2 7
c ---[1496]---> Adder-cost: 358   maxlim: 25472   bits: 16/15
c ---[1494]---> Adder-cost: 110   maxlim: 25472   bits: 16/15
c ---[1492]---> Adder-cost: 220   maxlim: 14336   bits: 15/14
c ---[1490]---> Adder-cost: 344   maxlim: 22784   bits: 16/15
c ---[1488]---> Adder-cost: 76   maxlim: 14336   bits: 15/14
c ---[1486]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[1484]---> Sorter-cost:  904     Base: 2 2 2 2 2 2 2 7
c ---[1482]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1480]---> Sorter-cost:  300     Base: 2 2 2 2 2 2 2 2
c ---[1478]---> Adder-cost: 326   maxlim: 22528   bits: 16/15
c ---[1476]---> Adder-cost: 378   maxlim: 28672   bits: 16/15
c ---[1474]---> Adder-cost: 492   maxlim: 34432   bits: 17/16
c ---[1472]---> Adder-cost: 148   maxlim: 34432   bits: 17/16
c ---[1470]---> Adder-cost: 602   maxlim: 40192   bits: 17/16
c ---[1468]---> Adder-cost: 148   maxlim: 40192   bits: 17/16
c ---[1466]---> Adder-cost: 190   maxlim: 15104   bits: 15/14
c ---[1464]---> Adder-cost: 188   maxlim: 15744   bits: 15/14
c ---[1462]---> Sorter-cost:  230     Base: 2 2 2 2 2 2 2 2
c ---[1460]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[1458]---> Adder-cost: 90   maxlim: 5632   bits: 14/13
c ---[1456]---> Adder-cost: 166   maxlim: 13824   bits: 15/14
c ---[1454]---> Adder-cost: 74   maxlim: 13824   bits: 15/14
c ---[1452]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 7
c ---[1450]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1448]---> Sorter-cost:  402     Base: 2 2 2 2 2 2 2 7
c ---[1446]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[1444]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[1442]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[1440]---> Sorter-cost:  250     Base: 2 2 2 2 2 2 2 2
c ---[1438]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 7
c ---[1436]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1434]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 7
c ---[1432]---> Sorter-cost:  580     Base: 2 2 2 2 2 2 2 7
c ---[1430]---> Adder-cost: 136   maxlim: 8832   bits: 15/14
c ---[1428]---> Sorter-cost:  368     Base: 2 2 2 2 2 2 2 7
c ---[1426]---> Sorter-cost:  572     Base: 2 2 2 2 2 2 2 7
c ---[1424]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2 7
c ---[1422]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 7
c ---[1420]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 7
c ---[1418]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[1416]---> Adder-cost: 202   maxlim: 16256   bits: 15/14
c ---[1414]---> Adder-cost: 82   maxlim: 7936   bits: 14/13
c ---[1412]---> Sorter-cost:  732     Base: 2 2 2 2 2 2 2 7
c ---[1410]---> Sorter-cost:  393     Base: 2 2 2 2 2 2 2 7
c ---[1408]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[1406]---> Adder-cost: 102   maxlim: 7296   bits: 14/13
c ---[1404]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 7
c ---[1402]---> Sorter-cost:  558     Base: 2 2 2 2 2 2 2 7
c ---[1400]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[1398]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 7
c ---[1396]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[1394]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[1392]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[1390]---> Adder-cost: 82   maxlim: 7040   bits: 14/13
c ---[1388]---> Sorter-cost:  569     Base: 2 2 2 2 2 2 2 7
c ---[1386]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[1384]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 7
c ---[1382]---> Sorter-cost:  687     Base: 2 2 2 2 2 2 2 7
c ---[1380]---> Adder-cost: 98   maxlim: 6784   bits: 14/13
c ---[1378]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 7
c ---[1376]---> Sorter-cost:  368     Base: 2 2 2 2 2 2 2 7
c ---[1374]---> Sorter-cost:  606     Base: 2 2 2 2 2 2 2 7
c ---[1372]---> Adder-cost: 220   maxlim: 16640   bits: 16/15
c ---[1370]---> Adder-cost: 116   maxlim: 9984   bits: 15/14
c ---[1368]---> Sorter-cost:  388     Base: 2 2 2 2 2 2 2 7
c ---[1366]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[1364]---> Adder-cost: 110   maxlim: 8064   bits: 14/13
c ---[1362]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 7
c ---[1360]---> Adder-cost: 184   maxlim: 12544   bits: 15/14
c ---[1358]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 7
c ---[1356]---> Sorter-cost: 1036     Base: 2 2 2 2 2 2 2 7
c ---[1354]---> Adder-cost: 92   maxlim: 5760   bits: 14/13
c ---[1352]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1350]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1348]---> Adder-cost: 102   maxlim: 6400   bits: 14/13
c ---[1346]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[1344]---> Adder-cost: 104   maxlim: 6912   bits: 14/13
c ---[1342]---> Adder-cost: 350   maxlim: 24320   bits: 16/15
c ---[1340]---> Adder-cost: 110   maxlim: 24320   bits: 16/15
c ---[1338]---> Adder-cost: 132   maxlim: 9472   bits: 15/14
c ---[1336]---> Adder-cost: 64   maxlim: 9472   bits: 15/14
c ---[1334]---> Adder-cost: 254   maxlim: 20864   bits: 16/15
c ---[1332]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[1330]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 7
c ---[1328]---> Adder-cost: 70   maxlim: 4992   bits: 14/13
c ---[1326]---> Sorter-cost:  654     Base: 2 2 2 2 2 2 2 7
c ---[1324]---> Adder-cost: 54   maxlim: 4352   bits: 14/13
c ---[1322]---> Adder-cost: 92   maxlim: 7296   bits: 14/13
c ---[1320]---> Adder-cost: 66   maxlim: 4864   bits: 14/13
c ---[1318]---> Adder-cost: 112   maxlim: 7552   bits: 14/13
c ---[1316]---> Adder-cost: 108   maxlim: 7552   bits: 14/13
c ---[1314]---> Adder-cost: 150   maxlim: 9216   bits: 15/14
c ---[1312]---> Adder-cost: 100   maxlim: 8064   bits: 14/13
c ---[1310]---> Adder-cost: 94   maxlim: 6272   bits: 14/13
c ---[1308]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1306]---> Adder-cost: 286   maxlim: 18944   bits: 16/15
c ---[1304]---> Adder-cost: 250   maxlim: 17920   bits: 16/15
c ---[1302]---> Adder-cost: 250   maxlim: 17152   bits: 16/15
c ---[1300]---> Adder-cost: 192   maxlim: 17152   bits: 16/15
c ---[1298]---> Adder-cost: 176   maxlim: 12160   bits: 15/14
c ---[1296]---> Adder-cost: 114   maxlim: 8576   bits: 15/14
c ---[1294]---> Adder-cost: 140   maxlim: 11008   bits: 15/14
c ---[1292]---> Adder-cost: 152   maxlim: 12800   bits: 15/14
c ---[1290]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1288]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1286]---> Sorter-cost:  650     Base: 2 2 2 2 2 2 2 7
c ---[1284]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1282]---> Sorter-cost:  264     Base: 2 2 2 2 2 2 2 2
c ---[1280]---> Adder-cost: 564   maxlim: 38784   bits: 17/16
c ---[1278]---> Adder-cost: 424   maxlim: 39296   bits: 17/16
c ---[1276]---> Sorter-cost:  860     Base: 2 2 2 2 2 2 2 7
c ---[1274]---> Adder-cost: 250   maxlim: 21376   bits: 16/15
c ---[1272]---> Adder-cost: 230   maxlim: 18688   bits: 16/15
c ---[1270]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1268]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[1266]---> Adder-cost: 172   maxlim: 12288   bits: 15/14
c ---[1264]---> Adder-cost: 100   maxlim: 6656   bits: 14/13
c ---[1262]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 7
c ---[1260]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[1258]---> Adder-cost: 90   maxlim: 7424   bits: 14/13
c ---[1256]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[1254]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[1252]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[1250]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1248]---> Adder-cost: 174   maxlim: 12032   bits: 15/14
c ---[1246]---> Adder-cost: 68   maxlim: 12032   bits: 15/14
c ---[1244]---> Adder-cost: 190   maxlim: 12800   bits: 15/14
c ---[1242]---> Adder-cost: 76   maxlim: 12800   bits: 15/14
c ---[1240]---> Adder-cost: 246   maxlim: 17024   bits: 16/15
c ---[1238]---> Adder-cost: 88   maxlim: 17024   bits: 16/15
c ---[1236]---> Adder-cost: 186   maxlim: 14208   bits: 15/14
c ---[1234]---> Adder-cost: 72   maxlim: 14208   bits: 15/14
c ---[1232]---> Adder-cost: 72   maxlim: 14208   bits: 15/14
c ---[1230]---> Adder-cost: 72   maxlim: 14208   bits: 15/14
c ---[1228]---> Sorter-cost:  684     Base: 2 2 2 2 2 2 2 7
c ---[1226]---> Adder-cost: 188   maxlim: 15872   bits: 15/14
c ---[1224]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[1222]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[1220]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[1218]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[1216]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1214]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1212]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1210]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1208]---> Adder-cost: 116   maxlim: 7680   bits: 14/13
c ---[1206]---> Adder-cost: 68   maxlim: 4736   bits: 14/13
c ---[1204]---> Adder-cost: 102   maxlim: 7296   bits: 14/13
c ---[1202]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 7
c ---[1200]---> Sorter-cost:  956     Base: 2 2 2 2 2 2 2 7
c ---[1198]---> Adder-cost: 102   maxlim: 6528   bits: 14/13
c ---[1196]---> Adder-cost: 78   maxlim: 5120   bits: 14/13
c ---[1194]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[1192]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[1190]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[1188]---> Sorter-cost:  596     Base: 2 2 2 2 2 2 2 7
c ---[1186]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1184]---> Sorter-cost:  770     Base: 2 2 2 2 2 2 2 7
c ---[1182]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[1180]---> Sorter-cost:  950     Base: 2 2 2 2 2 2 2 7
c ---[1178]---> Sorter-cost:  596     Base: 2 2 2 2 2 2 2 7
c ---[1176]---> Sorter-cost:  596     Base: 2 2 2 2 2 2 2 7
c ---[1174]---> Adder-cost: 210   maxlim: 16640   bits: 16/15
c ---[1172]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[1170]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1168]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1166]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1164]---> Sorter-cost:  264     Base: 2 2 2 2 2 2 2 2
c ---[1162]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1160]---> Adder-cost: 84   maxlim: 5248   bits: 14/13
c ---[1158]---> Adder-cost: 72   maxlim: 4992   bits: 14/13
c ---[1156]---> Sorter-cost:  958     Base: 2 2 2 2 2 2 2 7
c ---[1154]---> Sorter-cost:  950     Base: 2 2 2 2 2 2 2 7
c ---[1152]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1150]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1148]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1146]---> Sorter-cost:  926     Base: 2 2 2 2 2 2 2 7
c ---[1144]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[1142]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[1140]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[1138]---> Sorter-cost:  300     Base: 2 2 2 2 2 2 2 2
c ---[1136]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1134]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1132]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1130]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[1128]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1126]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1124]---> Adder-cost: 82   maxlim: 5248   bits: 14/13
c ---[1122]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[1120]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[1118]---> Adder-cost: 84   maxlim: 5376   bits: 14/13
c ---[1116]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[1114]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[1112]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[1110]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[1108]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[1106]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[1104]---> Adder-cost: 214   maxlim: 14592   bits: 15/14
c ---[1102]---> Adder-cost: 170   maxlim: 13056   bits: 15/14
c ---[1100]---> Adder-cost: 292   maxlim: 19456   bits: 16/15
c ---[1098]---> Adder-cost: 82   maxlim: 5376   bits: 14/13
c ---[1096]---> Adder-cost: 166   maxlim: 10880   bits: 15/14
c ---[1094]---> Adder-cost: 66   maxlim: 10880   bits: 15/14
c ---[1092]---> Adder-cost: 186   maxlim: 11904   bits: 15/14
c ---[1090]---> Adder-cost: 70   maxlim: 11904   bits: 15/14
c ---[1088]---> Adder-cost: 70   maxlim: 11904   bits: 15/14
c ---[1086]---> Adder-cost: 128   maxlim: 8320   bits: 15/14
c ---[1084]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[1082]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[1080]---> Adder-cost: 130   maxlim: 9984   bits: 15/14
c ---[1078]---> Adder-cost: 132   maxlim: 9472   bits: 15/14
c ---[1076]---> Adder-cost: 64   maxlim: 9472   bits: 15/14
c ---[1074]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[1072]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[1070]---> Adder-cost: 60   maxlim: 4352   bits: 14/13
c ---[1068]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 7
c ---[1066]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[1064]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[1062]---> Sorter-cost:  330     Base: 2 2 2 2 2 2 2 7
c ---[1060]---> Sorter-cost:  392     Base: 2 2 2 2 2 2 2 7
c ---[1058]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[1056]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[1054]---> Sorter-cost:  568     Base: 2 2 2 2 2 2 2 7
c ---[1052]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[1050]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[1048]---> Sorter-cost:  536     Base: 2 2 2 2 2 2 2 7
c ---[1046]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1044]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 7
c ---[1042]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[1040]---> Adder-cost: 218   maxlim: 14336   bits: 15/14
c ---[1038]---> Adder-cost: 76   maxlim: 14336   bits: 15/14
c ---[1036]---> Adder-cost: 180   maxlim: 14080   bits: 15/14
c ---[1034]---> Adder-cost: 74   maxlim: 14080   bits: 15/14
c ---[1032]---> Adder-cost: 174   maxlim: 12032   bits: 15/14
c ---[1030]---> Adder-cost: 208   maxlim: 14592   bits: 15/14
c ---[1028]---> Adder-cost: 162   maxlim: 14464   bits: 15/14
c ---[1026]---> Adder-cost: 148   maxlim: 9856   bits: 15/14
c ---[1024]---> Adder-cost: 136   maxlim: 8960   bits: 15/14
c ---[1022]---> Adder-cost: 170   maxlim: 10496   bits: 15/14
c ---[1020]---> Adder-cost: 68   maxlim: 10496   bits: 15/14
c ---[1018]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 7
c ---[1016]---> Sorter-cost:  668     Base: 2 2 2 2 2 2 2 7
c ---[1014]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[1012]---> Sorter-cost:  383     Base: 2 2 2 2 2 2 2 7
c ---[1010]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[1008]---> Adder-cost: 138   maxlim: 9344   bits: 15/14
c ---[1006]---> Adder-cost: 60   maxlim: 9344   bits: 15/14
c ---[1004]---> Sorter-cost:  627     Base: 2 2 2 2 2 2 2 7
c ---[1002]---> Adder-cost: 68   maxlim: 4480   bits: 14/13
c ---[1000]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[ 998]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[ 996]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[ 994]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[ 992]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[ 990]---> Adder-cost: 76   maxlim: 5376   bits: 14/13
c ---[ 988]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[ 986]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 7
c ---[ 984]---> Adder-cost: 168   maxlim: 10752   bits: 15/14
c ---[ 982]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[ 980]---> Adder-cost: 76   maxlim: 4992   bits: 14/13
c ---[ 978]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[ 976]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[ 974]---> Adder-cost: 52   maxlim: 4480   bits: 14/13
c ---[ 972]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 7
c ---[ 970]---> Sorter-cost:  478     Base: 2 2 2 2 2 2 2 7
c ---[ 968]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[ 966]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[ 964]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[ 962]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[ 960]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[ 958]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 7
c ---[ 956]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 7
c ---[ 954]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[ 952]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[ 950]---> Adder-cost: 184   maxlim: 12032   bits: 15/14
c ---[ 948]---> Adder-cost: 68   maxlim: 12032   bits: 15/14
c ---[ 946]---> Adder-cost: 268   maxlim: 18176   bits: 16/15
c ---[ 944]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[ 942]---> Sorter-cost:  932     Base: 2 2 2 2 2 2 2 7
c ---[ 940]---> Sorter-cost:  946     Base: 2 2 2 2 2 2 2 7
c ---[ 938]---> Adder-cost: 116   maxlim: 7936   bits: 14/13
c ---[ 936]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[ 934]---> Adder-cost: 134   maxlim: 8320   bits: 15/14
c ---[ 932]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[ 930]---> Adder-cost: 124   maxlim: 8832   bits: 15/14
c ---[ 928]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[ 926]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[ 924]---> Adder-cost: 126   maxlim: 9472   bits: 15/14
c ---[ 922]---> Adder-cost: 64   maxlim: 9472   bits: 15/14
c ---[ 920]---> Sorter-cost:  687     Base: 2 2 2 2 2 2 2 7
c ---[ 918]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[ 916]---> Sorter-cost:  680     Base: 2 2 2 2 2 2 2 7
c ---[ 914]---> Adder-cost: 250   maxlim: 17536   bits: 16/15
c ---[ 912]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[ 910]---> Adder-cost: 106   maxlim: 6912   bits: 14/13
c ---[ 908]---> Adder-cost: 84   maxlim: 6528   bits: 14/13
c ---[ 906]---> Adder-cost: 342   maxlim: 22656   bits: 16/15
c ---[ 904]---> Adder-cost: 194   maxlim: 13440   bits: 15/14
c ---[ 902]---> Adder-cost: 78   maxlim: 13440   bits: 15/14
c ---[ 900]---> Adder-cost: 120   maxlim: 7936   bits: 14/13
c ---[ 898]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[ 896]---> Adder-cost: 120   maxlim: 7424   bits: 14/13
c ---[ 894]---> Adder-cost: 118   maxlim: 7680   bits: 14/13
c ---[ 892]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[ 890]---> Adder-cost: 166   maxlim: 12160   bits: 15/14
c ---[ 888]---> Adder-cost: 64   maxlim: 12160   bits: 15/14
c ---[ 886]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[ 884]---> Adder-cost: 310   maxlim: 21376   bits: 16/15
c ---[ 882]---> Adder-cost: 90   maxlim: 5632   bits: 14/13
c ---[ 880]---> Adder-cost: 114   maxlim: 7552   bits: 14/13
c ---[ 878]---> Adder-cost: 98   maxlim: 7552   bits: 14/13
c ---[ 876]---> Adder-cost: 206   maxlim: 14208   bits: 15/14
c ---[ 874]---> Adder-cost: 72   maxlim: 14208   bits: 15/14
c ---[ 872]---> Adder-cost: 138   maxlim: 8960   bits: 15/14
c ---[ 870]---> Adder-cost: 136   maxlim: 10752   bits: 15/14
c ---[ 868]---> Adder-cost: 178   maxlim: 12928   bits: 15/14
c ---[ 866]---> Adder-cost: 76   maxlim: 12928   bits: 15/14
c ---[ 864]---> Adder-cost: 76   maxlim: 12928   bits: 15/14
c ---[ 862]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[ 860]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[ 858]---> Adder-cost: 88   maxlim: 5632   bits: 14/13
c ---[ 856]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[ 854]---> Adder-cost: 80   maxlim: 5248   bits: 14/13
c ---[ 852]---> Sorter-cost:  988     Base: 2 2 2 2 2 2 2 7
c ---[ 850]---> Adder-cost: 268   maxlim: 17920   bits: 16/15
c ---[ 848]---> Adder-cost: 88   maxlim: 5632   bits: 14/13
c ---[ 846]---> Adder-cost: 72   maxlim: 5888   bits: 14/13
c ---[ 844]---> Sorter-cost:  545     Base: 2 2 2 2 2 2 2 7
c ---[ 842]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[ 840]---> Adder-cost: 72   maxlim: 5376   bits: 14/13
c ---[ 838]---> Adder-cost: 74   maxlim: 5248   bits: 14/13
c ---[ 836]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[ 834]---> Adder-cost: 106   maxlim: 7808   bits: 14/13
c ---[ 832]---> Adder-cost: 78   maxlim: 4736   bits: 14/13
c ---[ 830]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[ 828]---> Adder-cost: 152   maxlim: 11904   bits: 15/14
c ---[ 826]---> Adder-cost: 86   maxlim: 5632   bits: 14/13
c ---[ 824]---> Sorter-cost:  973     Base: 2 2 2 2 2 2 2 7
c ---[ 822]---> Adder-cost: 172   maxlim: 12928   bits: 15/14
c ---[ 820]---> Adder-cost: 76   maxlim: 12928   bits: 15/14
c ---[ 818]---> Adder-cost: 76   maxlim: 12928   bits: 15/14
c ---[ 816]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[ 814]---> Sorter-cost:  585     Base: 2 2 2 2 2 2 2 7
c ---[ 812]---> Adder-cost: 176   maxlim: 11264   bits: 15/14
c ---[ 810]---> Adder-cost: 106   maxlim: 6912   bits: 14/13
c ---[ 808]---> Adder-cost: 100   maxlim: 7552   bits: 14/13
c ---[ 806]---> Adder-cost: 136   maxlim: 8704   bits: 15/14
c ---[ 804]---> Adder-cost: 62   maxlim: 8704   bits: 15/14
c ---[ 802]---> Adder-cost: 118   maxlim: 8832   bits: 15/14
c ---[ 800]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[ 798]---> Sorter-cost:  488     Base: 2 2 2 2 2 2 2 7
c ---[ 796]---> Adder-cost: 92   maxlim: 6016   bits: 14/13
c ---[ 794]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[ 792]---> Adder-cost: 100   maxlim: 6784   bits: 14/13
c ---[ 790]---> Adder-cost: 60   maxlim: 4352   bits: 14/13
c ---[ 788]---> Adder-cost: 82   maxlim: 5760   bits: 14/13
c ---[ 786]---> Adder-cost: 94   maxlim: 6784   bits: 14/13
c ---[ 784]---> Sorter-cost:  524     Base: 2 2 2 2 2 2 2 7
c ---[ 782]---> Adder-cost: 176   maxlim: 13056   bits: 15/14
c ---[ 780]---> Sorter-cost:  589     Base: 2 2 2 2 2 2 2 7
c ---[ 778]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[ 776]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 774]---> Adder-cost: 420   maxlim: 30336   bits: 16/15
c ---[ 772]---> Adder-cost: 314   maxlim: 29952   bits: 16/15
c ---[ 770]---> Adder-cost: 162   maxlim: 12160   bits: 15/14
c ---[ 768]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[ 766]---> Adder-cost: 138   maxlim: 10752   bits: 15/14
c ---[ 764]---> Adder-cost: 120   maxlim: 11136   bits: 15/14
c ---[ 762]---> Sorter-cost:  438     Base: 2 2 2 2 2 2 2 7
c ---[ 760]---> Sorter-cost:  254     Base: 2 2 2 2 2 2 2 2
c ---[ 758]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[ 756]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[ 754]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[ 752]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 7
c ---[ 750]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 7
c ---[ 748]---> Sorter-cost:  537     Base: 2 2 2 2 2 2 2 7
c ---[ 746]---> Sorter-cost:  571     Base: 2 2 2 2 2 2 2 7
c ---[ 744]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2
c ---[ 742]---> Adder-cost: 174   maxlim: 11776   bits: 15/14
c ---[ 740]---> Adder-cost: 142   maxlim: 9728   bits: 15/14
c ---[ 738]---> Adder-cost: 224   maxlim: 15104   bits: 15/14
c ---[ 736]---> Adder-cost: 214   maxlim: 15488   bits: 15/14
c ---[ 734]---> Sorter-cost:  790     Base: 2 2 2 2 2 2 2 7
c ---[ 732]---> Adder-cost: 254   maxlim: 16896   bits: 16/15
c ---[ 730]---> Adder-cost: 112   maxlim: 7936   bits: 14/13
c ---[ 728]---> Adder-cost: 138   maxlim: 8960   bits: 15/14
c ---[ 726]---> Adder-cost: 88   maxlim: 10112   bits: 15/14
c ---[ 724]---> Adder-cost: 92   maxlim: 9600   bits: 15/14
c ---[ 722]---> Adder-cost: 196   maxlim: 16384   bits: 16/15
c ---[ 720]---> Adder-cost: 90   maxlim: 16384   bits: 16/15
c ---[ 718]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[ 716]---> Adder-cost: 134   maxlim: 8192   bits: 15/14
c ---[ 714]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[ 712]---> Adder-cost: 136   maxlim: 9216   bits: 15/14
c ---[ 710]---> Adder-cost: 62   maxlim: 9216   bits: 15/14
c ---[ 708]---> Adder-cost: 62   maxlim: 9216   bits: 15/14
c ---[ 706]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[ 704]---> Adder-cost: 108   maxlim: 7296   bits: 14/13
c ---[ 702]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[ 700]---> Adder-cost: 110   maxlim: 7808   bits: 14/13
c ---[ 698]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2
c ---[ 696]---> Sorter-cost:  358     Base: 2 2 2 2 2 2 2 7
c ---[ 694]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[ 692]---> Adder-cost: 158   maxlim: 10496   bits: 15/14
c ---[ 690]---> Adder-cost: 162   maxlim: 12160   bits: 15/14
c ---[ 688]---> Adder-cost: 64   maxlim: 12160   bits: 15/14
c ---[ 686]---> Adder-cost: 64   maxlim: 12160   bits: 15/14
c ---[ 684]---> Adder-cost: 64   maxlim: 12160   bits: 15/14
c ---[ 682]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 680]---> Adder-cost: 132   maxlim: 8832   bits: 15/14
c ---[ 678]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[ 676]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[ 674]---> Adder-cost: 144   maxlim: 9728   bits: 15/14
c ---[ 672]---> Adder-cost: 108   maxlim: 7936   bits: 14/13
c ---[ 670]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 7
c ---[ 668]---> Sorter-cost: 1064     Base: 2 2 2 2 2 2 2 7
c ---[ 666]---> Adder-cost: 142   maxlim: 9600   bits: 15/14
c ---[ 664]---> Adder-cost: 188   maxlim: 13056   bits: 15/14
c ---[ 662]---> Adder-cost: 74   maxlim: 13056   bits: 15/14
c ---[ 660]---> Adder-cost: 128   maxlim: 8704   bits: 15/14
c ---[ 658]---> Adder-cost: 158   maxlim: 10368   bits: 15/14
c ---[ 656]---> Adder-cost: 104   maxlim: 6656   bits: 14/13
c ---[ 654]---> Adder-cost: 74   maxlim: 4992   bits: 14/13
c ---[ 652]---> Adder-cost: 78   maxlim: 6784   bits: 14/13
c ---[ 650]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[ 648]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 7
c ---[ 646]---> Adder-cost: 76   maxlim: 4992   bits: 14/13
c ---[ 644]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[ 642]---> Adder-cost: 98   maxlim: 6784   bits: 14/13
c ---[ 640]---> Adder-cost: 68   maxlim: 4480   bits: 14/13
c ---[ 638]---> Adder-cost: 160   maxlim: 11648   bits: 15/14
c ---[ 636]---> Adder-cost: 114   maxlim: 7680   bits: 14/13
c ---[ 634]---> Adder-cost: 156   maxlim: 16256   bits: 15/14
c ---[ 632]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[ 630]---> Adder-cost: 112   maxlim: 7168   bits: 14/13
c ---[ 628]---> Adder-cost: 146   maxlim: 9856   bits: 15/14
c ---[ 626]---> Adder-cost: 182   maxlim: 12288   bits: 15/14
c ---[ 624]---> Adder-cost: 144   maxlim: 12288   bits: 15/14
c ---[ 622]---> Adder-cost: 64   maxlim: 11648   bits: 15/14
c ---[ 620]---> Adder-cost: 212   maxlim: 16512   bits: 16/15
c ---[ 618]---> Adder-cost: 200   maxlim: 15232   bits: 15/14
c ---[ 616]---> Sorter-cost:  905     Base: 2 2 2 2 2 2 2 7
c ---[ 614]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[ 612]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[ 610]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 7
c ---[ 608]---> Sorter-cost:  958     Base: 2 2 2 2 2 2 2 7
c ---[ 606]---> Adder-cost: 132   maxlim: 9216   bits: 15/14
c ---[ 604]---> Adder-cost: 62   maxlim: 9216   bits: 15/14
c ---[ 602]---> Adder-cost: 64   maxlim: 11648   bits: 15/14
c ---[ 600]---> Adder-cost: 188   maxlim: 13056   bits: 15/14
c ---[ 598]---> Adder-cost: 74   maxlim: 13056   bits: 15/14
c ---[ 596]---> Adder-cost: 74   maxlim: 13056   bits: 15/14
c ---[ 594]---> Adder-cost: 120   maxlim: 8832   bits: 15/14
c ---[ 592]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 7
c ---[ 590]---> Sorter-cost:  368     Base: 2 2 2 2 2 2 2 7
c ---[ 588]---> Adder-cost: 104   maxlim: 11904   bits: 15/14
c ---[ 586]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 7
c ---[ 584]---> Sorter-cost:  916     Base: 2 2 2 2 2 2 2 7
c ---[ 582]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[ 580]---> Adder-cost: 124   maxlim: 8448   bits: 15/14
c ---[ 578]---> Adder-cost: 120   maxlim: 8192   bits: 15/14
c ---[ 576]---> Adder-cost: 56   maxlim: 7040   bits: 14/13
c ---[ 574]---> Adder-cost: 98   maxlim: 7040   bits: 14/13
c ---[ 572]---> Sorter-cost:  264     Base: 2 2 2 2 2 2 2 2
c ---[ 570]---> Adder-cost: 136   maxlim: 9728   bits: 15/14
c ---[ 568]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[ 566]---> Adder-cost: 92   maxlim: 6144   bits: 14/13
c ---[ 564]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[ 562]---> Adder-cost: 212   maxlim: 15872   bits: 15/14
c ---[ 560]---> Adder-cost: 104   maxlim: 7296   bits: 14/13
c ---[ 558]---> Adder-cost: 128   maxlim: 9088   bits: 15/14
c ---[ 556]---> Adder-cost: 134   maxlim: 8576   bits: 15/14
c ---[ 554]---> Adder-cost: 112   maxlim: 7424   bits: 14/13
c ---[ 552]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[ 550]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[ 548]---> Adder-cost: 164   maxlim: 11904   bits: 15/14
c ---[ 546]---> Adder-cost: 144   maxlim: 11008   bits: 15/14
c ---[ 544]---> Adder-cost: 184   maxlim: 16000   bits: 15/14
c ---[ 542]---> Adder-cost: 136   maxlim: 12416   bits: 15/14
c ---[ 540]---> Sorter-cost: 1017     Base: 2 2 2 2 2 2 2 7
c ---[ 538]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 7
c ---[ 536]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 7
c ---[ 534]---> Adder-cost: 148   maxlim: 9984   bits: 15/14
c ---[ 532]---> Adder-cost: 198   maxlim: 13952   bits: 15/14
c ---[ 530]---> Adder-cost: 196   maxlim: 13696   bits: 15/14
c ---[ 528]---> Adder-cost: 222   maxlim: 15744   bits: 15/14
c ---[ 526]---> Adder-cost: 152   maxlim: 12544   bits: 15/14
c ---[ 524]---> Adder-cost: 194   maxlim: 16512   bits: 16/15
c ---[ 522]---> Adder-cost: 132   maxlim: 8960   bits: 15/14
c ---[ 520]---> Sorter-cost:  992     Base: 2 2 2 2 2 2 2 7
c ---[ 518]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[ 516]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[ 514]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[ 512]---> Adder-cost: 62   maxlim: 9600   bits: 15/14
c ---[ 510]---> Adder-cost: 110   maxlim: 13696   bits: 15/14
c ---[ 508]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2
c ---[ 506]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[ 504]---> Sorter-cost:  252     Base: 2 2 2 2 2 2 2 2
c ---[ 502]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[ 500]---> Sorter-cost:  260     Base: 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost:  258     Base: 2 2 2 2 2 2 2 2
c ---[ 494]---> Adder-cost: 178   maxlim: 12672   bits: 15/14
c ---[ 492]---> Sorter-cost:  889     Base: 2 2 2 2 2 2 2 7
c ---[ 490]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 7
c ---[ 488]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2
c ---[ 486]---> Adder-cost: 118   maxlim: 8576   bits: 15/14
c ---[ 484]---> Adder-cost: 72   maxlim: 12672   bits: 15/14
c ---[ 482]---> Adder-cost: 222   maxlim: 16896   bits: 16/15
c ---[ 480]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[ 478]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[ 476]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[ 474]---> Sorter-cost:  905     Base: 2 2 2 2 2 2 2 7
c ---[ 472]---> Adder-cost: 104   maxlim: 7296   bits: 14/13
c ---[ 470]---> Adder-cost: 106   maxlim: 7424   bits: 14/13
c ---[ 468]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[ 466]---> Adder-cost: 72   maxlim: 12672   bits: 15/14
c ---[ 464]---> Adder-cost: 68   maxlim: 7552   bits: 14/13
c ---[ 462]---> Adder-cost: 98   maxlim: 7040   bits: 14/13
c ---[ 460]---> Adder-cost: 82   maxlim: 6272   bits: 14/13
c ---[ 458]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[ 456]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[ 454]---> Adder-cost: 66   maxlim: 6272   bits: 14/13
c ---[ 452]---> Adder-cost: 136   maxlim: 10240   bits: 15/14
c ---[ 450]---> Adder-cost: 166   maxlim: 11520   bits: 15/14
c ---[ 448]---> Adder-cost: 160   maxlim: 12032   bits: 15/14
c ---[ 446]---> Adder-cost: 68   maxlim: 12032   bits: 15/14
c ---[ 444]---> Adder-cost: 100   maxlim: 6528   bits: 14/13
c ---[ 442]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[ 440]---> Adder-cost: 134   maxlim: 8448   bits: 15/14
c ---[ 438]---> Adder-cost: 328   maxlim: 22656   bits: 16/15
c ---[ 436]---> Adder-cost: 106   maxlim: 22656   bits: 16/15
c ---[ 434]---> Adder-cost: 136   maxlim: 10112   bits: 15/14
c ---[ 432]---> Adder-cost: 74   maxlim: 4352   bits: 14/13
c ---[ 430]---> Adder-cost: 112   maxlim: 7680   bits: 14/13
c ---[ 428]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[ 426]---> Adder-cost: 64   maxlim: 4864   bits: 14/13
c ---[ 424]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[ 422]---> Adder-cost: 234   maxlim: 16896   bits: 16/15
c ---[ 420]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 7
c ---[ 418]---> Adder-cost: 384   maxlim: 31744   bits: 16/15
c ---[ 416]---> Adder-cost: 132   maxlim: 31744   bits: 16/15
c ---[ 414]---> Adder-cost: 92   maxlim: 6912   bits: 14/13
c ---[ 412]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2
c ---[ 410]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[ 408]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[ 406]---> Adder-cost: 170   maxlim: 13824   bits: 15/14
c ---[ 404]---> Adder-cost: 168   maxlim: 12160   bits: 15/14
c ---[ 402]---> Adder-cost: 120   maxlim: 7680   bits: 14/13
c ---[ 400]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[ 398]---> Adder-cost: 80   maxlim: 7168   bits: 14/13
c ---[ 396]---> Adder-cost: 64   maxlim: 7296   bits: 14/13
c ---[ 394]---> Adder-cost: 64   maxlim: 6016   bits: 14/13
c ---[ 392]---> Adder-cost: 68   maxlim: 5888   bits: 14/13
c ---[ 390]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[ 388]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[ 386]---> Adder-cost: 70   maxlim: 4864   bits: 14/13
c ---[ 384]---> Adder-cost: 208   maxlim: 13440   bits: 15/14
c ---[ 382]---> Adder-cost: 78   maxlim: 13440   bits: 15/14
c ---[ 380]---> Adder-cost: 142   maxlim: 13312   bits: 15/14
c ---[ 378]---> Sorter-cost:  588     Base: 2 2 2 2 2 2 2 7
c ---[ 376]---> Adder-cost: 106   maxlim: 6784   bits: 14/13
c ---[ 374]---> Adder-cost: 194   maxlim: 15104   bits: 15/14
c ---[ 372]---> Adder-cost: 132   maxlim: 11776   bits: 15/14
c ---[ 370]---> Adder-cost: 124   maxlim: 9728   bits: 15/14
c ---[ 368]---> Adder-cost: 78   maxlim: 5248   bits: 14/13
c ---[ 366]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[ 364]---> Adder-cost: 138   maxlim: 8320   bits: 15/14
c ---[ 362]---> Adder-cost: 150   maxlim: 9984   bits: 15/14
c ---[ 360]---> Adder-cost: 112   maxlim: 9216   bits: 15/14
c ---[ 358]---> Adder-cost: 202   maxlim: 13568   bits: 15/14
c ---[ 356]---> Adder-cost: 102   maxlim: 7168   bits: 14/13
c ---[ 354]---> Adder-cost: 64   maxlim: 6784   bits: 14/13
c ---[ 352]---> Adder-cost: 74   maxlim: 4736   bits: 14/13
c ---[ 350]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[ 348]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 346]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[ 344]---> Adder-cost: 116   maxlim: 9728   bits: 15/14
c ---[ 342]---> Adder-cost: 112   maxlim: 7168   bits: 14/13
c ---[ 340]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[ 338]---> Adder-cost: 88   maxlim: 5376   bits: 14/13
c ---[ 336]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[ 334]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[ 332]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[ 330]---> Adder-cost: 196   maxlim: 14848   bits: 15/14
c ---[ 328]---> Adder-cost: 64   maxlim: 9728   bits: 15/14
c ---[ 326]---> Adder-cost: 80   maxlim: 14848   bits: 15/14
c ---[ 324]---> Adder-cost: 206   maxlim: 14720   bits: 15/14
c ---[ 322]---> Adder-cost: 154   maxlim: 10112   bits: 15/14
c ---[ 320]---> Adder-cost: 250   maxlim: 16896   bits: 16/15
c ---[ 318]---> Adder-cost: 378   maxlim: 29056   bits: 16/15
c ---[ 316]---> Adder-cost: 124   maxlim: 29056   bits: 16/15
c ---[ 314]---> Adder-cost: 124   maxlim: 29056   bits: 16/15
c ---[ 312]---> Adder-cost: 124   maxlim: 29056   bits: 16/15
c ---[ 310]---> Adder-cost: 252   maxlim: 16640   bits: 16/15
c ---[ 308]---> Adder-cost: 114   maxlim: 7680   bits: 14/13
c ---[ 306]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[ 304]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[ 302]---> Sorter-cost:  926     Base: 2 2 2 2 2 2 2 7
c ---[ 300]---> Adder-cost: 184   maxlim: 11520   bits: 15/14
c ---[ 298]---> Sorter-cost:  687     Base: 2 2 2 2 2 2 2 7
c ---[ 296]---> Adder-cost: 184   maxlim: 13056   bits: 15/14
c ---[ 294]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[ 292]---> Adder-cost: 62   maxlim: 4992   bits: 14/13
c ---[ 290]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[ 288]---> Adder-cost: 118   maxlim: 7680   bits: 14/13
c ---[ 286]---> Adder-cost: 84   maxlim: 5248   bits: 14/13
c ---[ 284]---> Adder-cost: 416   maxlim: 31104   bits: 16/15
c ---[ 282]---> Adder-cost: 384   maxlim: 33408   bits: 17/16
c ---[ 280]---> Adder-cost: 142   maxlim: 33408   bits: 17/16
c ---[ 278]---> Adder-cost: 100   maxlim: 7808   bits: 14/13
c ---[ 276]---> Adder-cost: 84   maxlim: 7680   bits: 14/13
c ---[ 274]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[ 272]---> Adder-cost: 382   maxlim: 27648   bits: 16/15
c ---[ 270]---> Adder-cost: 78   maxlim: 5248   bits: 14/13
c ---[ 268]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[ 266]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[ 264]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[ 262]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[ 260]---> Adder-cost: 272   maxlim: 18048   bits: 16/15
c ---[ 258]---> Sorter-cost:  390     Base: 2 2 2 2 2 2 2 7
c ---[ 256]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 7
c ---[ 254]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 7
c ---[ 252]---> Adder-cost: 92   maxlim: 6016   bits: 14/13
c ---[ 250]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[ 248]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[ 246]---> Adder-cost: 104   maxlim: 7808   bits: 14/13
c ---[ 244]---> Adder-cost: 236   maxlim: 17792   bits: 16/15
c ---[ 242]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[ 240]---> Sorter-cost:  635     Base: 2 2 2 2 2 2 2 7
c ---[ 238]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 236]---> Adder-cost: 176   maxlim: 12672   bits: 15/14
c ---[ 234]---> Adder-cost: 198   maxlim: 13440   bits: 15/14
c ---[ 232]---> Adder-cost: 252   maxlim: 19072   bits: 16/15
c ---[ 230]---> Adder-cost: 94   maxlim: 19072   bits: 16/15
c ---[ 228]---> Adder-cost: 64   maxlim: 4736   bits: 14/13
c ---[ 226]---> Adder-cost: 158   maxlim: 12544   bits: 15/14
c ---[ 224]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[ 222]---> Adder-cost: 168   maxlim: 12160   bits: 15/14
c ---[ 220]---> Adder-cost: 64   maxlim: 12160   bits: 15/14
c ---[ 218]---> Adder-cost: 218   maxlim: 17408   bits: 16/15
c ---[ 216]---> Adder-cost: 138   maxlim: 9984   bits: 15/14
c ---[ 214]---> Adder-cost: 78   maxlim: 5248   bits: 14/13
c ---[ 212]---> Adder-cost: 128   maxlim: 8960   bits: 15/14
c ---[ 210]---> Adder-cost: 60   maxlim: 8960   bits: 15/14
c ---[ 208]---> Adder-cost: 222   maxlim: 15104   bits: 15/14
c ---[ 206]---> Adder-cost: 108   maxlim: 6784   bits: 14/13
c ---[ 204]---> Adder-cost: 46   maxlim: 6784   bits: 14/13
c ---[ 202]---> Adder-cost: 170   maxlim: 10752   bits: 15/14
c ---[ 200]---> Adder-cost: 174   maxlim: 11776   bits: 15/14
c ---[ 198]---> Adder-cost: 160   maxlim: 10624   bits: 15/14
c ---[ 196]---> Adder-cost: 94   maxlim: 7552   bits: 14/13
c ---[ 194]---> Sorter-cost:  932     Base: 2 2 2 2 2 2 2 7
c ---[ 192]---> Sorter-cost:  741     Base: 2 2 2 2 2 2 2 7
c ---[ 190]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 7
c ---[ 188]---> Adder-cost: 82   maxlim: 5248   bits: 14/13
c ---[ 186]---> Adder-cost: 74   maxlim: 4736   bits: 14/13
c ---[ 184]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 7
c ---[ 182]---> Sorter-cost:  612     Base: 2 2 2 2 2 2 2 7
c ---[ 180]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[ 178]---> Adder-cost: 360   maxlim: 30336   bits: 16/15
c ---[ 176]---> Adder-cost: 358   maxlim: 28672   bits: 16/15
c ---[ 174]---> Adder-cost: 94   maxlim: 6912   bits: 14/13
c ---[ 172]---> Adder-cost: 66   maxlim: 4480   bits: 14/13
c ---[ 170]---> Adder-cost: 192   maxlim: 14720   bits: 15/14
c ---[ 168]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[ 166]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[ 164]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[ 162]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[ 160]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[ 158]---> Sorter-cost:  608     Base: 2 2 2 2 2 2 2 7
c ---[ 156]---> Adder-cost: 88   maxlim: 6400   bits: 14/13
c ---[ 154]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[ 152]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[ 150]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[ 148]---> Sorter-cost:  930     Base: 2 2 2 2 2 2 2 7
c ---[ 146]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[ 144]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[ 142]---> Adder-cost: 132   maxlim: 9472   bits: 15/14
c ---[ 140]---> Adder-cost: 64   maxlim: 9472   bits: 15/14
c ---[ 138]---> Adder-cost: 122   maxlim: 8704   bits: 15/14
c ---[ 136]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[ 134]---> Sorter-cost:  258     Base: 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 7
c ---[ 128]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[ 126]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 7
c ---[ 124]---> Adder-cost: 122   maxlim: 9088   bits: 15/14
c ---[ 122]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[ 120]---> Adder-cost: 56   maxlim: 9088   bits: 15/14
c ---[ 118]---> Adder-cost: 88   maxlim: 7680   bits: 14/13
c ---[ 116]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[ 114]---> Adder-cost: 104   maxlim: 7936   bits: 14/13
c ---[ 112]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[ 110]---> Adder-cost: 86   maxlim: 5632   bits: 14/13
c ---[ 108]---> Adder-cost: 146   maxlim: 10880   bits: 15/14
c ---[ 106]---> Sorter-cost: 1018     Base: 2 2 2 2 2 2 2 7
c ---[ 104]---> Adder-cost: 74   maxlim: 4480   bits: 14/13
c ---[ 102]---> Sorter-cost:  930     Base: 2 2 2 2 2 2 2 7
c ---[ 100]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[  98]---> Sorter-cost:  733     Base: 2 2 2 2 2 2 2 7
c ---[  96]---> Adder-cost: 92   maxlim: 6144   bits: 14/13
c ---[  94]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[  92]---> Adder-cost: 140   maxlim: 10496   bits: 15/14
c ---[  90]---> Adder-cost: 70   maxlim: 4992   bits: 14/13
c ---[  88]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[  86]---> Adder-cost: 94   maxlim: 6784   bits: 14/13
c ---[ /oldhome/oroussel/solvers/minisat+_script: line 16: 12684 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.97 0.91 2/54 12679
Raw data (stat): 12679 (runsolver) R 12678 25568 25567 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784913716 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+20.0009 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+30.0005 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+40.0011 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+50.0023 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+60.0026 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+70.0026 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+80.0118 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+90.0116 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+100.012 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+110.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+130.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+170.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+220.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+230.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+240.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+260.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+280.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+290.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+300.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+310.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+320.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+330.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+340.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+350.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+360.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+370.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+390.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+400.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+420.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+430.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+440.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+500.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+530.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+550.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+560.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+570.031 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+580.033 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+590.033 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+600.033 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+610.033 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+620.034 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+630.034 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+640.035 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+650.036 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+660.036 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+670.036 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+680.036 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+690.037 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+700.038 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+710.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+720.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+730.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+740.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+750.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+760.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+770.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+780.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+790.071 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+800.072 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+810.071 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+820.072 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+830.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+840.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+850.073 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+860.075 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+870.075 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+880.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+890.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+900.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+910.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+920.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+930.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+940.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+950.081 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+960.082 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+970.083 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+980.083 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+990.083 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1040.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1050.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1060.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1210.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1220.09 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1229.94 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 12684
Raw data (stat): 12679 (minisat+_script) S 12678 25568 25567 0 -1 0 300 1903 0 0 0 0 27 5 18 0 1 0 784913716 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 0

Child status: 152
Real time (s): 1229.94
CPU time (s): 1230.31
CPU user time (s): 1227.37
CPU system time (s): 2.94555
CPU usage (%): 100.031
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####