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-dc1c.opb
MD5SUM	52ee1c9a03c9aae47fd9a079818acfac
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	41560
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	6649307310053731437
Number of bits of the sum of numbers in the objective function	63
Biggest number in a constraint	524288000000000000
Number of bits of the biggest number in a constraint	59
Biggest sum of numbers in a constraint	6777307310053731437
Number of bits of the biggest sum of numbers	63
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1264.1
Number of variables	41560
Total number of constraints	10029
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	8381
Number of constraints which are nor clauses,nor cardinality constraints	1648
Minimum length of a constraint	1
Maximum length of a constraint	41560
Trace number 31334

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-05-26 00:16:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22729 boxname=wulflinc5 idbench=1545 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  52ee1c9a03c9aae47fd9a079818acfac  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-dc1c.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-dc1c.opb
IDLAUNCH: 22729
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        856288 kB
Buffers:         20436 kB
Cached:         136852 kB
SwapCached:        608 kB
Active:          22560 kB
Inactive:       136748 kB
HighTotal:      131008 kB
HighFree:        15596 kB
LowTotal:       903652 kB
LowFree:        840692 kB
SwapTotal:     2097136 kB
SwapFree:      2095636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5084 kB
Slab:            13424 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:37:06 (client local time) WITH STATUS 152 IN 1230.24 SECONDS
stats: 22729 7 1230.24 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c PARSE ERROR! [line 10043] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 3282 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sss
c ---[3283]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[3281]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[3279]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[3277]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[3275]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[3273]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[3271]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[3269]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[3267]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 7
c ---[3265]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[3263]---> Sorter-cost:  984     Base: 2 2 2 2 2 2 2 7
c ---[3261]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[3259]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 7
c ---[3257]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[3255]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[3253]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[3251]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[3249]---> Sorter-cost:  683     Base: 2 2 2 2 2 2 2 7
c ---[3247]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[3245]---> Sorter-cost:  928     Base: 2 2 2 2 2 2 2 7
c ---[3243]---> Sorter-cost:  724     Base: 2 2 2 2 2 2 2 7
c ---[3241]---> Sorter-cost:  768     Base: 2 2 2 2 2 2 2 7
c ---[3239]---> Adder-cost: 176   maxlim: 10880   bits: 15/14
c ---[3237]---> Adder-cost: 66   maxlim: 10880   bits: 15/14
c ---[3235]---> Adder-cost: 112   maxlim: 7424   bits: 14/13
c ---[3233]---> Adder-cost: 96   maxlim: 6400   bits: 14/13
c ---[3231]---> Adder-cost: 148   maxlim: 8960   bits: 15/14
c ---[3229]---> Adder-cost: 142   maxlim: 8832   bits: 15/14
c ---[3227]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[3225]---> Sorter-cost:  738     Base: 2 2 2 2 2 2 2 7
c ---[3223]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 7
c ---[3221]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 7
c ---[3219]---> Sorter-cost:  642     Base: 2 2 2 2 2 2 2 7
c ---[3217]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 7
c ---[3215]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[3213]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[3211]---> Adder-cost: 78   maxlim: 4992   bits: 14/13
c ---[3209]---> Adder-cost: 74   maxlim: 4992   bits: 14/13
c ---[3207]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[3205]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[3203]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[3201]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[3199]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[3197]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[3195]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[3193]---> Adder-cost: 86   maxlim: 6016   bits: 14/13
c ---[3191]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[3189]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[3187]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[3185]---> Adder-cost: 76   maxlim: 6400   bits: 14/13
c ---[3183]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[3181]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[3179]---> Sorter-cost:  638     Base: 2 2 2 2 2 2 2 7
c ---[3177]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[3175]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 7
c ---[3173]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[3171]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[3169]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[3167]---> Adder-cost: 72   maxlim: 4352   bits: 14/13
c ---[3165]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[3163]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[3161]---> Sorter-cost:  657     Base: 2 2 2 2 2 2 2 7
c ---[3159]---> Sorter-cost:  758     Base: 2 2 2 2 2 2 2 7
c ---[3157]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[3155]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[3153]---> Sorter-cost:  978     Base: 2 2 2 2 2 2 2 7
c ---[3151]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 7
c ---[3149]---> Sorter-cost:  580     Base: 2 2 2 2 2 2 2 7
c ---[3147]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 7
c ---[3145]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[3143]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[3141]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[3139]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[3137]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[3135]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[3133]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[3131]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[3129]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[3127]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[3125]---> Adder-cost: 146   maxlim: 8832   bits: 15/14
c ---[3123]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[3121]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[3119]---> Adder-cost: 120   maxlim: 7808   bits: 14/13
c ---[3117]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[3115]---> Adder-cost: 132   maxlim: 8448   bits: 15/14
c ---[3113]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[3111]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[3109]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[3107]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[3105]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[3103]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[3101]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[3099]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[3097]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[3095]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[3093]---> Sorter-cost:  642     Base: 2 2 2 2 2 2 2 7
c ---[3091]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[3089]---> Adder-cost: 178   maxlim: 11008   bits: 15/14
c ---[3087]---> Adder-cost: 68   maxlim: 11008   bits: 15/14
c ---[3085]---> Adder-cost: 138   maxlim: 10752   bits: 15/14
c ---[3083]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[3081]---> Adder-cost: 120   maxlim: 7424   bits: 14/13
c ---[3079]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[3077]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[3075]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[3073]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[3071]---> Adder-cost: 104   maxlim: 6144   bits: 14/13
c ---[3069]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[3067]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[3065]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[3063]---> Adder-cost: 120   maxlim: 7552   bits: 14/13
c ---[3061]---> Adder-cost: 48   maxlim: 7552   bits: 14/13
c ---[3059]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[3057]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[3055]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[3053]---> Adder-cost: 58   maxlim: 5120   bits: 14/13
c ---[3051]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[3049]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[3047]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[3045]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[3043]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[3041]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[3039]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[3037]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[3035]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[3033]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[3031]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[3029]---> Adder-cost: 86   maxlim: 5120   bits: 14/13
c ---[3027]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[3025]---> Adder-cost: 112   maxlim: 6912   bits: 14/13
c ---[3023]---> Adder-cost: 48   maxlim: 6912   bits: 14/13
c ---[3021]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[3019]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[3017]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[3015]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[3013]---> Adder-cost: 96   maxlim: 6656   bits: 14/13
c ---[3011]---> Adder-cost: 112   maxlim: 6912   bits: 14/13
c ---[3009]---> Adder-cost: 48   maxlim: 6912   bits: 14/13
c ---[3007]---> Adder-cost: 104   maxlim: 6528   bits: 14/13
c ---[3005]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[3003]---> Adder-cost: 90   maxlim: 6016   bits: 14/13
c ---[3001]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[2999]---> Adder-cost: 94   maxlim: 5888   bits: 14/13
c ---[2997]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[2995]---> Adder-cost: 110   maxlim: 6912   bits: 14/13
c ---[2993]---> Adder-cost: 48   maxlim: 6912   bits: 14/13
c ---[2991]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[2989]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[2987]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[2985]---> Sorter-cost:  734     Base: 2 2 2 2 2 2 2 7
c ---[2983]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2981]---> Sorter-cost:  914     Base: 2 2 2 2 2 2 2 7
c ---[2979]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[2977]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[2975]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[2973]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 7
c ---[2971]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[2969]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[2967]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 7
c ---[2965]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[2963]---> Sorter-cost:  250     Base: 2 2 2 2 2 2 2 2
c ---[2961]---> Adder-cost: 156   maxlim: 9600   bits: 15/14
c ---[2959]---> Adder-cost: 62   maxlim: 9600   bits: 15/14
c ---[2957]---> Adder-cost: 198   maxlim: 13696   bits: 15/14
c ---[2955]---> Adder-cost: 132   maxlim: 8320   bits: 15/14
c ---[2953]---> Adder-cost: 78   maxlim: 13696   bits: 15/14
c ---[2951]---> Adder-cost: 396   maxlim: 25728   bits: 16/15
c ---[2949]---> Adder-cost: 116   maxlim: 25728   bits: 16/15
c ---[2947]---> Adder-cost: 396   maxlim: 26240   bits: 16/15
c ---[2945]---> Adder-cost: 112   maxlim: 26240   bits: 16/15
c ---[2943]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[2941]---> Adder-cost: 276   maxlim: 20224   bits: 16/15
c ---[2939]---> Adder-cost: 92   maxlim: 20224   bits: 16/15
c ---[2937]---> Adder-cost: 334   maxlim: 23808   bits: 16/15
c ---[2935]---> Adder-cost: 106   maxlim: 23808   bits: 16/15
c ---[2933]---> Adder-cost: 414   maxlim: 29568   bits: 16/15
c ---[2931]---> Adder-cost: 90   maxlim: 7296   bits: 14/13
c ---[2929]---> Adder-cost: 124   maxlim: 29568   bits: 16/15
c ---[2927]---> Adder-cost: 452   maxlim: 30848   bits: 16/15
c ---[2925]---> Adder-cost: 576   maxlim: 39296   bits: 17/16
c ---[2923]---> Adder-cost: 586   maxlim: 40576   bits: 17/16
c ---[2921]---> Adder-cost: 518   maxlim: 33152   bits: 17/16
c ---[2919]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[2917]---> Adder-cost: 482   maxlim: 31744   bits: 16/15
c ---[2915]---> Adder-cost: 558   maxlim: 37504   bits: 17/16
c ---[2913]---> Adder-cost: 410   maxlim: 28544   bits: 16/15
c ---[2911]---> Adder-cost: 368   maxlim: 25472   bits: 16/15
c ---[2909]---> Adder-cost: 110   maxlim: 25472   bits: 16/15
c ---[2907]---> Adder-cost: 334   maxlim: 25216   bits: 16/15
c ---[2905]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[2903]---> Adder-cost: 114   maxlim: 25216   bits: 16/15
c ---[2901]---> Adder-cost: 340   maxlim: 23680   bits: 16/15
c ---[2899]---> Adder-cost: 104   maxlim: 23680   bits: 16/15
c ---[2897]---> Adder-cost: 374   maxlim: 26240   bits: 16/15
c ---[2895]---> Adder-cost: 112   maxlim: 26240   bits: 16/15
c ---[2893]---> Adder-cost: 404   maxlim: 27264   bits: 16/15
c ---[2891]---> Adder-cost: 328   maxlim: 22784   bits: 16/15
c ---[2889]---> Adder-cost: 106   maxlim: 22784   bits: 16/15
c ---[2887]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[2885]---> Adder-cost: 182   maxlim: 11904   bits: 15/14
c ---[2883]---> Adder-cost: 70   maxlim: 11904   bits: 15/14
c ---[2881]---> Adder-cost: 216   maxlim: 14592   bits: 15/14
c ---[2879]---> Adder-cost: 78   maxlim: 14592   bits: 15/14
c ---[2877]---> Adder-cost: 192   maxlim: 12800   bits: 15/14
c ---[2875]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[2873]---> Adder-cost: 76   maxlim: 12800   bits: 15/14
c ---[2871]---> Adder-cost: 226   maxlim: 15360   bits: 15/14
c ---[2869]---> Adder-cost: 80   maxlim: 15360   bits: 15/14
c ---[2867]---> Adder-cost: 264   maxlim: 17792   bits: 16/15
c ---[2865]---> Adder-cost: 92   maxlim: 17792   bits: 16/15
c ---[2863]---> Adder-cost: 120   maxlim: 8576   bits: 15/14
c ---[2861]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[2859]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[2857]---> Adder-cost: 108   maxlim: 7296   bits: 14/13
c ---[2855]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[2853]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[2851]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[2849]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2847]---> Sorter-cost:  348     Base: 2 2 2 2 2 2 2 7
c ---[2845]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[2843]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[2841]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[2839]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[2837]---> Adder-cost: 86   maxlim: 8448   bits: 15/14
c ---[2835]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[2833]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[2831]---> Adder-cost: 146   maxlim: 8704   bits: 15/14
c ---[2829]---> Adder-cost: 134   maxlim: 9088   bits: 15/14
c ---[2827]---> Adder-cost: 138   maxlim: 8448   bits: 15/14
c ---[2825]---> Adder-cost: 90   maxlim: 7936   bits: 14/13
c ---[2823]---> Adder-cost: 108   maxlim: 7040   bits: 14/13
c ---[2821]---> Adder-cost: 102   maxlim: 6528   bits: 14/13
c ---[2819]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2817]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 7
c ---[2815]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 7
c ---[2813]---> Adder-cost: 106   maxlim: 6528   bits: 14/13
c ---[2811]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[2809]---> Adder-cost: 108   maxlim: 7424   bits: 14/13
c ---[2807]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[2805]---> Adder-cost: 120   maxlim: 7552   bits: 14/13
c ---[2803]---> Adder-cost: 114   maxlim: 7808   bits: 14/13
c ---[2801]---> Adder-cost: 96   maxlim: 6400   bits: 14/13
c ---[2799]---> Adder-cost: 78   maxlim: 6144   bits: 14/13
c ---[2797]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[2795]---> Adder-cost: 74   maxlim: 4736   bits: 14/13
c ---[2793]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[2791]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[2789]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[2787]---> Adder-cost: 92   maxlim: 5632   bits: 14/13
c ---[2785]---> Sorter-cost:  976     Base: 2 2 2 2 2 2 2 7
c ---[2783]---> Sorter-cost:  932     Base: 2 2 2 2 2 2 2 7
c ---[2781]---> Sorter-cost: 1027     Base: 2 2 2 2 2 2 2 7
c ---[2779]---> Sorter-cost:  896     Base: 2 2 2 2 2 2 2 7
c ---[2777]---> Sorter-cost:  596     Base: 2 2 2 2 2 2 2 7
c ---[2775]---> Adder-cost: 146   maxlim: 8704   bits: 15/14
c ---[2773]---> Adder-cost: 62   maxlim: 8704   bits: 15/14
c ---[2771]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[2769]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[2767]---> Sorter-cost:  457     Base: 2 2 2 2 2 2 2 7
c ---[2765]---> Adder-cost: 138   maxlim: 8320   bits: 15/14
c ---[2763]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[2761]---> Adder-cost: 106   maxlim: 6784   bits: 14/13
c ---[2759]---> Adder-cost: 46   maxlim: 6784   bits: 14/13
c ---[2757]---> Adder-cost: 122   maxlim: 7808   bits: 14/13
c ---[2755]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[2753]---> Adder-cost: 104   maxlim: 6400   bits: 14/13
c ---[2751]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[2749]---> Adder-cost: 120   maxlim: 7424   bits: 14/13
c ---[2747]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[2745]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[2743]---> Adder-cost: 106   maxlim: 7040   bits: 14/13
c ---[2741]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[2739]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[2737]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[2735]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[2733]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[2731]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[2729]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[2727]---> Adder-cost: 78   maxlim: 4864   bits: 14/13
c ---[2725]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[2723]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 7
c ---[2721]---> Adder-cost: 112   maxlim: 7040   bits: 14/13
c ---[2719]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[2717]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[2715]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[2713]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[2711]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[2709]---> Sorter-cost:  782     Base: 2 2 2 2 2 2 2 7
c ---[2707]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[2705]---> Sorter-cost:  932     Base: 2 2 2 2 2 2 2 7
c ---[2703]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[2701]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[2699]---> Sorter-cost: 1066     Base: 2 2 2 2 2 2 2 7
c ---[2697]---> Sorter-cost:  668     Base: 2 2 2 2 2 2 2 7
c ---[2695]---> Sorter-cost:  932     Base: 2 2 2 2 2 2 2 7
c ---[2693]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[2691]---> Sorter-cost:  684     Base: 2 2 2 2 2 2 2 7
c ---[2689]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2687]---> Adder-cost: 112   maxlim: 6912   bits: 14/13
c ---[2685]---> Adder-cost: 48   maxlim: 6912   bits: 14/13
c ---[2683]---> Adder-cost: 48   maxlim: 6912   bits: 14/13
c ---[2681]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[2679]---> Sorter-cost:  425     Base: 2 2 2 2 2 2 2 7
c ---[2677]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[2675]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 7
c ---[2673]---> Sorter-cost:  633     Base: 2 2 2 2 2 2 2 7
c ---[2671]---> Adder-cost: 124   maxlim: 7680   bits: 14/13
c ---[2669]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[2667]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2665]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[2663]---> Adder-cost: 110   maxlim: 6656   bits: 14/13
c ---[2661]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[2659]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[2657]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[2655]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[2653]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 7
c ---[2651]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[2649]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[2647]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[2645]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 7
c ---[2643]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[2641]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[2639]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[2637]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[2635]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 7
c ---[2633]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[2631]---> Sorter-cost:  784     Base: 2 2 2 2 2 2 2 7
c ---[2629]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[2627]---> Adder-cost: 146   maxlim: 8704   bits: 15/14
c ---[2625]---> Adder-cost: 62   maxlim: 8704   bits: 15/14
c ---[2623]---> Adder-cost: 126   maxlim: 7936   bits: 14/13
c ---[2621]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[2619]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[2617]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2615]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2
c ---[2613]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[2611]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[2609]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 7
c ---[2607]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[2605]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[2603]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[2601]---> Adder-cost: 82   maxlim: 5120   bits: 14/13
c ---[2599]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[2597]---> Adder-cost: 106   maxlim: 6400   bits: 14/13
c ---[2595]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[2593]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[2591]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 7
c ---[2589]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[2587]---> Sorter-cost:  960     Base: 2 2 2 2 2 2 2 7
c ---[2585]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[2583]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[2581]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[2579]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 7
c ---[2577]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[2575]---> Adder-cost: 110   maxlim: 6656   bits: 14/13
c ---[2573]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[2571]---> Adder-cost: 98   maxlim: 6528   bits: 14/13
c ---[2569]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[2567]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[2565]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[2563]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[2561]---> Adder-cost: 84   maxlim: 6144   bits: 14/13
c ---[2559]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[2557]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[2555]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[2553]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[2551]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 7
c ---[2549]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[2547]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[2545]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[2543]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[2541]---> Sorter-cost:  582     Base: 2 2 2 2 2 2 2 7
c ---[2539]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[2537]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[2535]---> Sorter-cost:  292     Base: 2 2 2 2 2 2 2 2
c ---[2533]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[2531]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2529]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[2527]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 7
c ---[2525]---> Sorter-cost:  362     Base: 2 2 2 2 2 2 2 7
c ---[2523]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[2521]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[2519]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[2517]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[2515]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[2513]---> Adder-cost: 104   maxlim: 6400   bits: 14/13
c ---[2511]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[2509]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[2507]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[2505]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[2503]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[2501]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[2499]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[2497]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[2495]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[2493]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[2491]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2489]---> Sorter-cost:  734     Base: 2 2 2 2 2 2 2 7
c ---[2487]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2485]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[2483]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[2481]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[2479]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2477]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[2475]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[2473]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[2471]---> Adder-cost: 72   maxlim: 4352   bits: 14/13
c ---[2469]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[2467]---> Adder-cost: 74   maxlim: 4352   bits: 14/13
c ---[2465]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[2463]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[2461]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[2459]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[2457]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[2455]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[2453]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[2451]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[2449]---> Adder-cost: 154   maxlim: 9344   bits: 15/14
c ---[2447]---> Adder-cost: 60   maxlim: 9344   bits: 15/14
c ---[2445]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[2443]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[2441]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[2439]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[2437]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[2435]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[2433]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[2431]---> Adder-cost: 46   maxlim: 6784   bits: 14/13
c ---[2429]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[2427]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2425]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[2423]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[2421]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[2419]---> Sorter-cost:  676     Base: 2 2 2 2 2 2 2 7
c ---[2417]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2415]---> Adder-cost: 112   maxlim: 7040   bits: 14/13
c ---[2413]---> Adder-cost: 112   maxlim: 7296   bits: 14/13
c ---[2411]---> Adder-cost: 104   maxlim: 6400   bits: 14/13
c ---[2409]---> Adder-cost: 112   maxlim: 7936   bits: 14/13
c ---[2407]---> Adder-cost: 158   maxlim: 9856   bits: 15/14
c ---[2405]---> Adder-cost: 144   maxlim: 9728   bits: 15/14
c ---[2403]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[2401]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[2399]---> Adder-cost: 118   maxlim: 7424   bits: 14/13
c ---[2397]---> Adder-cost: 126   maxlim: 8448   bits: 15/14
c ---[2395]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[2393]---> Adder-cost: 158   maxlim: 9856   bits: 15/14
c ---[2391]---> Adder-cost: 104   maxlim: 9984   bits: 15/14
c ---[2389]---> Adder-cost: 174   maxlim: 11008   bits: 15/14
c ---[2387]---> Adder-cost: 68   maxlim: 11008   bits: 15/14
c ---[2385]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2383]---> Sorter-cost:  888     Base: 2 2 2 2 2 2 2 7
c ---[2381]---> Adder-cost: 110   maxlim: 6912   bits: 14/13
c ---[2379]---> Adder-cost: 132   maxlim: 8192   bits: 15/14
c ---[2377]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[2375]---> Adder-cost: 68   maxlim: 4736   bits: 14/13
c ---[2373]---> Adder-cost: 322   maxlim: 20736   bits: 16/15
c ---[2371]---> Adder-cost: 74   maxlim: 4352   bits: 14/13
c ---[2369]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[2367]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[2365]---> Sorter-cost:  543     Base: 2 2 2 2 2 2 2 7
c ---[2363]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 7
c ---[2361]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[2359]---> Sorter-cost:  368     Base: 2 2 2 2 2 2 2 7
c ---[2357]---> Sorter-cost:  254     Base: 2 2 2 2 2 2 2 2
c ---[2355]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[2353]---> Adder-cost: 104   maxlim: 6144   bits: 14/13
c ---[2351]---> Adder-cost: 102   maxlim: 20736   bits: 16/15
c ---[2349]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[2347]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[2345]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[2343]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[2341]---> Adder-cost: 110   maxlim: 6656   bits: 14/13
c ---[2339]---> Adder-cost: 112   maxlim: 7168   bits: 14/13
c ---[2337]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[2335]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[2333]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[2331]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 7
c ---[2329]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[2327]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[2325]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[2323]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[2321]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[2319]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[2317]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[2315]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[2313]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[2311]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[2309]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[2307]---> Adder-cost: 70   maxlim: 4864   bits: 14/13
c ---[2305]---> Sorter-cost:  784     Base: 2 2 2 2 2 2 2 7
c ---[2303]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[2301]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 7
c ---[2299]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 7
c ---[2297]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 7
c ---[2295]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[2293]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[2291]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[2289]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[2287]---> Adder-cost: 70   maxlim: 4352   bits: 14/13
c ---[2285]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[2283]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[2281]---> Sorter-cost:  983     Base: 2 2 2 2 2 2 2 7
c ---[2279]---> Sorter-cost:  608     Base: 2 2 2 2 2 2 2 7
c ---[2277]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[2275]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[2273]---> Sorter-cost:  574     Base: 2 2 2 2 2 2 2 7
c ---[2271]---> Sorter-cost:  457     Base: 2 2 2 2 2 2 2 7
c ---[2269]---> Adder-cost: 102   maxlim: 20736   bits: 16/15
c ---[2267]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 7
c ---[2265]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[2263]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[2261]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[2259]---> Adder-cost: 92   maxlim: 6784   bits: 14/13
c ---[2257]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[2255]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2253]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 7
c ---[2251]---> Sorter-cost: 1021     Base: 2 2 2 2 2 2 2 7
c ---[2249]---> Adder-cost: 270   maxlim: 18176   bits: 16/15
c ---[2247]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[2245]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[2243]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[2241]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2
c ---[2239]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[2237]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2235]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[2233]---> Adder-cost: 78   maxlim: 4992   bits: 14/13
c ---[2231]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 7
c ---[2229]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[2227]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[2225]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[2223]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[2221]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[2219]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[2217]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[2215]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[2213]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[2211]---> Adder-cost: 46   maxlim: 6784   bits: 14/13
c ---[2209]---> Adder-cost: 126   maxlim: 7936   bits: 14/13
c ---[2207]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[2205]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[2203]---> Adder-cost: 122   maxlim: 7680   bits: 14/13
c ---[2201]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[2199]---> Adder-cost: 140   maxlim: 8320   bits: 15/14
c ---[2197]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[2195]---> Adder-cost: 106   maxlim: 6912   bits: 14/13
c ---[2193]---> Adder-cost: 48   maxlim: 6912   bits: 14/13
c ---[2191]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[2189]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[2187]---> Adder-cost: 88   maxlim: 6016   bits: 14/13
c ---[2185]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[2183]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[2181]---> Adder-cost: 116   maxlim: 7296   bits: 14/13
c ---[2179]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[2177]---> Adder-cost: 146   maxlim: 8960   bits: 15/14
c ---[2175]---> Adder-cost: 60   maxlim: 8960   bits: 15/14
c ---[2173]---> Adder-cost: 172   maxlim: 10496   bits: 15/14
c ---[2171]---> Adder-cost: 68   maxlim: 10496   bits: 15/14
c ---[2169]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[2167]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2165]---> Adder-cost: 106   maxlim: 6400   bits: 14/13
c ---[2163]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[2161]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[2159]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[2157]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[2155]---> Sorter-cost:  377     Base: 2 2 2 2 2 2 2 7
c ---[2153]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[2151]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[2149]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[2147]---> Sorter-cost:  644     Base: 2 2 2 2 2 2 2 7
c ---[2145]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[2143]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[2141]---> Adder-cost: 104   maxlim: 6912   bits: 14/13
c ---[2139]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[2137]---> Adder-cost: 48   maxlim: 6912   bits: 14/13
c ---[2135]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[2133]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[2131]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[2129]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[2127]---> Adder-cost: 174   maxlim: 10752   bits: 15/14
c ---[2125]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[2123]---> Adder-cost: 88   maxlim: 5376   bits: 14/13
c ---[2121]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[2119]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[2117]---> Adder-cost: 254   maxlim: 17536   bits: 16/15
c ---[2115]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[2113]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[2111]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[2109]---> Adder-cost: 72   maxlim: 4480   bits: 14/13
c ---[2107]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[2105]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[2103]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2101]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2099]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[2097]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[2095]---> Adder-cost: 94   maxlim: 17536   bits: 16/15
c ---[2093]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[2091]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[2089]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[2087]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[2085]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[2083]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[2081]---> Adder-cost: 86   maxlim: 5248   bits: 14/13
c ---[2079]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[2077]---> Adder-cost: 124   maxlim: 7680   bits: 14/13
c ---[2075]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[2073]---> Adder-cost: 94   maxlim: 17536   bits: 16/15
c ---[2071]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[2069]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[2067]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[2065]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[2063]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[2061]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[2059]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 7
c ---[2057]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[2055]---> Adder-cost: 160   maxlim: 9984   bits: 15/14
c ---[2053]---> Adder-cost: 98   maxlim: 10752   bits: 15/14
c ---[2051]---> Adder-cost: 94   maxlim: 17536   bits: 16/15
c ---[2049]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[2047]---> Adder-cost: 104   maxlim: 6528   bits: 14/13
c ---[2045]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[2043]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[2041]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2039]---> Adder-cost: 154   maxlim: 9600   bits: 15/14
c ---[2037]---> Adder-cost: 62   maxlim: 9600   bits: 15/14
c ---[2035]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[2033]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[2031]---> Adder-cost: 138   maxlim: 8320   bits: 15/14
c ---[2029]---> Adder-cost: 94   maxlim: 17536   bits: 16/15
c ---[2027]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[2025]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[2023]---> Adder-cost: 46   maxlim: 6784   bits: 14/13
c ---[2021]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[2019]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[2017]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[2015]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[2013]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[2011]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[2009]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[2007]---> Adder-cost: 94   maxlim: 17536   bits: 16/15
c ---[2005]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[2003]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[2001]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[1999]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[1997]---> Adder-cost: 86   maxlim: 5376   bits: 14/13
c ---[1995]---> Adder-cost: 88   maxlim: 5632   bits: 14/13
c ---[1993]---> Adder-cost: 102   maxlim: 6272   bits: 14/13
c ---[1991]---> Adder-cost: 86   maxlim: 6912   bits: 14/13
c ---[1989]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[1987]---> Adder-cost: 88   maxlim: 6656   bits: 14/13
c ---[1985]---> Adder-cost: 264   maxlim: 18176   bits: 16/15
c ---[1983]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 7
c ---[1981]---> Sorter-cost:  264     Base: 2 2 2 2 2 2 2 2
c ---[1979]---> Sorter-cost:  260     Base: 2 2 2 2 2 2 2 2
c ---[1977]---> Adder-cost: 104   maxlim: 6400   bits: 14/13
c ---[1975]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[1973]---> Adder-cost: 78   maxlim: 4992   bits: 14/13
c ---[1971]---> Adder-cost: 76   maxlim: 4736   bits: 14/13
c ---[1969]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[1967]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[1965]---> Adder-cost: 84   maxlim: 5504   bits: 14/13
c ---[1963]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[1961]---> Sorter-cost:  705     Base: 2 2 2 2 2 2 2 7
c ---[1959]---> Sorter-cost: 1078     Base: 2 2 2 2 2 2 2 7
c ---[1957]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 7
c ---[1955]---> Sorter-cost:  728     Base: 2 2 2 2 2 2 2 7
c ---[1953]---> Sorter-cost:  582     Base: 2 2 2 2 2 2 2 7
c ---[1951]---> Sorter-cost:  579     Base: 2 2 2 2 2 2 2 7
c ---[1949]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[1947]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[1945]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1943]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[1941]---> Sorter-cost: 1046     Base: 2 2 2 2 2 2 2 7
c ---[1939]---> Sorter-cost:  668     Base: 2 2 2 2 2 2 2 7
c ---[1937]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[1935]---> Adder-cost: 102   maxlim: 6144   bits: 14/13
c ---[1933]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[1931]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[1929]---> Adder-cost: 110   maxlim: 6656   bits: 14/13
c ---[1927]---> Adder-cost: 116   maxlim: 7296   bits: 14/13
c ---[1925]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[1923]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[1921]---> Adder-cost: 82   maxlim: 5120   bits: 14/13
c ---[1919]---> Adder-cost: 84   maxlim: 5376   bits: 14/13
c ---[1917]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[1915]---> Adder-cost: 78   maxlim: 4736   bits: 14/13
c ---[1913]---> Sorter-cost:  994     Base: 2 2 2 2 2 2 2 7
c ---[1911]---> Adder-cost: 118   maxlim: 7168   bits: 14/13
c ---[1909]---> Adder-cost: 100   maxlim: 6400   bits: 14/13
c ---[1907]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[1905]---> Adder-cost: 80   maxlim: 5120   bits: 14/13
c ---[1903]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[1901]---> Adder-cost: 106   maxlim: 6528   bits: 14/13
c ---[1899]---> Adder-cost: 68   maxlim: 5760   bits: 14/13
c ---[1897]---> Sorter-cost:  612     Base: 2 2 2 2 2 2 2 7
c ---[1895]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[1893]---> Sorter-cost:  612     Base: 2 2 2 2 2 2 2 7
c ---[1891]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[1889]---> Sorter-cost:  567     Base: 2 2 2 2 2 2 2 7
c ---[1887]---> Sorter-cost:  339     Base: 2 2 2 2 2 2 2 7
c ---[1885]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[1883]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1881]---> Adder-cost: 88   maxlim: 18176   bits: 16/15
c ---[1879]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[1877]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1875]---> Sorter-cost:  984     Base: 2 2 2 2 2 2 2 7
c ---[1873]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1871]---> Adder-cost: 112   maxlim: 7040   bits: 14/13
c ---[1869]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[1867]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[1865]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[1863]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[1861]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[1859]---> Adder-cost: 160   maxlim: 10624   bits: 15/14
c ---[1857]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[1855]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[1853]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[1851]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[1849]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[1847]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[1845]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[1843]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[1841]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[1839]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[1837]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[1835]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 7
c ---[1833]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1831]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1829]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1827]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1825]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1823]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1821]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1819]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1817]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[1815]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[1813]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[1811]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[1809]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[1807]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[1805]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[1803]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 7
c ---[1801]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1799]---> Adder-cost: 142   maxlim: 8576   bits: 15/14
c ---[1797]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[1795]---> Adder-cost: 92   maxlim: 5632   bits: 14/13
c ---[1793]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[1791]---> Adder-cost: 76   maxlim: 4992   bits: 14/13
c ---[1789]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[1787]---> Adder-cost: 78   maxlim: 4864   bits: 14/13
c ---[1785]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[1783]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[1781]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[1779]---> Adder-cost: 86   maxlim: 5376   bits: 14/13
c ---[1777]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[1775]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[1773]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[1771]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 7
c ---[1769]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[1767]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[1765]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1763]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 7
c ---[1761]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[1759]---> Sorter-cost: 1074     Base: 2 2 2 2 2 2 2 7
c ---[1757]---> Sorter-cost:  668     Base: 2 2 2 2 2 2 2 7
c ---[1755]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[1753]---> Sorter-cost:  994     Base: 2 2 2 2 2 2 2 7
c ---[1751]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1749]---> Sorter-cost:  708     Base: 2 2 2 2 2 2 2 7
c ---[1747]---> Adder-cost: 110   maxlim: 6656   bits: 14/13
c ---[1745]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[1743]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[1741]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[1739]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[1737]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[1735]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[1733]---> Adder-cost: 138   maxlim: 8448   bits: 15/14
c ---[1731]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[1729]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[1727]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[1725]---> Adder-cost: 110   maxlim: 6656   bits: 14/13
c ---[1723]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[1721]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[1719]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[1717]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[1715]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[1713]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[1711]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[1709]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[1707]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[1705]---> Adder-cost: 74   maxlim: 4480   bits: 14/13
c ---[1703]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[1701]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1699]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1697]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[1695]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[1693]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[1691]---> Sorter-cost:  331     Base: 2 2 2 2 2 2 2 7
c ---[1689]---> Sorter-cost:  657     Base: 2 2 2 2 2 2 2 7
c ---[1687]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[1685]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[1683]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[1681]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1679]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[1677]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[1675]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[1673]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[1671]---> Adder-cost: 124   maxlim: 7808   bits: 14/13
c ---[1669]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[1667]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1665]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1663]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1661]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1659]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1657]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[1655]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[1653]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[1651]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[1649]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[1647]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[1645]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1643]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1641]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[1639]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[1637]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[1635]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1633]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1631]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1629]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[1627]---> Sorter-cost:  262     Base: 2 2 2 2 2 2 2 2
c ---[1625]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1623]---> Sorter-cost:  360     Base: 2 2 2 2 2 2 2 7
c ---[1621]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1619]---> Adder-cost: 124   maxlim: 7936   bits: 14/13
c ---[1617]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[1615]---> Adder-cost: 136   maxlim: 8192   bits: 15/14
c ---[1613]---> Adder-cost: 62   maxlim: 8192   bits: 15/14
c ---[1611]---> Adder-cost: 102   maxlim: 6144   bits: 14/13
c ---[1609]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[1607]---> Adder-cost: 116   maxlim: 7424   bits: 14/13
c ---[1605]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[1603]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[1601]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[1599]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[1597]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 7
c ---[1595]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1593]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[1591]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[1589]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[1587]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[1585]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[1583]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1581]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1579]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[1577]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[1575]---> Sorter-cost:  302     Base: 2 2 2 2 2 2 2 2
c ---[1573]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1571]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 7
c ---[1569]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[1567]---> Sorter-cost:  256     Base: 2 2 2 2 2 2 2 2
c ---[1565]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1563]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[1561]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1559]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1557]---> Adder-cost: 106   maxlim: 6656   bits: 14/13
c ---[1555]---> Adder-cost: 82   maxlim: 6144   bits: 14/13
c ---[1553]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[1551]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[1549]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 7
c ---[1547]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[1545]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[1543]---> Adder-cost: 106   maxlim: 6528   bits: 14/13
c ---[1541]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[1539]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[1537]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[1535]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[1533]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[1531]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[1529]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1527]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1525]---> Sorter-cost:  324     Base: 2 2 2 2 2 2 2 7
c ---[1523]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1521]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1519]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[1517]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1515]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[1513]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[1511]---> Sorter-cost:  523     Base: 2 2 2 2 2 2 2 7
c ---[1509]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[1507]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[1505]---> Sorter-cost:  352     Base: 2 2 2 2 2 2 2 7
c ---[1503]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1501]---> Adder-cost: 110   maxlim: 6656   bits: 14/13
c ---[1499]---> Adder-cost: 90   maxlim: 6016   bits: 14/13
c ---[1497]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[1495]---> Adder-cost: 100   maxlim: 7040   bits: 14/13
c ---[1493]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[1491]---> Adder-cost: 110   maxlim: 6656   bits: 14/13
c ---[1489]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[1487]---> Adder-cost: 96   maxlim: 6272   bits: 14/13
c ---[1485]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[1483]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[1481]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1479]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1477]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[1475]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[1473]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[1471]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 7
c ---[1469]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[1467]---> Adder-cost: 126   maxlim: 7936   bits: 14/13
c ---[1465]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[1463]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1461]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 7
c ---[1459]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[1457]---> Adder-cost: 146   maxlim: 8704   bits: 15/14
c ---[1455]---> Adder-cost: 118   maxlim: 7680   bits: 14/13
c ---[1453]---> Adder-cost: 104   maxlim: 7680   bits: 14/13
c ---[1451]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[1449]---> Sorter-cost:  784     Base: 2 2 2 2 2 2 2 7
c ---[1447]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[1445]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[1443]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1441]---> Sorter-cost:  580     Base: 2 2 2 2 2 2 2 7
c ---[1439]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[1437]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1435]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1433]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[1431]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[1429]---> Sorter-cost:  734     Base: 2 2 2 2 2 2 2 7
c ---[1427]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[1425]---> Adder-cost: 112   maxlim: 7168   bits: 14/13
c ---[1423]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[1421]---> Adder-cost: 98   maxlim: 6400   bits: 14/13
c ---[1419]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[1417]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[1415]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[1413]---> Adder-cost: 104   maxlim: 7040   bits: 14/13
c ---[1411]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[1409]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[1407]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[1405]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[1403]---> Sorter-cost:  582     Base: 2 2 2 2 2 2 2 7
c ---[1401]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1399]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 7
c ---[1397]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[1395]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 7
c ---[1393]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[1391]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[1389]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[1387]---> Adder-cost: 56   maxlim: 5248   bits: 14/13
c ---[1385]---> Adder-cost: 106   maxlim: 6400   bits: 14/13
c ---[1383]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[1381]---> Adder-cost: 90   maxlim: 5760   bits: 14/13
c ---[1379]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[1377]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[1375]---> Adder-cost: 224   maxlim: 15744   bits: 15/14
c ---[1373]---> Adder-cost: 78   maxlim: 15744   bits: 15/14
c ---[1371]---> Adder-cost: 78   maxlim: 15744   bits: 15/14
c ---[1369]---> Adder-cost: 238   maxlim: 16128   bits: 15/14
c ---[1367]---> Adder-cost: 76   maxlim: 16128   bits: 15/14
c ---[1365]---> Adder-cost: 76   maxlim: 16128   bits: 15/14
c ---[1363]---> Adder-cost: 156   maxlim: 11648   bits: 15/14
c ---[1361]---> Adder-cost: 64   maxlim: 11648   bits: 15/14
c ---[1359]---> Adder-cost: 64   maxlim: 11648   bits: 15/14
c ---[1357]---> Adder-cost: 310   maxlim: 20352   bits: 16/15
c ---[1355]---> Adder-cost: 92   maxlim: 20352   bits: 16/15
c ---[1353]---> Adder-cost: 11926   maxlim: 752895   bits: 21/20
c ---[1350]---> Adder-cost: 3128   maxlim: 223616   bits: 19/18
c ---[1348]---> Adder-cost: 37768   maxlim: 11262207   bits: 25/24
c ---[1347]---> Adder-cost: 1201   maxlim: 717439   bits: 21/20
c ---[1346]---> Adder-cost: 19955   maxlim: 9306751   bits: 25/24
c ---[1345]---> Adder-cost: 1593   maxlim: 542847   bits: 21/20
c ---[1344]---> Adder-cost: 7486   maxlim: 695167   bits: 21/20
c ---[1342]---> Adder-cost: 92   maxlim: 20352   bits: 16/15
c ---[1340]---> Adder-cost: 202   maxlim: 15104   bits: 15/14
c ---[1338]---> Adder-cost: 80   maxlim: 15104   bits: 15/14
c ---[1336]---> Adder-cost: 80   maxlim: 15104   bits: 15/14
c ---[1334]---> Adder-cost: 146   maxlim: 9728   bits: 15/14
c ---[1332]---> Adder-cost: 64   maxlim: 9728   bits: 15/14
c ---[1330]---> Adder-cost: 64   maxlim: 9728   bits: 15/14
c ---[1328]---> Sorter-cost:  635     Base: 2 2 2 2 2 2 2 7
c ---[1326]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[1324]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[1322]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[1320]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[1318]---> Sorter-cost:  401     Base: 2 2 2 2 2 2 2 7
c ---[1316]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[1314]---> Adder-cost: 102   maxlim: 6272   bits: 14/13
c ---[1312]---> Adder-cost: 90   maxlim: 5632   bits: 14/13
c ---[1310]---> Adder-cost: 98   maxlim: 6528   bits: 14/13
c ---[1308]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[1306]---> Adder-cost: 138   maxlim: 8960   bits: 15/14
c ---[1304]---> Adder-cost: 60   maxlim: 8960   bits: 15/14
c ---[1302]---> Adder-cost: 92   maxlim: 6784   bits: 14/13
c ---[1300]---> Adder-cost: 46   maxlim: 6784   bits: 14/13
c ---[1298]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1296]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[1294]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[1292]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[1290]---> Adder-cost: 140   maxlim: 8320   bits: 15/14
c ---[1288]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[1286]---> Adder-cost: 106   maxlim: 7168   bits: 14/13
c ---[1284]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[1282]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[1280]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[1278]---> Adder-cost: 86   maxlim: 5888   bits: 14/13
c ---[1276]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[1274]---> Adder-cost: 148   maxlim: 8960   bits: 15/14
c ---[1272]---> Adder-cost: 60   maxlim: 8960   bits: 15/14
c ---[1270]---> Adder-cost: 142   maxlim: 9088   bits: 15/14
c ---[1268]---> Adder-cost: 56   maxlim: 9088   bits: 15/14
c ---[1266]---> Adder-cost: 92   maxlim: 6016   bits: 14/13
c ---[1264]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[1262]---> Adder-cost: 82   maxlim: 5504   bits: 14/13
c ---[1260]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[1258]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 7
c ---[1256]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[1254]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[1252]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1250]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[1248]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1246]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1244]---> Adder-cost: 102   maxlim: 6144   bits: 14/13
c ---[1242]---> Adder-cost: 92   maxlim: 6016   bits: 14/13
c ---[1240]---> Adder-cost: 140   maxlim: 8320   bits: 15/14
c ---[1238]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[1236]---> Adder-cost: 150   maxlim: 9856   bits: 15/14
c ---[1234]---> Adder-cost: 138   maxlim: 9472   bits: 15/14
c ---[1232]---> Adder-cost: 76   maxlim: 4736   bits: 14/13
c ---[1230]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[1228]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[1226]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[1224]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[1222]---> Sorter-cost:  654     Base: 2 2 2 2 2 2 2 7
c ---[1220]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1218]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1216]---> Adder-cost: 240   maxlim: 17408   bits: 16/15
c ---[1214]---> Adder-cost: 94   maxlim: 17408   bits: 16/15
c ---[1212]---> Adder-cost: 94   maxlim: 17408   bits: 16/15
c ---[1210]---> Adder-cost: 322   maxlim: 23296   bits: 16/15
c ---[1208]---> Adder-cost: 106   maxlim: 23296   bits: 16/15
c ---[1206]---> Adder-cost: 106   maxlim: 23296   bits: 16/15
c ---[1204]---> Adder-cost: 290   maxlim: 21120   bits: 16/15
c ---[1202]---> Adder-cost: 100   maxlim: 21120   bits: 16/15
c ---[1200]---> Adder-cost: 100   maxlim: 21120   bits: 16/15
c ---[1198]---> Adder-cost: 274   maxlim: 20224   bits: 16/15
c ---[1196]---> Adder-cost: 92   maxlim: 20224   bits: 16/15
c ---[1194]---> Adder-cost: 92   maxlim: 20224   bits: 16/15
c ---[1192]---> Adder-cost: 92   maxlim: 20224   bits: 16/15
c ---[1190]---> Adder-cost: 92   maxlim: 20224   bits: 16/15
c ---[1188]---> Adder-cost: 92   maxlim: 20224   bits: 16/15
c ---[1186]---> Adder-cost: 214   maxlim: 15360   bits: 15/14
c ---[1184]---> Adder-cost: 80   maxlim: 15360   bits: 15/14
c ---[1182]---> Adder-cost: 80   maxlim: 15360   bits: 15/14
c ---[1180]---> Adder-cost: 80   maxlim: 15360   bits: 15/14
c ---[1178]---> Adder-cost: 80   maxlim: 15360   bits: 15/14
c ---[1176]---> Adder-cost: 80   maxlim: 15360   bits: 15/14
c ---[1174]---> Adder-cost: 166   maxlim: 11520   bits: 15/14
c ---[1172]---> Adder-cost: 66   maxlim: 11520   bits: 15/14
c ---[1170]---> Adder-cost: 66   maxlim: 11520   bits: 15/14
c ---[1168]---> Adder-cost: 66   maxlim: 11520   bits: 15/14
c ---[1166]---> Adder-cost: 66   maxlim: 11520   bits: 15/14
c ---[1164]---> Adder-cost: 66   maxlim: 11520   bits: 15/14
c ---[1162]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1160]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1158]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1156]---> Sorter-cost:  302     Base: 2 2 2 2 2 2 2 2
c ---[1154]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[1152]---> Sorter-cost:  453     Base: 2 2 2 2 2 2 2 7
c ---[1150]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[1148]---> Adder-cost: 112   maxlim: 7168   bits: 14/13
c ---[1146]---> Adder-cost: 76   maxlim: 6016   bits: 14/13
c ---[1144]---> Adder-cost: 98   maxlim: 7168   bits: 14/13
c ---[1142]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[1140]---> Adder-cost: 116   maxlim: 7296   bits: 14/13
c ---[1138]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[1136]---> Adder-cost: 78   maxlim: 5120   bits: 14/13
c ---[1134]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[1132]---> Sorter-cost:  258     Base: 2 2 2 2 2 2 2 2
c ---[1130]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[1128]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1126]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1124]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1122]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[1120]---> Sorter-cost:  978     Base: 2 2 2 2 2 2 2 7
c ---[1118]---> Sorter-cost:  596     Base: 2 2 2 2 2 2 2 7
c ---[1116]---> Adder-cost: 134   maxlim: 8192   bits: 15/14
c ---[1114]---> Adder-cost: 62   maxlim: 8192   bits: 15/14
c ---[1112]---> Adder-cost: 118   maxlim: 7936   bits: 14/13
c ---[1110]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[1108]---> Sorter-cost:  784     Base: 2 2 2 2 2 2 2 7
c ---[1106]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[1104]---> Adder-cost: 94   maxlim: 6016   bits: 14/13
c ---[1102]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[1100]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[1098]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[1096]---> Sorter-cost:  569     Base: 2 2 2 2 2 2 2 7
c ---[1094]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[1092]---> Sorter-cost:  730     Base: 2 2 2 2 2 2 2 7
c ---[1090]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[1088]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[1086]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[1084]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 7
c ---[1082]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[1080]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[1078]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 7
c ---[1076]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[1074]---> Adder-cost: 94   maxlim: 5888   bits: 14/13
c ---[1072]---> Adder-cost: 76   maxlim: 5248   bits: 14/13
c ---[1070]---> Adder-cost: 96   maxlim: 6656   bits: 14/13
c ---[1068]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[1066]---> Adder-cost: 86   maxlim: 5760   bits: 14/13
c ---[1064]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[1062]---> Adder-cost: 82   maxlim: 5120   bits: 14/13
c ---[1060]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[1058]---> Adder-cost: 148   maxlim: 9344   bits: 15/14
c ---[1056]---> Adder-cost: 60   maxlim: 9344   bits: 15/14
c ---[1054]---> Adder-cost: 60   maxlim: 9344   bits: 15/14
c ---[1052]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[1050]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[1048]---> Adder-cost: 76   maxlim: 6784   bits: 14/13
c ---[1046]---> Adder-cost: 46   maxlim: 6784   bits: 14/13
c ---[1044]---> Adder-cost: 138   maxlim: 8448   bits: 15/14
c ---[1042]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[1040]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[1038]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[1036]---> Adder-cost: 92   maxlim: 6016   bits: 14/13
c ---[1034]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[1032]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 7
c ---[1030]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1028]---> Sorter-cost:  435     Base: 2 2 2 2 2 2 2 7
c ---[1026]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[1024]---> Sorter-cost:  453     Base: 2 2 2 2 2 2 2 7
c ---[1022]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[1020]---> Sorter-cost:  392     Base: 2 2 2 2 2 2 2 7
c ---[1018]---> Sorter-cost:  732     Base: 2 2 2 2 2 2 2 7
c ---[1016]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[1014]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[1012]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[1010]---> Sorter-cost:  930     Base: 2 2 2 2 2 2 2 7
c ---[1008]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[1006]---> Adder-cost: 46   maxlim: 6784   bits: 14/13
c ---[1004]---> Adder-cost: 136   maxlim: 8576   bits: 15/14
c ---[1002]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[1000]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 7
c ---[ 998]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[ 996]---> Adder-cost: 122   maxlim: 7680   bits: 14/13
c ---[ 994]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[ 992]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[ 990]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[ 988]---> Sorter-cost:  582     Base: 2 2 2 2 2 2 2 7
c ---[ 986]---> Sorter-cost:  647     Base: 2 2 2 2 2 2 2 7
c ---[ 984]---> Adder-cost: 82   maxlim: 5248   bits: 14/13
c ---[ 982]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[ 980]---> Adder-cost: 102   maxlim: 6528   bits: 14/13
c ---[ 978]---> Adder-cost: 92   maxlim: 6016   bits: 14/13
c ---[ 976]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[ 974]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[ 972]---> Sorter-cost:  687     Base: 2 2 2 2 2 2 2 7
c ---[ 970]---> Sorter-cost:  527     Base: 2 2 2 2 2 2 2 7
c ---[ 968]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 7
c ---[ 966]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[ 964]---> Adder-cost: 80   maxlim: 4864   bits: 14/13
c ---[ 962]---> Sorter-cost:  994     Base: 2 2 2 2 2 2 2 7
c ---[ 960]---> Sorter-cost:  940     Base: 2 2 2 2 2 2 2 7
c ---[ 958]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[ 956]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[ 954]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[ 952]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[ 950]---> Adder-cost: 92   maxlim: 5632   bits: 14/13
c ---[ 948]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[ 946]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[ 944]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[ 942]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[ 940]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 938]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[ 936]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[ 934]---> Adder-cost: 110   maxlim: 7424   bits: 14/13
c ---[ 932]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[ 930]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[ 928]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[ 926]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[ 924]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[ 922]---> Sorter-cost:  697     Base: 2 2 2 2 2 2 2 7
c ---[ 920]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[ 918]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[ 916]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[ 914]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 7
c ---[ 912]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[ 910]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[ 908]---> Adder-cost: 74   maxlim: 4480   bits: 14/13
c ---[ 906]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[ 904]---> Adder-cost: 86   maxlim: 5120   bits: 14/13
c ---[ 902]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[ 900]---> Adder-cost: 102   maxlim: 6144   bits: 14/13
c ---[ 898]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[ 896]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[ 894]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[ 892]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[ 890]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[ 888]---> Adder-cost: 108   maxlim: 6656   bits: 14/13
c ---[ 886]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[ 884]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[ 882]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[ 880]---> Sorter-cost:  734     Base: 2 2 2 2 2 2 2 7
c ---[ 878]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[ 876]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 7
c ---[ 874]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[ 872]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[ 870]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[ 868]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 7
c ---[ 866]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[ 864]---> Sorter-cost:  543     Base: 2 2 2 2 2 2 2 7
c ---[ 862]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[ 860]---> Adder-cost: 106   maxlim: 6656   bits: 14/13
c ---[ 858]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[ 856]---> Adder-cost: 102   maxlim: 7040   bits: 14/13
c ---[ 854]---> Adder-cost: 94   maxlim: 6016   bits: 14/13
c ---[ 852]---> Adder-cost: 166   maxlim: 10368   bits: 15/14
c ---[ 850]---> Adder-cost: 174   maxlim: 11008   bits: 15/14
c ---[ 848]---> Sorter-cost:  784     Base: 2 2 2 2 2 2 2 7
c ---[ 846]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[ 844]---> Sorter-cost:  689     Base: 2 2 2 2 2 2 2 7
c ---[ 842]---> Sorter-cost:  463     Base: 2 2 2 2 2 2 2 7
c ---[ 840]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[ 838]---> Sorter-cost:  638     Base: 2 2 2 2 2 2 2 7
c ---[ 836]---> Adder-cost: 112   maxlim: 7040   bits: 14/13
c ---[ 834]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[ 832]---> Adder-cost: 96   maxlim: 6272   bits: 14/13
c ---[ 830]---> Adder-cost: 88   maxlim: 6144   bits: 14/13
c ---[ 828]---> Adder-cost: 104   maxlim: 6144   bits: 14/13
c ---[ 826]---> Adder-cost: 92   maxlim: 6016   bits: 14/13
c ---[ 824]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[ 822]---> Sorter-cost:  776     Base: 2 2 2 2 2 2 2 7
c ---[ 820]---> Sorter-cost:  992     Base: 2 2 2 2 2 2 2 7
c ---[ 818]---> Sorter-cost:  744     Base: 2 2 2 2 2 2 2 7
c ---[ 816]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 7
c ---[ 814]---> Sorter-cost:  878     Base: 2 2 2 2 2 2 2 7
c ---[ 812]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[ 810]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[ 808]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 7
c ---[ 806]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 7
c ---[ 804]---> Sorter-cost:  402     Base: 2 2 2 2 2 2 2 7
c ---[ 802]---> Adder-cost: 90   maxlim: 6016   bits: 14/13
c ---[ 800]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[ 798]---> Adder-cost: 106   maxlim: 6656   bits: 14/13
c ---[ 796]---> Sorter-cost:  734     Base: 2 2 2 2 2 2 2 7
c ---[ 794]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[ 792]---> Sorter-cost:  571     Base: 2 2 2 2 2 2 2 7
c ---[ 790]---> Sorter-cost:  784     Base: 2 2 2 2 2 2 2 7
c ---[ 788]---> Adder-cost: 94   maxlim: 6016   bits: 14/13
c ---[ 786]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[ 784]---> Sorter-cost:  421     Base: 2 2 2 2 2 2 2 7
c ---[ 782]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 7
c ---[ 780]---> Adder-cost: 124   maxlim: 7936   bits: 14/13
c ---[ 778]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[ 776]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[ 774]---> Sorter-cost:  643     Base: 2 2 2 2 2 2 2 7
c ---[ 772]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 7
c ---[ 770]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[ 768]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[ 766]---> Adder-cost: 74   maxlim: 4992   bits: 14/13
c ---[ 764]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 7
c ---[ 762]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[ 760]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[ 758]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[ 756]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 7
c ---[ 754]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[ 752]---> Sorter-cost:  966     Base: 2 2 2 2 2 2 2 7
c ---[ 750]---> Sorter-cost:  646     Base: 2 2 2 2 2 2 2 7
c ---[ 748]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[ 746]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[ 744]---> Sorter-cost:  366     Base: 2 2 2 2 2 2 2 7
c ---[ 742]---> Adder-cost: 130   maxlim: 8448   bits: 15/14
c ---[ 740]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[ 738]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[ 736]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[ 734]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[ 732]---> Adder-cost: 100   maxlim: 6144   bits: 14/13
c ---[ 730]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[ 728]---> Adder-cost: 88   maxlim: 5376   bits: 14/13
c ---[ 726]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[ 724]---> Adder-cost: 90   maxlim: 5760   bits: 14/13
c ---[ 722]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[ 720]---> Adder-cost: 88   maxlim: 5632   bits: 14/13
c ---[ 718]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[ 716]---> Adder-cost: 148   maxlim: 9472   bits: 15/14
c ---[ 714]---> Adder-cost: 64   maxlim: 9472   bits: 15/14
c ---[ 712]---> Adder-cost: 156   maxlim: 9856   bits: 15/14
c ---[ 710]---> Adder-cost: 60   maxlim: 9856   bits: 15/14
c ---[ 708]---> Adder-cost: 74   maxlim: 4352   bits: 14/13
c ---[ 706]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[ 704]---> Adder-cost: 94   maxlim: 6144   bits: 14/13
c ---[ 702]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[ 700]---> Adder-cost: 104   maxlim: 7680   bits: 14/13
c ---[ 698]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[ 696]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[ 694]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[ 692]---> Adder-cost: 92   maxlim: 6016   bits: 14/13
c ---[ 690]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[ 688]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[ 686]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[ 684]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[ 682]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[ 680]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 7
c ---[ 678]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[ 676]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 7
c ---[ 674]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[ 672]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[ 670]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 668]---> Sorter-cost:  932     Base: 2 2 2 2 2 2 2 7
c ---[ 666]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[ 664]---> Sorter-cost:  683     Base: 2 2 2 2 2 2 2 7
c ---[ 662]---> Sorter-cost:  556     Base: 2 2 2 2 2 2 2 7
c ---[ 660]---> Adder-cost: 174   maxlim: 11392   bits: 15/14
c ---[ 658]---> Adder-cost: 72   maxlim: 11392   bits: 15/14
c ---[ 656]---> Adder-cost: 184   maxlim: 12672   bits: 15/14
c ---[ 654]---> Adder-cost: 342   maxlim: 24832   bits: 16/15
c ---[ 652]---> Adder-cost: 116   maxlim: 24832   bits: 16/15
c ---[ 650]---> Adder-cost: 326   maxlim: 23936   bits: 16/15
c ---[ 648]---> Adder-cost: 104   maxlim: 23936   bits: 16/15
c ---[ 646]---> Adder-cost: 334   maxlim: 24832   bits: 16/15
c ---[ 644]---> Adder-cost: 116   maxlim: 24832   bits: 16/15
c ---[ 642]---> Adder-cost: 350   maxlim: 29696   bits: 16/15
c ---[ 640]---> Adder-cost: 128   maxlim: 29696   bits: 16/15
c ---[ 638]---> Adder-cost: 350   maxlim: 24448   bits: 16/15
c ---[ 636]---> Adder-cost: 108   maxlim: 24448   bits: 16/15
c ---[ 634]---> Adder-cost: 314   maxlim: 24704   bits: 16/15
c ---[ 632]---> Adder-cost: 330   maxlim: 24576   bits: 16/15
c ---[ 630]---> Adder-cost: 518   maxlim: 37120   bits: 17/16
c ---[ 628]---> Adder-cost: 510   maxlim: 36608   bits: 17/16
c ---[ 626]---> Adder-cost: 386   maxlim: 28288   bits: 16/15
c ---[ 624]---> Adder-cost: 494   maxlim: 36480   bits: 17/16
c ---[ 622]---> Adder-cost: 426   maxlim: 31616   bits: 16/15
c ---[ 620]---> Adder-cost: 434   maxlim: 32384   bits: 16/15
c ---[ 618]---> Adder-cost: 390   maxlim: 29184   bits: 16/15
c ---[ 616]---> Adder-cost: 320   maxlim: 25088   bits: 16/15
c ---[ 614]---> Adder-cost: 344   maxlim: 25216   bits: 16/15
c ---[ 612]---> Adder-cost: 114   maxlim: 25216   bits: 16/15
c ---[ 610]---> Adder-cost: 431   maxlim: 33280   bits: 17/16
c ---[ 608]---> Adder-cost: 142   maxlim: 33280   bits: 17/16
c ---[ 606]---> Adder-cost: 398   maxlim: 32384   bits: 16/15
c ---[ 604]---> Adder-cost: 124   maxlim: 32384   bits: 16/15
c ---[ 602]---> Adder-cost: 358   maxlim: 27008   bits: 16/15
c ---[ 600]---> Adder-cost: 116   maxlim: 27008   bits: 16/15
c ---[ 598]---> Adder-cost: 248   maxlim: 18688   bits: 16/15
c ---[ 596]---> Adder-cost: 92   maxlim: 18688   bits: 16/15
c ---[ 594]---> Adder-cost: 92   maxlim: 18688   bits: 16/15
c ---[ 592]---> Adder-cost: 92   maxlim: 18688   bits: 16/15
c ---[ 590]---> Adder-cost: 160   maxlim: 11264   bits: 15/14
c ---[ 588]---> Adder-cost: 72   maxlim: 11264   bits: 15/14
c ---[ 586]---> Adder-cost: 138   maxlim: 10624   bits: 15/14
c ---[ 584]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[ 582]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[ 580]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[ 578]---> Adder-cost: 104   maxlim: 9728   bits: 15/14
c ---[ 576]---> Adder-cost: 64   maxlim: 9728   bits: 15/14
c ---[ 574]---> Adder-cost: 64   maxlim: 9728   bits: 15/14
c ---[ 572]---> Adder-cost: 64   maxlim: 9728   bits: 15/14
c ---[ 570]---> Adder-cost: 104   maxlim: 7808   bits: 14/13
c ---[ 568]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[ 566]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[ 564]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[ 562]---> Adder-cost: 68   maxlim: 4736   bits: 14/13
c ---[ 560]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[ 558]---> Adder-cost: 62   maxlim: 4352   bits: 14/13
c ---[ 556]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[ 554]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[ 552]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[ 550]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[ 548]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[ 546]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[ 544]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[ 542]---> Sorter-cost:  703     Base: 2 2 2 2 2 2 2 7
c ---[ 540]---> Sorter-cost:  710     Base: 2 2 2 2 2 2 2 7
c ---[ 538]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[ 536]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[ 534]---> Sorter-cost:  874     Base: 2 2 2 2 2 2 2 7
c ---[ 532]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[ 530]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[ 528]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[ 526]---> Adder-cost: 108   maxlim: 6656   bits: 14/13
c ---[ 524]---> Adder-cost: 88   maxlim: 5376   bits: 14/13
c ---[ 522]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[ 520]---> Adder-cost: 102   maxlim: 6400   bits: 14/13
c ---[ 518]---> Adder-cost: 98   maxlim: 6784   bits: 14/13
c ---[ 516]---> Adder-cost: 170   maxlim: 10752   bits: 15/14
c ---[ 514]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[ 512]---> Adder-cost: 164   maxlim: 10496   bits: 15/14
c ---[ 510]---> Adder-cost: 144   maxlim: 9984   bits: 15/14
c ---[ 508]---> Adder-cost: 122   maxlim: 7808   bits: 14/13
c ---[ 506]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[ 504]---> Sorter-cost:  264     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:  218     Base: 2 2 2 2 2 2 2 2
c ---[ 498]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[ 496]---> Adder-cost: 76   maxlim: 4864   bits: 14/13
c ---[ 494]---> Adder-cost: 104   maxlim: 6144   bits: 14/13
c ---[ 492]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[ 490]---> Adder-cost: 94   maxlim: 6400   bits: 14/13
c ---[ 488]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[ 486]---> Sorter-cost:  565     Base: 2 2 2 2 2 2 2 7
c ---[ 484]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[ 482]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[ 480]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[ 478]---> Sorter-cost:  651     Base: 2 2 2 2 2 2 2 7
c ---[ 476]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[ 474]---> Sorter-cost:  992     Base: 2 2 2 2 2 2 2 7
c ---[ 472]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[ 470]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[ 468]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[ 466]---> Adder-cost: 102   maxlim: 6528   bits: 14/13
c ---[ 464]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[ 462]---> Adder-cost: 116   maxlim: 7424   bits: 14/13
c ---[ 460]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[ 458]---> Adder-cost: 134   maxlim: 8320   bits: 15/14
c ---[ 456]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[ 454]---> Adder-cost: 99   maxlim: 6144   bits: 14/13
c ---[ 452]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[ 450]---> Adder-cost: 86   maxlim: 5376   bits: 14/13
c ---[ 448]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[ 446]---> Adder-cost: 154   maxlim: 9472   bits: 15/14
c ---[ 444]---> Adder-cost: 64   maxlim: 9472   bits: 15/14
c ---[ 442]---> Adder-cost: 154   maxlim: 10112   bits: 15/14
c ---[ 440]---> Adder-cost: 62   maxlim: 10112   bits: 15/14
c ---[ 438]---> Adder-cost: 140   maxlim: 8192   bits: 15/14
c ---[ 436]---> Adder-cost: 62   maxlim: 8192   bits: 15/14
c ---[ 434]---> Adder-cost: 160   maxlim: 10112   bits: 15/14
c ---[ 432]---> Adder-cost: 62   maxlim: 10112   bits: 15/14
c ---[ 430]---> Sorter-cost:  992     Base: 2 2 2 2 2 2 2 7
c ---[ 428]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[ 426]---> Sorter-cost:  302     Base: 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[ 420]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[ 418]---> Sorter-cost:  984     Base: 2 2 2 2 2 2 2 7
c ---[ 416]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[ 414]---> Sorter-cost:  944     Base: 2 2 2 2 2 2 2 7
c ---[ 412]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[ 410]---> Sorter-cost:  918     Base: 2 2 2 2 2 2 2 7
c ---[ 408]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[ 406]---> Adder-cost: 133   maxlim: 8192   bits: 15/14
c ---[ 404]---> Adder-cost: 62   maxlim: 8192   bits: 15/14
c ---[ 402]---> Adder-cost: 62   maxlim: 8192   bits: 15/14
c ---[ 400]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 7
c ---[ 398]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 396]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 7
c ---[ 394]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[ 392]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[ 390]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[ 388]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[ 386]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[ 384]---> Adder-cost: 110   maxlim: 6656   bits: 14/13
c ---[ 382]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[ 380]---> Adder-cost: 142   maxlim: 8448   bits: 15/14
c ---[ 378]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[ 376]---> Adder-cost: 136   maxlim: 8960   bits: 15/14
c ---[ 374]---> Adder-cost: 60   maxlim: 8960   bits: 15/14
c ---[ 372]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 7
c ---[ 370]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[ 368]---> Sorter-cost:  264     Base: 2 2 2 2 2 2 2 2
c ---[ 366]---> Adder-cost: 112   maxlim: 7936   bits: 14/13
c ---[ 364]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[ 362]---> Adder-cost: 90   maxlim: 6272   bits: 14/13
c ---[ 360]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[ 358]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[ 356]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[ 354]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[ 352]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[ 350]---> Adder-cost: 108   maxlim: 6656   bits: 14/13
c ---[ 348]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[ 346]---> Adder-cost: 116   maxlim: 7168   bits: 14/13
c ---[ 344]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[ 342]---> Adder-cost: 138   maxlim: 8320   bits: 15/14
c ---[ 340]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[ 338]---> Adder-cost: 92   maxlim: 6016   bits: 14/13
c ---[ 336]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[ 334]---> Adder-cost: 108   maxlim: 7040   bits: 14/13
c ---[ 332]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[ 330]---> Adder-cost: 164   maxlim: 10368   bits: 15/14
c ---[ 328]---> Adder-cost: 68   maxlim: 10368   bits: 15/14
c ---[ 326]---> Adder-cost: 146   maxlim: 9600   bits: 15/14
c ---[ 324]---> Adder-cost: 62   maxlim: 9600   bits: 15/14
c ---[ 322]---> Adder-cost: 104   maxlim: 6656   bits: 14/13
c ---[ 320]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[ 318]---> Adder-cost: 114   maxlim: 7168   bits: 14/13
c ---[ 316]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[ 314]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[ 312]---> Adder-cost: 46   maxlim: 6784   bits: 14/13
c ---[ 310]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[ 308]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 7
c ---[ 306]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[ 304]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[ 302]---> Sorter-cost:  646     Base: 2 2 2 2 2 2 2 7
c ---[ 300]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[ 298]---> Sorter-cost:  629     Base: 2 2 2 2 2 2 2 7
c ---[ 296]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 294]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[ 292]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[ 290]---> Sorter-cost:  857     Base: 2 2 2 2 2 2 2 7
c ---[ 288]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[ 286]---> Adder-cost: 228   maxlim: 14720   bits: 15/14
c ---[ 284]---> Adder-cost: 76   maxlim: 14720   bits: 15/14
c ---[ 282]---> Adder-cost: 76   maxlim: 14720   bits: 15/14
c ---[ 280]---> Adder-cost: 82   maxlim: 5120   bits: 14/13
c ---[ 278]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[ 276]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[ 274]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[ 272]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[ 270]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[ 268]---> Adder-cost: 112   maxlim: 7552   bits: 14/13
c ---[ 266]---> Adder-cost: 48   maxlim: 7552   bits: 14/13
c ---[ 264]---> Adder-cost: 74   maxlim: 4480   bits: 14/13
c ---[ 262]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[ 260]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 258]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[ 256]---> Adder-cost: 88   maxlim: 5376   bits: 14/13
c ---[ 254]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[ 252]---> Sorter-cost:  994     Base: 2 2 2 2 2 2 2 7
c ---[ 250]---> Adder-cost: 94   maxlim: 5888   bits: 14/13
c ---[ 248]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[ 246]---> Adder-cost: 108   maxlim: 8576   bits: 15/14
c ---[ 244]---> Adder-cost: 126   maxlim: 8704   bits: 15/14
c ---[ 242]---> Adder-cost: 128   maxlim: 8960   bits: 15/14
c ---[ 240]---> Adder-cost: 60   maxlim: 8960   bits: 15/14
c ---[ 238]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[ 236]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 234]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[ 232]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[ 230]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[ 228]---> Adder-cost: 92   maxlim: 6912   bits: 14/13
c ---[ 226]---> Adder-cost: 96   maxlim: 6272   bits: 14/13
c ---[ 224]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[ 222]---> Adder-cost: 84   maxlim: 5376   bits: 14/13
c ---[ 220]---> Adder-cost: 80   maxlim: 5504   bits: 14/13
c ---[ 218]---> Adder-cost: 88   maxlim: 5632   bits: 14/13
c ---[ 216]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[ 214]---> Adder-cost: 104   maxlim: 6400   bits: 14/13
c ---[ 212]---> Adder-cost: 82   maxlim: 6784   bits: 14/13
c ---[ 210]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 7
c ---[ 208]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[ 206]---> Sorter-cost:  903     Base: 2 2 2 2 2 2 2 7
c ---[ 204]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[ 202]---> Sorter-cost:  942     Base: 2 2 2 2 2 2 2 7
c ---[ 200]---> Sorter-cost:  596     Base: 2 2 2 2 2 2 2 7
c ---[ 198]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[ 196]---> Adder-cost: 68   maxlim: 4352   bits: 14/13
c ---[ 194]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[ 192]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[ 190]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[ 188]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[ 186]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[ 184]---> Adder-cost: 172   maxlim: 11264   bits: 15/14
c ---[ 182]---> Adder-cost: 104   maxlim: 11392   bits: 15/14
c ---[ 180]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[ 178]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[ 176]---> Sorter-cost:  461     Base: 2 2 2 2 2 2 2 7
c ---[ 174]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[ 172]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[ 170]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[ 168]---> Adder-cost: 98   maxlim: 6400   bits: 14/13
c ---[ 166]---> Adder-cost: 96   maxlim: 6144   bits: 14/13
c ---[ 164]---> Adder-cost: 140   maxlim: 8960   bits: 15/14
c ---[ 162]---> Adder-cost: 60   maxlim: 8960   bits: 15/14
c ---[ 160]---> Adder-cost: 110   maxlim: 7168   bits: 14/13
c ---[ 158]---> Adder-cost: 86   maxlim: 7296   bits: 14/13
c ---[ 156]---> Adder-cost: 104   maxlim: 6400   bits: 14/13
c ---[ 154]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[ 152]---> Adder-cost: 118   maxlim: 7168   bits: 14/13
c ---[ 150]---> Adder-cost: 98   maxlim: 6272   bits: 14/13
c ---[ 148]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[ 146]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[ 144]---> Sorter-cost:  569     Base: 2 2 2 2 2 2 2 7
c ---[ 142]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 7
c ---[ 140]---> Sorter-cost:  432     Base: 2 2 2 2 2 2 2 7
c ---[ 138]---> Sorter-cost:  306     Base: 2 2 2 2 2 2 2 7
c ---[ 136]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 7
c ---[ 134]---> Sorter-cost:  608     Base: 2 2 2 2 2 2 2 7
c ---[ 132]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[ 130]---> Sorter-cost:  956     Base: 2 2 2 2 2 2 2 7
c ---[ 128]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[ 126]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 7
c ---[ 124]---> Sorter-cost:  656     Base: 2 2 2 2 2 2 2 7
c ---[ 122]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[ 120]---> Adder-cost: 106   maxlim: 6528   bits: 14/13
c ---[ 118]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[ 116]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 114]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[ 112]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[ 110]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[ 108]---> Adder-cost: 118   maxlim: 7168   bits: 14/13
c ---[ 106]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[ 104]---> Adder-cost: 74   maxlim: 4736   bits: 14/13
c ---[ 102]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[ 100]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[  98]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[  96]---> Sorter-cost:  930     Base: 2 2 2 2 2 2 2 7
c ---[  94]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[  92]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[  90]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[  88]---> Adder-cost: 38 /oldhome/oroussel/solvers/minisat+_script: line 16: 27841 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.92 0.97 0.92 2/54 27836
Raw data (stat): 27836 (runsolver) R 27835 7266 7265 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784908613 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 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.93 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.0002 s]
Raw data (loadavg): 0.94 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.0008 s]
Raw data (loadavg): 0.95 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.0006 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.0007 s]
Raw data (loadavg): 0.96 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.0012 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.0009 s]
Raw data (loadavg): 0.97 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.0017 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.0015 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 0.98 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.07 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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 s]
Raw data (loadavg): 1.06 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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 s]
Raw data (loadavg): 1.05 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.04 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.04 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.03 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 1.03 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.02 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.02 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 1.01 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.001 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.002 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.003 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.003 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.003 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.003 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.003 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.004 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.004 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.005 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.005 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.005 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.005 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.005 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.005 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.004 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.012 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.013 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.014 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.015 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.044 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.043 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.044 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.044 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.043 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.043 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.04 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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+1230.05 s]
Raw data (loadavg): 1.00 0.99 0.93 2/55 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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+1230.23 s]
Raw data (loadavg): 1.00 0.99 0.93 1/53 27841
Raw data (stat): 27836 (minisat+_script) S 27835 7266 7265 0 -1 0 300 790 0 0 0 0 9 2 17 0 1 0 784908613 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): 1230.23
CPU time (s): 1230.24
CPU user time (s): 1224.15
CPU system time (s): 6.08308
CPU usage (%): 100.001
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####