PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-dc1c.opb
MD5SUM	bd6d0785955b31f4cbdede5ce3d2b1e9
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	58150
Biggest coefficient in the objective function	536870912000000000000
Number of bits for the biggest coefficient in the objective function	69
Sum of the numbers in the objective function	6807821537690881359872
Number of bits of the sum of numbers in the objective function	73
Biggest number in a constraint	536870912000000000000
Number of bits of the biggest number in a constraint	69
Biggest sum of numbers in a constraint	6808845537690881359872
Number of bits of the biggest sum of numbers	73
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1305.36
Number of variables	58150
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	58150
Trace number 30942

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-05-25 21:05:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22344 boxname=wulflinc13 idbench=1160 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  bd6d0785955b31f4cbdede5ce3d2b1e9  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-dc1c.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-20-10-dc1c.opb
IDLAUNCH: 22344
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        633220 kB
Buffers:         16884 kB
Cached:         363024 kB
SwapCached:        416 kB
Active:          26444 kB
Inactive:       355780 kB
HighTotal:      131008 kB
HighFree:        44156 kB
LowTotal:       903652 kB
LowFree:        589064 kB
SwapTotal:     2097136 kB
SwapFree:      2096040 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5948 kB
Slab:            13224 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 21:19:28 (client local time) WITH STATUS 139 IN 848.858 SECONDS
stats: 22344 7 848.858 139
#### 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): ssssssss
c ---[3288]---> Sorter-cost:  910     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3286]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3284]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3282]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3280]---> Sorter-cost:  642     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3278]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3276]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3274]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3272]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3270]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3268]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3266]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3264]---> Sorter-cost:  983     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3262]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3260]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3258]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3256]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3254]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3252]---> Sorter-cost: 1085     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3250]---> Sorter-cost:  865     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3248]---> Sorter-cost:  727     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3246]---> Sorter-cost:  765     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3244]---> Adder-cost: 176   maxlim: 87040   bits: 18/17
c ---[3242]---> Adder-cost: 66   maxlim: 87040   bits: 18/17
c ---[3240]---> Adder-cost: 112   maxlim: 59392   bits: 17/16
c ---[3238]---> Adder-cost: 96   maxlim: 51200   bits: 17/16
c ---[3236]---> Adder-cost: 148   maxlim: 71680   bits: 18/17
c ---[3234]---> Adder-cost: 142   maxlim: 70656   bits: 18/17
c ---[3232]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3230]---> Sorter-cost:  741     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3228]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3226]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3224]---> Sorter-cost:  645     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3222]---> Sorter-cost:  678     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3220]---> Sorter-cost: 1188     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3218]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3216]---> Sorter-cost: 1034     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3214]---> Sorter-cost: 1046     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3212]---> Sorter-cost:  375     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3210]---> Sorter-cost: 1250     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3208]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3206]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3204]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3202]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3200]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3198]---> Sorter-cost: 1225     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3196]---> Sorter-cost: 1076     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3194]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3192]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[3190]---> Adder-cost: 76   maxlim: 51200   bits: 17/16
c ---[3188]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3186]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3184]---> Sorter-cost:  641     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3182]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3180]---> Sorter-cost:  716     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3178]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3176]---> Sorter-cost: 1215     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3174]---> Sorter-cost: 1065     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3172]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3170]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3168]---> Sorter-cost:  787     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3166]---> Sorter-cost:  660     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3164]---> Sorter-cost:  761     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3162]---> Sorter-cost:  991     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3160]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3158]---> Sorter-cost:  923     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3156]---> Sorter-cost:  593     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3154]---> Sorter-cost:  583     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3152]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3150]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3148]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3146]---> Sorter-cost: 1223     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3144]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3142]---> Sorter-cost:  688     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3140]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3138]---> Sorter-cost:  991     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3136]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3134]---> Sorter-cost:  684     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3132]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3130]---> Adder-cost: 146   maxlim: 70656   bits: 18/17
c ---[3128]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3126]---> Adder-cost: 60   maxlim: 70656   bits: 18/17
c ---[3124]---> Adder-cost: 120   maxlim: 62464   bits: 17/16
c ---[3122]---> Adder-cost: 48   maxlim: 62464   bits: 17/16
c ---[3120]---> Adder-cost: 132   maxlim: 67584   bits: 18/17
c ---[3118]---> Adder-cost: 60   maxlim: 67584   bits: 18/17
c ---[3116]---> Sorter-cost: 1185     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3114]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3112]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3110]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3108]---> Sorter-cost:  684     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3106]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3104]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3102]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3100]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3098]---> Sorter-cost:  645     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3096]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3094]---> Adder-cost: 178   maxlim: 88064   bits: 18/17
c ---[3092]---> Adder-cost: 68   maxlim: 88064   bits: 18/17
c ---[3090]---> Adder-cost: 138   maxlim: 86016   bits: 18/17
c ---[3088]---> Adder-cost: 66   maxlim: 86016   bits: 18/17
c ---[3086]---> Adder-cost: 120   maxlim: 59392   bits: 17/16
c ---[3084]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3082]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[3080]---> Sorter-cost: 1185     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3078]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3076]---> Sorter-cost: 1285     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3074]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3072]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3070]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3068]---> Adder-cost: 120   maxlim: 60416   bits: 17/16
c ---[3066]---> Adder-cost: 48   maxlim: 60416   bits: 17/16
c ---[3064]---> Sorter-cost: 1250     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3062]---> Sorter-cost: 1223     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3060]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3058]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3056]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3054]---> Sorter-cost: 1250     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3052]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3050]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3048]---> Sorter-cost:  375     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3046]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3044]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3042]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3040]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3038]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3036]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3034]---> Sorter-cost: 1081     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3032]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3030]---> Adder-cost: 112   maxlim: 55296   bits: 17/16
c ---[3028]---> Adder-cost: 48   maxlim: 55296   bits: 17/16
c ---[3026]---> Sorter-cost: 1084     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3024]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3022]---> Sorter-cost: 1171     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3020]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3018]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[3016]---> Adder-cost: 112   maxlim: 55296   bits: 17/16
c ---[3014]---> Adder-cost: 48   maxlim: 55296   bits: 17/16
c ---[3012]---> Adder-cost: 104   maxlim: 52224   bits: 17/16
c ---[3010]---> Adder-cost: 44   maxlim: 52224   bits: 17/16
c ---[3008]---> Sorter-cost: 1271     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3006]---> Sorter-cost:  763     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3004]---> Sorter-cost: 1236     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3002]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3000]---> Adder-cost: 112   maxlim: 55296   bits: 17/16
c ---[2998]---> Adder-cost: 48   maxlim: 55296   bits: 17/16
c ---[2996]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[2994]---> Sorter-cost:  937     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2992]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2990]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2988]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2986]---> Sorter-cost:  917     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2984]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2982]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2980]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2978]---> Sorter-cost:  589     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2976]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2974]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[2972]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2970]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2968]---> Sorter-cost:  253     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2966]---> Adder-cost: 156   maxlim: 76800   bits: 18/17
c ---[2964]---> Adder-cost: 62   maxlim: 76800   bits: 18/17
c ---[2962]---> Adder-cost: 198   maxlim: 109568   bits: 18/17
c ---[2960]---> Adder-cost: 132   maxlim: 66560   bits: 18/17
c ---[2958]---> Adder-cost: 78   maxlim: 109568   bits: 18/17
c ---[2956]---> Adder-cost: 396   maxlim: 205824   bits: 19/18
c ---[2954]---> Adder-cost: 116   maxlim: 205824   bits: 19/18
c ---[2952]---> Adder-cost: 396   maxlim: 209920   bits: 19/18
c ---[2950]---> Adder-cost: 112   maxlim: 209920   bits: 19/18
c ---[2948]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[2946]---> Adder-cost: 276   maxlim: 161792   bits: 19/18
c ---[2944]---> Adder-cost: 92   maxlim: 161792   bits: 19/18
c ---[2942]---> Adder-cost: 334   maxlim: 190464   bits: 19/18
c ---[2940]---> Adder-cost: 106   maxlim: 190464   bits: 19/18
c ---[2938]---> Adder-cost: 414   maxlim: 236544   bits: 19/18
c ---[2936]---> Adder-cost: 90   maxlim: 58368   bits: 17/16
c ---[2934]---> Adder-cost: 124   maxlim: 236544   bits: 19/18
c ---[2932]---> Adder-cost: 452   maxlim: 246784   bits: 19/18
c ---[2930]---> Adder-cost: 576   maxlim: 314368   bits: 20/19
c ---[2928]---> Adder-cost: 586   maxlim: 324608   bits: 20/19
c ---[2926]---> Adder-cost: 518   maxlim: 265216   bits: 20/19
c ---[2924]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[2922]---> Adder-cost: 482   maxlim: 253952   bits: 19/18
c ---[2920]---> Adder-cost: 558   maxlim: 300032   bits: 20/19
c ---[2918]---> Adder-cost: 410   maxlim: 228352   bits: 19/18
c ---[2916]---> Adder-cost: 368   maxlim: 203776   bits: 19/18
c ---[2914]---> Adder-cost: 110   maxlim: 203776   bits: 19/18
c ---[2912]---> Adder-cost: 334   maxlim: 201728   bits: 19/18
c ---[2910]---> Sorter-cost:  910     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2908]---> Adder-cost: 114   maxlim: 201728   bits: 19/18
c ---[2906]---> Adder-cost: 340   maxlim: 189440   bits: 19/18
c ---[2904]---> Adder-cost: 104   maxlim: 189440   bits: 19/18
c ---[2902]---> Adder-cost: 374   maxlim: 209920   bits: 19/18
c ---[2900]---> Adder-cost: 112   maxlim: 209920   bits: 19/18
c ---[2898]---> Adder-cost: 404   maxlim: 218112   bits: 19/18
c ---[2896]---> Adder-cost: 328   maxlim: 182272   bits: 19/18
c ---[2894]---> Adder-cost: 106   maxlim: 182272   bits: 19/18
c ---[2892]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2890]---> Adder-cost: 182   maxlim: 95232   bits: 18/17
c ---[2888]---> Adder-cost: 70   maxlim: 95232   bits: 18/17
c ---[2886]---> Adder-cost: 216   maxlim: 116736   bits: 18/17
c ---[2884]---> Adder-cost: 78   maxlim: 116736   bits: 18/17
c ---[2882]---> Adder-cost: 192   maxlim: 102400   bits: 18/17
c ---[2880]---> Sorter-cost: 1049     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2878]---> Adder-cost: 76   maxlim: 102400   bits: 18/17
c ---[2876]---> Adder-cost: 226   maxlim: 122880   bits: 18/17
c ---[2874]---> Adder-cost: 80   maxlim: 122880   bits: 18/17
c ---[2872]---> Adder-cost: 264   maxlim: 142336   bits: 19/18
c ---[2870]---> Adder-cost: 92   maxlim: 142336   bits: 19/18
c ---[2868]---> Adder-cost: 120   maxlim: 68608   bits: 18/17
c ---[2866]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2864]---> Adder-cost: 58   maxlim: 68608   bits: 18/17
c ---[2862]---> Adder-cost: 108   maxlim: 58368   bits: 17/16
c ---[2860]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[2858]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2856]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2854]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2852]---> Sorter-cost:  351     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2850]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2848]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2846]---> Adder-cost: 118   maxlim: 58368   bits: 17/16
c ---[2844]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[2842]---> Adder-cost: 86   maxlim: 67584   bits: 18/17
c ---[2840]---> Adder-cost: 60   maxlim: 67584   bits: 18/17
c ---[2838]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2836]---> Adder-cost: 146   maxlim: 69632   bits: 18/17
c ---[2834]---> Adder-cost: 134   maxlim: 72704   bits: 18/17
c ---[2832]---> Adder-cost: 138   maxlim: 67584   bits: 18/17
c ---[2830]---> Adder-cost: 90   maxlim: 63488   bits: 17/16
c ---[2828]---> Adder-cost: 108   maxlim: 56320   bits: 17/16
c ---[2826]---> Adder-cost: 102   maxlim: 52224   bits: 17/16
c ---[2824]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2822]---> Sorter-cost: 1033     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2820]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2818]---> Adder-cost: 106   maxlim: 52224   bits: 17/16
c ---[2816]---> Sorter-cost:  684     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2814]---> Adder-cost: 108   maxlim: 59392   bits: 17/16
c ---[2812]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[2810]---> Adder-cost: 120   maxlim: 60416   bits: 17/16
c ---[2808]---> Adder-cost: 114   maxlim: 62464   bits: 17/16
c ---[2806]---> Adder-cost: 96   maxlim: 51200   bits: 17/16
c ---[2804]---> Sorter-cost: 1285     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2802]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2800]---> Sorter-cost:  966     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2798]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2796]---> Sorter-cost: 1175     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2794]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2792]---> Sorter-cost: 1158     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2790]---> Sorter-cost:  813     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2788]---> Sorter-cost:  935     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2786]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2784]---> Sorter-cost:  899     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2782]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2780]---> Adder-cost: 146   maxlim: 69632   bits: 18/17
c ---[2778]---> Adder-cost: 62   maxlim: 69632   bits: 18/17
c ---[2776]---> Adder-cost: 110   maxlim: 56320   bits: 17/16
c ---[2774]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[2772]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2770]---> Adder-cost: 138   maxlim: 66560   bits: 18/17
c ---[2768]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[2766]---> Adder-cost: 106   maxlim: 54272   bits: 17/16
c ---[2764]---> Adder-cost: 46   maxlim: 54272   bits: 17/16
c ---[2762]---> Adder-cost: 122   maxlim: 62464   bits: 17/16
c ---[2760]---> Adder-cost: 48   maxlim: 62464   bits: 17/16
c ---[2758]---> Adder-cost: 104   maxlim: 51200   bits: 17/16
c ---[2756]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[2754]---> Adder-cost: 120   maxlim: 59392   bits: 17/16
c ---[2752]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[2750]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2748]---> Adder-cost: 106   maxlim: 56320   bits: 17/16
c ---[2746]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[2744]---> Sorter-cost: 1061     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2742]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2740]---> Sorter-cost:  593     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2738]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2736]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2734]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2732]---> Sorter-cost: 1039     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2730]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2728]---> Sorter-cost:  420     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2726]---> Adder-cost: 112   maxlim: 56320   bits: 17/16
c ---[2724]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[2722]---> Sorter-cost: 1185     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2720]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2718]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2716]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2714]---> Sorter-cost:  783     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2712]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2710]---> Sorter-cost:  935     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2708]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2706]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2704]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2702]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2700]---> Sorter-cost:  935     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2698]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2696]---> Sorter-cost:  687     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2694]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2692]---> Adder-cost: 112   maxlim: 55296   bits: 17/16
c ---[2690]---> Adder-cost: 48   maxlim: 55296   bits: 17/16
c ---[2688]---> Adder-cost: 48   maxlim: 55296   bits: 17/16
c ---[2686]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2684]---> Sorter-cost:  428     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2682]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2680]---> Sorter-cost: 1016     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2678]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2676]---> Adder-cost: 124   maxlim: 61440   bits: 17/16
c ---[2674]---> Adder-cost: 50   maxlim: 61440   bits: 17/16
c ---[2672]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2670]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2668]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[2666]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[2664]---> Sorter-cost:  470     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2662]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2660]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2658]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2656]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2654]---> Sorter-cost:  642     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2652]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2650]---> Sorter-cost:  566     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2648]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2646]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2644]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2642]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2640]---> Sorter-cost:  716     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2638]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2636]---> Sorter-cost:  787     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2634]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2632]---> Adder-cost: 146   maxlim: 69632   bits: 18/17
c ---[2630]---> Adder-cost: 62   maxlim: 69632   bits: 18/17
c ---[2628]---> Adder-cost: 126   maxlim: 63488   bits: 17/16
c ---[2626]---> Adder-cost: 52   maxlim: 63488   bits: 17/16
c ---[2624]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2622]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2620]---> Sorter-cost:  313     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2618]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2616]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2614]---> Sorter-cost:  420     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2612]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2610]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2608]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2606]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2604]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2602]---> Adder-cost: 106   maxlim: 51200   bits: 17/16
c ---[2600]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[2598]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2596]---> Sorter-cost:  678     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2594]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2592]---> Sorter-cost:  961     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2590]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2588]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2586]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2584]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2582]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2580]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[2578]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[2576]---> Adder-cost: 98   maxlim: 52224   bits: 17/16
c ---[2574]---> Sorter-cost:  910     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2572]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2570]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2568]---> Sorter-cost: 1190     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2566]---> Sorter-cost: 1073     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2564]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2562]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2560]---> Sorter-cost: 1188     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2558]---> Sorter-cost: 1175     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2556]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2554]---> Sorter-cost:  283     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2552]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2550]---> Sorter-cost:  720     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2548]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2546]---> Sorter-cost:  585     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2544]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2542]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2540]---> Sorter-cost:  295     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2538]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2536]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2534]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2532]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2530]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2528]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2526]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2524]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2522]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2520]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2518]---> Adder-cost: 106   maxlim: 51200   bits: 17/16
c ---[2516]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[2514]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[2512]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2510]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2508]---> Sorter-cost:  470     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2506]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2504]---> Sorter-cost: 1311     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2502]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2500]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2498]---> Sorter-cost:  739     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2496]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2494]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2492]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2490]---> Sorter-cost: 1133     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2488]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2486]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2484]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2482]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2480]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2478]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2476]---> Sorter-cost:  971     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2474]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2472]---> Sorter-cost:  953     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2470]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2468]---> Adder-cost: 118   maxlim: 58368   bits: 17/16
c ---[2466]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[2464]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[2462]---> Sorter-cost: 1250     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2460]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2458]---> Sorter-cost:  971     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2456]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2454]---> Adder-cost: 154   maxlim: 74752   bits: 18/17
c ---[2452]---> Adder-cost: 60   maxlim: 74752   bits: 18/17
c ---[2450]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2448]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2446]---> Sorter-cost:  896     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2444]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2442]---> Sorter-cost:  597     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2440]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2438]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[2436]---> Adder-cost: 46   maxlim: 54272   bits: 17/16
c ---[2434]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2432]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2430]---> Sorter-cost:  424     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2428]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2426]---> Sorter-cost:  470     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2424]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2422]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2420]---> Adder-cost: 112   maxlim: 56320   bits: 17/16
c ---[2418]---> Adder-cost: 112   maxlim: 58368   bits: 17/16
c ---[2416]---> Adder-cost: 104   maxlim: 51200   bits: 17/16
c ---[2414]---> Adder-cost: 112   maxlim: 63488   bits: 17/16
c ---[2412]---> Adder-cost: 158   maxlim: 78848   bits: 18/17
c ---[2410]---> Adder-cost: 144   maxlim: 77824   bits: 18/17
c ---[2408]---> Sorter-cost:  967     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2406]---> Sorter-cost: 1068     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2404]---> Adder-cost: 120   maxlim: 59392   bits: 17/16
c ---[2402]---> Adder-cost: 130   maxlim: 67584   bits: 18/17
c ---[2400]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2398]---> Adder-cost: 158   maxlim: 78848   bits: 18/17
c ---[2396]---> Adder-cost: 104   maxlim: 79872   bits: 18/17
c ---[2394]---> Adder-cost: 174   maxlim: 88064   bits: 18/17
c ---[2392]---> Adder-cost: 68   maxlim: 88064   bits: 18/17
c ---[2390]---> Sorter-cost:  995     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2388]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2386]---> Adder-cost: 112   maxlim: 55296   bits: 17/16
c ---[2384]---> Adder-cost: 134   maxlim: 65536   bits: 18/17
c ---[2382]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2380]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2378]---> Adder-cost: 322   maxlim: 165888   bits: 19/18
c ---[2376]---> Sorter-cost:  961     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2374]---> Sorter-cost:  579     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2372]---> Sorter-cost:  739     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2370]---> Sorter-cost:  546     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2368]---> Sorter-cost:  680     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2366]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2364]---> Sorter-cost:  371     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2362]---> Sorter-cost:  257     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2360]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2358]---> Sorter-cost: 1287     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2356]---> Adder-cost: 102   maxlim: 165888   bits: 19/18
c ---[2354]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2352]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2350]---> Sorter-cost:  789     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2348]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2346]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[2344]---> Adder-cost: 112   maxlim: 57344   bits: 17/16
c ---[2342]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2340]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2338]---> Sorter-cost:  640     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2336]---> Sorter-cost:  588     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2334]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2332]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2330]---> Sorter-cost: 1127     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2328]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2326]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2324]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2322]---> Sorter-cost: 1082     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2320]---> Sorter-cost: 1168     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2318]---> Sorter-cost:  908     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2316]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2314]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2312]---> Sorter-cost:  989     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2310]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2308]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2306]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2304]---> Sorter-cost:  632     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2302]---> Sorter-cost:  556     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2300]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2298]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2296]---> Sorter-cost:  971     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2294]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2292]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2290]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2288]---> Sorter-cost:  739     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2286]---> Sorter-cost:  986     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2284]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2282]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2280]---> Sorter-cost:  640     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2278]---> Sorter-cost:  577     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2276]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2274]---> Adder-cost: 102   maxlim: 165888   bits: 19/18
c ---[2272]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2270]---> Adder-cost: 110   maxlim: 56320   bits: 17/16
c ---[2268]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[2266]---> Adder-cost: 118   maxlim: 58368   bits: 17/16
c ---[2264]---> Adder-cost: 92   maxlim: 54272   bits: 17/16
c ---[2262]---> Sorter-cost: 1082     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2260]---> Sorter-cost:  951     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2258]---> Sorter-cost: 1121     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2256]---> Sorter-cost: 1022     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2254]---> Adder-cost: 270   maxlim: 145408   bits: 19/18
c ---[2252]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2250]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2248]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2246]---> Sorter-cost:  313     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2244]---> Sorter-cost: 1183     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2242]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2240]---> Sorter-cost: 1057     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2238]---> Sorter-cost: 1058     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2236]---> Sorter-cost:  895     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2234]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2232]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[2230]---> Sorter-cost: 1313     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2228]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2226]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2224]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2222]---> Sorter-cost: 1061     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2220]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2218]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[2216]---> Adder-cost: 46   maxlim: 54272   bits: 17/16
c ---[2214]---> Adder-cost: 126   maxlim: 63488   bits: 17/16
c ---[2212]---> Adder-cost: 52   maxlim: 63488   bits: 17/16
c ---[2210]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[2208]---> Adder-cost: 122   maxlim: 61440   bits: 17/16
c ---[2206]---> Adder-cost: 50   maxlim: 61440   bits: 17/16
c ---[2204]---> Adder-cost: 140   maxlim: 66560   bits: 18/17
c ---[2202]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[2200]---> Adder-cost: 106   maxlim: 55296   bits: 17/16
c ---[2198]---> Adder-cost: 48   maxlim: 55296   bits: 17/16
c ---[2196]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2194]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2192]---> Sorter-cost: 1251     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2190]---> Sorter-cost:  763     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2188]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[2186]---> Adder-cost: 118   maxlim: 58368   bits: 17/16
c ---[2184]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[2182]---> Adder-cost: 146   maxlim: 71680   bits: 18/17
c ---[2180]---> Adder-cost: 60   maxlim: 71680   bits: 18/17
c ---[2178]---> Adder-cost: 172   maxlim: 83968   bits: 18/17
c ---[2176]---> Adder-cost: 68   maxlim: 83968   bits: 18/17
c ---[2174]---> Sorter-cost: 1185     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2172]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2170]---> Adder-cost: 106   maxlim: 51200   bits: 17/16
c ---[2168]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[2166]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[2164]---> Sorter-cost:  937     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2162]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2160]---> Sorter-cost:  380     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2158]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2156]---> Sorter-cost:  609     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2154]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2152]---> Sorter-cost:  647     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2150]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2148]---> Sorter-cost: 1248     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2146]---> Adder-cost: 112   maxlim: 55296   bits: 17/16
c ---[2144]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[2142]---> Adder-cost: 48   maxlim: 55296   bits: 17/16
c ---[2140]---> Sorter-cost: 1267     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2138]---> Sorter-cost:  763     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2136]---> Sorter-cost: 1183     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2134]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2132]---> Adder-cost: 176   maxlim: 86016   bits: 18/17
c ---[2130]---> Adder-cost: 66   maxlim: 86016   bits: 18/17
c ---[2128]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2126]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2124]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2122]---> Adder-cost: 254   maxlim: 140288   bits: 19/18
c ---[2120]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2118]---> Sorter-cost: 1059     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2116]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2114]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2112]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2110]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2108]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2106]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2104]---> Sorter-cost:  910     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2102]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2100]---> Adder-cost: 94   maxlim: 140288   bits: 19/18
c ---[2098]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2096]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2094]---> Sorter-cost: 1311     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2092]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2090]---> Sorter-cost: 1082     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2088]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2086]---> Sorter-cost: 1127     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2084]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2082]---> Adder-cost: 124   maxlim: 61440   bits: 17/16
c ---[2080]---> Adder-cost: 50   maxlim: 61440   bits: 17/16
c ---[2078]---> Adder-cost: 94   maxlim: 140288   bits: 19/18
c ---[2076]---> Sorter-cost:  910     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2074]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2072]---> Sorter-cost: 1133     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2070]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2068]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2066]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2064]---> Sorter-cost:  680     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2062]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2060]---> Adder-cost: 162   maxlim: 79872   bits: 18/17
c ---[2058]---> Adder-cost: 98   maxlim: 86016   bits: 18/17
c ---[2056]---> Adder-cost: 94   maxlim: 140288   bits: 19/18
c ---[2054]---> Adder-cost: 66   maxlim: 86016   bits: 18/17
c ---[2052]---> Adder-cost: 104   maxlim: 52224   bits: 17/16
c ---[2050]---> Adder-cost: 44   maxlim: 52224   bits: 17/16
c ---[2048]---> Sorter-cost:  739     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2046]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2044]---> Adder-cost: 154   maxlim: 76800   bits: 18/17
c ---[2042]---> Adder-cost: 62   maxlim: 76800   bits: 18/17
c ---[2040]---> Sorter-cost: 1269     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2038]---> Sorter-cost:  763     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2036]---> Adder-cost: 140   maxlim: 66560   bits: 18/17
c ---[2034]---> Adder-cost: 94   maxlim: 140288   bits: 19/18
c ---[2032]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[2030]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[2028]---> Adder-cost: 46   maxlim: 54272   bits: 17/16
c ---[2026]---> Sorter-cost: 1084     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2024]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2022]---> Sorter-cost:  574     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2020]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2018]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2016]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2014]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2012]---> Adder-cost: 94   maxlim: 140288   bits: 19/18
c ---[2010]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2008]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2006]---> Sorter-cost:  597     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2004]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2002]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2000]---> Sorter-cost: 1138     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1998]---> Sorter-cost: 1311     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1996]---> Adder-cost: 112   maxlim: 55296   bits: 17/16
c ---[1994]---> Adder-cost: 110   maxlim: 56320   bits: 17/16
c ---[1992]---> Adder-cost: 88   maxlim: 53248   bits: 17/16
c ---[1990]---> Adder-cost: 264   maxlim: 145408   bits: 19/18
c ---[1988]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1986]---> Sorter-cost:  267     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1984]---> Sorter-cost:  263     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1982]---> Adder-cost: 104   maxlim: 51200   bits: 17/16
c ---[1980]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[1978]---> Sorter-cost: 1084     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1976]---> Sorter-cost:  980     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1974]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[1972]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1970]---> Sorter-cost: 1137     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1968]---> Sorter-cost:  605     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1966]---> Sorter-cost:  708     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1964]---> Sorter-cost: 1077     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1962]---> Sorter-cost:  734     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1960]---> Sorter-cost:  731     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1958]---> Sorter-cost:  585     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1956]---> Sorter-cost:  582     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1954]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1952]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[1950]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1948]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1946]---> Sorter-cost: 1049     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1944]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1942]---> Sorter-cost: 1246     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1940]---> Sorter-cost: 1247     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1938]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1936]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1934]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[1932]---> Adder-cost: 116   maxlim: 58368   bits: 17/16
c ---[1930]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[1928]---> Sorter-cost: 1061     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1926]---> Sorter-cost: 1063     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1924]---> Sorter-cost: 1131     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1922]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1920]---> Sorter-cost: 1020     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1918]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1916]---> Adder-cost: 118   maxlim: 57344   bits: 17/16
c ---[1914]---> Adder-cost: 102   maxlim: 51200   bits: 17/16
c ---[1912]---> Sorter-cost: 1185     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1910]---> Sorter-cost: 1043     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1908]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[1906]---> Adder-cost: 106   maxlim: 52224   bits: 17/16
c ---[1904]---> Sorter-cost: 1215     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1902]---> Sorter-cost:  615     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1900]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1898]---> Sorter-cost:  615     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1896]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1894]---> Sorter-cost:  570     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1892]---> Sorter-cost:  340     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1890]---> Sorter-cost:  269     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1888]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1886]---> Adder-cost: 88   maxlim: 145408   bits: 19/18
c ---[1884]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1882]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1880]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1878]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1876]---> Adder-cost: 112   maxlim: 56320   bits: 17/16
c ---[1874]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[1872]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[1870]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[1868]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1866]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1864]---> Adder-cost: 160   maxlim: 84992   bits: 18/17
c ---[1862]---> Sorter-cost:  601     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1860]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1858]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1856]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1854]---> Sorter-cost: 1223     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1852]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1850]---> Sorter-cost: 1061     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1848]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1846]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1844]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1842]---> Adder-cost: 68   maxlim: 84992   bits: 18/17
c ---[1840]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1838]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1836]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1834]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1832]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1830]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1828]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1826]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1824]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1822]---> Sorter-cost: 1084     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1820]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1818]---> Sorter-cost:  576     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1816]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1814]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1812]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1810]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1808]---> Sorter-cost:  593     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1806]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1804]---> Adder-cost: 142   maxlim: 68608   bits: 18/17
c ---[1802]---> Adder-cost: 58   maxlim: 68608   bits: 18/17
c ---[1800]---> Sorter-cost: 1188     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1798]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1796]---> Sorter-cost: 1076     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1794]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1792]---> Sorter-cost: 1033     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1790]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1788]---> Sorter-cost:  981     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1786]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1784]---> Sorter-cost: 1151     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1782]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1780]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1778]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1776]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1774]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1772]---> Sorter-cost:  375     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1770]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1768]---> Sorter-cost:  617     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1766]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1764]---> Sorter-cost: 1077     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1762]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1760]---> Adder-cost: 68   maxlim: 84992   bits: 18/17
c ---[1758]---> Sorter-cost:  997     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1756]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1754]---> Sorter-cost:  711     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1752]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[1750]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[1748]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1746]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1744]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1742]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1740]---> Sorter-cost:  971     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1738]---> Adder-cost: 138   maxlim: 67584   bits: 18/17
c ---[1736]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1734]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1732]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1730]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[1728]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[1726]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[1724]---> Sorter-cost: 1305     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1722]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1720]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1718]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1716]---> Adder-cost: 60   maxlim: 67584   bits: 18/17
c ---[1714]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1712]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1710]---> Sorter-cost:  947     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1708]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1706]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1704]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1702]---> Sorter-cost: 1248     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1700]---> Sorter-cost: 1133     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1698]---> Sorter-cost:  574     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1696]---> Sorter-cost:  334     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1694]---> Sorter-cost:  660     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1692]---> Sorter-cost:  739     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1690]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1688]---> Sorter-cost:  375     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1686]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1684]---> Sorter-cost: 1223     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1682]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1680]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1678]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1676]---> Adder-cost: 124   maxlim: 62464   bits: 17/16
c ---[1674]---> Adder-cost: 48   maxlim: 62464   bits: 17/16
c ---[1672]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1670]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1668]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1666]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1664]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1662]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1660]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1658]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1656]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1654]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1652]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1650]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1648]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1646]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1644]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1642]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1640]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1638]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1636]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1634]---> Adder-cost: 60   maxlim: 67584   bits: 18/17
c ---[1632]---> Sorter-cost:  265     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1630]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1628]---> Sorter-cost:  363     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1626]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1624]---> Adder-cost: 126   maxlim: 63488   bits: 17/16
c ---[1622]---> Adder-cost: 52   maxlim: 63488   bits: 17/16
c ---[1620]---> Adder-cost: 136   maxlim: 65536   bits: 18/17
c ---[1618]---> Adder-cost: 62   maxlim: 65536   bits: 18/17
c ---[1616]---> Sorter-cost: 1285     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1614]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1612]---> Adder-cost: 116   maxlim: 59392   bits: 17/16
c ---[1610]---> Sorter-cost: 1137     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1608]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1606]---> Sorter-cost: 1238     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1604]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1602]---> Sorter-cost:  645     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1600]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1598]---> Adder-cost: 118   maxlim: 58368   bits: 17/16
c ---[1596]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[1594]---> Sorter-cost:  470     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1592]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1590]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[1588]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1586]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1584]---> Sorter-cost:  576     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1582]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1580]---> Sorter-cost:  305     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1578]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1576]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1574]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1572]---> Sorter-cost:  259     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1570]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1568]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[1566]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1564]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1562]---> Adder-cost: 106   maxlim: 53248   bits: 17/16
c ---[1560]---> Sorter-cost: 1285     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1558]---> Sorter-cost:  716     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1556]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1554]---> Sorter-cost:  626     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1552]---> Sorter-cost:  989     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1550]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1548]---> Adder-cost: 106   maxlim: 52224   bits: 17/16
c ---[1546]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[1544]---> Adder-cost: 44   maxlim: 52224   bits: 17/16
c ---[1542]---> Sorter-cost:  971     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1540]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1538]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1536]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1534]---> Sorter-cost:  434     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1532]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1530]---> Sorter-cost:  327     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1528]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1526]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1524]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[1522]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1520]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1518]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1516]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1514]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1512]---> Sorter-cost:  269     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1510]---> Sorter-cost:  355     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1508]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1506]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[1504]---> Sorter-cost: 1271     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1502]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[1500]---> Adder-cost: 102   maxlim: 56320   bits: 17/16
c ---[1498]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[1496]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[1494]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[1492]---> Sorter-cost: 1303     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1490]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1488]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1486]---> Sorter-cost:  995     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1484]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1482]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1480]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1478]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1476]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1474]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1472]---> Adder-cost: 126   maxlim: 63488   bits: 17/16
c ---[1470]---> Adder-cost: 52   maxlim: 63488   bits: 17/16
c ---[1468]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1466]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1464]---> Sorter-cost:  283     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1462]---> Adder-cost: 146   maxlim: 69632   bits: 18/17
c ---[1460]---> Adder-cost: 118   maxlim: 61440   bits: 17/16
c ---[1458]---> Adder-cost: 104   maxlim: 61440   bits: 17/16
c ---[1456]---> Adder-cost: 50   maxlim: 61440   bits: 17/16
c ---[1454]---> Sorter-cost:  787     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1452]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1450]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1448]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1446]---> Sorter-cost:  583     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1444]---> Sorter-cost:  375     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1442]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1440]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1438]---> Sorter-cost:  718     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1436]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1434]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1432]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1430]---> Adder-cost: 116   maxlim: 57344   bits: 17/16
c ---[1428]---> Adder-cost: 52   maxlim: 57344   bits: 17/16
c ---[1426]---> Adder-cost: 98   maxlim: 51200   bits: 17/16
c ---[1424]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[1422]---> Sorter-cost: 1028     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1420]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1418]---> Adder-cost: 112   maxlim: 56320   bits: 17/16
c ---[1416]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[1414]---> Sorter-cost: 1028     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1412]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1410]---> Sorter-cost:  733     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1408]---> Sorter-cost:  581     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1406]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1404]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1402]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1400]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1398]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1396]---> Sorter-cost: 1143     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1394]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1392]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1390]---> Adder-cost: 106   maxlim: 51200   bits: 17/16
c ---[1388]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[1386]---> Sorter-cost: 1223     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1384]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1382]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1380]---> Adder-cost: 224   maxlim: 125952   bits: 18/17
c ---[1378]---> Adder-cost: 78   maxlim: 125952   bits: 18/17
c ---[1376]---> Adder-cost: 78   maxlim: 125952   bits: 18/17
c ---[1374]---> Adder-cost: 238   maxlim: 129024   bits: 18/17
c ---[1372]---> Adder-cost: 76   maxlim: 129024   bits: 18/17
c ---[1370]---> Adder-cost: 76   maxlim: 129024   bits: 18/17
c ---[1368]---> Adder-cost: 156   maxlim: 93184   bits: 18/17
c ---[1366]---> Adder-cost: 64   maxlim: 93184   bits: 18/17
c ---[1364]---> Adder-cost: 64   maxlim: 93184   bits: 18/17
c ---[1362]---> Adder-cost: 310   maxlim: 162816   bits: 19/18
c ---[1360]---> Adder-cost: 92   maxlim: 162816   bits: 19/18
c ---[1358]---> Adder-cost: 12031   maxlim: 6023167   bits: 24/23
c ---[1355]---> Adder-cost: 3128   maxlim: 1788928   bits: 22/21
c ---[1347]---> Adder-cost: 92   maxlim: 162816   bits: 19/18
c ---[1345]---> Adder-cost: 202   maxlim: 120832   bits: 18/17
c ---[1343]---> Adder-cost: 80   maxlim: 120832   bits: 18/17
c ---[1341]---> Adder-cost: 80   maxlim: 120832   bits: 18/17
c ---[1339]---> Adder-cost: 148   maxlim: 77824   bits: 18/17
c ---[1337]---> Adder-cost: 64   maxlim: 77824   bits: 18/17
c ---[1335]---> Adder-cost: 64   maxlim: 77824   bits: 18/17
c ---[1333]---> Sorter-cost:  638     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1331]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1329]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1327]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1325]---> Sorter-cost:  375     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1323]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1321]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1319]---> Sorter-cost: 1309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1317]---> Sorter-cost: 1154     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1315]---> Adder-cost: 104   maxlim: 52224   bits: 17/16
c ---[1313]---> Adder-cost: 44   maxlim: 52224   bits: 17/16
c ---[1311]---> Adder-cost: 142   maxlim: 71680   bits: 18/17
c ---[1309]---> Adder-cost: 60   maxlim: 71680   bits: 18/17
c ---[1307]---> Adder-cost: 92   maxlim: 54272   bits: 17/16
c ---[1305]---> Adder-cost: 46   maxlim: 54272   bits: 17/16
c ---[1303]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1301]---> Sorter-cost:  789     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1299]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1297]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1295]---> Adder-cost: 140   maxlim: 66560   bits: 18/17
c ---[1293]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[1291]---> Adder-cost: 106   maxlim: 57344   bits: 17/16
c ---[1289]---> Adder-cost: 52   maxlim: 57344   bits: 17/16
c ---[1287]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1285]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1283]---> Sorter-cost: 1226     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1281]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1279]---> Adder-cost: 148   maxlim: 71680   bits: 18/17
c ---[1277]---> Adder-cost: 60   maxlim: 71680   bits: 18/17
c ---[1275]---> Adder-cost: 142   maxlim: 72704   bits: 18/17
c ---[1273]---> Adder-cost: 56   maxlim: 72704   bits: 18/17
c ---[1271]---> Sorter-cost: 1263     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1269]---> Sorter-cost:  763     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1267]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1265]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1263]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1261]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1259]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1257]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1255]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1253]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1251]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1249]---> Sorter-cost: 1285     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1247]---> Sorter-cost: 1261     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1245]---> Adder-cost: 140   maxlim: 66560   bits: 18/17
c ---[1243]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[1241]---> Adder-cost: 150   maxlim: 78848   bits: 18/17
c ---[1239]---> Adder-cost: 138   maxlim: 75776   bits: 18/17
c ---[1237]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1235]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1233]---> Sorter-cost:  854     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1231]---> Sorter-cost: 1082     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1229]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1227]---> Sorter-cost:  617     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1225]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1223]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1221]---> Adder-cost: 240   maxlim: 139264   bits: 19/18
c ---[1219]---> Adder-cost: 94   maxlim: 139264   bits: 19/18
c ---[1217]---> Adder-cost: 94   maxlim: 139264   bits: 19/18
c ---[1215]---> Adder-cost: 326   maxlim: 186368   bits: 19/18
c ---[1213]---> Adder-cost: 106   maxlim: 186368   bits: 19/18
c ---[1211]---> Adder-cost: 106   maxlim: 186368   bits: 19/18
c ---[1209]---> Adder-cost: 290   maxlim: 168960   bits: 19/18
c ---[1207]---> Adder-cost: 100   maxlim: 168960   bits: 19/18
c ---[1205]---> Adder-cost: 100   maxlim: 168960   bits: 19/18
c ---[1203]---> Adder-cost: 276   maxlim: 161792   bits: 19/18
c ---[1201]---> Adder-cost: 92   maxlim: 161792   bits: 19/18
c ---[1199]---> Adder-cost: 92   maxlim: 161792   bits: 19/18
c ---[1197]---> Adder-cost: 92   maxlim: 161792   bits: 19/18
c ---[1195]---> Adder-cost: 92   maxlim: 161792   bits: 19/18
c ---[1193]---> Adder-cost: 92   maxlim: 161792   bits: 19/18
c ---[1191]---> Adder-cost: 216   maxlim: 122880   bits: 18/17
c ---[1189]---> Adder-cost: 80   maxlim: 122880   bits: 18/17
c ---[1187]---> Adder-cost: 80   maxlim: 122880   bits: 18/17
c ---[1185]---> Adder-cost: 80   maxlim: 122880   bits: 18/17
c ---[1183]---> Adder-cost: 80   maxlim: 122880   bits: 18/17
c ---[1181]---> Adder-cost: 80   maxlim: 122880   bits: 18/17
c ---[1179]---> Adder-cost: 166   maxlim: 92160   bits: 18/17
c ---[1177]---> Adder-cost: 66   maxlim: 92160   bits: 18/17
c ---[1175]---> Adder-cost: 66   maxlim: 92160   bits: 18/17
c ---[1173]---> Adder-cost: 66   maxlim: 92160   bits: 18/17
c ---[1171]---> Adder-cost: 66   maxlim: 92160   bits: 18/17
c ---[1169]---> Adder-cost: 66   maxlim: 92160   bits: 18/17
c ---[1167]---> Sorter-cost:  269     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1165]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1163]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1161]---> Sorter-cost:  305     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1159]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1157]---> Sorter-cost:  454     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1155]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1153]---> Adder-cost: 118   maxlim: 57344   bits: 17/16
c ---[1151]---> Sorter-cost: 1265     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1149]---> Adder-cost: 98   maxlim: 57344   bits: 17/16
c ---[1147]---> Adder-cost: 52   maxlim: 57344   bits: 17/16
c ---[1145]---> Adder-cost: 118   maxlim: 58368   bits: 17/16
c ---[1143]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[1141]---> Sorter-cost: 1087     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1139]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1137]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1135]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1133]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1131]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1129]---> Sorter-cost:  438     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1127]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1125]---> Sorter-cost:  979     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1123]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1121]---> Adder-cost: 138   maxlim: 65536   bits: 18/17
c ---[1119]---> Adder-cost: 62   maxlim: 65536   bits: 18/17
c ---[1117]---> Adder-cost: 118   maxlim: 63488   bits: 17/16
c ---[1115]---> Adder-cost: 52   maxlim: 63488   bits: 17/16
c ---[1113]---> Sorter-cost:  787     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1111]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1109]---> Sorter-cost: 1267     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1107]---> Sorter-cost:  763     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1105]---> Sorter-cost:  908     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1103]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1101]---> Sorter-cost:  572     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1099]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1097]---> Sorter-cost:  733     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1095]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1093]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1091]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1089]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1087]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1085]---> Sorter-cost:  576     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1083]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1081]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1079]---> Sorter-cost: 1246     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1077]---> Sorter-cost: 1095     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1075]---> Adder-cost: 106   maxlim: 53248   bits: 17/16
c ---[1073]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[1071]---> Sorter-cost: 1213     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1069]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1067]---> Sorter-cost: 1077     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1065]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1063]---> Adder-cost: 148   maxlim: 74752   bits: 18/17
c ---[1061]---> Adder-cost: 60   maxlim: 74752   bits: 18/17
c ---[1059]---> Adder-cost: 60   maxlim: 74752   bits: 18/17
c ---[1057]---> Sorter-cost: 1135     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1055]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1053]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[1051]---> Adder-cost: 46   maxlim: 54272   bits: 17/16
c ---[1049]---> Adder-cost: 138   maxlim: 67584   bits: 18/17
c ---[1047]---> Adder-cost: 60   maxlim: 67584   bits: 18/17
c ---[1045]---> Sorter-cost: 1057     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1043]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1041]---> Sorter-cost: 1257     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1039]---> Sorter-cost:  763     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1037]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1035]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1033]---> Sorter-cost:  438     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1031]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1029]---> Sorter-cost:  456     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1027]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1025]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1023]---> Sorter-cost:  735     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1021]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1019]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1017]---> Sorter-cost:  937     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1015]---> Sorter-cost:  933     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1013]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[1011]---> Adder-cost: 46   maxlim: 54272   bits: 17/16
c ---[1009]---> Adder-cost: 136   maxlim: 68608   bits: 18/17
c ---[1007]---> Adder-cost: 58   maxlim: 68608   bits: 18/17
c ---[1005]---> Sorter-cost:  659     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1003]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1001]---> Adder-cost: 122   maxlim: 61440   bits: 17/16
c ---[ 999]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[ 997]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 995]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 993]---> Sorter-cost:  583     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 991]---> Sorter-cost:  650     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 989]---> Sorter-cost: 1115     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 987]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 985]---> Adder-cost: 104   maxlim: 52224   bits: 17/16
c ---[ 983]---> Sorter-cost: 1259     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 981]---> Sorter-cost: 1059     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 979]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 977]---> Sorter-cost:  648     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 975]---> Sorter-cost:  530     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 973]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 971]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 969]---> Sorter-cost: 1057     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 967]---> Sorter-cost:  929     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 965]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 963]---> Sorter-cost:  910     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 961]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 959]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 957]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 955]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 953]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 951]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 949]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 947]---> Sorter-cost:  640     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 945]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 943]---> Sorter-cost: 1240     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 941]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 939]---> Adder-cost: 118   maxlim: 59392   bits: 17/16
c ---[ 937]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[ 935]---> Sorter-cost:  680     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 933]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 931]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 929]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 927]---> Sorter-cost:  700     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 925]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 923]---> Sorter-cost:  576     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 921]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 919]---> Sorter-cost:  390     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 917]---> Sorter-cost:  991     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 915]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 913]---> Sorter-cost:  977     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 911]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 909]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 907]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 905]---> Sorter-cost: 1287     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 903]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 901]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 899]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 897]---> Sorter-cost:  718     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 895]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 893]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[ 891]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[ 889]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 887]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 885]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 883]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 881]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 879]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 877]---> Sorter-cost:  729     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 875]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 873]---> Sorter-cost:  670     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 871]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 869]---> Sorter-cost:  546     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 867]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 865]---> Adder-cost: 108   maxlim: 53248   bits: 17/16
c ---[ 863]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[ 861]---> Adder-cost: 102   maxlim: 56320   bits: 17/16
c ---[ 859]---> Sorter-cost: 1269     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 857]---> Adder-cost: 166   maxlim: 82944   bits: 18/17
c ---[ 855]---> Adder-cost: 174   maxlim: 88064   bits: 18/17
c ---[ 853]---> Sorter-cost:  787     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 851]---> Sorter-cost:  684     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 849]---> Sorter-cost:  692     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 847]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 845]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 843]---> Sorter-cost:  641     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 841]---> Adder-cost: 112   maxlim: 56320   bits: 17/16
c ---[ 839]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[ 837]---> Sorter-cost: 1305     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 835]---> Sorter-cost: 1247     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 833]---> Sorter-cost: 1285     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 831]---> Sorter-cost: 1255     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 829]---> Sorter-cost:  688     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 827]---> Sorter-cost:  771     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 825]---> Sorter-cost:  995     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 823]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 821]---> Sorter-cost:  697     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 819]---> Sorter-cost:  879     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 817]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 815]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 813]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 811]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 809]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 807]---> Sorter-cost: 1271     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 805]---> Sorter-cost:  763     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 803]---> Adder-cost: 108   maxlim: 53248   bits: 17/16
c ---[ 801]---> Sorter-cost:  735     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 799]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 797]---> Sorter-cost:  574     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 795]---> Sorter-cost:  781     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 793]---> Sorter-cost: 1245     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 791]---> Sorter-cost:  763     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 789]---> Sorter-cost:  422     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 787]---> Sorter-cost:  468     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 785]---> Adder-cost: 124   maxlim: 63488   bits: 17/16
c ---[ 783]---> Adder-cost: 52   maxlim: 63488   bits: 17/16
c ---[ 781]---> Sorter-cost:  692     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 779]---> Sorter-cost:  646     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 777]---> Sorter-cost:  775     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 775]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 773]---> Sorter-cost: 1123     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 771]---> Sorter-cost: 1048     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 769]---> Sorter-cost:  591     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 767]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 765]---> Sorter-cost: 1135     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 763]---> Sorter-cost: 1050     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 761]---> Sorter-cost:  680     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 759]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 757]---> Sorter-cost:  969     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 755]---> Sorter-cost:  649     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 753]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 751]---> Sorter-cost:  283     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 749]---> Sorter-cost:  369     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 747]---> Adder-cost: 132   maxlim: 67584   bits: 18/17
c ---[ 745]---> Adder-cost: 60   maxlim: 67584   bits: 18/17
c ---[ 743]---> Adder-cost: 60   maxlim: 67584   bits: 18/17
c ---[ 741]---> Sorter-cost: 1024     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 739]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 737]---> Sorter-cost: 1279     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 735]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 733]---> Sorter-cost: 1149     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 731]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 729]---> Sorter-cost: 1219     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 727]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 725]---> Sorter-cost: 1180     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 723]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 721]---> Adder-cost: 150   maxlim: 75776   bits: 18/17
c ---[ 719]---> Adder-cost: 64   maxlim: 75776   bits: 18/17
c ---[ 717]---> Adder-cost: 156   maxlim: 78848   bits: 18/17
c ---[ 715]---> Adder-cost: 60   maxlim: 78848   bits: 18/17
c ---[ 713]---> Sorter-cost:  971     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 711]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 709]---> Sorter-cost: 1263     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 707]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 705]---> Adder-cost: 118   maxlim: 61440   bits: 17/16
c ---[ 703]---> Adder-cost: 50   maxlim: 61440   bits: 17/16
c ---[ 701]---> Sorter-cost: 1307     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 699]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 697]---> Sorter-cost: 1265     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 695]---> Sorter-cost:  763     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 693]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 691]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 689]---> Sorter-cost:  688     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 687]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 685]---> Sorter-cost:  668     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 683]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 681]---> Sorter-cost:  775     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 679]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 677]---> Sorter-cost:  640     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 675]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 673]---> Sorter-cost:  935     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 671]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 669]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 667]---> Sorter-cost:  559     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 665]---> Adder-cost: 174   maxlim: 91136   bits: 18/17
c ---[ 663]---> Adder-cost: 72   maxlim: 91136   bits: 18/17
c ---[ 661]---> Adder-cost: 190   maxlim: 101376   bits: 18/17
c ---[ 659]---> Adder-cost: 348   maxlim: 198656   bits: 19/18
c ---[ 657]---> Adder-cost: 116   maxlim: 198656   bits: 19/18
c ---[ 655]---> Adder-cost: 332   maxlim: 191488   bits: 19/18
c ---[ 653]---> Adder-cost: 104   maxlim: 191488   bits: 19/18
c ---[ 651]---> Adder-cost: 334   maxlim: 198656   bits: 19/18
c ---[ 649]---> Adder-cost: 116   maxlim: 198656   bits: 19/18
c ---[ 647]---> Adder-cost: 350   maxlim: 237568   bits: 19/18
c ---[ 645]---> Adder-cost: 128   maxlim: 237568   bits: 19/18
c ---[ 643]---> Adder-cost: 352   maxlim: 195584   bits: 19/18
c ---[ 641]---> Adder-cost: 108   maxlim: 195584   bits: 19/18
c ---[ 639]---> Adder-cost: 314   maxlim: 197632   bits: 19/18
c ---[ 637]---> Adder-cost: 330   maxlim: 196608   bits: 19/18
c ---[ 635]---> Adder-cost: 522   maxlim: 296960   bits: 20/19
c ---[ 633]---> Adder-cost: 512   maxlim: 292864   bits: 20/19
c ---[ 631]---> Adder-cost: 390   maxlim: 226304   bits: 19/18
c ---[ 629]---> Adder-cost: 498   maxlim: 291840   bits: 20/19
c ---[ 627]---> Adder-cost: 426   maxlim: 252928   bits: 19/18
c ---[ 625]---> Adder-cost: 434   maxlim: 259072   bits: 19/18
c ---[ 623]---> Adder-cost: 390   maxlim: 233472   bits: 19/18
c ---[ 621]---> Adder-cost: 320   maxlim: 200704   bits: 19/18
c ---[ 619]---> Adder-cost: 346   maxlim: 201728   bits: 19/18
c ---[ 617]---> Adder-cost: 114   maxlim: 201728   bits: 19/18
c ---[ 615]---> Adder-cost: 432   maxlim: 266240   bits: 20/19
c ---[ 613]---> Adder-cost: 142   maxlim: 266240   bits: 20/19
c ---[ 611]---> Adder-cost: 398   maxlim: 259072   bits: 19/18
c ---[ 609]---> Adder-cost: 124   maxlim: 259072   bits: 19/18
c ---[ 607]---> Adder-cost: 360   maxlim: 216064   bits: 19/18
c ---[ 605]---> Adder-cost: 116   maxlim: 216064   bits: 19/18
c ---[ 603]---> Adder-cost: 248   maxlim: 149504   bits: 19/18
c ---[ 601]---> Adder-cost: 92   maxlim: 149504   bits: 19/18
c ---[ 599]---> Adder-cost: 92   maxlim: 149504   bits: 19/18
c ---[ 597]---> Adder-cost: 92   maxlim: 149504   bits: 19/18
c ---[ 595]---> Adder-cost: 160   maxlim: 90112   bits: 18/17
c ---[ 593]---> Adder-cost: 72   maxlim: 90112   bits: 18/17
c ---[ 591]---> Adder-cost: 138   maxlim: 84992   bits: 18/17
c ---[ 589]---> Adder-cost: 68   maxlim: 84992   bits: 18/17
c ---[ 587]---> Adder-cost: 68   maxlim: 84992   bits: 18/17
c ---[ 585]---> Adder-cost: 68   maxlim: 84992   bits: 18/17
c ---[ 583]---> Adder-cost: 104   maxlim: 77824   bits: 18/17
c ---[ 581]---> Adder-cost: 64   maxlim: 77824   bits: 18/17
c ---[ 579]---> Adder-cost: 64   maxlim: 77824   bits: 18/17
c ---[ 577]---> Adder-cost: 64   maxlim: 77824   bits: 18/17
c ---[ 575]---> Adder-cost: 104   maxlim: 62464   bits: 17/16
c ---[ 573]---> Adder-cost: 48   maxlim: 62464   bits: 17/16
c ---[ 571]---> Adder-cost: 48   maxlim: 62464   bits: 17/16
c ---[ 569]---> Adder-cost: 48   maxlim: 62464   bits: 17/16
c ---[ 567]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 565]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 563]---> Sorter-cost:  933     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 561]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 559]---> Sorter-cost:  572     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 557]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 555]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 553]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 551]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 549]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 547]---> Sorter-cost:  704     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 545]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 543]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 541]---> Sorter-cost:  787     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 539]---> Sorter-cost:  877     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 537]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 535]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 533]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[ 531]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[ 529]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 527]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 525]---> Adder-cost: 106   maxlim: 51200   bits: 17/16
c ---[ 523]---> Adder-cost: 102   maxlim: 54272   bits: 17/16
c ---[ 521]---> Adder-cost: 170   maxlim: 86016   bits: 18/17
c ---[ 519]---> Adder-cost: 66   maxlim: 86016   bits: 18/17
c ---[ 517]---> Adder-cost: 164   maxlim: 83968   bits: 18/17
c ---[ 515]---> Adder-cost: 144   maxlim: 79872   bits: 18/17
c ---[ 513]---> Adder-cost: 122   maxlim: 62464   bits: 17/16
c ---[ 511]---> Adder-cost: 48   maxlim: 62464   bits: 17/16
c ---[ 509]---> Sorter-cost:  267     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 507]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 505]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 503]---> Sorter-cost: 1183     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 501]---> Sorter-cost: 1023     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 499]---> Sorter-cost: 1271     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 497]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 495]---> Adder-cost: 104   maxlim: 51200   bits: 17/16
c ---[ 493]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[ 491]---> Sorter-cost:  568     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 489]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 487]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 485]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 483]---> Sorter-cost:  654     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 481]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 479]---> Sorter-cost:  989     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 477]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 475]---> Sorter-cost: 1309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 473]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 471]---> Adder-cost: 106   maxlim: 52224   bits: 17/16
c ---[ 469]---> Adder-cost: 44   maxlim: 52224   bits: 17/16
c ---[ 467]---> Adder-cost: 118   maxlim: 59392   bits: 17/16
c ---[ 465]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[ 463]---> Adder-cost: 134   maxlim: 66560   bits: 18/17
c ---[ 461]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[ 459]---> Sorter-cost: 1285     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 457]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 455]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 453]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 451]---> Adder-cost: 154   maxlim: 75776   bits: 18/17
c ---[ 449]---> Adder-cost: 64   maxlim: 75776   bits: 18/17
c ---[ 447]---> Adder-cost: 154   maxlim: 80896   bits: 18/17
c ---[ 445]---> Adder-cost: 62   maxlim: 80896   bits: 18/17
c ---[ 443]---> Adder-cost: 140   maxlim: 65536   bits: 18/17
c ---[ 441]---> Adder-cost: 62   maxlim: 65536   bits: 18/17
c ---[ 439]---> Adder-cost: 160   maxlim: 80896   bits: 18/17
c ---[ 437]---> Adder-cost: 62   maxlim: 80896   bits: 18/17
c ---[ 435]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 433]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 431]---> Sorter-cost:  305     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 429]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 425]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 423]---> Sorter-cost:  985     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 421]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 419]---> Sorter-cost:  947     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 417]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 415]---> Sorter-cost:  921     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 413]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 411]---> Adder-cost: 140   maxlim: 65536   bits: 18/17
c ---[ 409]---> Adder-cost: 62   maxlim: 65536   bits: 18/17
c ---[ 407]---> Adder-cost: 62   maxlim: 65536   bits: 18/17
c ---[ 405]---> Sorter-cost:  632     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 403]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 401]---> Sorter-cost:  676     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 399]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 397]---> Adder-cost: 118   maxlim: 58368   bits: 17/16
c ---[ 395]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[ 393]---> Sorter-cost: 1223     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 391]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 389]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[ 387]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[ 385]---> Adder-cost: 142   maxlim: 67584   bits: 18/17
c ---[ 383]---> Adder-cost: 60   maxlim: 67584   bits: 18/17
c ---[ 381]---> Adder-cost: 138   maxlim: 71680   bits: 18/17
c ---[ 379]---> Adder-cost: 60   maxlim: 71680   bits: 18/17
c ---[ 377]---> Sorter-cost:  593     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 375]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 373]---> Sorter-cost:  267     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> Adder-cost: 114   maxlim: 63488   bits: 17/16
c ---[ 369]---> Adder-cost: 52   maxlim: 63488   bits: 17/16
c ---[ 367]---> Sorter-cost: 1303     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 365]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 363]---> Sorter-cost:  464     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 361]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 359]---> Sorter-cost:  609     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 357]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 355]---> Adder-cost: 108   maxlim: 53248   bits: 17/16
c ---[ 353]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[ 351]---> Adder-cost: 116   maxlim: 57344   bits: 17/16
c ---[ 349]---> Adder-cost: 52   maxlim: 57344   bits: 17/16
c ---[ 347]---> Adder-cost: 138   maxlim: 66560   bits: 18/17
c ---[ 345]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[ 343]---> Sorter-cost: 1251     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 341]---> Sorter-cost:  763     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 339]---> Adder-cost: 110   maxlim: 56320   bits: 17/16
c ---[ 337]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[ 335]---> Adder-cost: 164   maxlim: 82944   bits: 18/17
c ---[ 333]---> Adder-cost: 68   maxlim: 82944   bits: 18/17
c ---[ 331]---> Adder-cost: 146   maxlim: 76800   bits: 18/17
c ---[ 329]---> Adder-cost: 62   maxlim: 76800   bits: 18/17
c ---[ 327]---> Adder-cost: 108   maxlim: 53248   bits: 17/16
c ---[ 325]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[ 323]---> Adder-cost: 114   maxlim: 57344   bits: 17/16
c ---[ 321]---> Adder-cost: 52   maxlim: 57344   bits: 17/16
c ---[ 319]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[ 317]---> Adder-cost: 46   maxlim: 54272   bits: 17/16
c ---[ 315]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 313]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 311]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 309]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 307]---> Sorter-cost:  649     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 305]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 303]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 301]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 299]---> Sorter-cost:  714     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 297]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 295]---> Sorter-cost:  860     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 293]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 291]---> Adder-cost: 228   maxlim: 117760   bits: 18/17
c ---[ 289]---> Adder-cost: 76   maxlim: 117760   bits: 18/17
c ---[ 287]---> Adder-cost: 76   maxlim: 117760   bits: 18/17
c ---[ 285]---> Sorter-cost: 1085     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 283]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 281]---> Sorter-cost:  662     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 279]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 277]---> Sorter-cost: 1186     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 275]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 273]---> Adder-cost: 116   maxlim: 60416   bits: 17/16
c ---[ 271]---> Adder-cost: 48   maxlim: 60416   bits: 17/16
c ---[ 269]---> Sorter-cost:  989     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 267]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 265]---> Sorter-cost:  917     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 263]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 261]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 259]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 257]---> Sorter-cost:  959     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 255]---> Sorter-cost: 1238     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 253]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 251]---> Adder-cost: 138   maxlim: 68608   bits: 18/17
c ---[ 249]---> Adder-cost: 126   maxlim: 69632   bits: 18/17
c ---[ 247]---> Adder-cost: 130   maxlim: 71680   bits: 18/17
c ---[ 245]---> Adder-cost: 60   maxlim: 71680   bits: 18/17
c ---[ 243]---> Sorter-cost:  632     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 241]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 239]---> Sorter-cost:  661     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 237]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 235]---> Adder-cost: 118   maxlim: 58368   bits: 17/16
c ---[ 233]---> Adder-cost: 92   maxlim: 55296   bits: 17/16
c ---[ 231]---> Sorter-cost: 1307     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 229]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 227]---> Sorter-cost: 1149     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 225]---> Sorter-cost: 1123     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 223]---> Sorter-cost: 1136     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 221]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 219]---> Adder-cost: 104   maxlim: 51200   bits: 17/16
c ---[ 217]---> Adder-cost: 82   maxlim: 54272   bits: 17/16
c ---[ 215]---> Sorter-cost:  682     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 213]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 211]---> Sorter-cost:  904     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 209]---> Sorter-cost:  739     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 207]---> Sorter-cost:  945     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 205]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 203]---> Sorter-cost: 1024     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 201]---> Sorter-cost:  945     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 199]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 197]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 195]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 193]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 191]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 189]---> Adder-cost: 176   maxlim: 90112   bits: 18/17
c ---[ 187]---> Adder-cost: 104   maxlim: 91136   bits: 18/17
c ---[ 185]---> Sorter-cost:  716     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 183]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 181]---> Sorter-cost:  464     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 179]---> Sorter-cost:  438     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 177]---> Sorter-cost: 1074     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 175]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 173]---> Adder-cost: 104   maxlim: 51200   bits: 17/16
c ---[ 171]---> Sorter-cost: 1271     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 169]---> Adder-cost: 140   maxlim: 71680   bits: 18/17
c ---[ 167]---> Adder-cost: 60   maxlim: 71680   bits: 18/17
c ---[ 165]---> Adder-cost: 110   maxlim: 57344   bits: 17/16
c ---[ 163]---> Adder-cost: 86   maxlim: 58368   bits: 17/16
c ---[ 161]---> Adder-cost: 106   maxlim: 51200   bits: 17/16
c ---[ 159]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[ 157]---> Adder-cost: 118   maxlim: 57344   bits: 17/16
c ---[ 155]---> Sorter-cost: 1309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 153]---> Sorter-cost:  659     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 151]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 149]---> Sorter-cost:  572     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 147]---> Sorter-cost:  416     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 145]---> Sorter-cost:  435     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 143]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 141]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 139]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 137]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 135]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 133]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 131]---> Sorter-cost:  587     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 129]---> Sorter-cost:  659     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 127]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 125]---> Adder-cost: 106   maxlim: 52224   bits: 17/16
c ---[ 123]---> Adder-cost: 44   maxlim: 52224   bits: 17/16
c ---[ 121]---> Sorter-cost:  937     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 119]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 117]---> Sorter-cost:  787     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 115]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 113]---> Adder-cost: 118   maxlim: 57344   bits: 17/16
c ---[ 111]---> Adder-cost: 52   maxlim: 57344   bits: 17/16
c ---[ 109]---> Sorter-cost: 1028     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 107]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 105]---> Sorter-cost:  739     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 103]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[ 101]---> Sorter-cost:  933     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  99]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  97]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  95]---> Sorter-cost: 1028     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  93]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  91]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  89]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  87]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  85]---> Adder-cost: 110   maxlim: 55296   bits: 17/16
c ---[  83]---> Adder-cost: 48   maxlim: 55296   bits: 17/16
c ---[  81]---> Sorter-cost: 1285     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  79]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  77]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  75]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  73]---> Sorter-cost:  995     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  71]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  69]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  67]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  65]---> Sorter-cost:  735     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  63]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  61]---> Adder-cost: 112   maxlim: 58368   bits: 17/16
c ---[  59]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[  57]---> Adder-cost: 118   maxlim: 57344   bits: 17/16
c ---[  55]---> Adder-cost: 52   maxlim: 57344   bits: 17/16
c ---[  53]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  51]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  49]---> Sorter-cost:  647     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  47]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  45]---> Sorter-cost:  638     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[  43]---> Sorter-cost:  476     Base: 2 2 2 2 2 /oldhome/oroussel/solvers/minisat+_script: line 16: 16714 Segmentation fault      $XDIR/minisat+_bignum_static* "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.98 0.96 2/54 16709
Raw data (stat): 16709 (runsolver) R 16708 1269 1268 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783767090 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.94 0.98 0.96 2/55 16714
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.002 s]
Raw data (loadavg): 0.95 0.98 0.96 2/55 16714
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.0018 s]
Raw data (loadavg): 0.95 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.0019 s]
Raw data (loadavg): 0.96 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.0021 s]
Raw data (loadavg): 0.97 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.0018 s]
Raw data (loadavg): 0.97 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.0024 s]
Raw data (loadavg): 0.97 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.0031 s]
Raw data (loadavg): 0.98 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.0028 s]
Raw data (loadavg): 0.98 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.004 s]
Raw data (loadavg): 0.98 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.004 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.005 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.004 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.004 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.012 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.012 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.023 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.031 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.031 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.031 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.031 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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.829 s]
Raw data (loadavg): 0.99 0.98 0.96 1/53 16716
Raw data (stat): 16709 (minisat+_script) S 16708 1269 1268 0 -1 0 300 668 0 0 0 0 6 2 17 0 1 0 783767090 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: 139
Real time (s): 850.829
CPU time (s): 848.858
CPU user time (s): 841.883
CPU system time (s): 6.97494
CPU usage (%): 99.7684
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####