PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-siena1.opb
MD5SUM	8330cc07523804a723f9a9440606c313
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	51095
Biggest coefficient in the objective function	524288000000000000
Number of bits for the biggest coefficient in the objective function	59
Sum of the numbers in the objective function	27564135378019700736
Number of bits of the sum of numbers in the objective function	65
Biggest number in a constraint	524288000000000000
Number of bits of the biggest number in a constraint	59
Biggest sum of numbers in a constraint	27576935378019700736
Number of bits of the biggest sum of numbers	65
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.502923
Number of variables	51095
Total number of constraints	13995
Number of constraints which are clauses	310
Number of constraints which are cardinality constraints (but not clauses)	11776
Number of constraints which are nor clauses,nor cardinality constraints	1909
Minimum length of a constraint	1
Maximum length of a constraint	51095
Trace number 31332

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        804692 kB
Buffers:         31304 kB
Cached:         177128 kB
SwapCached:        396 kB
Active:          25196 kB
Inactive:       185500 kB
HighTotal:      131008 kB
HighFree:        55104 kB
LowTotal:       903652 kB
LowFree:        749588 kB
SwapTotal:     2097136 kB
SwapFree:      2096076 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            13436 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:36:44 (client local time) WITH STATUS 139 IN 957.337 SECONDS
stats: 22740 7 957.337 139
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c PARSE ERROR! [line 13745] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 4027 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #########################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################=#######################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................sssssssssssssssssssssssssssssss...............................
c ---[4056]---> Adder-cost: 154   maxlim: 9216   bits: 15/14
c ---[4054]---> Adder-cost: 172   maxlim: 10624   bits: 15/14
c ---[4052]---> Adder-cost: 308   maxlim: 19200   bits: 16/15
c ---[4050]---> Adder-cost: 212   maxlim: 16256   bits: 15/14
c ---[4047]---> Adder-cost: 120   maxlim: 7552   bits: 14/13
c ---[4045]---> Adder-cost: 84   maxlim: 8064   bits: 14/13
c ---[4043]---> Adder-cost: 106   maxlim: 8064   bits: 14/13
c ---[4041]---> Adder-cost: 120   maxlim: 8192   bits: 15/14
c ---[4039]---> Adder-cost: 112   maxlim: 7296   bits: 14/13
c ---[4037]---> Adder-cost: 92   maxlim: 6272   bits: 14/13
c ---[4035]---> Adder-cost: 102   maxlim: 10752   bits: 15/14
c ---[4033]---> Adder-cost: 84   maxlim: 5760   bits: 14/13
c ---[4031]---> Adder-cost: 78   maxlim: 5760   bits: 14/13
c ---[4029]---> Adder-cost: 182   maxlim: 12160   bits: 15/14
c ---[4027]---> Adder-cost: 190   maxlim: 12288   bits: 15/14
c ---[4025]---> Adder-cost: 176   maxlim: 12672   bits: 15/14
c ---[4023]---> Adder-cost: 122   maxlim: 11136   bits: 15/14
c ---[4021]---> Adder-cost: 154   maxlim: 11136   bits: 15/14
c ---[4019]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[4017]---> Adder-cost: 148   maxlim: 12032   bits: 15/14
c ---[4015]---> Adder-cost: 150   maxlim: 11520   bits: 15/14
c ---[4013]---> Adder-cost: 90   maxlim: 5760   bits: 14/13
c ---[4011]---> Adder-cost: 82   maxlim: 5888   bits: 14/13
c ---[4009]---> Adder-cost: 166   maxlim: 11008   bits: 15/14
c ---[4007]---> Adder-cost: 186   maxlim: 11648   bits: 15/14
c ---[4005]---> Adder-cost: 134   maxlim: 11648   bits: 15/14
c ---[4003]---> Adder-cost: 108   maxlim: 9600   bits: 15/14
c ---[4000]---> Adder-cost: 166   maxlim: 13440   bits: 15/14
c ---[3998]---> Adder-cost: 200   maxlim: 13312   bits: 15/14
c ---[3996]---> Adder-cost: 256   maxlim: 18432   bits: 16/15
c ---[3994]---> Adder-cost: 248   maxlim: 18688   bits: 16/15
c ---[3992]---> Adder-cost: 216   maxlim: 19840   bits: 16/15
c ---[3990]---> Adder-cost: 236   maxlim: 20096   bits: 16/15
c ---[3988]---> Adder-cost: 210   maxlim: 20608   bits: 16/15
c ---[3986]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[3984]---> Adder-cost: 100   maxlim: 20608   bits: 16/15
c ---[3982]---> Adder-cost: 316   maxlim: 24960   bits: 16/15
c ---[3980]---> Adder-cost: 288   maxlim: 21888   bits: 16/15
c ---[3978]---> Adder-cost: 200   maxlim: 20608   bits: 16/15
c ---[3976]---> Adder-cost: 224   maxlim: 16384   bits: 16/15
c ---[3974]---> Adder-cost: 194   maxlim: 13824   bits: 15/14
c ---[3972]---> Adder-cost: 158   maxlim: 10880   bits: 15/14
c ---[3970]---> Adder-cost: 144   maxlim: 10240   bits: 15/14
c ---[3968]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[3966]---> Sorter-cost:  358     Base: 2 2 2 2 2 2 2 7
c ---[3964]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[3962]---> Adder-cost: 86   maxlim: 6144   bits: 14/13
c ---[3960]---> Adder-cost: 80   maxlim: 6272   bits: 14/13
c ---[3958]---> Adder-cost: 74   maxlim: 5760   bits: 14/13
c ---[3956]---> Adder-cost: 60   maxlim: 4864   bits: 14/13
c ---[3954]---> Adder-cost: 66   maxlim: 5760   bits: 14/13
c ---[3952]---> Adder-cost: 148   maxlim: 9344   bits: 15/14
c ---[3950]---> Adder-cost: 194   maxlim: 12800   bits: 15/14
c ---[3948]---> Adder-cost: 150   maxlim: 12672   bits: 15/14
c ---[3946]---> Adder-cost: 178   maxlim: 12032   bits: 15/14
c ---[3944]---> Adder-cost: 136   maxlim: 11520   bits: 15/14
c ---[3942]---> Adder-cost: 106   maxlim: 7808   bits: 14/13
c ---[3940]---> Adder-cost: 110   maxlim: 7168   bits: 14/13
c ---[3937]---> Adder-cost: 82   maxlim: 7296   bits: 14/13
c ---[3935]---> Adder-cost: 232   maxlim: 15616   bits: 15/14
c ---[3933]---> Adder-cost: 260   maxlim: 17664   bits: 16/15
c ---[3931]---> Adder-cost: 92   maxlim: 17664   bits: 16/15
c ---[3929]---> Adder-cost: 272   maxlim: 19200   bits: 16/15
c ---[3927]---> Adder-cost: 226   maxlim: 19584   bits: 16/15
c ---[3925]---> Adder-cost: 272   maxlim: 20224   bits: 16/15
c ---[3923]---> Adder-cost: 92   maxlim: 20224   bits: 16/15
c ---[3921]---> Adder-cost: 266   maxlim: 19968   bits: 16/15
c ---[3919]---> Adder-cost: 266   maxlim: 16384   bits: 16/15
c ---[3917]---> Adder-cost: 182   maxlim: 20352   bits: 16/15
c ---[3915]---> Adder-cost: 166   maxlim: 19968   bits: 16/15
c ---[3913]---> Adder-cost: 94   maxlim: 19968   bits: 16/15
c ---[3911]---> Adder-cost: 250   maxlim: 19712   bits: 16/15
c ---[3909]---> Adder-cost: 92   maxlim: 19712   bits: 16/15
c ---[3907]---> Adder-cost: 180   maxlim: 19584   bits: 16/15
c ---[3905]---> Adder-cost: 96   maxlim: 19584   bits: 16/15
c ---[3903]---> Adder-cost: 216   maxlim: 19456   bits: 16/15
c ---[3901]---> Adder-cost: 96   maxlim: 19456   bits: 16/15
c ---[3899]---> Adder-cost: 102   maxlim: 19584   bits: 16/15
c ---[3897]---> Adder-cost: 90   maxlim: 16384   bits: 16/15
c ---[3895]---> Adder-cost: 96   maxlim: 19584   bits: 16/15
c ---[3893]---> Adder-cost: 96   maxlim: 19584   bits: 16/15
c ---[3891]---> Adder-cost: 96   maxlim: 19584   bits: 16/15
c ---[3889]---> Adder-cost: 260   maxlim: 24064   bits: 16/15
c ---[3886]---> Adder-cost: 146   maxlim: 8704   bits: 15/14
c ---[3884]---> Adder-cost: 94   maxlim: 8832   bits: 15/14
c ---[3882]---> Adder-cost: 84   maxlim: 5120   bits: 14/13
c ---[3880]---> Adder-cost: 94   maxlim: 6016   bits: 14/13
c ---[3878]---> Adder-cost: 168   maxlim: 14848   bits: 15/14
c ---[3876]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[3874]---> Adder-cost: 100   maxlim: 6528   bits: 14/13
c ---[3872]---> Adder-cost: 96   maxlim: 6400   bits: 14/13
c ---[3870]---> Adder-cost: 156   maxlim: 9600   bits: 15/14
c ---[3868]---> Adder-cost: 136   maxlim: 9344   bits: 15/14
c ---[3865]---> Adder-cost: 98   maxlim: 7040   bits: 14/13
c ---[3863]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[3861]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[3859]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[3857]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[3855]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[3853]---> Adder-cost: 86   maxlim: 5120   bits: 14/13
c ---[3850]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[3848]---> Adder-cost: 104   maxlim: 7296   bits: 14/13
c ---[3846]---> Adder-cost: 74   maxlim: 7296   bits: 14/13
c ---[3844]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[3842]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[3840]---> Adder-cost: 80   maxlim: 5632   bits: 14/13
c ---[3838]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[3836]---> Adder-cost: 64   maxlim: 5632   bits: 14/13
c ---[3834]---> Adder-cost: 56   maxlim: 5760   bits: 14/13
c ---[3832]---> Adder-cost: 142   maxlim: 8576   bits: 15/14
c ---[3830]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[3828]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[3826]---> Adder-cost: 132   maxlim: 9216   bits: 15/14
c ---[3824]---> Adder-cost: 102   maxlim: 8960   bits: 15/14
c ---[3822]---> Adder-cost: 120   maxlim: 8576   bits: 15/14
c ---[3820]---> Adder-cost: 84   maxlim: 8960   bits: 15/14
c ---[3818]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[3816]---> Sorter-cost:  523     Base: 2 2 2 2 2 2 2 7
c ---[3814]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[3812]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 7
c ---[3810]---> Adder-cost: 204   maxlim: 12672   bits: 15/14
c ---[3808]---> Adder-cost: 118   maxlim: 12800   bits: 15/14
c ---[3806]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[3804]---> Adder-cost: 74   maxlim: 4992   bits: 14/13
c ---[3802]---> Adder-cost: 204   maxlim: 12672   bits: 15/14
c ---[3800]---> Adder-cost: 72   maxlim: 12672   bits: 15/14
c ---[3798]---> Adder-cost: 184   maxlim: 11776   bits: 15/14
c ---[3796]---> Adder-cost: 104   maxlim: 11904   bits: 15/14
c ---[3794]---> Adder-cost: 74   maxlim: 11776   bits: 15/14
c ---[3792]---> Adder-cost: 70   maxlim: 11776   bits: 15/14
c ---[3790]---> Adder-cost: 104   maxlim: 6144   bits: 14/13
c ---[3788]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[3785]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[3783]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[3781]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[3779]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[3777]---> Sorter-cost:  463     Base: 2 2 2 2 2 2 2 7
c ---[3775]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[3773]---> Adder-cost: 78   maxlim: 4992   bits: 14/13
c ---[3771]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[3769]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[3767]---> Adder-cost: 86   maxlim: 5504   bits: 14/13
c ---[3765]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 7
c ---[3763]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[3761]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[3759]---> Adder-cost: 154   maxlim: 9216   bits: 15/14
c ---[3756]---> Adder-cost: 62   maxlim: 6144   bits: 14/13
c ---[3753]---> Adder-cost: 170   maxlim: 10368   bits: 15/14
c ---[3751]---> Adder-cost: 140   maxlim: 8320   bits: 15/14
c ---[3749]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[3747]---> Adder-cost: 152   maxlim: 9856   bits: 15/14
c ---[3745]---> Adder-cost: 122   maxlim: 9984   bits: 15/14
c ---[3743]---> Adder-cost: 120   maxlim: 7808   bits: 14/13
c ---[3741]---> Adder-cost: 190   maxlim: 12032   bits: 15/14
c ---[3739]---> Adder-cost: 122   maxlim: 7936   bits: 14/13
c ---[3737]---> Adder-cost: 134   maxlim: 8320   bits: 15/14
c ---[3735]---> Adder-cost: 130   maxlim: 8192   bits: 15/14
c ---[3733]---> Adder-cost: 186   maxlim: 11520   bits: 15/14
c ---[3731]---> Adder-cost: 96   maxlim: 11648   bits: 15/14
c ---[3729]---> Adder-cost: 122   maxlim: 10880   bits: 15/14
c ---[3727]---> Adder-cost: 86   maxlim: 5120   bits: 14/13
c ---[3725]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[3723]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[3721]---> Adder-cost: 98   maxlim: 6528   bits: 14/13
c ---[3719]---> Adder-cost: 100   maxlim: 7424   bits: 14/13
c ---[3717]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[3715]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[3713]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[3711]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 7
c ---[3709]---> Sorter-cost:  308     Base: 2 2 2 2 2 2 2 2
c ---[3707]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[3705]---> Adder-cost: 270   maxlim: 16384   bits: 16/15
c ---[3702]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[3700]---> Adder-cost: 126   maxlim: 7936   bits: 14/13
c ---[3698]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[3696]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[3694]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[3692]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[3690]---> Sorter-cost:  601     Base: 2 2 2 2 2 2 2 7
c ---[3687]---> Adder-cost: 156   maxlim: 9600   bits: 15/14
c ---[3685]---> Adder-cost: 134   maxlim: 8448   bits: 15/14
c ---[3683]---> Adder-cost: 130   maxlim: 8576   bits: 15/14
c ---[3681]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[3679]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[3677]---> Adder-cost: 102   maxlim: 6400   bits: 14/13
c ---[3675]---> Adder-cost: 176   maxlim: 10880   bits: 15/14
c ---[3673]---> Adder-cost: 146   maxlim: 10368   bits: 15/14
c ---[3671]---> Adder-cost: 202   maxlim: 12288   bits: 15/14
c ---[3669]---> Adder-cost: 178   maxlim: 12416   bits: 15/14
c ---[3667]---> Adder-cost: 124   maxlim: 7808   bits: 14/13
c ---[3665]---> Adder-cost: 144   maxlim: 9984   bits: 15/14
c ---[3663]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[3661]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[3659]---> Adder-cost: 78   maxlim: 5760   bits: 14/13
c ---[3657]---> Adder-cost: 62   maxlim: 6144   bits: 14/13
c ---[3654]---> Adder-cost: 188   maxlim: 11904   bits: 15/14
c ---[3650]---> Adder-cost: 230   maxlim: 14336   bits: 15/14
c ---[3648]---> Adder-cost: 184   maxlim: 11904   bits: 15/14
c ---[3646]---> Adder-cost: 70   maxlim: 11904   bits: 15/14
c ---[3644]---> Adder-cost: 122   maxlim: 7680   bits: 14/13
c ---[3642]---> Adder-cost: 82   maxlim: 5248   bits: 14/13
c ---[3640]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[3638]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[3636]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[3634]---> Adder-cost: 78   maxlim: 7296   bits: 14/13
c ---[3632]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[3630]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[3628]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[3626]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 7
c ---[3624]---> Adder-cost: 160   maxlim: 9728   bits: 15/14
c ---[3622]---> Adder-cost: 118   maxlim: 8064   bits: 14/13
c ---[3620]---> Adder-cost: 124   maxlim: 8448   bits: 15/14
c ---[3618]---> Adder-cost: 96   maxlim: 7296   bits: 14/13
c ---[3616]---> Adder-cost: 184   maxlim: 11392   bits: 15/14
c ---[3614]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[3612]---> Adder-cost: 72   maxlim: 11392   bits: 15/14
c ---[3610]---> Adder-cost: 132   maxlim: 9472   bits: 15/14
c ---[3608]---> Adder-cost: 64   maxlim: 9472   bits: 15/14
c ---[3606]---> Adder-cost: 180   maxlim: 11904   bits: 15/14
c ---[3604]---> Adder-cost: 70   maxlim: 11904   bits: 15/14
c ---[3602]---> Adder-cost: 92   maxlim: 5632   bits: 14/13
c ---[3600]---> Adder-cost: 200   maxlim: 12288   bits: 15/14
c ---[3598]---> Adder-cost: 152   maxlim: 9856   bits: 15/14
c ---[3596]---> Adder-cost: 246   maxlim: 15488   bits: 15/14
c ---[3594]---> Adder-cost: 78   maxlim: 15488   bits: 15/14
c ---[3592]---> Adder-cost: 268   maxlim: 16896   bits: 16/15
c ---[3590]---> Adder-cost: 88   maxlim: 16896   bits: 16/15
c ---[3588]---> Adder-cost: 150   maxlim: 16256   bits: 15/14
c ---[3586]---> Adder-cost: 74   maxlim: 16256   bits: 15/14
c ---[3584]---> Adder-cost: 176   maxlim: 10880   bits: 15/14
c ---[3582]---> Adder-cost: 66   maxlim: 10880   bits: 15/14
c ---[3580]---> Adder-cost: 86   maxlim: 5760   bits: 14/13
c ---[3578]---> Adder-cost: 124   maxlim: 7680   bits: 14/13
c ---[3574]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[3572]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[3569]---> Adder-cost: 110   maxlim: 6656   bits: 14/13
c ---[3567]---> Adder-cost: 78   maxlim: 5376   bits: 14/13
c ---[3565]---> Adder-cost: 48   maxlim: 4480   bits: 14/13
c ---[3563]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[3561]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[3559]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[3557]---> Adder-cost: 60   maxlim: 5504   bits: 14/13
c ---[3555]---> Adder-cost: 40   maxlim: 5504   bits: 14/13
c ---[3553]---> Adder-cost: 126   maxlim: 8064   bits: 14/13
c ---[3551]---> Adder-cost: 124   maxlim: 7936   bits: 14/13
c ---[3549]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[3547]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[3545]---> Adder-cost: 96   maxlim: 6272   bits: 14/13
c ---[3543]---> Adder-cost: 104   maxlim: 6784   bits: 14/13
c ---[3541]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[3539]---> Sorter-cost:  687     Base: 2 2 2 2 2 2 2 7
c ---[3537]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[3535]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 7
c ---[3533]---> Sorter-cost: 1080     Base: 2 2 2 2 2 2 2 7
c ---[3531]---> Sorter-cost:  403     Base: 2 2 2 2 2 2 2 7
c ---[3529]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[3527]---> Adder-cost: 146   maxlim: 8832   bits: 15/14
c ---[3525]---> Adder-cost: 156   maxlim: 10624   bits: 15/14
c ---[3523]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[3521]---> Adder-cost: 156   maxlim: 11776   bits: 15/14
c ---[3519]---> Adder-cost: 156   maxlim: 11392   bits: 15/14
c ---[3517]---> Adder-cost: 72   maxlim: 11392   bits: 15/14
c ---[3515]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[3513]---> Adder-cost: 76   maxlim: 5632   bits: 14/13
c ---[3511]---> Adder-cost: 52   maxlim: 5760   bits: 14/13
c ---[3509]---> Adder-cost: 102   maxlim: 7040   bits: 14/13
c ---[3507]---> Adder-cost: 112   maxlim: 6912   bits: 14/13
c ---[3505]---> Adder-cost: 212   maxlim: 14208   bits: 15/14
c ---[3503]---> Adder-cost: 136   maxlim: 14720   bits: 15/14
c ---[3499]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[3497]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[3495]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[3493]---> Sorter-cost:  625     Base: 2 2 2 2 2 2 2 7
c ---[3491]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 2
c ---[3489]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[3487]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 7
c ---[3485]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 7
c ---[3483]---> Sorter-cost:  280     Base: 2 2 2 2 2 2 2 7
c ---[3481]---> Adder-cost: 146   maxlim: 8704   bits: 15/14
c ---[3479]---> Adder-cost: 146   maxlim: 8832   bits: 15/14
c ---[3475]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[3473]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[3471]---> Adder-cost: 110   maxlim: 7168   bits: 14/13
c ---[3468]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[3466]---> Adder-cost: 64   maxlim: 5632   bits: 14/13
c ---[3464]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[3462]---> Adder-cost: 110   maxlim: 7552   bits: 14/13
c ---[3460]---> Adder-cost: 48   maxlim: 7552   bits: 14/13
c ---[3458]---> Adder-cost: 90   maxlim: 5632   bits: 14/13
c ---[3456]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[3454]---> Adder-cost: 64   maxlim: 5888   bits: 14/13
c ---[3452]---> Adder-cost: 104   maxlim: 6912   bits: 14/13
c ---[3450]---> Adder-cost: 82   maxlim: 7424   bits: 14/13
c ---[3448]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[3446]---> Adder-cost: 126   maxlim: 8704   bits: 15/14
c ---[3444]---> Adder-cost: 62   maxlim: 8704   bits: 15/14
c ---[3442]---> Adder-cost: 100   maxlim: 6272   bits: 14/13
c ---[3440]---> Adder-cost: 54   maxlim: 5504   bits: 14/13
c ---[3438]---> Adder-cost: 86   maxlim: 5120   bits: 14/13
c ---[3436]---> Adder-cost: 52   maxlim: 4864   bits: 14/13
c ---[3434]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[3432]---> Adder-cost: 102   maxlim: 6784   bits: 14/13
c ---[3430]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[3428]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[3426]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[3424]---> Sorter-cost:  897     Base: 2 2 2 2 2 2 2 7
c ---[3422]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[3420]---> Adder-cost: 172   maxlim: 10624   bits: 15/14
c ---[3418]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[3416]---> Adder-cost: 120   maxlim: 7808   bits: 14/13
c ---[3414]---> Adder-cost: 68   maxlim: 7424   bits: 14/13
c ---[3412]---> Adder-cost: 104   maxlim: 7040   bits: 14/13
c ---[3410]---> Adder-cost: 82   maxlim: 7168   bits: 14/13
c ---[3408]---> Adder-cost: 146   maxlim: 8704   bits: 15/14
c ---[3406]---> Adder-cost: 126   maxlim: 8192   bits: 15/14
c ---[3404]---> Adder-cost: 110   maxlim: 6912   bits: 14/13
c ---[3402]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[3400]---> Adder-cost: 130   maxlim: 9216   bits: 15/14
c ---[3398]---> Adder-cost: 84   maxlim: 9088   bits: 15/14
c ---[3396]---> Adder-cost: 126   maxlim: 8832   bits: 15/14
c ---[3394]---> Adder-cost: 82   maxlim: 9216   bits: 15/14
c ---[3392]---> Adder-cost: 282   maxlim: 17664   bits: 16/15
c ---[3390]---> Adder-cost: 136   maxlim: 8576   bits: 15/14
c ---[3388]---> Adder-cost: 92   maxlim: 17664   bits: 16/15
c ---[3386]---> Adder-cost: 246   maxlim: 17024   bits: 16/15
c ---[3384]---> Adder-cost: 88   maxlim: 17024   bits: 16/15
c ---[3382]---> Adder-cost: 186   maxlim: 17152   bits: 16/15
c ---[3378]---> Adder-cost: 92   maxlim: 5760   bits: 14/13
c ---[3376]---> Adder-cost: 64   maxlim: 5632   bits: 14/13
c ---[3374]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[3372]---> Adder-cost: 182   maxlim: 11264   bits: 15/14
c ---[3370]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[3368]---> Sorter-cost:  720     Base: 2 2 2 2 2 2 2 7
c ---[3366]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 7
c ---[3364]---> Sorter-cost:  796     Base: 2 2 2 2 2 2 2 7
c ---[3362]---> Sorter-cost:  463     Base: 2 2 2 2 2 2 2 7
c ---[3360]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[3358]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[3356]---> Sorter-cost:  282     Base: 2 2 2 2 2 2 2 2
c ---[3354]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[3352]---> Adder-cost: 138   maxlim: 8192   bits: 15/14
c ---[3350]---> Sorter-cost:  905     Base: 2 2 2 2 2 2 2 7
c ---[3348]---> Sorter-cost: 1236     Base: 2 2 2 2 2 2 2 7
c ---[3346]---> Sorter-cost:  687     Base: 2 2 2 2 2 2 2 7
c ---[3344]---> Adder-cost: 154   maxlim: 9344   bits: 15/14
c ---[3342]---> Adder-cost: 134   maxlim: 8576   bits: 15/14
c ---[3340]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[3338]---> Adder-cost: 154   maxlim: 9984   bits: 15/14
c ---[3336]---> Adder-cost: 96   maxlim: 7296   bits: 14/13
c ---[3334]---> Adder-cost: 102   maxlim: 7424   bits: 14/13
c ---[3332]---> Adder-cost: 176   maxlim: 12416   bits: 15/14
c ---[3330]---> Adder-cost: 62   maxlim: 8192   bits: 15/14
c ---[3328]---> Adder-cost: 132   maxlim: 8832   bits: 15/14
c ---[3326]---> Adder-cost: 94   maxlim: 8960   bits: 15/14
c ---[3324]---> Adder-cost: 118   maxlim: 7936   bits: 14/13
c ---[3322]---> Adder-cost: 116   maxlim: 8064   bits: 14/13
c ---[3320]---> Adder-cost: 94   maxlim: 7040   bits: 14/13
c ---[3318]---> Adder-cost: 126   maxlim: 8320   bits: 15/14
c ---[3316]---> Adder-cost: 144   maxlim: 9344   bits: 15/14
c ---[3314]---> Adder-cost: 182   maxlim: 12544   bits: 15/14
c ---[3312]---> Adder-cost: 164   maxlim: 12544   bits: 15/14
c ---[3310]---> Adder-cost: 148   maxlim: 12160   bits: 15/14
c ---[3308]---> Adder-cost: 124   maxlim: 8448   bits: 15/14
c ---[3306]---> Adder-cost: 116   maxlim: 7936   bits: 14/13
c ---[3304]---> Adder-cost: 106   maxlim: 7424   bits: 14/13
c ---[3302]---> Adder-cost: 90   maxlim: 5632   bits: 14/13
c ---[3300]---> Adder-cost: 54   maxlim: 5632   bits: 14/13
c ---[3298]---> Adder-cost: 72   maxlim: 4480   bits: 14/13
c ---[3296]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[3294]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[3292]---> Sorter-cost:  449     Base: 2 2 2 2 2 2 2 7
c ---[3290]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 7
c ---[3288]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[3286]---> Sorter-cost:  486     Base: 2 2 2 2 2 2 2 7
c ---[3284]---> Adder-cost: 142   maxlim: 8704   bits: 15/14
c ---[3282]---> Adder-cost: 210   maxlim: 13696   bits: 15/14
c ---[3280]---> Adder-cost: 78   maxlim: 13696   bits: 15/14
c ---[3278]---> Adder-cost: 200   maxlim: 13312   bits: 15/14
c ---[3275]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[3272]---> Adder-cost: 202   maxlim: 12672   bits: 15/14
c ---[3270]---> Adder-cost: 92   maxlim: 8832   bits: 15/14
c ---[3268]---> Adder-cost: 160   maxlim: 12800   bits: 15/14
c ---[3266]---> Adder-cost: 76   maxlim: 12800   bits: 15/14
c ---[3263]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[3261]---> Sorter-cost:  438     Base: 2 2 2 2 2 2 2 7
c ---[3259]---> Sorter-cost:  256     Base: 2 2 2 2 2 2 2 2
c ---[3257]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[3255]---> Adder-cost: 160   maxlim: 10752   bits: 15/14
c ---[3253]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[3251]---> Adder-cost: 114   maxlim: 9856   bits: 15/14
c ---[3249]---> Adder-cost: 170   maxlim: 10240   bits: 15/14
c ---[3247]---> Adder-cost: 100   maxlim: 6144   bits: 14/13
c ---[3245]---> Adder-cost: 58   maxlim: 6016   bits: 14/13
c ---[3243]---> Adder-cost: 100   maxlim: 6912   bits: 14/13
c ---[3241]---> Adder-cost: 150   maxlim: 9600   bits: 15/14
c ---[3239]---> Adder-cost: 92   maxlim: 9728   bits: 15/14
c ---[3237]---> Adder-cost: 154   maxlim: 9984   bits: 15/14
c ---[3235]---> Adder-cost: 138   maxlim: 8576   bits: 15/14
c ---[3233]---> Adder-cost: 192   maxlim: 12160   bits: 15/14
c ---[3231]---> Adder-cost: 160   maxlim: 12928   bits: 15/14
c ---[3229]---> Adder-cost: 150   maxlim: 12160   bits: 15/14
c ---[3227]---> Adder-cost: 64   maxlim: 12160   bits: 15/14
c ---[3225]---> Adder-cost: 108   maxlim: 11904   bits: 15/14
c ---[3221]---> Adder-cost: 218   maxlim: 13696   bits: 15/14
c ---[3218]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[3216]---> Adder-cost: 186   maxlim: 14336   bits: 15/14
c ---[3212]---> Adder-cost: 152   maxlim: 9344   bits: 15/14
c ---[3210]---> Adder-cost: 60   maxlim: 9344   bits: 15/14
c ---[3206]---> Adder-cost: 282   maxlim: 17536   bits: 16/15
c ---[3204]---> Adder-cost: 272   maxlim: 17024   bits: 16/15
c ---[3202]---> Adder-cost: 214   maxlim: 16640   bits: 16/15
c ---[3200]---> Adder-cost: 250   maxlim: 16128   bits: 15/14
c ---[3196]---> Adder-cost: 154   maxlim: 9728   bits: 15/14
c ---[3194]---> Adder-cost: 112   maxlim: 7552   bits: 14/13
c ---[3192]---> Adder-cost: 112   maxlim: 7680   bits: 14/13
c ---[3190]---> Adder-cost: 68   maxlim: 6016   bits: 14/13
c ---[3188]---> Adder-cost: 76   maxlim: 6016   bits: 14/13
c ---[3186]---> Adder-cost: 54   maxlim: 6016   bits: 14/13
c ---[3184]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[3182]---> Sorter-cost:  379     Base: 2 2 2 2 2 2 2 7
c ---[3180]---> Adder-cost: 76   maxlim: 16128   bits: 15/14
c ---[3178]---> Sorter-cost:  580     Base: 2 2 2 2 2 2 2 7
c ---[3176]---> Sorter-cost:  435     Base: 2 2 2 2 2 2 2 7
c ---[3174]---> Sorter-cost:  398     Base: 2 2 2 2 2 2 2 7
c ---[3172]---> Adder-cost: 112   maxlim: 6912   bits: 14/13
c ---[3170]---> Adder-cost: 92   maxlim: 7040   bits: 14/13
c ---[3168]---> Adder-cost: 62   maxlim: 6912   bits: 14/13
c ---[3166]---> Adder-cost: 88   maxlim: 7168   bits: 14/13
c ---[3164]---> Adder-cost: 292   maxlim: 18176   bits: 16/15
c ---[3162]---> Adder-cost: 274   maxlim: 20224   bits: 16/15
c ---[3160]---> Adder-cost: 310   maxlim: 20736   bits: 16/15
c ---[3158]---> Adder-cost: 198   maxlim: 13568   bits: 15/14
c ---[3156]---> Adder-cost: 88   maxlim: 5632   bits: 14/13
c ---[3154]---> Adder-cost: 156   maxlim: 9472   bits: 15/14
c ---[3152]---> Adder-cost: 136   maxlim: 9984   bits: 15/14
c ---[3150]---> Adder-cost: 128   maxlim: 9472   bits: 15/14
c ---[3148]---> Adder-cost: 92   maxlim: 7424   bits: 14/13
c ---[3146]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[3144]---> Sorter-cost: 1068     Base: 2 2 2 2 2 2 2 7
c ---[3142]---> Adder-cost: 88   maxlim: 5376   bits: 14/13
c ---[3140]---> Adder-cost: 100   maxlim: 6272   bits: 14/13
c ---[3138]---> Adder-cost: 102   maxlim: 6912   bits: 14/13
c ---[3136]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 7
c ---[3134]---> Adder-cost: 78   maxlim: 13568   bits: 15/14
c ---[3132]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[3130]---> Adder-cost: 68   maxlim: 7296   bits: 14/13
c ---[3128]---> Adder-cost: 116   maxlim: 7808   bits: 14/13
c ---[3126]---> Adder-cost: 162   maxlim: 10752   bits: 15/14
c ---[3124]---> Adder-cost: 160   maxlim: 12672   bits: 15/14
c ---[3122]---> Adder-cost: 170   maxlim: 14336   bits: 15/14
c ---[3120]---> Adder-cost: 174   maxlim: 14976   bits: 15/14
c ---[3117]---> Adder-cost: 156   maxlim: 9472   bits: 15/14
c ---[3115]---> Adder-cost: 178   maxlim: 12544   bits: 15/14
c ---[3112]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[3110]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[3108]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 7
c ---[3106]---> Sorter-cost:  402     Base: 2 2 2 2 2 2 2 7
c ---[3104]---> Adder-cost: 178   maxlim: 11136   bits: 15/14
c ---[3102]---> Adder-cost: 280   maxlim: 17664   bits: 16/15
c ---[3099]---> Adder-cost: 106   maxlim: 6656   bits: 14/13
c ---[3097]---> Adder-cost: 106   maxlim: 6912   bits: 14/13
c ---[3095]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[3093]---> Adder-cost: 74   maxlim: 6528   bits: 14/13
c ---[3091]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[3089]---> Adder-cost: 70   maxlim: 5632   bits: 14/13
c ---[3087]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[3085]---> Sorter-cost: 1016     Base: 2 2 2 2 2 2 2 7
c ---[3083]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[3081]---> Adder-cost: 100   maxlim: 6144   bits: 14/13
c ---[3079]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 7
c ---[3077]---> Adder-cost: 140   maxlim: 8832   bits: 15/14
c ---[3075]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 7
c ---[3073]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[3071]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 7
c ---[3069]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 7
c ---[3067]---> Sorter-cost:  952     Base: 2 2 2 2 2 2 2 7
c ---[3065]---> Sorter-cost: 1001     Base: 2 2 2 2 2 2 2 7
c ---[3063]---> Sorter-cost: 1037     Base: 2 2 2 2 2 2 2 7
c ---[3061]---> Sorter-cost:  953     Base: 2 2 2 2 2 2 2 7
c ---[3059]---> Adder-cost: 172   maxlim: 10624   bits: 15/14
c ---[3057]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[3055]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[3053]---> Adder-cost: 170   maxlim: 11520   bits: 15/14
c ---[3051]---> Adder-cost: 146   maxlim: 13440   bits: 15/14
c ---[3049]---> Adder-cost: 136   maxlim: 13312   bits: 15/14
c ---[3047]---> Adder-cost: 174   maxlim: 11904   bits: 15/14
c ---[3045]---> Adder-cost: 252   maxlim: 16896   bits: 16/15
c ---[3043]---> Adder-cost: 232   maxlim: 16640   bits: 16/15
c ---[3041]---> Adder-cost: 170   maxlim: 12928   bits: 15/14
c ---[3039]---> Adder-cost: 170   maxlim: 12416   bits: 15/14
c ---[3037]---> Adder-cost: 160   maxlim: 12288   bits: 15/14
c ---[3035]---> Adder-cost: 156   maxlim: 10624   bits: 15/14
c ---[3033]---> Adder-cost: 228   maxlim: 15360   bits: 15/14
c ---[3031]---> Adder-cost: 226   maxlim: 17664   bits: 16/15
c ---[3029]---> Adder-cost: 92   maxlim: 17664   bits: 16/15
c ---[3027]---> Adder-cost: 146   maxlim: 9472   bits: 15/14
c ---[3025]---> Adder-cost: 164   maxlim: 10624   bits: 15/14
c ---[3023]---> Adder-cost: 96   maxlim: 9984   bits: 15/14
c ---[3021]---> Adder-cost: 234   maxlim: 15360   bits: 15/14
c ---[3019]---> Adder-cost: 206   maxlim: 14720   bits: 15/14
c ---[3017]---> Adder-cost: 76   maxlim: 14720   bits: 15/14
c ---[3015]---> Adder-cost: 188   maxlim: 14336   bits: 15/14
c ---[3013]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[3011]---> Adder-cost: 190   maxlim: 14080   bits: 15/14
c ---[3009]---> Adder-cost: 74   maxlim: 14080   bits: 15/14
c ---[3007]---> Adder-cost: 108   maxlim: 10624   bits: 15/14
c ---[3005]---> Adder-cost: 66   maxlim: 5248   bits: 14/13
c ---[3003]---> Adder-cost: 40   maxlim: 5248   bits: 14/13
c ---[3001]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[2998]---> Adder-cost: 104   maxlim: 6272   bits: 14/13
c ---[2996]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[2994]---> Adder-cost: 260   maxlim: 16768   bits: 16/15
c ---[2992]---> Adder-cost: 174   maxlim: 11648   bits: 15/14
c ---[2990]---> Adder-cost: 104   maxlim: 6784   bits: 14/13
c ---[2988]---> Adder-cost: 72   maxlim: 6016   bits: 14/13
c ---[2984]---> Adder-cost: 310   maxlim: 19456   bits: 16/15
c ---[2982]---> Adder-cost: 302   maxlim: 18944   bits: 16/15
c ---[2980]---> Adder-cost: 280   maxlim: 19200   bits: 16/15
c ---[2978]---> Adder-cost: 92   maxlim: 19200   bits: 16/15
c ---[2974]---> Adder-cost: 208   maxlim: 13056   bits: 15/14
c ---[2972]---> Adder-cost: 146   maxlim: 11648   bits: 15/14
c ---[2970]---> Adder-cost: 64   maxlim: 11648   bits: 15/14
c ---[2968]---> Adder-cost: 64   maxlim: 11648   bits: 15/14
c ---[2966]---> Adder-cost: 64   maxlim: 11648   bits: 15/14
c ---[2962]---> Adder-cost: 138   maxlim: 8704   bits: 15/14
c ---[2960]---> Adder-cost: 116   maxlim: 9088   bits: 15/14
c ---[2958]---> Adder-cost: 278   maxlim: 17280   bits: 16/15
c ---[2956]---> Adder-cost: 146   maxlim: 9344   bits: 15/14
c ---[2954]---> Adder-cost: 178   maxlim: 12288   bits: 15/14
c ---[2952]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[2950]---> Sorter-cost:  308     Base: 2 2 2 2 2 2 2 2
c ---[2948]---> Adder-cost: 234   maxlim: 14720   bits: 15/14
c ---[2946]---> Adder-cost: 136   maxlim: 8192   bits: 15/14
c ---[2944]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[2942]---> Adder-cost: 62   maxlim: 4352   bits: 14/13
c ---[2940]---> Adder-cost: 76   maxlim: 4736   bits: 14/13
c ---[2938]---> Adder-cost: 224   maxlim: 14080   bits: 15/14
c ---[2936]---> Adder-cost: 88   maxlim: 17280   bits: 16/15
c ---[2934]---> Adder-cost: 250   maxlim: 16128   bits: 15/14
c ---[2932]---> Adder-cost: 206   maxlim: 12928   bits: 15/14
c ---[2930]---> Adder-cost: 148   maxlim: 12288   bits: 15/14
c ---[2928]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[2926]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[2924]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[2922]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[2920]---> Adder-cost: 202   maxlim: 12544   bits: 15/14
c ---[2918]---> Adder-cost: 104   maxlim: 6528   bits: 14/13
c ---[2916]---> Adder-cost: 110   maxlim: 7168   bits: 14/13
c ---[2914]---> Adder-cost: 206   maxlim: 13056   bits: 15/14
c ---[2912]---> Adder-cost: 78   maxlim: 5248   bits: 14/13
c ---[2910]---> Adder-cost: 74   maxlim: 5120   bits: 14/13
c ---[2908]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[2906]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 7
c ---[2904]---> Sorter-cost:  362     Base: 2 2 2 2 2 2 2 7
c ---[2902]---> Adder-cost: 228   maxlim: 14336   bits: 15/14
c ---[2899]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[2897]---> Sorter-cost:  994     Base: 2 2 2 2 2 2 2 7
c ---[2895]---> Sorter-cost: 1208     Base: 2 2 2 2 2 2 2 7
c ---[2893]---> Adder-cost: 74   maxlim: 13056   bits: 15/14
c ---[2889]---> Adder-cost: 140   maxlim: 8320   bits: 15/14
c ---[2887]---> Adder-cost: 148   maxlim: 9728   bits: 15/14
c ---[2885]---> Adder-cost: 64   maxlim: 9728   bits: 15/14
c ---[2883]---> Adder-cost: 122   maxlim: 9344   bits: 15/14
c ---[2881]---> Adder-cost: 168   maxlim: 10368   bits: 15/14
c ---[2879]---> Adder-cost: 68   maxlim: 10368   bits: 15/14
c ---[2875]---> Adder-cost: 100   maxlim: 13056   bits: 15/14
c ---[2873]---> Adder-cost: 224   maxlim: 15360   bits: 15/14
c ---[2871]---> Adder-cost: 94   maxlim: 7040   bits: 14/13
c ---[2868]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[2866]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[2864]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[2862]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[2860]---> Sorter-cost:  589     Base: 2 2 2 2 2 2 2 7
c ---[2858]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[2856]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[2854]---> Adder-cost: 74   maxlim: 13056   bits: 15/14
c ---[2852]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[2850]---> Sorter-cost:  984     Base: 2 2 2 2 2 2 2 7
c ---[2848]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[2846]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 7
c ---[2844]---> Sorter-cost:  399     Base: 2 2 2 2 2 2 2 7
c ---[2842]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2840]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[2838]---> Sorter-cost:  852     Base: 2 2 2 2 2 2 2 7
c ---[2836]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[2834]---> Sorter-cost: 1138     Base: 2 2 2 2 2 2 2 7
c ---[2832]---> Adder-cost: 122   maxlim: 12800   bits: 15/14
c ---[2830]---> Sorter-cost:  752     Base: 2 2 2 2 2 2 2 7
c ---[2828]---> Adder-cost: 216   maxlim: 13568   bits: 15/14
c ---[2826]---> Adder-cost: 78   maxlim: 13568   bits: 15/14
c ---[2824]---> Adder-cost: 198   maxlim: 13952   bits: 15/14
c ---[2822]---> Adder-cost: 134   maxlim: 13824   bits: 15/14
c ---[2820]---> Adder-cost: 144   maxlim: 13952   bits: 15/14
c ---[2818]---> Adder-cost: 94   maxlim: 13952   bits: 15/14
c ---[2816]---> Adder-cost: 238   maxlim: 15232   bits: 15/14
c ---[2814]---> Adder-cost: 80   maxlim: 15232   bits: 15/14
c ---[2812]---> Adder-cost: 210   maxlim: 14720   bits: 15/14
c ---[2810]---> Adder-cost: 76   maxlim: 12800   bits: 15/14
c ---[2808]---> Adder-cost: 154   maxlim: 14336   bits: 15/14
c ---[2806]---> Adder-cost: 142   maxlim: 8576   bits: 15/14
c ---[2804]---> Adder-cost: 128   maxlim: 8704   bits: 15/14
c ---[2802]---> Adder-cost: 114   maxlim: 8960   bits: 15/14
c ---[2800]---> Adder-cost: 60   maxlim: 8960   bits: 15/14
c ---[2798]---> Adder-cost: 234   maxlim: 14720   bits: 15/14
c ---[2796]---> Adder-cost: 150   maxlim: 14336   bits: 15/14
c ---[2794]---> Adder-cost: 206   maxlim: 13440   bits: 15/14
c ---[2792]---> Adder-cost: 78   maxlim: 13440   bits: 15/14
c ---[2790]---> Adder-cost: 78   maxlim: 13440   bits: 15/14
c ---[2788]---> Adder-cost: 76   maxlim: 12800   bits: 15/14
c ---[2786]---> Adder-cost: 102   maxlim: 13824   bits: 15/14
c ---[2784]---> Adder-cost: 96   maxlim: 14592   bits: 15/14
c ---[2781]---> Adder-cost: 126   maxlim: 8064   bits: 14/13
c ---[2779]---> Adder-cost: 174   maxlim: 10752   bits: 15/14
c ---[2777]---> Adder-cost: 140   maxlim: 10240   bits: 15/14
c ---[2775]---> Adder-cost: 136   maxlim: 9600   bits: 15/14
c ---[2773]---> Adder-cost: 76   maxlim: 12800   bits: 15/14
c ---[2771]---> Adder-cost: 122   maxlim: 9344   bits: 15/14
c ---[2769]---> Adder-cost: 106   maxlim: 7424   bits: 14/13
c ---[2767]---> Adder-cost: 88   maxlim: 5632   bits: 14/13
c ---[2765]---> Adder-cost: 120   maxlim: 7552   bits: 14/13
c ---[2763]---> Adder-cost: 86   maxlim: 5888   bits: 14/13
c ---[2761]---> Adder-cost: 76   maxlim: 12800   bits: 15/14
c ---[2759]---> Adder-cost: 208   maxlim: 13056   bits: 15/14
c ---[2757]---> Adder-cost: 158   maxlim: 13184   bits: 15/14
c ---[2755]---> Adder-cost: 190   maxlim: 11776   bits: 15/14
c ---[2753]---> Adder-cost: 182   maxlim: 11648   bits: 15/14
c ---[2751]---> Adder-cost: 152   maxlim: 12288   bits: 15/14
c ---[2749]---> Sorter-cost:  431     Base: 2 2 2 2 2 2 2 7
c ---[2746]---> Adder-cost: 194   maxlim: 13312   bits: 15/14
c ---[2744]---> Adder-cost: 214   maxlim: 14976   bits: 15/14
c ---[2742]---> Adder-cost: 188   maxlim: 13952   bits: 15/14
c ---[2740]---> Adder-cost: 106   maxlim: 6528   bits: 14/13
c ---[2738]---> Adder-cost: 108   maxlim: 7168   bits: 14/13
c ---[2735]---> Adder-cost: 92   maxlim: 6144   bits: 14/13
c ---[2733]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2731]---> Sorter-cost:  884     Base: 2 2 2 2 2 2 2 7
c ---[2729]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[2727]---> Sorter-cost: 1117     Base: 2 2 2 2 2 2 2 7
c ---[2725]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[2722]---> Adder-cost: 78   maxlim: 4736   bits: 14/13
c ---[2720]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[2718]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[2715]---> Adder-cost: 274   maxlim: 17024   bits: 16/15
c ---[2713]---> Adder-cost: 236   maxlim: 15360   bits: 15/14
c ---[2711]---> Adder-cost: 106   maxlim: 6400   bits: 14/13
c ---[2708]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[2706]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[2704]---> Adder-cost: 132   maxlim: 8576   bits: 15/14
c ---[2702]---> Adder-cost: 102   maxlim: 6272   bits: 14/13
c ---[2698]---> Adder-cost: 46   maxlim: 6272   bits: 14/13
c ---[2696]---> Adder-cost: 60   maxlim: 7168   bits: 14/13
c ---[2694]---> Adder-cost: 154   maxlim: 9216   bits: 15/14
c ---[2692]---> Adder-cost: 146   maxlim: 9344   bits: 15/14
c ---[2690]---> Adder-cost: 88   maxlim: 5632   bits: 14/13
c ---[2688]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[2685]---> Adder-cost: 154   maxlim: 9344   bits: 15/14
c ---[2683]---> Adder-cost: 60   maxlim: 9344   bits: 15/14
c ---[2681]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[2678]---> Adder-cost: 212   maxlim: 13568   bits: 15/14
c ---[2675]---> Adder-cost: 142   maxlim: 8576   bits: 15/14
c ---[2671]---> Adder-cost: 286   maxlim: 18432   bits: 16/15
c ---[2669]---> Adder-cost: 114   maxlim: 7296   bits: 14/13
c ---[2665]---> Adder-cost: 148   maxlim: 8960   bits: 15/14
c ---[2662]---> Sorter-cost: 1074     Base: 2 2 2 2 2 2 2 7
c ---[2660]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[2657]---> Adder-cost: 48   maxlim: 7296   bits: 14/13
c ---[2654]---> Adder-cost: 270   maxlim: 16640   bits: 16/15
c ---[2650]---> Adder-cost: 248   maxlim: 15744   bits: 15/14
c ---[2646]---> Adder-cost: 238   maxlim: 14848   bits: 15/14
c ---[2644]---> Adder-cost: 92   maxlim: 5760   bits: 14/13
c ---[2642]---> Adder-cost: 98   maxlim: 6656   bits: 14/13
c ---[2638]---> Adder-cost: 274   maxlim: 16896   bits: 16/15
c ---[2636]---> Adder-cost: 176   maxlim: 11136   bits: 15/14
c ---[2632]---> Adder-cost: 276   maxlim: 17920   bits: 16/15
c ---[2628]---> Adder-cost: 86   maxlim: 5248   bits: 14/13
c ---[2626]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[2623]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[2621]---> Adder-cost: 88   maxlim: 6912   bits: 14/13
c ---[2619]---> Adder-cost: 168   maxlim: 10368   bits: 15/14
c ---[2615]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[2613]---> Adder-cost: 358   maxlim: 23040   bits: 16/15
c ---[2611]---> Adder-cost: 330   maxlim: 22784   bits: 16/15
c ---[2607]---> Adder-cost: 198   maxlim: 13568   bits: 15/14
c ---[2605]---> Adder-cost: 290   maxlim: 19328   bits: 16/15
c ---[2603]---> Adder-cost: 176   maxlim: 10752   bits: 15/14
c ---[2599]---> Adder-cost: 150   maxlim: 11136   bits: 15/14
c ---[2597]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2593]---> Adder-cost: 238   maxlim: 14848   bits: 15/14
c ---[2590]---> Adder-cost: 124   maxlim: 7808   bits: 14/13
c ---[2588]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[2584]---> Adder-cost: 118   maxlim: 7680   bits: 14/13
c ---[2582]---> Sorter-cost:  881     Base: 2 2 2 2 2 2 2 7
c ---[2580]---> Adder-cost: 124   maxlim: 7680   bits: 14/13
c ---[2576]---> Adder-cost: 112   maxlim: 7680   bits: 14/13
c ---[2574]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2572]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 7
c ---[2570]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[2567]---> Sorter-cost:  844     Base: 2 2 2 2 2 2 2 7
c ---[2565]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[2561]---> Adder-cost: 144   maxlim: 8832   bits: 15/14
c ---[2559]---> Adder-cost: 222   maxlim: 13952   bits: 15/14
c ---[2557]---> Adder-cost: 130   maxlim: 14080   bits: 15/14
c ---[2553]---> Adder-cost: 158   maxlim: 10112   bits: 15/14
c ---[2550]---> Sorter-cost:  784     Base: 2 2 2 2 2 2 2 7
c ---[2547]---> Adder-cost: 106   maxlim: 6528   bits: 14/13
c ---[2545]---> Adder-cost: 274   maxlim: 17152   bits: 16/15
c ---[2543]---> Adder-cost: 140   maxlim: 17280   bits: 16/15
c ---[2539]---> Adder-cost: 184   maxlim: 11264   bits: 15/14
c ---[2535]---> Adder-cost: 264   maxlim: 17280   bits: 16/15
c ---[2533]---> Sorter-cost:  781     Base: 2 2 2 2 2 2 2 7
c ---[2530]---> Adder-cost: 162   maxlim: 10112   bits: 15/14
c ---[2528]---> Adder-cost: 62   maxlim: 10112   bits: 15/14
c ---[2524]---> Adder-cost: 184   maxlim: 11392   bits: 15/14
c ---[2522]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[2520]---> Sorter-cost:  224     Base: 2 2 2 2 2 2 2 2
c ---[2518]---> Sorter-cost:  700     Base: 2 2 2 2 2 2 2 7
c ---[2516]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[2514]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[2512]---> Sorter-cost:  463     Base: 2 2 2 2 2 2 2 7
c ---[2510]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 7
c ---[2508]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 7
c ---[2506]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 7
c ---[2503]---> Adder-cost: 122   maxlim: 7680   bits: 14/13
c ---[2501]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2499]---> Adder-cost: 98   maxlim: 7552   bits: 14/13
c ---[2496]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[2494]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 7
c ---[2492]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[2490]---> Sorter-cost:  666     Base: 2 2 2 2 2 2 2 7
c ---[2488]---> Adder-cost: 276   maxlim: 18304   bits: 16/15
c ---[2486]---> Adder-cost: 88   maxlim: 18304   bits: 16/15
c ---[2482]---> Adder-cost: 138   maxlim: 9344   bits: 15/14
c ---[2478]---> Adder-cost: 176   maxlim: 11008   bits: 15/14
c ---[2476]---> Adder-cost: 184   maxlim: 11264   bits: 15/14
c ---[2474]---> Adder-cost: 72   maxlim: 11264   bits: 15/14
c ---[2472]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[2468]---> Adder-cost: 152   maxlim: 9728   bits: 15/14
c ---[2465]---> Adder-cost: 182   maxlim: 11392   bits: 15/14
c ---[2463]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[2460]---> Adder-cost: 170   maxlim: 10368   bits: 15/14
c ---[2458]---> Adder-cost: 296   maxlim: 18688   bits: 16/15
c ---[2456]---> Adder-cost: 210   maxlim: 13184   bits: 15/14
c ---[2454]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[2452]---> Adder-cost: 40   maxlim: 5888   bits: 14/13
c ---[2448]---> Adder-cost: 290   maxlim: 18688   bits: 16/15
c ---[2446]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[2443]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[2441]---> Sorter-cost:  782     Base: 2 2 2 2 2 2 2 7
c ---[2439]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[2437]---> Adder-cost: 74   maxlim: 13184   bits: 15/14
c ---[2435]---> Adder-cost: 204   maxlim: 12800   bits: 15/14
c ---[2433]---> Adder-cost: 134   maxlim: 9856   bits: 15/14
c ---[2431]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2429]---> Sorter-cost:  893     Base: 2 2 2 2 2 2 2 7
c ---[2427]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 7
c ---[2425]---> Sorter-cost:  922     Base: 2 2 2 2 2 2 2 7
c ---[2423]---> Adder-cost: 154   maxlim: 9216   bits: 15/14
c ---[2421]---> Adder-cost: 252   maxlim: 16128   bits: 15/14
c ---[2419]---> Adder-cost: 112   maxlim: 13056   bits: 15/14
c ---[2416]---> Adder-cost: 154   maxlim: 10368   bits: 15/14
c ---[2414]---> Adder-cost: 130   maxlim: 10240   bits: 15/14
c ---[2410]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[2408]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[2406]---> Adder-cost: 180   maxlim: 13184   bits: 15/14
c ---[2403]---> Adder-cost: 152   maxlim: 9600   bits: 15/14
c ---[2401]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[2399]---> Sorter-cost:  600     Base: 2 2 2 2 2 2 2 7
c ---[2397]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[2395]---> Sorter-cost:  902     Base: 2 2 2 2 2 2 2 7
c ---[2391]---> Adder-cost: 92   maxlim: 5760   bits: 14/13
c ---[2389]---> Adder-cost: 146   maxlim: 9344   bits: 15/14
c ---[2387]---> Adder-cost: 92   maxlim: 5632   bits: 14/13
c ---[2385]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[2383]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 7
c ---[2381]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 7
c ---[2379]---> Sorter-cost:  581     Base: 2 2 2 2 2 2 2 7
c ---[2377]---> Sorter-cost:  410     Base: 2 2 2 2 2 2 2 7
c ---[2375]---> Adder-cost: 130   maxlim: 9088   bits: 15/14
c ---[2373]---> Sorter-cost:  433     Base: 2 2 2 2 2 2 2 7
c ---[2371]---> Sorter-cost:  329     Base: 2 2 2 2 2 2 2 7
c ---[2369]---> Sorter-cost:  392     Base: 2 2 2 2 2 2 2 7
c ---[2366]---> Adder-cost: 102   maxlim: 6272   bits: 14/13
c ---[2364]---> Adder-cost: 100   maxlim: 6272   bits: 14/13
c ---[2362]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[2360]---> Adder-cost: 144   maxlim: 8832   bits: 15/14
c ---[2357]---> Adder-cost: 202   maxlim: 12416   bits: 15/14
c ---[2355]---> Adder-cost: 70   maxlim: 12416   bits: 15/14
c ---[2353]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[2350]---> Adder-cost: 112   maxlim: 7552   bits: 14/13
c ---[2346]---> Adder-cost: 166   maxlim: 10880   bits: 15/14
c ---[2344]---> Adder-cost: 136   maxlim: 8704   bits: 15/14
c ---[2342]---> Adder-cost: 132   maxlim: 9600   bits: 15/14
c ---[2340]---> Adder-cost: 62   maxlim: 8704   bits: 15/14
c ---[2337]---> Adder-cost: 66   maxlim: 10880   bits: 15/14
c ---[2333]---> Adder-cost: 70   maxlim: 4992   bits: 14/13
c ---[2331]---> Sorter-cost:  658     Base: 2 2 2 2 2 2 2 7
c ---[2329]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2 7
c ---[2327]---> Adder-cost: 136   maxlim: 8832   bits: 15/14
c ---[2325]---> Adder-cost: 88   maxlim: 5376   bits: 14/13
c ---[2323]---> Adder-cost: 122   maxlim: 7680   bits: 14/13
c ---[2321]---> Adder-cost: 138   maxlim: 8448   bits: 15/14
c ---[2318]---> Adder-cost: 92   maxlim: 7808   bits: 14/13
c ---[2316]---> Adder-cost: 84   maxlim: 8960   bits: 15/14
c ---[2314]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[2312]---> Adder-cost: 294   maxlim: 18944   bits: 16/15
c ---[2310]---> Adder-cost: 302   maxlim: 19200   bits: 16/15
c ---[2308]---> Adder-cost: 222   maxlim: 13824   bits: 15/14
c ---[2305]---> Adder-cost: 186   maxlim: 11904   bits: 15/14
c ---[2303]---> Adder-cost: 226   maxlim: 15744   bits: 15/14
c ---[2301]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 7
c ---[2299]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[2297]---> Sorter-cost:  644     Base: 2 2 2 2 2 2 2 7
c ---[2295]---> Adder-cost: 194   maxlim: 12672   bits: 15/14
c ---[2291]---> Adder-cost: 92   maxlim: 5760   bits: 14/13
c ---[2289]---> Adder-cost: 144   maxlim: 9472   bits: 15/14
c ---[2287]---> Adder-cost: 104   maxlim: 7424   bits: 14/13
c ---[2285]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[2283]---> Adder-cost: 88   maxlim: 5376   bits: 14/13
c ---[2281]---> Adder-cost: 164   maxlim: 12416   bits: 15/14
c ---[2278]---> Adder-cost: 218   maxlim: 13568   bits: 15/14
c ---[2276]---> Adder-cost: 214   maxlim: 14848   bits: 15/14
c ---[2274]---> Adder-cost: 80   maxlim: 14848   bits: 15/14
c ---[2272]---> Adder-cost: 174   maxlim: 10752   bits: 15/14
c ---[2270]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[2268]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[2264]---> Adder-cost: 200   maxlim: 12416   bits: 15/14
c ---[2262]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 7
c ---[2260]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 7
c ---[2258]---> Sorter-cost:  674     Base: 2 2 2 2 2 2 2 7
c ---[2256]---> Adder-cost: 184   maxlim: 11264   bits: 15/14
c ---[2254]---> Adder-cost: 102   maxlim: 6272   bits: 14/13
c ---[2252]---> Adder-cost: 126   maxlim: 7936   bits: 14/13
c ---[2250]---> Adder-cost: 252   maxlim: 17024   bits: 16/15
c ---[2247]---> Sorter-cost:  897     Base: 2 2 2 2 2 2 2 7
c ---[2245]---> Adder-cost: 70   maxlim: 12416   bits: 15/14
c ---[2243]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[2241]---> Adder-cost: 84   maxlim: 6016   bits: 14/13
c ---[2238]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[2236]---> Adder-cost: 138   maxlim: 9088   bits: 15/14
c ---[2234]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[2232]---> Adder-cost: 188   maxlim: 12288   bits: 15/14
c ---[2229]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[2227]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[2225]---> Adder-cost: 106   maxlim: 6784   bits: 14/13
c ---[2223]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[2219]---> Adder-cost: 108   maxlim: 12160   bits: 15/14
c ---[2217]---> Adder-cost: 168   maxlim: 10752   bits: 15/14
c ---[2215]---> Sorter-cost:  685     Base: 2 2 2 2 2 2 2 7
c ---[2211]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[2209]---> Sorter-cost:  517     Base: 2 2 2 2 2 2 2 7
c ---[2207]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[2203]---> Adder-cost: 158   maxlim: 12032   bits: 15/14
c ---[2201]---> Sorter-cost: 1045     Base: 2 2 2 2 2 2 2 7
c ---[2197]---> Sorter-cost:  780     Base: 2 2 2 2 2 2 2 7
c ---[2195]---> Sorter-cost:  392     Base: 2 2 2 2 2 2 2 7
c ---[2192]---> Sorter-cost:  457     Base: 2 2 2 2 2 2 2 7
c ---[2188]---> Adder-cost: 108   maxlim: 11904   bits: 15/14
c ---[2186]---> Sorter-cost:  404     Base: 2 2 2 2 2 2 2 7
c ---[2182]---> Adder-cost: 168   maxlim: 10240   bits: 15/14
c ---[2179]---> Adder-cost: 144   maxlim: 8704   bits: 15/14
c ---[2176]---> Adder-cost: 110   maxlim: 6784   bits: 14/13
c ---[2174]---> Adder-cost: 70   maxlim: 11904   bits: 15/14
c ---[2172]---> Adder-cost: 112   maxlim: 7552   bits: 14/13
c ---[2170]---> Adder-cost: 48   maxlim: 7552   bits: 14/13
c ---[2166]---> Adder-cost: 314   maxlim: 20352   bits: 16/15
c ---[2164]---> Adder-cost: 92   maxlim: 20352   bits: 16/15
c ---[2162]---> Adder-cost: 310   maxlim: 20864   bits: 16/15
c ---[2160]---> Adder-cost: 100   maxlim: 20864   bits: 16/15
c ---[2157]---> Adder-cost: 100   maxlim: 20864   bits: 16/15
c ---[2155]---> Adder-cost: 100   maxlim: 20864   bits: 16/15
c ---[2152]---> Sorter-cost:  616     Base: 2 2 2 2 2 2 2 7
c ---[2150]---> Adder-cost: 112   maxlim: 7040   bits: 14/13
c ---[2148]---> Adder-cost: 92   maxlim: 6784   bits: 14/13
c ---[2146]---> Adder-cost: 78   maxlim: 6400   bits: 14/13
c ---[2144]---> Adder-cost: 278   maxlim: 17664   bits: 16/15
c ---[2140]---> Adder-cost: 128   maxlim: 8576   bits: 15/14
c ---[2138]---> Adder-cost: 96   maxlim: 8320   bits: 15/14
c ---[2136]---> Adder-cost: 136   maxlim: 8192   bits: 15/14
c ---[2132]---> Adder-cost: 86   maxlim: 6656   bits: 14/13
c ---[2130]---> Adder-cost: 364   maxlim: 23040   bits: 16/15
c ---[2128]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[2124]---> Adder-cost: 178   maxlim: 11136   bits: 15/14
c ---[2122]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[2119]---> Adder-cost: 108   maxlim: 6656   bits: 14/13
c ---[2117]---> Adder-cost: 142   maxlim: 9088   bits: 15/14
c ---[2115]---> Adder-cost: 116   maxlim: 8832   bits: 15/14
c ---[2113]---> Adder-cost: 254   maxlim: 19200   bits: 16/15
c ---[2110]---> Adder-cost: 148   maxlim: 9216   bits: 15/14
c ---[2108]---> Adder-cost: 100   maxlim: 6912   bits: 14/13
c ---[2104]---> Adder-cost: 230   maxlim: 14976   bits: 15/14
c ---[2102]---> Adder-cost: 80   maxlim: 14976   bits: 15/14
c ---[2099]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 7
c ---[2096]---> Adder-cost: 168   maxlim: 19072   bits: 16/15
c ---[2093]---> Sorter-cost:  618     Base: 2 2 2 2 2 2 2 7
c ---[2091]---> Sorter-cost:  545     Base: 2 2 2 2 2 2 2 7
c ---[2089]---> Sorter-cost:  529     Base: 2 2 2 2 2 2 2 7
c ---[2087]---> Sorter-cost:  703     Base: 2 2 2 2 2 2 2 7
c ---[2085]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[2083]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[2081]---> Adder-cost: 118   maxlim: 7296   bits: 14/13
c ---[2078]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[2076]---> Adder-cost: 146   maxlim: 19456   bits: 16/15
c ---[2072]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[2068]---> Adder-cost: 124   maxlim: 7680   bits: 14/13
c ---[2066]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[2064]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[2062]---> Sorter-cost:  610     Base: 2 2 2 2 2 2 2 7
c ---[2060]---> Adder-cost: 96   maxlim: 19456   bits: 16/15
c ---[2058]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[2054]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 7
c ---[2052]---> Adder-cost: 170   maxlim: 10880   bits: 15/14
c ---[2050]---> Adder-cost: 220   maxlim: 14976   bits: 15/14
c ---[2048]---> Adder-cost: 142   maxlim: 9216   bits: 15/14
c ---[2046]---> Adder-cost: 62   maxlim: 9216   bits: 15/14
c ---[2041]---> Sorter-cost:  551     Base: 2 2 2 2 2 2 2 7
c ---[2037]---> Sorter-cost:  930     Base: 2 2 2 2 2 2 2 7
c ---[2034]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[2032]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[2030]---> Adder-cost: 154   maxlim: 9216   bits: 15/14
c ---[2028]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[2025]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[2023]---> Adder-cost: 104   maxlim: 6656   bits: 14/13
c ---[2019]---> Sorter-cost:  732     Base: 2 2 2 2 2 2 2 7
c ---[2015]---> Sorter-cost:  360     Base: 2 2 2 2 2 2 2 7
c ---[2013]---> Adder-cost: 88   maxlim: 9216   bits: 15/14
c ---[2010]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[2007]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[2005]---> Sorter-cost:  258     Base: 2 2 2 2 2 2 2 2
c ---[2003]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[2001]---> Sorter-cost:  531     Base: 2 2 2 2 2 2 2 7
c ---[1998]---> Sorter-cost:  691     Base: 2 2 2 2 2 2 2 7
c ---[1996]---> Adder-cost: 108   maxlim: 7680   bits: 14/13
c ---[1994]---> Adder-cost: 186   maxlim: 11648   bits: 15/14
c ---[1992]---> Adder-cost: 84   maxlim: 11648   bits: 15/14
c ---[1989]---> Adder-cost: 86   maxlim: 5376   bits: 14/13
c ---[1987]---> Sorter-cost:  780     Base: 2 2 2 2 2 2 2 7
c ---[1985]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 7
c ---[1983]---> Sorter-cost:  711     Base: 2 2 2 2 2 2 2 7
c ---[1979]---> Adder-cost: 172   maxlim: 11264   bits: 15/14
c ---[1977]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1974]---> Adder-cost: 82   maxlim: 4992   bits: 14/13
c ---[1972]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[1970]---> Adder-cost: 172   maxlim: 10752   bits: 15/14
c ---[1968]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[1966]---> Sorter-cost:  463     Base: 2 2 2 2 2 2 2 7
c ---[1964]---> Sorter-cost:  673     Base: 2 2 2 2 2 2 2 7
c ---[1962]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 7
c ---[1960]---> Sorter-cost:  242     Base: 2 2 2 2 2 2 2 2
c ---[1958]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[1955]---> Adder-cost: 88   maxlim: 5248   bits: 14/13
c ---[1953]---> Adder-cost: 108   maxlim: 9984   bits: 15/14
c ---[1951]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1949]---> Sorter-cost:  228     Base: 2 2 2 2 2 2 2 2
c ---[1947]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[1945]---> Sorter-cost:  705     Base: 2 2 2 2 2 2 2 7
c ---[1942]---> Sorter-cost:  621     Base: 2 2 2 2 2 2 2 7
c ---[1940]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2
c ---[1938]---> Adder-cost: 150   maxlim: 9728   bits: 15/14
c ---[1935]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 7
c ---[1933]---> Adder-cost: 230   maxlim: 14464   bits: 15/14
c ---[1931]---> Adder-cost: 160   maxlim: 14336   bits: 15/14
c ---[1929]---> Adder-cost: 204   maxlim: 14592   bits: 15/14
c ---[1926]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[1924]---> Adder-cost: 64   maxlim: 9728   bits: 15/14
c ---[1921]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[1919]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[1917]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 7
c ---[1913]---> Adder-cost: 202   maxlim: 13056   bits: 15/14
c ---[1911]---> Adder-cost: 90   maxlim: 5504   bits: 14/13
c ---[1909]---> Adder-cost: 104   maxlim: 6400   bits: 14/13
c ---[1905]---> Adder-cost: 94   maxlim: 6272   bits: 14/13
c ---[1902]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1900]---> Sorter-cost:  268     Base: 2 2 2 2 2 2 2 2
c ---[1898]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1895]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[1893]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[1891]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1888]---> Sorter-cost:  654     Base: 2 2 2 2 2 2 2 7
c ---[1885]---> Sorter-cost:  730     Base: 2 2 2 2 2 2 2 7
c ---[1882]---> Adder-cost: 76   maxlim: 5376   bits: 14/13
c ---[1879]---> Sorter-cost:  891     Base: 2 2 2 2 2 2 2 7
c ---[1877]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[1875]---> Adder-cost: 76   maxlim: 4352   bits: 14/13
c ---[1873]---> Adder-cost: 76   maxlim: 6016   bits: 14/13
c ---[1870]---> Adder-cost: 82   maxlim: 5120   bits: 14/13
c ---[1868]---> Adder-cost: 44   maxlim: 5120   bits: 14/13
c ---[1865]---> Adder-cost: 114   maxlim: 7424   bits: 14/13
c ---[1863]---> Adder-cost: 50   maxlim: 7424   bits: 14/13
c ---[1861]---> Adder-cost: 90   maxlim: 7296   bits: 14/13
c ---[1858]---> Adder-cost: 106   maxlim: 6912   bits: 14/13
c ---[1856]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[1854]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 7
c ---[1852]---> Adder-cost: 96   maxlim: 6016   bits: 14/13
c ---[1850]---> Adder-cost: 102   maxlim: 7296   bits: 14/13
c ---[1848]---> Adder-cost: 72   maxlim: 6016   bits: 14/13
c ---[1846]---> Adder-cost: 128   maxlim: 9216   bits: 15/14
c ---[1843]---> Sorter-cost:  654     Base: 2 2 2 2 2 2 2 7
c ---[1841]---> Adder-cost: 92   maxlim: 6016   bits: 14/13
c ---[1839]---> Sorter-cost:  717     Base: 2 2 2 2 2 2 2 7
c ---[1837]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1835]---> Adder-cost: 304   maxlim: 20480   bits: 16/15
c ---[1833]---> Adder-cost: 120   maxlim: 7680   bits: 14/13
c ---[1830]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 7
c ---[1827]---> Adder-cost: 90   maxlim: 6016   bits: 14/13
c ---[1825]---> Adder-cost: 152   maxlim: 10368   bits: 15/14
c ---[1823]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 7
c ---[1819]---> Adder-cost: 146   maxlim: 9984   bits: 15/14
c ---[1817]---> Adder-cost: 84   maxlim: 5632   bits: 14/13
c ---[1814]---> Adder-cost: 212   maxlim: 13952   bits: 15/14
c ---[1811]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 7
c ---[1809]---> Sorter-cost:  730     Base: 2 2 2 2 2 2 2 7
c ---[1807]---> Adder-cost: 102   maxlim: 6144   bits: 14/13
c ---[1805]---> Adder-cost: 132   maxlim: 9472   bits: 15/14
c ---[1801]---> Sorter-cost:  360     Base: 2 2 2 2 2 2 2 7
c ---[1799]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 7
c ---[1796]---> Adder-cost: 106   maxlim: 6528   bits: 14/13
c ---[1793]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[1790]---> Adder-cost: 94   maxlim: 5632   bits: 14/13
c ---[1787]---> Sorter-cost:  936     Base: 2 2 2 2 2 2 2 7
c ---[1785]---> Adder-cost: 86   maxlim: 5120   bits: 14/13
c ---[1783]---> Sorter-cost: 1090     Base: 2 2 2 2 2 2 2 7
c ---[1781]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 7
c ---[1779]---> Sorter-cost:  679     Base: 2 2 2 2 2 2 2 7
c ---[1777]---> Sorter-cost:  908     Base: 2 2 2 2 2 2 2 7
c ---[1775]---> Adder-cost: 218   maxlim: 13824   bits: 15/14
c ---[1773]---> Adder-cost: 192   maxlim: 12672   bits: 15/14
c ---[1771]---> Adder-cost: 114   maxlim: 7168   bits: 14/13
c ---[1768]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 7
c ---[1766]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1764]---> Sorter-cost:  262     Base: 2 2 2 2 2 2 2 2
c ---[1762]---> Sorter-cost:  258     Base: 2 2 2 2 2 2 2 2
c ---[1760]---> Adder-cost: 96   maxlim: 6272   bits: 14/13
c ---[1758]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[1756]---> Adder-cost: 92   maxlim: 5888   bits: 14/13
c ---[1754]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[1752]---> Adder-cost: 174   maxlim: 11136   bits: 15/14
c ---[1750]---> Sorter-cost:  403     Base: 2 2 2 2 2 2 2 7
c ---[1748]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[1746]---> Sorter-cost:  293     Base: 2 2 2 2 2 2 2 7
c ---[1744]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 7
c ---[1742]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[1740]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[1736]---> Adder-cost: 122   maxlim: 7808   bits: 14/13
c ---[1734]---> Adder-cost: 174   maxlim: 13568   bits: 15/14
c ---[1732]---> Adder-cost: 164   maxlim: 10368   bits: 15/14
c ---[1729]---> Sorter-cost:  612     Base: 2 2 2 2 2 2 2 7
c ---[1727]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2
c ---[1725]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[1723]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[1721]---> Adder-cost: 242   maxlim: 15488   bits: 15/14
c ---[1719]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[1716]---> Sorter-cost:  654     Base: 2 2 2 2 2 2 2 7
c ---[1714]---> Adder-cost: 110   maxlim: 6912   bits: 14/13
c ---[1710]---> Adder-cost: 94   maxlim: 5888   bits: 14/13
c ---[1708]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[1706]---> Adder-cost: 200   maxlim: 15744   bits: 15/14
c ---[1704]---> Adder-cost: 104   maxlim: 6528   bits: 14/13
c ---[1702]---> Adder-cost: 108   maxlim: 7552   bits: 14/13
c ---[1700]---> Adder-cost: 110   maxlim: 8064   bits: 14/13
c ---[1698]---> Adder-cost: 102   maxlim: 7296   bits: 14/13
c ---[1696]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1694]---> Adder-cost: 72   maxlim: 4352   bits: 14/13
c ---[1692]---> Adder-cost: 90   maxlim: 5376   bits: 14/13
c ---[1690]---> Adder-cost: 268   maxlim: 16768   bits: 16/15
c ---[1688]---> Adder-cost: 106   maxlim: 6656   bits: 14/13
c ---[1684]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[1682]---> Adder-cost: 82   maxlim: 5120   bits: 14/13
c ---[1679]---> Adder-cost: 154   maxlim: 9216   bits: 15/14
c ---[1676]---> Adder-cost: 242   maxlim: 17280   bits: 16/15
c ---[1674]---> Sorter-cost:  463     Base: 2 2 2 2 2 2 2 7
c ---[1672]---> Sorter-cost:  256     Base: 2 2 2 2 2 2 2 2
c ---[1669]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[1666]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[1664]---> Adder-cost: 264   maxlim: 17664   bits: 16/15
c ---[1662]---> Sorter-cost: 1133     Base: 2 2 2 2 2 2 2 7
c ---[1660]---> Adder-cost: 76   maxlim: 4736   bits: 14/13
c ---[1656]---> Adder-cost: 108   maxlim: 8064   bits: 14/13
c ---[1654]---> Sorter-cost:  310     Base: 2 2 2 2 2 2 2 2
c ---[1652]---> Sorter-cost:  176     Base: 2 2 2 2 2 2 2 2
c ---[1648]---> Sorter-cost:  637     Base: 2 2 2 2 2 2 2 7
c ---[1645]---> Sorter-cost:  974     Base: 2 2 2 2 2 2 2 7
c ---[1643]---> Sorter-cost:  665     Base: 2 2 2 2 2 2 2 7
c ---[1640]---> Adder-cost: 160   maxlim: 9856   bits: 15/14
c ---[1638]---> Adder-cost: 60   maxlim: 9856   bits: 15/14
c ---[1636]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[1634]---> Adder-cost: 98   maxlim: 6144   bits: 14/13
c ---[1631]---> Sorter-cost:  467     Base: 2 2 2 2 2 2 2 7
c ---[1629]---> Adder-cost: 156   maxlim: 9728   bits: 15/14
c ---[1627]---> Adder-cost: 94   maxlim: 9984   bits: 15/14
c ---[1625]---> Adder-cost: 266   maxlim: 17024   bits: 16/15
c ---[1623]---> Adder-cost: 226   maxlim: 16896   bits: 16/15
c ---[1621]---> Adder-cost: 280   maxlim: 17792   bits: 16/15
c ---[1619]---> Adder-cost: 92   maxlim: 17792   bits: 16/15
c ---[1617]---> Sorter-cost:  556     Base: 2 2 2 2 2 2 2 7
c ---[1614]---> Sorter-cost:  415     Base: 2 2 2 2 2 2 2 7
c ---[1612]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[1610]---> Adder-cost: 140   maxlim: 8192   bits: 15/14
c ---[1608]---> Adder-cost: 76   maxlim: 5120   bits: 14/13
c ---[1606]---> Adder-cost: 74   maxlim: 4992   bits: 14/13
c ---[1603]---> Adder-cost: 244   maxlim: 16000   bits: 15/14
c ---[1601]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 7
c ---[1599]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[1597]---> Sorter-cost: 1028     Base: 2 2 2 2 2 2 2 7
c ---[1595]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[1591]---> Sorter-cost:  578     Base: 2 2 2 2 2 2 2 7
c ---[1589]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 7
c ---[1587]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[1585]---> Sorter-cost:  224     Base: 2 2 2 2 2 2 2 2
c ---[1583]---> Sorter-cost:  218     Base: 2 2 2 2 2 2 2 2
c ---[1580]---> Adder-cost: 180   maxlim: 11392   bits: 15/14
c ---[1578]---> Adder-cost: 98   maxlim: 6528   bits: 14/13
c ---[1576]---> Adder-cost: 158   maxlim: 10624   bits: 15/14
c ---[1573]---> Adder-cost: 142   maxlim: 8448   bits: 15/14
c ---[1571]---> Adder-cost: 200   maxlim: 12416   bits: 15/14
c ---[1569]---> Adder-cost: 70   maxlim: 12416   bits: 15/14
c ---[1565]---> Adder-cost: 120   maxlim: 7808   bits: 14/13
c ---[1561]---> Sorter-cost:  772     Base: 2 2 2 2 2 2 2 7
c ---[1558]---> Sorter-cost: 1005     Base: 2 2 2 2 2 2 2 7
c ---[1556]---> Adder-cost: 72   maxlim: 4352   bits: 14/13
c ---[1554]---> Adder-cost: 152   maxlim: 11264   bits: 15/14
c ---[1551]---> Adder-cost: 282   maxlim: 19968   bits: 16/15
c ---[1549]---> Adder-cost: 106   maxlim: 7296   bits: 14/13
c ---[1547]---> Adder-cost: 84   maxlim: 7424   bits: 14/13
c ---[1545]---> Adder-cost: 108   maxlim: 7680   bits: 14/13
c ---[1542]---> Sorter-cost:  965     Base: 2 2 2 2 2 2 2 7
c ---[1540]---> Sorter-cost:  610     Base: 2 2 2 2 2 2 2 7
c ---[1538]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2
c ---[1536]---> Adder-cost: 78   maxlim: 4992   bits: 14/13
c ---[1534]---> Adder-cost: 112   maxlim: 7552   bits: 14/13
c ---[1532]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[1530]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 7
c ---[1528]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1526]---> Sorter-cost:  492     Base: 2 2 2 2 2 2 2 7
c ---[1524]---> Adder-cost: 108   maxlim: 6656   bits: 14/13
c ---[1522]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[1518]---> Adder-cost: 104   maxlim: 8064   bits: 14/13
c ---[1515]---> Sorter-cost:  905     Base: 2 2 2 2 2 2 2 7
c ---[1512]---> Adder-cost: 220   maxlim: 13952   bits: 15/14
c ---[1510]---> Sorter-cost:  681     Base: 2 2 2 2 2 2 2 7
c ---[1508]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[1506]---> Adder-cost: 100   maxlim: 6272   bits: 14/13
c ---[1504]---> Adder-cost: 64   maxlim: 6272   bits: 14/13
c ---[1501]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 7
c ---[1499]---> Sorter-cost:  308     Base: 2 2 2 2 2 2 2 2
c ---[1497]---> Adder-cost: 94   maxlim: 5760   bits: 14/13
c ---[1495]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[1491]---> Sorter-cost:  256     Base: 2 2 2 2 2 2 2 2
c ---[1489]---> Adder-cost: 82   maxlim: 4864   bits: 14/13
c ---[1487]---> Adder-cost: 82   maxlim: 5248   bits: 14/13
c ---[1485]---> Adder-cost: 236   maxlim: 15360   bits: 15/14
c ---[1483]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[1481]---> Adder-cost: 206   maxlim: 14976   bits: 15/14
c ---[1476]---> Adder-cost: 102   maxlim: 6272   bits: 14/13
c ---[1474]---> Adder-cost: 138   maxlim: 8320   bits: 15/14
c ---[1471]---> Sorter-cost:  447     Base: 2 2 2 2 2 2 2 7
c ---[1469]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 7
c ---[1467]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 7
c ---[1464]---> Adder-cost: 78   maxlim: 5248   bits: 14/13
c ---[1462]---> Adder-cost: 120   maxlim: 8448   bits: 15/14
c ---[1460]---> Adder-cost: 88   maxlim: 5504   bits: 14/13
c ---[1458]---> Adder-cost: 100   maxlim: 6144   bits: 14/13
c ---[1456]---> Adder-cost: 124   maxlim: 7680   bits: 14/13
c ---[1454]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 7
c ---[1452]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[1450]---> Adder-cost: 202   maxlim: 12800   bits: 15/14
c ---[1448]---> Adder-cost: 138   maxlim: 12672   bits: 15/14
c ---[1446]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1444]---> Adder-cost: 168   maxlim: 11136   bits: 15/14
c ---[1442]---> Adder-cost: 146   maxlim: 9088   bits: 15/14
c ---[1440]---> Adder-cost: 318   maxlim: 19968   bits: 16/15
c ---[1438]---> Adder-cost: 114   maxlim: 7296   bits: 14/13
c ---[1436]---> Adder-cost: 86   maxlim: 6528   bits: 14/13
c ---[1434]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[1432]---> Sorter-cost:  879     Base: 2 2 2 2 2 2 2 7
c ---[1430]---> Adder-cost: 146   maxlim: 8704   bits: 15/14
c ---[1428]---> Adder-cost: 158   maxlim: 9856   bits: 15/14
c ---[1426]---> Adder-cost: 206   maxlim: 13056   bits: 15/14
c ---[1424]---> Adder-cost: 96   maxlim: 5888   bits: 14/13
c ---[1422]---> Adder-cost: 224   maxlim: 14976   bits: 15/14
c ---[1420]---> Adder-cost: 186   maxlim: 12032   bits: 15/14
c ---[1418]---> Adder-cost: 236   maxlim: 15872   bits: 15/14
c ---[1416]---> Adder-cost: 192   maxlim: 13312   bits: 15/14
c ---[1414]---> Adder-cost: 156   maxlim: 9472   bits: 15/14
c ---[1412]---> Adder-cost: 172   maxlim: 10880   bits: 15/14
c ---[1410]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[1408]---> Adder-cost: 238   maxlim: 16128   bits: 15/14
c ---[1406]---> Adder-cost: 92   maxlim: 5760   bits: 14/13
c ---[1403]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[1401]---> Adder-cost: 102   maxlim: 6400   bits: 14/13
c ---[1399]---> Adder-cost: 92   maxlim: 7168   bits: 14/13
c ---[1397]---> Adder-cost: 76   maxlim: 6784   bits: 14/13
c ---[1395]---> Adder-cost: 214   maxlim: 13824   bits: 15/14
c ---[1393]---> Adder-cost: 256   maxlim: 16896   bits: 16/15
c ---[1391]---> Adder-cost: 262   maxlim: 17664   bits: 16/15
c ---[1389]---> Adder-cost: 352   maxlim: 24960   bits: 16/15
c ---[1387]---> Adder-cost: 230   maxlim: 19072   bits: 16/15
c ---[1385]---> Adder-cost: 338   maxlim: 24576   bits: 16/15
c ---[1383]---> Adder-cost: 264   maxlim: 24320   bits: 16/15
c ---[1381]---> Adder-cost: 310   maxlim: 23936   bits: 16/15
c ---[1379]---> Adder-cost: 276   maxlim: 22272   bits: 16/15
c ---[1377]---> Adder-cost: 266   maxlim: 18944   bits: 16/15
c ---[1375]---> Adder-cost: 274   maxlim: 21376   bits: 16/15
c ---[1373]---> Adder-cost: 366   maxlim: 25472   bits: 16/15
c ---[1371]---> Adder-cost: 364   maxlim: 27264   bits: 16/15
c ---[1369]---> Adder-cost: 346   maxlim: 27008   bits: 16/15
c ---[1367]---> Adder-cost: 306   maxlim: 24448   bits: 16/15
c ---[1365]---> Adder-cost: 216   maxlim: 17792   bits: 16/15
c ---[1363]---> Adder-cost: 198   maxlim: 14848   bits: 15/14
c ---[1361]---> Adder-cost: 184   maxlim: 13824   bits: 15/14
c ---[1359]---> Adder-cost: 196   maxlim: 15104   bits: 15/14
c ---[1357]---> Adder-cost: 184   maxlim: 14464   bits: 15/14
c ---[1355]---> Adder-cost: 168   maxlim: 11776   bits: 15/14
c ---[1353]---> Adder-cost: 272   maxlim: 17792   bits: 16/15
c ---[1351]---> Adder-cost: 186   maxlim: 17920   bits: 16/15
c ---[1349]---> Adder-cost: 252   maxlim: 17664   bits: 16/15
c ---[1347]---> Adder-cost: 168   maxlim: 18304   bits: 16/15
c ---[1345]---> Adder-cost: 190   maxlim: 18048   bits: 16/15
c ---[1343]---> Adder-cost: 196   maxlim: 18560   bits: 16/15
c ---[1341]---> Adder-cost: 248   maxlim: 19584   bits: 16/15
c ---[1339]---> Adder-cost: 180   maxlim: 19328   bits: 16/15
c ---[1337]---> Adder-cost: 106   maxlim: 6656   bits: 14/13
c ---[1335]---> Adder-cost: 208   maxlim: 17536   bits: 16/15
c ---[1333]---> Adder-cost: 210   maxlim: 17664   bits: 16/15
c ---[1331]---> Adder-cost: 170   maxlim: 17024   bits: 16/15
c ---[1329]---> Adder-cost: 228   maxlim: 16896   bits: 16/15
c ---[1327]---> Adder-cost: 216   maxlim: 17408   bits: 16/15
c ---[1325]---> Adder-cost: 156   maxlim: 17024   bits: 16/15
c ---[1323]---> Adder-cost: 176   maxlim: 13952   bits: 15/14
c ---[1321]---> Adder-cost: 156   maxlim: 10112   bits: 15/14
c ---[1319]---> Adder-cost: 176   maxlim: 13696   bits: 15/14
c ---[1318]---> Adder-cost: 2294   maxlim: 140671   bits: 19/18
c ---[1317]---> Adder-cost: 11084   maxlim: 721919   bits: 20/20
c ---[1315]---> Adder-cost: 253   maxlim: 16895   bits: 16/15
c ---[1314]---> Adder-cost: 269   maxlim: 18303   bits: 16/15
c ---[1313]---> Adder-cost: 307   maxlim: 18687   bits: 16/15
c ---[1311]---> Adder-cost: 323   maxlim: 19711   bits: 16/15
c ---[1310]---> Adder-cost: 343   maxlim: 21631   bits: 16/15
c ---[1308]---> Adder-cost: 518   maxlim: 30591   bits: 16/15
c ---[1307]---> Adder-cost: 295   maxlim: 18815   bits: 16/15
c ---[1305]---> Adder-cost: 496   maxlim: 30463   bits: 16/15
c ---[1299]---> Adder-cost: 347   maxlim: 20351   bits: 16/15
c ---[1297]---> Adder-cost: 496   maxlim: 31871   bits: 16/15
c ---[1296]---> Adder-cost: 599   maxlim: 37631   bits: 17/16
c ---[1292]---> Adder-cost: 406   maxlim: 24447   bits: 16/15
c ---[1291]---> Adder-cost: 2970   maxlim: 199423   bits: 19/18
c ---[1288]---> Adder-cost: 7387   maxlim: 487423   bits: 20/19
c ---[1287]---> Adder-cost: 725   maxlim: 44927   bits: 17/16
c ---[1286]---> Adder-cost: 3268   maxlim: 162559   bits: 18/18
c ---[1285]---> Adder-cost: 77   maxlim: 5247   bits: 14/13
c ---[1284]---> Adder-cost: 172   maxlim: 2943   bits: 13/12
c ---[1281]---> Adder-cost: 232   maxlim: 11903   bits: 15/14
c ---[1279]---> Adder-cost: 135   maxlim: 5759   bits: 14/13
c ---[1278]---> Adder-cost: 75   maxlim: 6271   bits: 14/13
c ---[1276]---> Adder-cost: 416   maxlim: 23039   bits: 16/15
c ---[1275]---> Adder-cost: 194   maxlim: 2559   bits: 13/12
c ---[1272]---> Adder-cost: 105   maxlim: 3455   bits: 13/12
c ---[1271]---> Adder-cost: 1116   maxlim: 63743   bits: 17/16
c ---[1270]---> Adder-cost: 12456   maxlim: 581375   bits: 21/20
c ---[1268]---> Adder-cost: 21598   maxlim: 1482239   bits: 21/21
c ---[1266]---> Adder-cost: 156   maxlim: 12672   bits: 15/14
c ---[1264]---> Adder-cost: 3472   maxlim: 184063   bits: 19/18
c ---[1263]---> Adder-cost: 53984   maxlim: 15965567   bits: 25/24
c ---[1261]---> Adder-cost: 70526   maxlim: 47273727   bits: 27/26
c ---[1260]---> Adder-cost: 4596   maxlim: 1339647   bits: 22/21
c ---[1259]---> Adder-cost: 26986   maxlim: 8842239   bits: 25/24
c ---[1257]---> Adder-cost: 621   maxlim: 282239   bits: 20/19
c ---[1256]---> Adder-cost: 752   maxlim: 573951   bits: 21/20
c ---[1255]---> Adder-cost: 687   maxlim: 374399   bits: 20/19
c ---[1254]---> Adder-cost: 931   maxlim: 306559   bits: 20/19
c ---[1253]---> Adder-cost: 972   maxlim: 790143   bits: 21/20
c ---[1251]---> Adder-cost: 148   maxlim: 9472   bits: 15/14
c ---[1250]---> Adder-cost: 1379   maxlim: 865663   bits: 21/20
c ---[1249]---> Adder-cost: 856   maxlim: 1084671   bits: 22/21
c ---[1248]---> Adder-cost: 545   maxlim: 342527   bits: 20/19
c ---[1247]---> Adder-cost: 1189   maxlim: 183807   bits: 19/18
c ---[1246]---> Adder-cost: 428   maxlim: 477439   bits: 20/19
c ---[1245]---> Adder-cost: 415   maxlim: 152319   bits: 19/18
c ---[1243]---> Adder-cost: 888   maxlim: 707967   bits: 21/20
c ---[1241]---> Adder-cost: 1418   maxlim: 1451007   bits: 22/21
c ---[1240]---> Adder-cost: 1604   maxlim: 1089279   bits: 22/21
c ---[1238]---> Adder-cost: 505   maxlim: 237183   bits: 19/18
c ---[1237]---> Adder-cost: 1042   maxlim: 835199   bits: 21/20
c ---[1236]---> Adder-cost: 6857   maxlim: 2035583   bits: 22/21
c ---[1235]---> Adder-cost: 439   maxlim: 284159   bits: 20/19
c ---[1234]---> Adder-cost: 498   maxlim: 147071   bits: 19/18
c ---[1233]---> Adder-cost: 6092   maxlim: 609023   bits: 21/20
c ---[1232]---> Adder-cost: 34132   maxlim: 20249599   bits: 26/25
c ---[1231]---> Adder-cost: 857   maxlim: 485759   bits: 20/19
c ---[1230]---> Adder-cost: 727   maxlim: 721919   bits: 21/20
c ---[1229]---> Adder-cost: 818   maxlim: 479999   bits: 20/19
c ---[1228]---> Sorter-cost:13837     Base: 2 2 2 2 2 2 2 5 3 2 2 2
c ---[1227]---> Adder-cost: 1049   maxlim: 675839   bits: 21/20
c ---[1226]---> Adder-cost: 1492   maxlim: 1043839   bits: 21/20
c ---[1225]---> Adder-cost: 571   maxlim: 526719   bits: 21/20
c ---[1224]---> Adder-cost: 1461   maxlim: 132735   bits: 19/18
c ---[1222]---> Adder-cost: 888   maxlim: 1132799   bits: 22/21
c ---[1221]---> Adder-cost: 1324   maxlim: 2545919   bits: 22/22
c ---[1219]---> Adder-cost: 246   maxlim: 197759   bits: 19/18
c ---[1218]---> Adder-cost: 604   maxlim: 392319   bits: 20/19
c ---[1217]---> Adder-cost: 995   maxlim: 446079   bits: 20/19
c ---[1216]---> Adder-cost: 9522   maxlim: 6486015   bits: 24/23
c ---[1213]---> Adder-cost: 284   maxlim: 18816   bits: 16/15
c ---[1211]---> Adder-cost: 278   maxlim: 19968   bits: 16/15
c ---[1209]---> Adder-cost: 314   maxlim: 23680   bits: 16/15
c ---[1207]---> Adder-cost: 104   maxlim: 23680   bits: 16/15
c ---[1205]---> Adder-cost: 260   maxlim: 22144   bits: 16/15
c ---[1203]---> Adder-cost: 276   maxlim: 21248   bits: 16/15
c ---[1201]---> Adder-cost: 176   maxlim: 13696   bits: 15/14
c ---[1199]---> Adder-cost: 78   maxlim: 13696   bits: 15/14
c ---[1197]---> Adder-cost: 290   maxlim: 19456   bits: 16/15
c ---[1195]---> Adder-cost: 300   maxlim: 21120   bits: 16/15
c ---[1193]---> Adder-cost: 282   maxlim: 19968   bits: 16/15
c ---[1191]---> Adder-cost: 94   maxlim: 19968   bits: 16/15
c ---[1189]---> Adder-cost: 284   maxlim: 19968   bits: 16/15
c ---[1187]---> Adder-cost: 246   maxlim: 20224   bits: 16/15
c ---[1185]---> Adder-cost: 242   maxlim: 18944   bits: 16/15
c ---[1183]---> Adder-cost: 132   maxlim: 9344   bits: 15/14
c ---[1181]---> Adder-cost: 254   maxlim: 21248   bits: 16/15
c ---[1179]---> Adder-cost: 266   maxlim: 20608   bits: 16/15
c ---[1177]---> Adder-cost: 248   maxlim: 20480   bits: 16/15
c ---[1175]---> Adder-cost: 246   maxlim: 21120   bits: 16/15
c ---[1173]---> Adder-cost: 226   maxlim: 20480   bits: 16/15
c ---[1171]---> Adder-cost: 210   maxlim: 20096   bits: 16/15
c ---[1169]---> Adder-cost: 186   maxlim: 21376   bits: 16/15
c ---[1167]---> Adder-cost: 100   maxlim: 21376   bits: 16/15
c ---[1165]---> Adder-cost: 100   maxlim: 21376   bits: 16/15
c ---[1163]---> Adder-cost: 120   maxlim: 21248   bits: 16/15
c ---[1161]---> Adder-cost: 170   maxlim: 20352   bits: 16/15
c ---[1159]---> Adder-cost: 92   maxlim: 20352   bits: 16/15
c ---[1157]---> Adder-cost: 132   maxlim: 19840   bits: 16/15
c ---[1155]---> Adder-cost: 92   maxlim: 19840   bits: 16/15
c ---[1153]---> Adder-cost: 236   maxlim: 21760   bits: 16/15
c ---[1151]---> Adder-cost: 174   maxlim: 12928   bits: 15/14
c ---[1149]---> Adder-cost: 184   maxlim: 13184   bits: 15/14
c ---[1147]---> Adder-cost: 100   maxlim: 6144   bits: 14/13
c ---[1145]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[1143]---> Adder-cost: 80   maxlim: 5760   bits: 14/13
c ---[1141]---> Adder-cost: 56   maxlim: 5888   bits: 14/13
c ---[1139]---> Sorter-cost: 1008     Base: 2 2 2 2 2 2 2 7
c ---[1137]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 7
c ---[1133]---> Adder-cost: 142   maxlim: 8576   bits: 15/14
c ---[1131]---> Adder-cost: 138   maxlim: 8832   bits: 15/14
c ---[1129]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[1127]---> Adder-cost: 300   maxlim: 20736   bits: 16/15
c ---[1125]---> Adder-cost: 102   maxlim: 20736   bits: 16/15
c ---[1123]---> Adder-cost: 264   maxlim: 18944   bits: 16/15
c ---[1121]---> Adder-cost: 96   maxlim: 18944   bits: 16/15
c ---[1119]---> Adder-cost: 108   maxlim: 8192   bits: 15/14
c ---[1117]---> Adder-cost: 106   maxlim: 7296   bits: 14/13
c ---[1115]---> Adder-cost: 146   maxlim: 10240   bits: 15/14
c ---[1113]---> Adder-cost: 104   maxlim: 7552   bits: 14/13
c ---[1111]---> Adder-cost: 194   maxlim: 13568   bits: 15/14
c ---[1109]---> Adder-cost: 78   maxlim: 13568   bits: 15/14
c ---[1107]---> Adder-cost: 178   maxlim: 13952   bits: 15/14
c ---[1105]---> Adder-cost: 122   maxlim: 12416   bits: 15/14
c ---[1103]---> Adder-cost: 70   maxlim: 12416   bits: 15/14
c ---[1101]---> Adder-cost: 124   maxlim: 12672   bits: 15/14
c ---[1099]---> Adder-cost: 160   maxlim: 14080   bits: 15/14
c ---[1097]---> Adder-cost: 142   maxlim: 9856   bits: 15/14
c ---[1095]---> Adder-cost: 142   maxlim: 9984   bits: 15/14
c ---[1093]---> Adder-cost: 126   maxlim: 9344   bits: 15/14
c ---[1091]---> Adder-cost: 124   maxlim: 9216   bits: 15/14
c ---[1089]---> Adder-cost: 112   maxlim: 8192   bits: 15/14
c ---[1087]---> Adder-cost: 116   maxlim: 8320   bits: 15/14
c ---[1085]---> Adder-cost: 124   maxlim: 8320   bits: 15/14
c ---[1083]---> Adder-cost: 118   maxlim: 7424   bits: 14/13
c ---[1081]---> Sorter-cost:  786     Base: 2 2 2 2 2 2 2 7
c ---[1079]---> Sorter-cost:  550     Base: 2 2 2 2 2 2 2 7
c ---[1077]---> Adder-cost: 142   maxlim: 8832   bits: 15/14
c ---[1075]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[1073]---> Sorter-cost:  531     Base: 2 2 2 2 2 2 2 7
c ---[1071]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[1069]---> Sorter-cost:  675     Base: 2 2 2 2 2 2 2 7
c ---[1067]---> Sorter-cost:  589     Base: 2 2 2 2 2 2 2 7
c ---[1065]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[1063]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 7
c ---[1061]---> Sorter-cost:  732     Base: 2 2 2 2 2 2 2 7
c ---[1059]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[1057]---> Adder-cost: 152   maxlim: 9344   bits: 15/14
c ---[1055]---> Adder-cost: 138   maxlim: 9472   bits: 15/14
c ---[1053]---> Adder-cost: 106   maxlim: 9600   bits: 15/14
c ---[1051]---> Adder-cost: 108   maxlim: 6784   bits: 14/13
c ---[1049]---> Adder-cost: 86   maxlim: 7936   bits: 14/13
c ---[1047]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[1045]---> Adder-cost: 120   maxlim: 8064   bits: 14/13
c ---[1043]---> Adder-cost: 120   maxlim: 8192   bits: 15/14
c ---[1041]---> Adder-cost: 62   maxlim: 8192   bits: 15/14
c ---[1039]---> Adder-cost: 102   maxlim: 8320   bits: 15/14
c ---[1037]---> Adder-cost: 128   maxlim: 9472   bits: 15/14
c ---[1035]---> Adder-cost: 86   maxlim: 7808   bits: 14/13
c ---[1032]---> Adder-cost: 164   maxlim: 11264   bits: 15/14
c ---[1030]---> Adder-cost: 156   maxlim: 11392   bits: 15/14
c ---[1028]---> Adder-cost: 132   maxlim: 11264   bits: 15/14
c ---[1026]---> Adder-cost: 272   maxlim: 16896   bits: 16/15
c ---[1024]---> Adder-cost: 230   maxlim: 16384   bits: 16/15
c ---[1022]---> Adder-cost: 182   maxlim: 12672   bits: 15/14
c ---[1020]---> Adder-cost: 183   maxlim: 12288   bits: 15/14
c ---[1018]---> Adder-cost: 224   maxlim: 14720   bits: 15/14
c ---[1016]---> Adder-cost: 278   maxlim: 18176   bits: 16/15
c ---[1014]---> Adder-cost: 90   maxlim: 9728   bits: 15/14
c ---[1012]---> Adder-cost: 220   maxlim: 15616   bits: 15/14
c ---[1010]---> Adder-cost: 228   maxlim: 15488   bits: 15/14
c ---[1008]---> Adder-cost: 186   maxlim: 14592   bits: 15/14
c ---[1006]---> Adder-cost: 78   maxlim: 14592   bits: 15/14
c ---[1004]---> Adder-cost: 70   maxlim: 4992   bits: 14/13
c ---[1002]---> Adder-cost: 66   maxlim: 4480   bits: 14/13
c ---[1000]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[ 998]---> Adder-cost: 72   maxlim: 4992   bits: 14/13
c ---[ 996]---> Adder-cost: 68   maxlim: 5376   bits: 14/13
c ---[ 994]---> Adder-cost: 40   maxlim: 5376   bits: 14/13
c ---[ 992]---> Adder-cost: 116   maxlim: 7936   bits: 14/13
c ---[ 990]---> Adder-cost: 62   maxlim: 5248   bits: 14/13
c ---[ 988]---> Adder-cost: 82   maxlim: 5888   bits: 14/13
c ---[ 986]---> Adder-cost: 78   maxlim: 4736   bits: 14/13
c ---[ 984]---> Adder-cost: 80   maxlim: 5248   bits: 14/13
c ---[ 982]---> Adder-cost: 94   maxlim: 7552   bits: 14/13
c ---[ 980]---> Adder-cost: 124   maxlim: 8192   bits: 15/14
c ---[ 978]---> Adder-cost: 132   maxlim: 8448   bits: 15/14
c ---[ 976]---> Adder-cost: 118   maxlim: 8320   bits: 15/14
c ---[ 974]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[ 972]---> Adder-cost: 144   maxlim: 9216   bits: 15/14
c ---[ 970]---> Adder-cost: 184   maxlim: 12672   bits: 15/14
c ---[ 968]---> Adder-cost: 140   maxlim: 10624   bits: 15/14
c ---[ 966]---> Adder-cost: 88   maxlim: 5760   bits: 14/13
c ---[ 964]---> Adder-cost: 148   maxlim: 9856   bits: 15/14
c ---[ 962]---> Adder-cost: 118   maxlim: 8576   bits: 15/14
c ---[ 960]---> Adder-cost: 174   maxlim: 11392   bits: 15/14
c ---[ 958]---> Adder-cost: 174   maxlim: 12416   bits: 15/14
c ---[ 956]---> Adder-cost: 178   maxlim: 12544   bits: 15/14
c ---[ 954]---> Adder-cost: 72   maxlim: 5632   bits: 14/13
c ---[ 952]---> Adder-cost: 158   maxlim: 13184   bits: 15/14
c ---[ 950]---> Adder-cost: 98   maxlim: 6144   bits: 14/13
c ---[ 948]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[ 946]---> Adder-cost: 98   maxlim: 6912   bits: 14/13
c ---[ 944]---> Adder-cost: 48   maxlim: 6912   bits: 14/13
c ---[ 942]---> Adder-cost: 98   maxlim: 6656   bits: 14/13
c ---[ 940]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[ 938]---> Adder-cost: 108   maxlim: 7936   bits: 14/13
c ---[ 936]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[ 934]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 7
c ---[ 932]---> Adder-cost: 106   maxlim: 7680   bits: 14/13
c ---[ 930]---> Adder-cost: 132   maxlim: 8832   bits: 15/14
c ---[ 928]---> Adder-cost: 122   maxlim: 9344   bits: 15/14
c ---[ 926]---> Adder-cost: 132   maxlim: 9728   bits: 15/14
c ---[ 924]---> Adder-cost: 198   maxlim: 13824   bits: 15/14
c ---[ 922]---> Adder-cost: 74   maxlim: 13824   bits: 15/14
c ---[ 920]---> Adder-cost: 48   maxlim: 6656   bits: 14/13
c ---[ 918]---> Adder-cost: 146   maxlim: 11392   bits: 15/14
c ---[ 916]---> Adder-cost: 164   maxlim: 12160   bits: 15/14
c ---[ 914]---> Adder-cost: 64   maxlim: 12160   bits: 15/14
c ---[ 912]---> Adder-cost: 168   maxlim: 13952   bits: 15/14
c ---[ 910]---> Adder-cost: 72   maxlim: 13952   bits: 15/14
c ---[ 908]---> Adder-cost: 270   maxlim: 17920   bits: 16/15
c ---[ 906]---> Adder-cost: 90   maxlim: 17920   bits: 16/15
c ---[ 904]---> Adder-cost: 208   maxlim: 16000   bits: 15/14
c ---[ 902]---> Adder-cost: 78   maxlim: 16000   bits: 15/14
c ---[ 900]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 7
c ---[ 898]---> Adder-cost: 224   maxlim: 14848   bits: 15/14
c ---[ 896]---> Adder-cost: 80   maxlim: 14848   bits: 15/14
c ---[ 894]---> Adder-cost: 190   maxlim: 13440   bits: 15/14
c ---[ 892]---> Adder-cost: 78   maxlim: 13440   bits: 15/14
c ---[ 890]---> Adder-cost: 270   maxlim: 18944   bits: 16/15
c ---[ 888]---> Adder-cost: 96   maxlim: 18944   bits: 16/15
c ---[ 886]---> Adder-cost: 210   maxlim: 14976   bits: 15/14
c ---[ 884]---> Adder-cost: 80   maxlim: 14976   bits: 15/14
c ---[ 882]---> Adder-cost: 184   maxlim: 14720   bits: 15/14
c ---[ 880]---> Adder-cost: 76   maxlim: 14720   bits: 15/14
c ---[ 878]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 7
c ---[ 876]---> Adder-cost: 208   maxlim: 14848   bits: 15/14
c ---[ 874]---> Adder-cost: 80   maxlim: 14848   bits: 15/14
c ---[ 872]---> Adder-cost: 190   maxlim: 14080   bits: 15/14
c ---[ 870]---> Adder-cost: 74   maxlim: 14080   bits: 15/14
c ---[ 868]---> Adder-cost: 172   maxlim: 14336   bits: 15/14
c ---[ 866]---> Adder-cost: 76   maxlim: 14336   bits: 15/14
c ---[ 864]---> Adder-cost: 174   maxlim: 12032   bits: 15/14
c ---[ 862]---> Adder-cost: 68   maxlim: 12032   bits: 15/14
c ---[ 860]---> Adder-cost: 154   maxlim: 10624   bits: 15/14
c ---[ 858]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[ 856]---> Sorter-cost:  403     Base: 2 2 2 2 2 2 2 7
c ---[ 854]---> Adder-cost: 128   maxlim: 8576   bits: 15/14
c ---[ 852]---> Adder-cost: 138   maxlim: 9088   bits: 15/14
c ---[ 850]---> Adder-cost: 56   maxlim: 9088   bits: 15/14
c ---[ 848]---> Adder-cost: 116   maxlim: 7680   bits: 14/13
c ---[ 846]---> Adder-cost: 50   maxlim: 7680   bits: 14/13
c ---[ 844]---> Adder-cost: 142   maxlim: 10112   bits: 15/14
c ---[ 842]---> Adder-cost: 62   maxlim: 10112   bits: 15/14
c ---[ 840]---> Adder-cost: 120   maxlim: 7808   bits: 14/13
c ---[ 838]---> Adder-cost: 48   maxlim: 7808   bits: 14/13
c ---[ 836]---> Sorter-cost:  397     Base: 2 2 2 2 2 2 2 7
c ---[ 834]---> Adder-cost: 110   maxlim: 7552   bits: 14/13
c ---[ 832]---> Adder-cost: 48   maxlim: 7552   bits: 14/13
c ---[ 830]---> Adder-cost: 138   maxlim: 11008   bits: 15/14
c ---[ 828]---> Adder-cost: 68   maxlim: 11008   bits: 15/14
c ---[ 826]---> Adder-cost: 124   maxlim: 11392   bits: 15/14
c ---[ 824]---> Adder-cost: 72   maxlim: 11392   bits: 15/14
c ---[ 822]---> Adder-cost: 202   maxlim: 15232   bits: 15/14
c ---[ 820]---> Adder-cost: 80   maxlim: 15232   bits: 15/14
c ---[ 818]---> Adder-cost: 80   maxlim: 15232   bits: 15/14
c ---[ 816]---> Adder-cost: 80   maxlim: 15232   bits: 15/14
c ---[ 814]---> Adder-cost: 160   maxlim: 14848   bits: 15/14
c ---[ 810]---> Adder-cost: 136   maxlim: 8960   bits: 15/14
c ---[ 808]---> Adder-cost: 60   maxlim: 8960   bits: 15/14
c ---[ 806]---> Adder-cost: 128   maxlim: 8320   bits: 15/14
c ---[ 804]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[ 802]---> Adder-cost: 108   maxlim: 8320   bits: 15/14
c ---[ 800]---> Adder-cost: 60   maxlim: 8320   bits: 15/14
c ---[ 798]---> Adder-cost: 156   maxlim: 9600   bits: 15/14
c ---[ 796]---> Sorter-cost:  652     Base: 2 2 2 2 2 2 2 7
c ---[ 794]---> Adder-cost: 94   maxlim: 9344   bits: 15/14
c ---[ 792]---> Sorter-cost:  887     Base: 2 2 2 2 2 2 2 7
c ---[ 790]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[ 788]---> Sorter-cost:  851     Base: 2 2 2 2 2 2 2 7
c ---[ 786]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 7
c ---[ 784]---> Adder-cost: 154   maxlim: 9728   bits: 15/14
c ---[ 782]---> Adder-cost: 64   maxlim: 9728   bits: 15/14
c ---[ 780]---> Adder-cost: 130   maxlim: 8576   bits: 15/14
c ---[ 778]---> Adder-cost: 58   maxlim: 8576   bits: 15/14
c ---[ 776]---> Adder-cost: 94   maxlim: 6016   bits: 14/13
c ---[ 774]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[ 772]---> Adder-cost: 108   maxlim: 7040   bits: 14/13
c ---[ 770]---> Adder-cost: 46   maxlim: 7040   bits: 14/13
c ---[ 768]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2
c ---[ 766]---> Sorter-cost:  246     Base: 2 2 2 2 2 2 2 7
c ---[ 764]---> Sorter-cost:  885     Base: 2 2 2 2 2 2 2 7
c ---[ 762]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 7
c ---[ 760]---> Adder-cost: 62   maxlim: 4480   bits: 14/13
c ---[ 758]---> Adder-cost: 110   maxlim: 7040   bits: 14/13
c ---[ 756]---> Adder-cost: 168   maxlim: 11136   bits: 15/14
c ---[ 754]---> Adder-cost: 192   maxlim: 12672   bits: 15/14
c ---[ 752]---> Adder-cost: 116   maxlim: 7808   bits: 14/13
c ---[ 750]---> Adder-cost: 104   maxlim: 6528   bits: 14/13
c ---[ 748]---> Adder-cost: 138   maxlim: 8448   bits: 15/14
c ---[ 746]---> Adder-cost: 138   maxlim: 9088   bits: 15/14
c ---[ 744]---> Adder-cost: 112   maxlim: 9472   bits: 15/14
c ---[ 742]---> Adder-cost: 210   maxlim: 13824   bits: 15/14
c ---[ 740]---> Adder-cost: 74   maxlim: 13824   bits: 15/14
c ---[ 738]---> Adder-cost: 212   maxlim: 15744   bits: 15/14
c ---[ 736]---> Adder-cost: 78   maxlim: 15744   bits: 15/14
c ---[ 734]---> Sorter-cost:  994     Base: 2 2 2 2 2 2 2 7
c ---[ 732]---> Adder-cost: 132   maxlim: 8832   bits: 15/14
c ---[ 730]---> Adder-cost: 60   maxlim: 8832   bits: 15/14
c ---[ 728]---> Adder-cost: 174   maxlim: 11008   bits: 15/14
c ---[ 726]---> Adder-cost: 68   maxlim: 11008   bits: 15/14
c ---[ 724]---> Adder-cost: 186   maxlim: 12544   bits: 15/14
c ---[ 722]---> Adder-cost: 72   maxlim: 12544   bits: 15/14
c ---[ 720]---> Adder-cost: 150   maxlim: 11520   bits: 15/14
c ---[ 718]---> Adder-cost: 66   maxlim: 11520   bits: 15/14
c ---[ 716]---> Adder-cost: 110   maxlim: 12032   bits: 15/14
c ---[ 714]---> Adder-cost: 68   maxlim: 12032   bits: 15/14
c ---[ 712]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 7
c ---[ 709]---> Adder-cost: 96   maxlim: 7040   bits: 14/13
c ---[ 707]---> Adder-cost: 102   maxlim: 7808   bits: 14/13
c ---[ 705]---> Adder-cost: 106   maxlim: 7424   bits: 14/13
c ---[ 703]---> Sorter-cost:  573     Base: 2 2 2 2 2 2 2 7
c ---[ 701]---> Sorter-cost:  893     Base: 2 2 2 2 2 2 2 7
c ---[ 698]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[ 696]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[ 694]---> Adder-cost: 78   maxlim: 4864   bits: 14/13
c ---[ 692]---> Adder-cost: 40   maxlim: 4864   bits: 14/13
c ---[ 690]---> Adder-cost: 170   maxlim: 10752   bits: 15/14
c ---[ 688]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[ 686]---> Adder-cost: 166   maxlim: 11008   bits: 15/14
c ---[ 683]---> Adder-cost: 68   maxlim: 11008   bits: 15/14
c ---[ 681]---> Adder-cost: 90   maxlim: 5888   bits: 14/13
c ---[ 679]---> Adder-cost: 88   maxlim: 6528   bits: 14/13
c ---[ 677]---> Adder-cost: 172   maxlim: 11648   bits: 15/14
c ---[ 674]---> Adder-cost: 100   maxlim: 6144   bits: 14/13
c ---[ 672]---> Adder-cost: 62   maxlim: 6912   bits: 14/13
c ---[ 670]---> Adder-cost: 74   maxlim: 4352   bits: 14/13
c ---[ 668]---> Adder-cost: 74   maxlim: 6784   bits: 14/13
c ---[ 666]---> Adder-cost: 40   maxlim: 4352   bits: 14/13
c ---[ 664]---> Adder-cost: 88   maxlim: 5120   bits: 14/13
c ---[ 662]---> Adder-cost: 58   maxlim: 5248   bits: 14/13
c ---[ 660]---> Adder-cost: 66   maxlim: 4480   bits: 14/13
c ---[ 658]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[ 656]---> Adder-cost: 202   maxlim: 12800   bits: 15/14
c ---[ 654]---> Adder-cost: 76   maxlim: 12800   bits: 15/14
c ---[ 652]---> Adder-cost: 182   maxlim: 12800   bits: 15/14
c ---[ 650]---> Adder-cost: 76   maxlim: 12800   bits: 15/14
c ---[ 648]---> Adder-cost: 142   maxlim: 11136   bits: 15/14
c ---[ 646]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 7
c ---[ 644]---> Adder-cost: 122   maxlim: 10496   bits: 15/14
c ---[ 642]---> Adder-cost: 242   maxlim: 15616   bits: 15/14
c ---[ 640]---> Adder-cost: 138   maxlim: 15360   bits: 15/14
c ---[ 638]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 636]---> Sorter-cost:  916     Base: 2 2 2 2 2 2 2 7
c ---[ 634]---> Adder-cost: 100   maxlim: 6528   bits: 14/13
c ---[ 632]---> Adder-cost: 44   maxlim: 6528   bits: 14/13
c ---[ 630]---> Adder-cost: 76   maxlim: 4736   bits: 14/13
c ---[ 628]---> Adder-cost: 38   maxlim: 4736   bits: 14/13
c ---[ 626]---> Adder-cost: 94   maxlim: 6144   bits: 14/13
c ---[ 624]---> Sorter-cost:  266     Base: 2 2 2 2 2 2 2 2
c ---[ 622]---> Adder-cost: 74   maxlim: 6528   bits: 14/13
c ---[ 620]---> Sorter-cost:  907     Base: 2 2 2 2 2 2 2 7
c ---[ 618]---> Sorter-cost:  525     Base: 2 2 2 2 2 2 2 7
c ---[ 616]---> Sorter-cost:  934     Base: 2 2 2 2 2 2 2 7
c ---[ 614]---> Sorter-cost:  740     Base: 2 2 2 2 2 2 2 7
c ---[ 611]---> Adder-cost: 136   maxlim: 10112   bits: 15/14
c ---[ 609]---> Adder-cost: 58   maxlim: 6016   bits: 14/13
c ---[ 607]---> Sorter-cost:  542     Base: 2 2 2 2 2 2 2 7
c ---[ 605]---> Adder-cost: 40   maxlim: 6016   bits: 14/13
c ---[ 603]---> Adder-cost: 88   maxlim: 6144   bits: 14/13
c ---[ 601]---> Adder-cost: 46   maxlim: 6144   bits: 14/13
c ---[ 599]---> Adder-cost: 96   maxlim: 7168   bits: 14/13
c ---[ 597]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[ 595]---> Adder-cost: 172   maxlim: 10496   bits: 15/14
c ---[ 593]---> Adder-cost: 68   maxlim: 10496   bits: 15/14
c ---[ 591]---> Adder-cost: 150   maxlim: 9600   bits: 15/14
c ---[ 589]---> Adder-cost: 62   maxlim: 9600   bits: 15/14
c ---[ 587]---> Adder-cost: 74   maxlim: 4480   bits: 14/13
c ---[ 585]---> Sorter-cost:  499     Base: 2 2 2 2 2 2 2 7
c ---[ 583]---> Adder-cost: 40   maxlim: 4480   bits: 14/13
c ---[ 581]---> Adder-cost: 86   maxlim: 5376   bits: 14/13
c ---[ 579]---> Adder-cost: 74   maxlim: 5504   bits: 14/13
c ---[ 575]---> Adder-cost: 198   maxlim: 13184   bits: 15/14
c ---[ 573]---> Adder-cost: 74   maxlim: 13184   bits: 15/14
c ---[ 571]---> Adder-cost: 152   maxlim: 12928   bits: 15/14
c ---[ 569]---> Adder-cost: 76   maxlim: 12928   bits: 15/14
c ---[ 567]---> Adder-cost: 164   maxlim: 11136   bits: 15/14
c ---[ 565]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 562]---> Adder-cost: 184   maxlim: 12416   bits: 15/14
c ---[ 558]---> Adder-cost: 82   maxlim: 5632   bits: 14/13
c ---[ 556]---> Adder-cost: 90   maxlim: 5760   bits: 14/13
c ---[ 554]---> Adder-cost: 42   maxlim: 5760   bits: 14/13
c ---[ 552]---> Adder-cost: 98   maxlim: 6272   bits: 14/13
c ---[ 550]---> Adder-cost: 116   maxlim: 7808   bits: 14/13
c ---[ 548]---> Adder-cost: 100   maxlim: 7168   bits: 14/13
c ---[ 546]---> Sorter-cost:  645     Base: 2 2 2 2 2 2 2 7
c ---[ 544]---> Adder-cost: 94   maxlim: 6400   bits: 14/13
c ---[ 542]---> Adder-cost: 44   maxlim: 6400   bits: 14/13
c ---[ 540]---> Adder-cost: 76   maxlim: 4480   bits: 14/13
c ---[ 538]---> Adder-cost: 64   maxlim: 4352   bits: 14/13
c ---[ 536]---> Adder-cost: 106   maxlim: 6400   bits: 14/13
c ---[ 534]---> Adder-cost: 94   maxlim: 6144   bits: 14/13
c ---[ 532]---> Adder-cost: 82   maxlim: 5632   bits: 14/13
c ---[ 530]---> Adder-cost: 42   maxlim: 5632   bits: 14/13
c ---[ 528]---> Adder-cost: 174   maxlim: 11136   bits: 15/14
c ---[ 526]---> Adder-cost: 68   maxlim: 11136   bits: 15/14
c ---[ 524]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 7
c ---[ 522]---> Adder-cost: 160   maxlim: 11520   bits: 15/14
c ---[ 520]---> Adder-cost: 66   maxlim: 11520   bits: 15/14
c ---[ 518]---> Adder-cost: 160   maxlim: 10240   bits: 15/14
c ---[ 515]---> Adder-cost: 88   maxlim: 5760   bits: 14/13
c ---[ 513]---> Adder-cost: 76   maxlim: 6656   bits: 14/13
c ---[ 511]---> Adder-cost: 100   maxlim: 7552   bits: 14/13
c ---[ 509]---> Adder-cost: 78   maxlim: 4736   bits: 14/13
c ---[ 507]---> Adder-cost: 108   maxlim: 7040   bits: 14/13
c ---[ 505]---> Adder-cost: 72   maxlim: 4736   bits: 14/13
c ---[ 503]---> Adder-cost: 80   maxlim: 4736   bits: 14/13
c ---[ 501]---> Adder-cost: 76   maxlim: 4736   bits: 14/13
c ---[ 499]---> Adder-cost: 208   maxlim: 13184   bits: 15/14
c ---[ 497]---> Adder-cost: 46   maxlim: 4480   bits: 14/13
c ---[ 495]---> Adder-cost: 202   maxlim: 13440   bits: 15/14
c ---[ 493]---> Adder-cost: 156   maxlim: 10752   bits: 15/14
c ---[ 491]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[ 489]---> Adder-cost: 224   maxlim: 14336   bits: 15/14
c ---[ 487]---> Adder-cost: 76   maxlim: 14336   bits: 15/14
c ---[ 485]---> Adder-cost: 140   maxlim: 8704   bits: 15/14
c ---[ 483]---> Adder-cost: 214   maxlim: 13952   bits: 15/14
c ---[ 481]---> Adder-cost: 72   maxlim: 13952   bits: 15/14
c ---[ 479]---> Sorter-cost:  594     Base: 2 2 2 2 2 2 2 7
c ---[ 477]---> Adder-cost: 192   maxlim: 14208   bits: 15/14
c ---[ 475]---> Adder-cost: 72   maxlim: 14208   bits: 15/14
c ---[ 473]---> Adder-cost: 72   maxlim: 14208   bits: 15/14
c ---[ 470]---> Adder-cost: 130   maxlim: 8448   bits: 15/14
c ---[ 468]---> Adder-cost: 78   maxlim: 6400   bits: 14/13
c ---[ 466]---> Adder-cost: 78   maxlim: 5888   bits: 14/13
c ---[ 464]---> Adder-cost: 158   maxlim: 10368   bits: 15/14
c ---[ 462]---> Sorter-cost:  430     Base: 2 2 2 2 2 2 2 7
c ---[ 460]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2
c ---[ 458]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 7
c ---[ 456]---> Adder-cost: 70   maxlim: 4480   bits: 14/13
c ---[ 454]---> Sorter-cost:  960     Base: 2 2 2 2 2 2 2 7
c ---[ 452]---> Adder-cost: 154   maxlim: 9728   bits: 15/14
c ---[ 450]---> Adder-cost: 118   maxlim: 7168   bits: 14/13
c ---[ 448]---> Adder-cost: 116   maxlim: 9344   bits: 15/14
c ---[ 446]---> Adder-cost: 134   maxlim: 8192   bits: 15/14
c ---[ 444]---> Adder-cost: 62   maxlim: 8192   bits: 15/14
c ---[ 442]---> Adder-cost: 108   maxlim: 7552   bits: 14/13
c ---[ 440]---> Adder-cost: 48   maxlim: 7552   bits: 14/13
c ---[ 438]---> Adder-cost: 172   maxlim: 10624   bits: 15/14
c ---[ 436]---> Adder-cost: 68   maxlim: 10624   bits: 15/14
c ---[ 434]---> Adder-cost: 262   maxlim: 16640   bits: 16/15
c ---[ 432]---> Adder-cost: 52   maxlim: 7168   bits: 14/13
c ---[ 430]---> Adder-cost: 88   maxlim: 16640   bits: 16/15
c ---[ 428]---> Adder-cost: 200   maxlim: 14976   bits: 15/14
c ---[ 426]---> Adder-cost: 80   maxlim: 14976   bits: 15/14
c ---[ 422]---> Adder-cost: 80   maxlim: 4992   bits: 14/13
c ---[ 420]---> Adder-cost: 40   maxlim: 4992   bits: 14/13
c ---[ 418]---> Adder-cost: 78   maxlim: 5120   bits: 14/13
c ---[ 416]---> Sorter-cost:  715     Base: 2 2 2 2 2 2 2 7
c ---[ 414]---> Adder-cost: 124   maxlim: 7680   bits: 14/13
c ---[ 412]---> Sorter-cost:  507     Base: 2 2 2 2 2 2 2 7
c ---[ 410]---> Sorter-cost:  996     Base: 2 2 2 2 2 2 2 7
c ---[ 408]---> Adder-cost: 124   maxlim: 7936   bits: 14/13
c ---[ 406]---> Adder-cost: 122   maxlim: 7936   bits: 14/13
c ---[ 404]---> Sorter-cost:  994     Base: 2 2 2 2 2 2 2 7
c ---[ 402]---> Sorter-cost: 1072     Base: 2 2 2 2 2 2 2 7
c ---[ 400]---> Adder-cost: 84   maxlim: 5248   bits: 14/13
c ---[ 398]---> Sorter-cost:  736     Base: 2 2 2 2 2 2 2 7
c ---[ 396]---> Adder-cost: 66   maxlim: 7808   bits: 14/13
c ---[ 394]---> Sorter-cost:  560     Base: 2 2 2 2 2 2 2 7
c ---[ 392]---> Sorter-cost:  685     Base: 2 2 2 2 2 2 2 7
c ---[ 390]---> Sorter-cost:  541     Base: 2 2 2 2 2 2 2 7
c ---[ 388]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 7
c ---[ 386]---> Sorter-cost:  614     Base: 2 2 2 2 2 2 2 7
c ---[ 384]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 7
c ---[ 382]---> Sorter-cost:  984     Base: 2 2 2 2 2 2 2 7
c ---[ 380]---> Adder-cost: 208   maxlim: 13184   bits: 15/14
c ---[ 378]---> Adder-cost: 108   maxlim: 8448   bits: 15/14
c ---[ 376]---> Adder-cost: 74   maxlim: 13184   bits: 15/14
c ---[ 374]---> Adder-cost: 216   maxlim: 13312   bits: 15/14
c ---[ 372]---> Adder-cost: 78   maxlim: 13312   bits: 15/14
c ---[ 369]---> Adder-cost: 134   maxlim: 8448   bits: 15/14
c ---[ 367]---> Adder-cost: 108   maxlim: 7936   bits: 14/13
c ---[ 365]---> Adder-cost: 74   maxlim: 4736   bits: 14/13
c ---[ 363]---> Adder-cost: 60   maxlim: 8448   bits: 15/14
c ---[ 361]---> Adder-cost: 78   maxlim: 4992   bits: 14/13
c ---[ 359]---> Adder-cost: 76   maxlim: 5120   bits: 14/13
c ---[ 357]---> Adder-cost: 72   maxlim: 5632   bits: 14/13
c ---[ 355]---> Adder-cost: 78   maxlim: 5888   bits: 14/13
c ---[ 353]---> Adder-cost: 88   maxlim: 6272   bits: 14/13
c ---[ 351]---> Adder-cost: 170   maxlim: 11136   bits: 15/14
c ---[ 349]---> Adder-cost: 92   maxlim: 6528   bits: 14/13
c ---[ 347]---> Adder-cost: 92   maxlim: 6400   bits: 14/13
c ---[ 345]---> Adder-cost: 108   maxlim: 6784   bits: 14/13
c ---[ 343]---> Adder-cost: 100   maxlim: 7808   bits: 14/13
c ---[ 341]---> Adder-cost: 100   maxlim: 7552   bits: 14/13
c ---[ 339]---> Adder-cost: 68   maxlim: 11136   bits: 15/14
c ---[ 337]---> Adder-cost: 152   maxlim: 9600   bits: 15/14
c ---[ 335]---> Adder-cost: 152   maxlim: 10240   bits: 15/14
c ---[ 333]---> Adder-cost: 148   maxlim: 10368   bits: 15/14
c ---[ 331]---> Adder-cost: 216   maxlim: 15104   bits: 15/14
c ---[ 329]---> Adder-cost: 80   maxlim: 15104   bits: 15/14
c ---[ 327]---> Adder-cost: 186   maxlim: 14208   bits: 15/14
c ---[ 325]---> Adder-cost: 72   maxlim: 14208   bits: 15/14
c ---[ 323]---> Adder-cost: 152   maxlim: 11520   bits: 15/14
c ---[ 321]---> Adder-cost: 208   maxlim: 16000   bits: 15/14
c ---[ 319]---> Adder-cost: 78   maxlim: 16000   bits: 15/14
c ---[ 317]---> Adder-cost: 194   maxlim: 15232   bits: 15/14
c ---[ 315]---> Adder-cost: 80   maxlim: 15232   bits: 15/14
c ---[ 313]---> Adder-cost: 194   maxlim: 16768   bits: 16/15
c ---[ 311]---> Adder-cost: 84   maxlim: 16768   bits: 16/15
c ---[ 309]---> Adder-cost: 180   maxlim: 16256   bits: 15/14
c ---[ 307]---> Adder-cost: 74   maxlim: 16256   bits: 15/14
c ---[ 305]---> Adder-cost: 128   maxlim: 9600   bits: 15/14
c ---[ 303]---> Adder-cost: 62   maxlim: 9600   bits: 15/14
c ---[ 301]---> Adder-cost: 130   maxlim: 11392   bits: 15/14
c ---[ 299]---> Adder-cost: 106   maxlim: 9984   bits: 15/14
c ---[ 297]---> Adder-cost: 62   maxlim: 9984   bits: 15/14
c ---[ 295]---> Adder-cost: 82   maxlim: 5248   bits: 14/13
c ---[ 293]---> Adder-cost: 116   maxlim: 8064   bits: 14/13
c ---[ 291]---> Adder-cost: 220   maxlim: 14976   bits: 15/14
c ---[ 289]---> Adder-cost: 174   maxlim: 11776   bits: 15/14
c ---[ 287]---> Adder-cost: 94   maxlim: 6144   bits: 14/13
c ---[ 285]---> Adder-cost: 194   maxlim: 13056   bits: 15/14
c ---[ 283]---> Adder-cost: 74   maxlim: 13056   bits: 15/14
c ---[ 281]---> Adder-cost: 166   maxlim: 10752   bits: 15/14
c ---[ 279]---> Adder-cost: 66   maxlim: 10752   bits: 15/14
c ---[ 277]---> Adder-cost: 174   maxlim: 11904   bits: 15/14
c ---[ 275]---> Adder-cost: 70   maxlim: 11904   bits: 15/14
c ---[ 273]---> Adder-cost: 190   maxlim: 13952   bits: 15/14
c ---[ 271]---> Adder-cost: 72   maxlim: 13952   bits: 15/14
c ---[ 269]---> Adder-cost: 200   maxlim: 16128   bits: 15/14
c ---[ 267]---> Adder-cost: 76   maxlim: 16128   bits: 15/14
c ---[ 265]---> Adder-cost: 62   maxlim: 5376   bits: 14/13
c ---[ 263]---> Adder-cost: 176   maxlim: 14720   bits: 15/14
c ---[ 261]---> Adder-cost: 76   maxlim: 14720   bits: 15/14
c ---[ 259]---> Adder-cost: 214   maxlim: 16000   bits: 15/14
c ---[ 257]---> Adder-cost: 264   maxlim: 17920   bits: 16/15
c ---[ 255]---> Adder-cost: 478   maxlim: 33152   bits: 17/16
c ---[ 253]---> Adder-cost: 138   maxlim: 33152   bits: 17/16
c ---[ 251]---> Adder-cost: 444   maxlim: 33664   bits: 17/16
c ---[ 249]---> Adder-cost: 144   maxlim: 33664   bits: 17/16
c ---[ 247]---> Adder-cost: 146   maxlim: 9856   bits: 15/14
c ---[ 245]---> Adder-cost: 460   maxlim: 35584   bits: 17/16
c ---[ 243]---> Adder-cost: 140   maxlim: 35584   bits: 17/16
c ---[ 241]---> Adder-cost: 390   maxlim: 34560   bits: 17/16
c ---[ 239]---> Adder-cost: 138   maxlim: 34560   bits: 17/16
c ---[ 237]---> Adder-cost: 388   maxlim: 34688   bits: 17/16
c ---[ 235]---> Adder-cost: 136   maxlim: 34688   bits: 17/16
c ---[ 233]---> Adder-cost: 322   maxlim: 31744   bits: 16/15
c ---[ 231]---> Adder-cost: 132   maxlim: 31744   bits: 16/15
c ---[ 229]---> Adder-cost: 372   maxlim: 31104   bits: 16/15
c ---[ 227]---> Adder-cost: 128   maxlim: 31104   bits: 16/15
c ---[ 225]---> Adder-cost: 104   maxlim: 9856   bits: 15/14
c ---[ 223]---> Adder-cost: 324   maxlim: 31616   bits: 16/15
c ---[ 221]---> Adder-cost: 126   maxlim: 31616   bits: 16/15
c ---[ 219]---> Adder-cost: 258   maxlim: 31232   bits: 16/15
c ---[ 217]---> Adder-cost: 130   maxlim: 31232   bits: 16/15
c ---[ 215]---> Adder-cost: 130   maxlim: 31232   bits: 16/15
c ---[ 213]---> Adder-cost: 130   maxlim: 31232   bits: 16/15
c ---[ 211]---> Adder-cost: 164   maxlim: 29952   bits: 16/15
c ---[ 208]---> Adder-cost: 202   maxlim: 13568   bits: 15/14
c ---[ 206]---> Adder-cost: 116   maxlim: 8192   bits: 15/14
c ---[ 204]---> Adder-cost: 166   maxlim: 11392   bits: 15/14
c ---[ 202]---> Adder-cost: 78   maxlim: 13568   bits: 15/14
c ---[ 200]---> Adder-cost: 220   maxlim: 14976   bits: 15/14
c ---[ 198]---> Adder-cost: 144   maxlim: 14848   bits: 15/14
c ---[ 196]---> Adder-cost: 134   maxlim: 15232   bits: 15/14
c ---[ 194]---> Adder-cost: 116   maxlim: 15104   bits: 15/14
c ---[ 192]---> Adder-cost: 162   maxlim: 12160   bits: 15/14
c ---[ 190]---> Adder-cost: 228   maxlim: 15744   bits: 15/14
c ---[ 188]---> Adder-cost: 182   maxlim: 13696   bits: 15/14
c ---[ 186]---> Adder-cost: 142   maxlim: 11264   bits: 15/14
c ---[ 184]---> Adder-cost: 214   maxlim: 14208   bits: 15/14
c ---[ 182]---> Adder-cost: 278   maxlim: 20096   bits: 16/15
c ---[ 180]---> Adder-cost: 232   maxlim: 19584   bits: 16/15
c ---[ 178]---> Adder-cost: 216   maxlim: 15360   bits: 15/14
c ---[ 175]---> Adder-cost: 118   maxlim: 7680   bits: 14/13
c ---[ 173]---> Adder-cost: 136   maxlim: 8960   bits: 15/14
c ---[ 171]---> Adder-cost: 194   maxlim: 13440   bits: 15/14
c ---[ 169]---> Adder-cost: 60   maxlim: 8960   bits: 15/14
c ---[ 167]---> Adder-cost: 119   maxlim: 7936   bits: 14/13
c ---[ 165]---> Adder-cost: 52   maxlim: 7936   bits: 14/13
c ---[ 161]---> Adder-cost: 246   maxlim: 16768   bits: 16/15
c ---[ 158]---> Adder-cost: 160   maxlim: 11776   bits: 15/14
c ---[ 154]---> Adder-cost: 178   maxlim: 13568   bits: 15/14
c ---[ 152]---> Adder-cost: 118   maxlim: 7424   bits: 14/13
c ---[ 150]---> Adder-cost: 112   maxlim: 7168   bits: 14/13
c ---[ 146]---> Adder-cost: 128   maxlim: 8448   bits: 15/14
c ---[ 144]---> Adder-cost: 156   maxlim: 12416   bits: 15/14
c ---[ 142]---> Adder-cost: 112   maxlim: 9728   bits: 15/14
c ---[ 140]---> Adder-cost: 176   maxlim: 12288   bits: 15/14
c ---[ 138]---> Adder-cost: 194   maxlim: 14080   bits: 15/14
c ---[ 136]---> Adder-cost: 86   maxlim: 5760   bits: 14/13
c ---[ 134]---> Sorter-cost:  402     Base: 2 2 2 2 2 2 2 7
c ---[ 132]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 7
c ---[ 130]---> Sorter-cost:  437     Base: 2 2 2 2 2 2 2 7
c ---[ 128]---> Adder-cost: 154   maxlim: 12160   bits: 15/14
c ---[ 126]---> Adder-cost: 142   maxlim: 9600   bits: 15/14
c ---[ 124]---> Adder-cost: 230   maxlim: 15360   bits: 15/14
c ---[ 122]---> Adder-cost: 80   maxlim: 15360   bits: 15/14
c ---[ 120]---> Adder-cost: 168   maxlim: 14848   bits: 15/14
c ---[ 118]---> Adder-cost: 80   maxlim: 14848   bits: 15/14
c ---[ 116]---> Adder-cost: 158   maxlim: 10240   bits: 15/14
c ---[ 114]---> Adder-cost: 128   maxlim: 8320   bits: 15/14
c ---[ 112]---> Adder-cost: 118   maxlim: 11008   bits: 15/14
c ---[ 110]---> Adder-cost: 118   maxlim: 7168   bits: 14/13
c ---[ 108]---> Adder-cost: 182   maxlim: 11392   bits: 15/14
c ---[ 106]---> Adder-cost: 72   maxlim: 11392   bits: 15/14
c ---[ 104]---> Adder-cost: 112   maxlim: 6912   bits: 14/13
c ---[ 102]---> Adder-cost: 48   maxlim: 6912   bits: 14/13
c ---[ 100]---> Adder-cost: 98   m/oldhome/oroussel/solvers/minisat+_script: line 16: 17946 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.95 0.97 0.94 2/54 17941
Raw data (stat): 17941 (runsolver) R 17940 32284 32283 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784926990 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.96 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+20.0031 s]
Raw data (loadavg): 0.97 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+30.0039 s]
Raw data (loadavg): 0.97 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+40.0048 s]
Raw data (loadavg): 0.97 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+50.0057 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+60.0066 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+70.0074 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+80.0083 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+90.0082 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+100.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+110.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+140.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+150.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+180.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+210.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+230.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+240.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+350.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+370.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+380.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+390.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+400.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+420.038 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+440.039 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+450.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+470.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+480.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+490.041 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+500.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+510.042 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+520.043 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+530.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+540.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+550.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+560.044 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+570.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+580.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+600.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+610.046 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+630.047 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+690.06 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+700.061 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+710.062 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+720.063 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+730.064 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+740.065 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+750.066 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+760.067 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+770.067 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+780.068 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+790.068 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+800.069 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+810.07 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+820.072 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+830.072 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+840.072 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+850.073 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+860.073 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+870.074 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+880.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+890.075 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+900.076 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+910.077 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+920.078 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+930.078 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+940.078 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+950.079 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+957.312 s]
Raw data (loadavg): 0.99 0.97 0.94 1/53 17946
Raw data (stat): 17941 (minisat+_script) S 17940 32284 32283 0 -1 0 300 1978 0 0 0 0 30 5 18 0 1 0 784926990 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 0

Child status: 139
Real time (s): 957.311
CPU time (s): 957.337
CPU user time (s): 955.85
CPU system time (s): 1.48777
CPU usage (%): 100.003
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####