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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-siena1.opb
MD5SUM575f632072d90cb1b2032661c3842261
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 70755
Biggest coefficient in the objective function 536870912000000000000
Number of bits for the biggest coefficient in the objective function 69
Sum of the numbers in the objective function 28224865138562973040640
Number of bits of the sum of numbers in the objective function 75
Biggest number in a constraint 536870912000000000000
Number of bits of the biggest number in a constraint 69
Biggest sum of numbers in a constraint 28224967538562973040640
Number of bits of the biggest sum of numbers75
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables70755
Total number of constraints13995
Number of constraints which are clauses310
Number of constraints which are cardinality constraints (but not clauses)11776
Number of constraints which are nor clauses,nor cardinality constraints1909
Minimum length of a constraint1
Maximum length of a constraint70755

Trace number 5940

Launcher Data

LAUNCH ON wulflinc11 THE 2005-09-20 02:11:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3113 boxname=wulflinc11 idbench=769 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  575f632072d90cb1b2032661c3842261  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-siena1.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-siena1.opb
IDLAUNCH: 3113
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        890384 kB
Buffers:         19256 kB
Cached:          98440 kB
SwapCached:        760 kB
Active:          28912 kB
Inactive:        91144 kB
HighTotal:      131008 kB
HighFree:        29708 kB
LowTotal:       903652 kB
LowFree:        860676 kB
SwapTotal:     2097136 kB
SwapFree:      2095596 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5584 kB
Slab:            18588 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 02:31:42 (client local time) WITH STATUS 0 IN 1208.42 SECONDS
stats: 3113 7 1208.42 0

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): ......................................................................................................................................................................................................................................................................................sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss...............................
c ---[4094]---> Adder-cost: 154   maxlim: 73728   bits: 18/17
c ---[4092]---> Adder-cost: 172   maxlim: 84992   bits: 18/17
c ---[4090]---> Adder-cost: 308   maxlim: 153600   bits: 19/18
c ---[4088]---> Adder-cost: 212   maxlim: 130048   bits: 18/17
c ---[4085]---> Adder-cost: 120   maxlim: 60416   bits: 17/16
c ---[4083]---> Adder-cost: 84   maxlim: 64512   bits: 17/16
c ---[4081]---> Adder-cost: 106   maxlim: 64512   bits: 17/16
c ---[4079]---> Adder-cost: 120   maxlim: 65536   bits: 18/17
c ---[4077]---> Adder-cost: 112   maxlim: 58368   bits: 17/16
c ---[4075]---> Sorter-cost: 1313     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[4073]---> Adder-cost: 102   maxlim: 86016   bits: 18/17
c ---[4071]---> Sorter-cost: 1191     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[4069]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[4067]---> Adder-cost: 188   maxlim: 97280   bits: 18/17
c ---[4065]---> Adder-cost: 190   maxlim: 98304   bits: 18/17
c ---[4063]---> Adder-cost: 176   maxlim: 101376   bits: 18/17
c ---[4061]---> Adder-cost: 122   maxlim: 89088   bits: 18/17
c ---[4059]---> Adder-cost: 154   maxlim: 89088   bits: 18/17
c ---[4057]---> Adder-cost: 66   maxlim: 86016   bits: 18/17
c ---[4055]---> Adder-cost: 148   maxlim: 96256   bits: 18/17
c ---[4053]---> Adder-cost: 150   maxlim: 92160   bits: 18/17
c ---[4051]---> Sorter-cost: 1219     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[4049]---> Sorter-cost: 1200     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[4047]---> Adder-cost: 178   maxlim: 88064   bits: 18/17
c ---[4045]---> Adder-cost: 186   maxlim: 93184   bits: 18/17
c ---[4043]---> Adder-cost: 134   maxlim: 93184   bits: 18/17
c ---[4041]---> Adder-cost: 108   maxlim: 76800   bits: 18/17
c ---[4038]---> Adder-cost: 166   maxlim: 107520   bits: 18/17
c ---[4036]---> Adder-cost: 200   maxlim: 106496   bits: 18/17
c ---[4034]---> Adder-cost: 256   maxlim: 147456   bits: 19/18
c ---[4032]---> Adder-cost: 248   maxlim: 149504   bits: 19/18
c ---[4030]---> Adder-cost: 216   maxlim: 158720   bits: 19/18
c ---[4028]---> Adder-cost: 236   maxlim: 160768   bits: 19/18
c ---[4026]---> Adder-cost: 210   maxlim: 164864   bits: 19/18
c ---[4024]---> Sorter-cost:  995     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[4022]---> Adder-cost: 100   maxlim: 164864   bits: 19/18
c ---[4020]---> Adder-cost: 316   maxlim: 199680   bits: 19/18
c ---[4018]---> Adder-cost: 288   maxlim: 175104   bits: 19/18
c ---[4016]---> Adder-cost: 200   maxlim: 164864   bits: 19/18
c ---[4014]---> Adder-cost: 224   maxlim: 131072   bits: 19/18
c ---[4012]---> Adder-cost: 194   maxlim: 110592   bits: 18/17
c ---[4010]---> Adder-cost: 158   maxlim: 87040   bits: 18/17
c ---[4008]---> Adder-cost: 144   maxlim: 81920   bits: 18/17
c ---[4006]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[4004]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[4002]---> Sorter-cost: 1313     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[4000]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3998]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3996]---> Sorter-cost: 1163     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3994]---> Sorter-cost: 1013     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3992]---> Sorter-cost: 1117     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3990]---> Adder-cost: 154   maxlim: 74752   bits: 18/17
c ---[3988]---> Adder-cost: 200   maxlim: 102400   bits: 18/17
c ---[3986]---> Adder-cost: 162   maxlim: 101376   bits: 18/17
c ---[3984]---> Adder-cost: 180   maxlim: 96256   bits: 18/17
c ---[3982]---> Adder-cost: 136   maxlim: 92160   bits: 18/17
c ---[3980]---> Adder-cost: 106   maxlim: 62464   bits: 17/16
c ---[3978]---> Adder-cost: 110   maxlim: 57344   bits: 17/16
c ---[3975]---> Adder-cost: 82   maxlim: 58368   bits: 17/16
c ---[3973]---> Adder-cost: 232   maxlim: 124928   bits: 18/17
c ---[3971]---> Adder-cost: 260   maxlim: 141312   bits: 19/18
c ---[3969]---> Adder-cost: 92   maxlim: 141312   bits: 19/18
c ---[3967]---> Adder-cost: 272   maxlim: 153600   bits: 19/18
c ---[3965]---> Adder-cost: 226   maxlim: 156672   bits: 19/18
c ---[3963]---> Adder-cost: 272   maxlim: 161792   bits: 19/18
c ---[3961]---> Adder-cost: 92   maxlim: 161792   bits: 19/18
c ---[3959]---> Adder-cost: 266   maxlim: 159744   bits: 19/18
c ---[3957]---> Adder-cost: 266   maxlim: 131072   bits: 19/18
c ---[3955]---> Adder-cost: 182   maxlim: 162816   bits: 19/18
c ---[3953]---> Adder-cost: 166   maxlim: 159744   bits: 19/18
c ---[3951]---> Adder-cost: 94   maxlim: 159744   bits: 19/18
c ---[3949]---> Adder-cost: 250   maxlim: 157696   bits: 19/18
c ---[3947]---> Adder-cost: 92   maxlim: 157696   bits: 19/18
c ---[3945]---> Adder-cost: 180   maxlim: 156672   bits: 19/18
c ---[3943]---> Adder-cost: 96   maxlim: 156672   bits: 19/18
c ---[3941]---> Adder-cost: 216   maxlim: 155648   bits: 19/18
c ---[3939]---> Adder-cost: 96   maxlim: 155648   bits: 19/18
c ---[3937]---> Adder-cost: 102   maxlim: 156672   bits: 19/18
c ---[3935]---> Adder-cost: 90   maxlim: 131072   bits: 19/18
c ---[3933]---> Adder-cost: 96   maxlim: 156672   bits: 19/18
c ---[3931]---> Adder-cost: 96   maxlim: 156672   bits: 19/18
c ---[3929]---> Adder-cost: 96   maxlim: 156672   bits: 19/18
c ---[3927]---> Adder-cost: 260   maxlim: 192512   bits: 19/18
c ---[3924]---> Adder-cost: 146   maxlim: 69632   bits: 18/17
c ---[3922]---> Adder-cost: 94   maxlim: 70656   bits: 18/17
c ---[3920]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3918]---> Sorter-cost: 1271     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3916]---> Adder-cost: 168   maxlim: 118784   bits: 18/17
c ---[3914]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[3912]---> Adder-cost: 100   maxlim: 52224   bits: 17/16
c ---[3910]---> Adder-cost: 96   maxlim: 51200   bits: 17/16
c ---[3908]---> Adder-cost: 156   maxlim: 76800   bits: 18/17
c ---[3906]---> Adder-cost: 136   maxlim: 74752   bits: 18/17
c ---[3903]---> Adder-cost: 98   maxlim: 56320   bits: 17/16
c ---[3901]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[3899]---> Sorter-cost:  971     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3897]---> Sorter-cost:  632     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3895]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3893]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3891]---> Sorter-cost: 1073     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3888]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3886]---> Adder-cost: 116   maxlim: 58368   bits: 17/16
c ---[3884]---> Adder-cost: 82   maxlim: 58368   bits: 17/16
c ---[3882]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3880]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3878]---> Sorter-cost: 1154     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3876]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3874]---> Sorter-cost: 1012     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3872]---> Sorter-cost:  793     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3870]---> Adder-cost: 142   maxlim: 68608   bits: 18/17
c ---[3868]---> Sorter-cost: 1271     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3866]---> Adder-cost: 58   maxlim: 68608   bits: 18/17
c ---[3864]---> Adder-cost: 132   maxlim: 73728   bits: 18/17
c ---[3862]---> Adder-cost: 102   maxlim: 71680   bits: 18/17
c ---[3860]---> Adder-cost: 120   maxlim: 68608   bits: 18/17
c ---[3858]---> Adder-cost: 84   maxlim: 71680   bits: 18/17
c ---[3856]---> Sorter-cost:  375     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3854]---> Sorter-cost:  526     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3852]---> Sorter-cost:  283     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3850]---> Sorter-cost:  414     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3848]---> Adder-cost: 204   maxlim: 101376   bits: 18/17
c ---[3846]---> Adder-cost: 118   maxlim: 102400   bits: 18/17
c ---[3844]---> Sorter-cost: 1061     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3842]---> Sorter-cost: 1036     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3840]---> Adder-cost: 204   maxlim: 101376   bits: 18/17
c ---[3838]---> Adder-cost: 72   maxlim: 101376   bits: 18/17
c ---[3836]---> Adder-cost: 186   maxlim: 94208   bits: 18/17
c ---[3834]---> Adder-cost: 104   maxlim: 95232   bits: 18/17
c ---[3832]---> Adder-cost: 74   maxlim: 94208   bits: 18/17
c ---[3830]---> Adder-cost: 70   maxlim: 94208   bits: 18/17
c ---[3828]---> Sorter-cost: 1287     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3826]---> Sorter-cost:  763     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3823]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3821]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3819]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3817]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3815]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3813]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3811]---> Sorter-cost: 1070     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3809]---> Sorter-cost: 1175     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3807]---> Sorter-cost: 1131     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3805]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3803]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3801]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3799]---> Sorter-cost: 1267     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3797]---> Adder-cost: 154   maxlim: 73728   bits: 18/17
c ---[3794]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3791]---> Adder-cost: 170   maxlim: 82944   bits: 18/17
c ---[3789]---> Adder-cost: 140   maxlim: 66560   bits: 18/17
c ---[3787]---> Adder-cost: 60   maxlim: 66560   bits: 18/17
c ---[3785]---> Adder-cost: 152   maxlim: 78848   bits: 18/17
c ---[3783]---> Adder-cost: 122   maxlim: 79872   bits: 18/17
c ---[3781]---> Adder-cost: 120   maxlim: 62464   bits: 17/16
c ---[3779]---> Adder-cost: 190   maxlim: 96256   bits: 18/17
c ---[3777]---> Adder-cost: 122   maxlim: 63488   bits: 17/16
c ---[3775]---> Adder-cost: 134   maxlim: 66560   bits: 18/17
c ---[3773]---> Adder-cost: 130   maxlim: 65536   bits: 18/17
c ---[3771]---> Adder-cost: 186   maxlim: 92160   bits: 18/17
c ---[3769]---> Adder-cost: 96   maxlim: 93184   bits: 18/17
c ---[3767]---> Adder-cost: 122   maxlim: 87040   bits: 18/17
c ---[3765]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3763]---> Sorter-cost:  896     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3761]---> Sorter-cost: 1135     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3759]---> Adder-cost: 104   maxlim: 52224   bits: 17/16
c ---[3757]---> Adder-cost: 102   maxlim: 59392   bits: 17/16
c ---[3755]---> Sorter-cost: 1061     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3753]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3751]---> Sorter-cost:  593     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3749]---> Sorter-cost:  680     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3747]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3745]---> Sorter-cost: 1084     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3743]---> Adder-cost: 270   maxlim: 131072   bits: 19/18
c ---[3740]---> Sorter-cost:  789     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3738]---> Adder-cost: 126   maxlim: 63488   bits: 17/16
c ---[3736]---> Adder-cost: 52   maxlim: 63488   bits: 17/16
c ---[3734]---> Adder-cost: 52   maxlim: 63488   bits: 17/16
c ---[3732]---> Adder-cost: 52   maxlim: 63488   bits: 17/16
c ---[3730]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3728]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3725]---> Adder-cost: 156   maxlim: 76800   bits: 18/17
c ---[3723]---> Adder-cost: 134   maxlim: 67584   bits: 18/17
c ---[3721]---> Adder-cost: 130   maxlim: 68608   bits: 18/17
c ---[3719]---> Sorter-cost: 1185     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3717]---> Sorter-cost: 1185     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3715]---> Adder-cost: 106   maxlim: 51200   bits: 17/16
c ---[3713]---> Adder-cost: 176   maxlim: 87040   bits: 18/17
c ---[3711]---> Adder-cost: 146   maxlim: 82944   bits: 18/17
c ---[3709]---> Adder-cost: 202   maxlim: 98304   bits: 18/17
c ---[3707]---> Adder-cost: 178   maxlim: 99328   bits: 18/17
c ---[3705]---> Adder-cost: 124   maxlim: 62464   bits: 17/16
c ---[3703]---> Adder-cost: 144   maxlim: 79872   bits: 18/17
c ---[3701]---> Sorter-cost:  684     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3699]---> Sorter-cost: 1224     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3697]---> Sorter-cost: 1149     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3695]---> Sorter-cost:  889     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3692]---> Adder-cost: 188   maxlim: 95232   bits: 18/17
c ---[3688]---> Adder-cost: 230   maxlim: 114688   bits: 18/17
c ---[3686]---> Adder-cost: 184   maxlim: 95232   bits: 18/17
c ---[3684]---> Adder-cost: 70   maxlim: 95232   bits: 18/17
c ---[3682]---> Adder-cost: 122   maxlim: 61440   bits: 17/16
c ---[3680]---> Sorter-cost: 1113     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3678]---> Adder-cost: 50   maxlim: 61440   bits: 17/16
c ---[3676]---> Adder-cost: 50   maxlim: 61440   bits: 17/16
c ---[3674]---> Adder-cost: 50   maxlim: 61440   bits: 17/16
c ---[3672]---> Adder-cost: 78   maxlim: 58368   bits: 17/16
c ---[3670]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[3668]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3666]---> Sorter-cost:  373     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3664]---> Sorter-cost:  422     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3662]---> Adder-cost: 160   maxlim: 77824   bits: 18/17
c ---[3660]---> Adder-cost: 118   maxlim: 64512   bits: 17/16
c ---[3658]---> Adder-cost: 124   maxlim: 67584   bits: 18/17
c ---[3656]---> Adder-cost: 96   maxlim: 58368   bits: 17/16
c ---[3654]---> Adder-cost: 184   maxlim: 91136   bits: 18/17
c ---[3652]---> Sorter-cost:  935     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3650]---> Adder-cost: 72   maxlim: 91136   bits: 18/17
c ---[3648]---> Adder-cost: 132   maxlim: 75776   bits: 18/17
c ---[3646]---> Adder-cost: 64   maxlim: 75776   bits: 18/17
c ---[3644]---> Adder-cost: 180   maxlim: 95232   bits: 18/17
c ---[3642]---> Adder-cost: 70   maxlim: 95232   bits: 18/17
c ---[3640]---> Sorter-cost: 1178     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3638]---> Adder-cost: 200   maxlim: 98304   bits: 18/17
c ---[3636]---> Adder-cost: 152   maxlim: 78848   bits: 18/17
c ---[3634]---> Adder-cost: 246   maxlim: 123904   bits: 18/17
c ---[3632]---> Adder-cost: 78   maxlim: 123904   bits: 18/17
c ---[3630]---> Adder-cost: 268   maxlim: 135168   bits: 19/18
c ---[3628]---> Adder-cost: 88   maxlim: 135168   bits: 19/18
c ---[3626]---> Adder-cost: 150   maxlim: 130048   bits: 18/17
c ---[3624]---> Adder-cost: 74   maxlim: 130048   bits: 18/17
c ---[3622]---> Adder-cost: 176   maxlim: 87040   bits: 18/17
c ---[3620]---> Adder-cost: 66   maxlim: 87040   bits: 18/17
c ---[3618]---> Sorter-cost: 1185     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3616]---> Adder-cost: 124   maxlim: 61440   bits: 17/16
c ---[3612]---> Sorter-cost: 1311     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3610]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3607]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[3605]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3603]---> Sorter-cost:  605     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3601]---> Sorter-cost: 1181     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3599]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3597]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3595]---> Sorter-cost: 1017     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3593]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3591]---> Adder-cost: 126   maxlim: 64512   bits: 17/16
c ---[3589]---> Adder-cost: 124   maxlim: 63488   bits: 17/16
c ---[3587]---> Sorter-cost: 1059     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3585]---> Adder-cost: 52   maxlim: 63488   bits: 17/16
c ---[3583]---> Sorter-cost: 1311     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3581]---> Adder-cost: 108   maxlim: 54272   bits: 17/16
c ---[3579]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3577]---> Sorter-cost:  690     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3575]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3573]---> Sorter-cost:  420     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3571]---> Sorter-cost: 1083     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3569]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3567]---> Sorter-cost:  959     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3565]---> Adder-cost: 146   maxlim: 70656   bits: 18/17
c ---[3563]---> Adder-cost: 156   maxlim: 84992   bits: 18/17
c ---[3561]---> Adder-cost: 68   maxlim: 84992   bits: 18/17
c ---[3559]---> Adder-cost: 156   maxlim: 94208   bits: 18/17
c ---[3557]---> Adder-cost: 156   maxlim: 91136   bits: 18/17
c ---[3555]---> Adder-cost: 72   maxlim: 91136   bits: 18/17
c ---[3553]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3551]---> Sorter-cost: 1052     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3549]---> Sorter-cost:  793     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3547]---> Adder-cost: 112   maxlim: 56320   bits: 17/16
c ---[3545]---> Adder-cost: 112   maxlim: 55296   bits: 17/16
c ---[3543]---> Adder-cost: 214   maxlim: 113664   bits: 18/17
c ---[3541]---> Adder-cost: 136   maxlim: 117760   bits: 18/17
c ---[3537]---> Sorter-cost:  470     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3535]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3533]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3531]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3529]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3527]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3525]---> Sorter-cost:  414     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3523]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3521]---> Sorter-cost:  283     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3519]---> Adder-cost: 146   maxlim: 69632   bits: 18/17
c ---[3517]---> Adder-cost: 146   maxlim: 70656   bits: 18/17
c ---[3513]---> Sorter-cost:  642     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3511]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3509]---> Adder-cost: 112   maxlim: 57344   bits: 17/16
c ---[3506]---> Sorter-cost: 1183     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3504]---> Sorter-cost:  800     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3502]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3500]---> Adder-cost: 120   maxlim: 60416   bits: 17/16
c ---[3498]---> Adder-cost: 48   maxlim: 60416   bits: 17/16
c ---[3496]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3494]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3492]---> Sorter-cost: 1210     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3490]---> Adder-cost: 110   maxlim: 55296   bits: 17/16
c ---[3488]---> Adder-cost: 84   maxlim: 59392   bits: 17/16
c ---[3486]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[3484]---> Adder-cost: 126   maxlim: 69632   bits: 18/17
c ---[3482]---> Adder-cost: 62   maxlim: 69632   bits: 18/17
c ---[3480]---> Sorter-cost: 1313     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3478]---> Sorter-cost: 1001     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3476]---> Sorter-cost: 1077     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3474]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3472]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3470]---> Adder-cost: 102   maxlim: 54272   bits: 17/16
c ---[3468]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3466]---> Sorter-cost: 1051     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3464]---> Sorter-cost:  667     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3462]---> Sorter-cost:  852     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3460]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3458]---> Adder-cost: 172   maxlim: 84992   bits: 18/17
c ---[3456]---> Adder-cost: 68   maxlim: 84992   bits: 18/17
c ---[3454]---> Adder-cost: 120   maxlim: 62464   bits: 17/16
c ---[3452]---> Adder-cost: 68   maxlim: 59392   bits: 17/16
c ---[3450]---> Adder-cost: 104   maxlim: 56320   bits: 17/16
c ---[3448]---> Adder-cost: 82   maxlim: 57344   bits: 17/16
c ---[3446]---> Adder-cost: 146   maxlim: 69632   bits: 18/17
c ---[3444]---> Adder-cost: 126   maxlim: 65536   bits: 18/17
c ---[3442]---> Adder-cost: 110   maxlim: 55296   bits: 17/16
c ---[3440]---> Adder-cost: 110   maxlim: 56320   bits: 17/16
c ---[3438]---> Adder-cost: 130   maxlim: 73728   bits: 18/17
c ---[3436]---> Adder-cost: 84   maxlim: 72704   bits: 18/17
c ---[3434]---> Adder-cost: 126   maxlim: 70656   bits: 18/17
c ---[3432]---> Adder-cost: 82   maxlim: 73728   bits: 18/17
c ---[3430]---> Adder-cost: 282   maxlim: 141312   bits: 19/18
c ---[3428]---> Adder-cost: 136   maxlim: 68608   bits: 18/17
c ---[3426]---> Adder-cost: 92   maxlim: 141312   bits: 19/18
c ---[3424]---> Adder-cost: 246   maxlim: 136192   bits: 19/18
c ---[3422]---> Adder-cost: 88   maxlim: 136192   bits: 19/18
c ---[3420]---> Adder-cost: 186   maxlim: 137216   bits: 19/18
c ---[3416]---> Sorter-cost: 1221     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3414]---> Sorter-cost:  800     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3412]---> Adder-cost: 58   maxlim: 68608   bits: 18/17
c ---[3410]---> Adder-cost: 184   maxlim: 90112   bits: 18/17
c ---[3408]---> Sorter-cost:  789     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3406]---> Sorter-cost:  723     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3404]---> Sorter-cost: 1156     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3402]---> Sorter-cost:  799     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3400]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3398]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3396]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3394]---> Sorter-cost:  285     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3392]---> Sorter-cost: 1024     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3390]---> Adder-cost: 138   maxlim: 65536   bits: 18/17
c ---[3388]---> Sorter-cost:  862     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3386]---> Sorter-cost: 1237     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3384]---> Sorter-cost:  688     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3382]---> Adder-cost: 154   maxlim: 74752   bits: 18/17
c ---[3380]---> Adder-cost: 134   maxlim: 68608   bits: 18/17
c ---[3378]---> Adder-cost: 58   maxlim: 68608   bits: 18/17
c ---[3376]---> Adder-cost: 154   maxlim: 79872   bits: 18/17
c ---[3374]---> Adder-cost: 96   maxlim: 58368   bits: 17/16
c ---[3372]---> Adder-cost: 104   maxlim: 59392   bits: 17/16
c ---[3370]---> Adder-cost: 176   maxlim: 99328   bits: 18/17
c ---[3368]---> Adder-cost: 62   maxlim: 65536   bits: 18/17
c ---[3366]---> Adder-cost: 134   maxlim: 70656   bits: 18/17
c ---[3364]---> Adder-cost: 94   maxlim: 71680   bits: 18/17
c ---[3362]---> Adder-cost: 118   maxlim: 63488   bits: 17/16
c ---[3360]---> Adder-cost: 116   maxlim: 64512   bits: 17/16
c ---[3358]---> Adder-cost: 94   maxlim: 56320   bits: 17/16
c ---[3356]---> Adder-cost: 126   maxlim: 66560   bits: 18/17
c ---[3354]---> Adder-cost: 144   maxlim: 74752   bits: 18/17
c ---[3352]---> Adder-cost: 182   maxlim: 100352   bits: 18/17
c ---[3350]---> Adder-cost: 164   maxlim: 100352   bits: 18/17
c ---[3348]---> Adder-cost: 148   maxlim: 97280   bits: 18/17
c ---[3346]---> Adder-cost: 124   maxlim: 67584   bits: 18/17
c ---[3344]---> Adder-cost: 116   maxlim: 63488   bits: 17/16
c ---[3342]---> Adder-cost: 106   maxlim: 59392   bits: 17/16
c ---[3340]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3338]---> Sorter-cost:  968     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3336]---> Sorter-cost:  981     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3334]---> Sorter-cost:  672     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3332]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3330]---> Sorter-cost:  452     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3328]---> Sorter-cost:  401     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3326]---> Adder-cost: 60   maxlim: 67584   bits: 18/17
c ---[3324]---> Sorter-cost:  489     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3322]---> Adder-cost: 144   maxlim: 69632   bits: 18/17
c ---[3320]---> Adder-cost: 212   maxlim: 109568   bits: 18/17
c ---[3318]---> Adder-cost: 78   maxlim: 109568   bits: 18/17
c ---[3316]---> Adder-cost: 200   maxlim: 106496   bits: 18/17
c ---[3313]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3310]---> Adder-cost: 202   maxlim: 101376   bits: 18/17
c ---[3308]---> Adder-cost: 92   maxlim: 70656   bits: 18/17
c ---[3306]---> Adder-cost: 160   maxlim: 102400   bits: 18/17
c ---[3304]---> Adder-cost: 76   maxlim: 102400   bits: 18/17
c ---[3301]---> Sorter-cost:  720     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3299]---> Sorter-cost:  441     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3297]---> Sorter-cost:  259     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3295]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[3293]---> Adder-cost: 160   maxlim: 86016   bits: 18/17
c ---[3291]---> Adder-cost: 60   maxlim: 70656   bits: 18/17
c ---[3289]---> Adder-cost: 114   maxlim: 78848   bits: 18/17
c ---[3287]---> Adder-cost: 170   maxlim: 81920   bits: 18/17
c ---[3285]---> Sorter-cost: 1287     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3283]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3281]---> Adder-cost: 110   maxlim: 55296   bits: 17/16
c ---[3279]---> Adder-cost: 150   maxlim: 76800   bits: 18/17
c ---[3277]---> Adder-cost: 92   maxlim: 77824   bits: 18/17
c ---[3275]---> Adder-cost: 154   maxlim: 79872   bits: 18/17
c ---[3273]---> Adder-cost: 138   maxlim: 68608   bits: 18/17
c ---[3271]---> Adder-cost: 192   maxlim: 97280   bits: 18/17
c ---[3269]---> Adder-cost: 160   maxlim: 103424   bits: 18/17
c ---[3267]---> Adder-cost: 150   maxlim: 97280   bits: 18/17
c ---[3265]---> Adder-cost: 64   maxlim: 97280   bits: 18/17
c ---[3263]---> Adder-cost: 108   maxlim: 95232   bits: 18/17
c ---[3259]---> Adder-cost: 218   maxlim: 109568   bits: 18/17
c ---[3256]---> Adder-cost: 58   maxlim: 68608   bits: 18/17
c ---[3254]---> Adder-cost: 186   maxlim: 114688   bits: 18/17
c ---[3250]---> Adder-cost: 152   maxlim: 74752   bits: 18/17
c ---[3248]---> Adder-cost: 60   maxlim: 74752   bits: 18/17
c ---[3244]---> Adder-cost: 282   maxlim: 140288   bits: 19/18
c ---[3242]---> Adder-cost: 272   maxlim: 136192   bits: 19/18
c ---[3240]---> Adder-cost: 214   maxlim: 133120   bits: 19/18
c ---[3238]---> Adder-cost: 250   maxlim: 129024   bits: 18/17
c ---[3234]---> Adder-cost: 154   maxlim: 77824   bits: 18/17
c ---[3232]---> Adder-cost: 112   maxlim: 60416   bits: 17/16
c ---[3230]---> Adder-cost: 112   maxlim: 61440   bits: 17/16
c ---[3228]---> Sorter-cost: 1271     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3226]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3224]---> Sorter-cost:  885     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3222]---> Sorter-cost:  468     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3220]---> Sorter-cost:  382     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3218]---> Adder-cost: 76   maxlim: 129024   bits: 18/17
c ---[3216]---> Sorter-cost:  583     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3214]---> Sorter-cost:  438     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3212]---> Sorter-cost:  401     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3210]---> Adder-cost: 112   maxlim: 55296   bits: 17/16
c ---[3208]---> Adder-cost: 92   maxlim: 56320   bits: 17/16
c ---[3206]---> Adder-cost: 62   maxlim: 55296   bits: 17/16
c ---[3204]---> Adder-cost: 88   maxlim: 57344   bits: 17/16
c ---[3202]---> Adder-cost: 292   maxlim: 145408   bits: 19/18
c ---[3200]---> Adder-cost: 274   maxlim: 161792   bits: 19/18
c ---[3198]---> Adder-cost: 310   maxlim: 165888   bits: 19/18
c ---[3196]---> Adder-cost: 198   maxlim: 108544   bits: 18/17
c ---[3194]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3192]---> Adder-cost: 156   maxlim: 75776   bits: 18/17
c ---[3190]---> Adder-cost: 136   maxlim: 79872   bits: 18/17
c ---[3188]---> Adder-cost: 128   maxlim: 75776   bits: 18/17
c ---[3186]---> Adder-cost: 92   maxlim: 59392   bits: 17/16
c ---[3184]---> Sorter-cost:  789     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3182]---> Sorter-cost: 1071     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3180]---> Sorter-cost: 1143     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3178]---> Sorter-cost: 1269     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3176]---> Adder-cost: 112   maxlim: 55296   bits: 17/16
c ---[3174]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3172]---> Adder-cost: 78   maxlim: 108544   bits: 18/17
c ---[3170]---> Adder-cost: 118   maxlim: 58368   bits: 17/16
c ---[3168]---> Adder-cost: 68   maxlim: 58368   bits: 17/16
c ---[3166]---> Adder-cost: 116   maxlim: 62464   bits: 17/16
c ---[3164]---> Adder-cost: 162   maxlim: 86016   bits: 18/17
c ---[3162]---> Adder-cost: 160   maxlim: 101376   bits: 18/17
c ---[3160]---> Adder-cost: 170   maxlim: 114688   bits: 18/17
c ---[3158]---> Adder-cost: 174   maxlim: 119808   bits: 18/17
c ---[3155]---> Adder-cost: 156   maxlim: 75776   bits: 18/17
c ---[3153]---> Adder-cost: 178   maxlim: 100352   bits: 18/17
c ---[3150]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3148]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[3146]---> Sorter-cost:  605     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3144]---> Sorter-cost:  405     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3142]---> Adder-cost: 178   maxlim: 89088   bits: 18/17
c ---[3140]---> Adder-cost: 280   maxlim: 141312   bits: 19/18
c ---[3137]---> Adder-cost: 106   maxlim: 53248   bits: 17/16
c ---[3135]---> Adder-cost: 106   maxlim: 55296   bits: 17/16
c ---[3133]---> Adder-cost: 72   maxlim: 100352   bits: 18/17
c ---[3131]---> Adder-cost: 74   maxlim: 52224   bits: 17/16
c ---[3129]---> Adder-cost: 44   maxlim: 52224   bits: 17/16
c ---[3127]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3125]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3123]---> Sorter-cost: 1017     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3121]---> Sorter-cost: 1299     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3119]---> Sorter-cost: 1267     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3117]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3115]---> Adder-cost: 140   maxlim: 70656   bits: 18/17
c ---[3113]---> Sorter-cost:  458     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3111]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3109]---> Sorter-cost:  442     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3107]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3105]---> Sorter-cost:  955     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3103]---> Sorter-cost: 1004     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3101]---> Sorter-cost: 1040     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3099]---> Sorter-cost:  956     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3097]---> Adder-cost: 172   maxlim: 84992   bits: 18/17
c ---[3095]---> Adder-cost: 60   maxlim: 70656   bits: 18/17
c ---[3093]---> Adder-cost: 68   maxlim: 84992   bits: 18/17
c ---[3091]---> Adder-cost: 170   maxlim: 92160   bits: 18/17
c ---[3089]---> Adder-cost: 146   maxlim: 107520   bits: 18/17
c ---[3087]---> Adder-cost: 136   maxlim: 106496   bits: 18/17
c ---[3085]---> Adder-cost: 174   maxlim: 95232   bits: 18/17
c ---[3083]---> Adder-cost: 252   maxlim: 135168   bits: 19/18
c ---[3081]---> Adder-cost: 232   maxlim: 133120   bits: 19/18
c ---[3079]---> Adder-cost: 170   maxlim: 103424   bits: 18/17
c ---[3077]---> Adder-cost: 170   maxlim: 99328   bits: 18/17
c ---[3075]---> Adder-cost: 160   maxlim: 98304   bits: 18/17
c ---[3073]---> Adder-cost: 156   maxlim: 84992   bits: 18/17
c ---[3071]---> Adder-cost: 228   maxlim: 122880   bits: 18/17
c ---[3069]---> Adder-cost: 226   maxlim: 141312   bits: 19/18
c ---[3067]---> Adder-cost: 92   maxlim: 141312   bits: 19/18
c ---[3065]---> Adder-cost: 146   maxlim: 75776   bits: 18/17
c ---[3063]---> Adder-cost: 164   maxlim: 84992   bits: 18/17
c ---[3061]---> Adder-cost: 96   maxlim: 79872   bits: 18/17
c ---[3059]---> Adder-cost: 234   maxlim: 122880   bits: 18/17
c ---[3057]---> Adder-cost: 206   maxlim: 117760   bits: 18/17
c ---[3055]---> Adder-cost: 76   maxlim: 117760   bits: 18/17
c ---[3053]---> Adder-cost: 188   maxlim: 114688   bits: 18/17
c ---[3051]---> Adder-cost: 68   maxlim: 84992   bits: 18/17
c ---[3049]---> Adder-cost: 190   maxlim: 112640   bits: 18/17
c ---[3047]---> Adder-cost: 74   maxlim: 112640   bits: 18/17
c ---[3045]---> Adder-cost: 108   maxlim: 84992   bits: 18/17
c ---[3043]---> Sorter-cost: 1035     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3041]---> Sorter-cost:  713     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3039]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3036]---> Sorter-cost: 1311     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3034]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3032]---> Adder-cost: 260   maxlim: 134144   bits: 19/18
c ---[3030]---> Adder-cost: 184   maxlim: 93184   bits: 18/17
c ---[3028]---> Adder-cost: 104   maxlim: 54272   bits: 17/16
c ---[3026]---> Sorter-cost: 1261     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[3022]---> Adder-cost: 310   maxlim: 155648   bits: 19/18
c ---[3020]---> Adder-cost: 302   maxlim: 151552   bits: 19/18
c ---[3018]---> Adder-cost: 280   maxlim: 153600   bits: 19/18
c ---[3016]---> Adder-cost: 92   maxlim: 153600   bits: 19/18
c ---[3012]---> Adder-cost: 208   maxlim: 104448   bits: 18/17
c ---[3010]---> Adder-cost: 146   maxlim: 93184   bits: 18/17
c ---[3008]---> Adder-cost: 64   maxlim: 93184   bits: 18/17
c ---[3006]---> Adder-cost: 64   maxlim: 93184   bits: 18/17
c ---[3004]---> Adder-cost: 64   maxlim: 93184   bits: 18/17
c ---[3000]---> Adder-cost: 140   maxlim: 69632   bits: 18/17
c ---[2998]---> Adder-cost: 116   maxlim: 72704   bits: 18/17
c ---[2996]---> Adder-cost: 278   maxlim: 138240   bits: 19/18
c ---[2994]---> Adder-cost: 146   maxlim: 74752   bits: 18/17
c ---[2992]---> Adder-cost: 178   maxlim: 98304   bits: 18/17
c ---[2990]---> Sorter-cost:  468     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2988]---> Sorter-cost:  311     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2986]---> Adder-cost: 234   maxlim: 117760   bits: 18/17
c ---[2984]---> Adder-cost: 136   maxlim: 65536   bits: 18/17
c ---[2982]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2980]---> Sorter-cost:  915     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2978]---> Sorter-cost: 1010     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2976]---> Adder-cost: 224   maxlim: 112640   bits: 18/17
c ---[2974]---> Adder-cost: 88   maxlim: 138240   bits: 19/18
c ---[2972]---> Adder-cost: 250   maxlim: 129024   bits: 18/17
c ---[2970]---> Adder-cost: 206   maxlim: 103424   bits: 18/17
c ---[2968]---> Adder-cost: 148   maxlim: 98304   bits: 18/17
c ---[2966]---> Sorter-cost: 1061     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2964]---> Sorter-cost:  672     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2962]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2960]---> Adder-cost: 112   maxlim: 56320   bits: 17/16
c ---[2958]---> Adder-cost: 202   maxlim: 100352   bits: 18/17
c ---[2956]---> Adder-cost: 104   maxlim: 52224   bits: 17/16
c ---[2954]---> Adder-cost: 110   maxlim: 57344   bits: 17/16
c ---[2952]---> Adder-cost: 206   maxlim: 104448   bits: 18/17
c ---[2950]---> Sorter-cost: 1131     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2948]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2946]---> Sorter-cost:  921     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2944]---> Sorter-cost:  446     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2942]---> Sorter-cost:  365     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2940]---> Adder-cost: 228   maxlim: 114688   bits: 18/17
c ---[2937]---> Sorter-cost: 1076     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2935]---> Sorter-cost:  983     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2933]---> Sorter-cost: 1191     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2931]---> Adder-cost: 74   maxlim: 104448   bits: 18/17
c ---[2927]---> Adder-cost: 140   maxlim: 66560   bits: 18/17
c ---[2925]---> Adder-cost: 148   maxlim: 77824   bits: 18/17
c ---[2923]---> Adder-cost: 64   maxlim: 77824   bits: 18/17
c ---[2921]---> Adder-cost: 122   maxlim: 74752   bits: 18/17
c ---[2919]---> Adder-cost: 168   maxlim: 82944   bits: 18/17
c ---[2917]---> Adder-cost: 68   maxlim: 82944   bits: 18/17
c ---[2913]---> Adder-cost: 100   maxlim: 104448   bits: 18/17
c ---[2911]---> Adder-cost: 224   maxlim: 122880   bits: 18/17
c ---[2909]---> Adder-cost: 94   maxlim: 56320   bits: 17/16
c ---[2906]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2904]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2902]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2900]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2898]---> Sorter-cost:  592     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2896]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2894]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2892]---> Adder-cost: 74   maxlim: 104448   bits: 18/17
c ---[2890]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2888]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2886]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2884]---> Sorter-cost:  676     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2882]---> Sorter-cost:  402     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2880]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2878]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2876]---> Sorter-cost:  855     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2874]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2872]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2870]---> Adder-cost: 122   maxlim: 102400   bits: 18/17
c ---[2868]---> Sorter-cost:  755     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2866]---> Adder-cost: 216   maxlim: 108544   bits: 18/17
c ---[2864]---> Adder-cost: 78   maxlim: 108544   bits: 18/17
c ---[2862]---> Adder-cost: 198   maxlim: 111616   bits: 18/17
c ---[2860]---> Adder-cost: 134   maxlim: 110592   bits: 18/17
c ---[2858]---> Adder-cost: 144   maxlim: 111616   bits: 18/17
c ---[2856]---> Adder-cost: 94   maxlim: 111616   bits: 18/17
c ---[2854]---> Adder-cost: 238   maxlim: 121856   bits: 18/17
c ---[2852]---> Adder-cost: 80   maxlim: 121856   bits: 18/17
c ---[2850]---> Adder-cost: 210   maxlim: 117760   bits: 18/17
c ---[2848]---> Adder-cost: 76   maxlim: 102400   bits: 18/17
c ---[2846]---> Adder-cost: 154   maxlim: 114688   bits: 18/17
c ---[2844]---> Adder-cost: 142   maxlim: 68608   bits: 18/17
c ---[2842]---> Adder-cost: 128   maxlim: 69632   bits: 18/17
c ---[2840]---> Adder-cost: 114   maxlim: 71680   bits: 18/17
c ---[2838]---> Adder-cost: 60   maxlim: 71680   bits: 18/17
c ---[2836]---> Adder-cost: 234   maxlim: 117760   bits: 18/17
c ---[2834]---> Adder-cost: 150   maxlim: 114688   bits: 18/17
c ---[2832]---> Adder-cost: 206   maxlim: 107520   bits: 18/17
c ---[2830]---> Adder-cost: 78   maxlim: 107520   bits: 18/17
c ---[2828]---> Adder-cost: 78   maxlim: 107520   bits: 18/17
c ---[2826]---> Adder-cost: 76   maxlim: 102400   bits: 18/17
c ---[2824]---> Adder-cost: 102   maxlim: 110592   bits: 18/17
c ---[2822]---> Adder-cost: 96   maxlim: 116736   bits: 18/17
c ---[2819]---> Adder-cost: 126   maxlim: 64512   bits: 17/16
c ---[2817]---> Adder-cost: 174   maxlim: 86016   bits: 18/17
c ---[2815]---> Adder-cost: 140   maxlim: 81920   bits: 18/17
c ---[2813]---> Adder-cost: 136   maxlim: 76800   bits: 18/17
c ---[2811]---> Adder-cost: 76   maxlim: 102400   bits: 18/17
c ---[2809]---> Adder-cost: 122   maxlim: 74752   bits: 18/17
c ---[2807]---> Adder-cost: 106   maxlim: 59392   bits: 17/16
c ---[2805]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2803]---> Adder-cost: 120   maxlim: 60416   bits: 17/16
c ---[2801]---> Sorter-cost: 1250     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2799]---> Adder-cost: 76   maxlim: 102400   bits: 18/17
c ---[2797]---> Adder-cost: 208   maxlim: 104448   bits: 18/17
c ---[2795]---> Adder-cost: 158   maxlim: 105472   bits: 18/17
c ---[2793]---> Adder-cost: 190   maxlim: 94208   bits: 18/17
c ---[2791]---> Adder-cost: 182   maxlim: 93184   bits: 18/17
c ---[2789]---> Adder-cost: 152   maxlim: 98304   bits: 18/17
c ---[2787]---> Sorter-cost:  434     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2784]---> Adder-cost: 196   maxlim: 106496   bits: 18/17
c ---[2782]---> Adder-cost: 220   maxlim: 119808   bits: 18/17
c ---[2780]---> Adder-cost: 188   maxlim: 111616   bits: 18/17
c ---[2778]---> Adder-cost: 106   maxlim: 52224   bits: 17/16
c ---[2776]---> Adder-cost: 108   maxlim: 57344   bits: 17/16
c ---[2773]---> Sorter-cost: 1287     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2771]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2769]---> Sorter-cost:  887     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2767]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2765]---> Sorter-cost: 1120     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2763]---> Sorter-cost:  317     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2760]---> Sorter-cost: 1030     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2758]---> Sorter-cost:  601     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2756]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2753]---> Adder-cost: 274   maxlim: 136192   bits: 19/18
c ---[2751]---> Adder-cost: 238   maxlim: 122880   bits: 18/17
c ---[2749]---> Adder-cost: 106   maxlim: 51200   bits: 17/16
c ---[2746]---> Sorter-cost: 1084     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2744]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2742]---> Adder-cost: 132   maxlim: 68608   bits: 18/17
c ---[2740]---> Sorter-cost: 1313     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2736]---> Sorter-cost:  803     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2734]---> Adder-cost: 60   maxlim: 57344   bits: 17/16
c ---[2732]---> Adder-cost: 154   maxlim: 73728   bits: 18/17
c ---[2730]---> Adder-cost: 146   maxlim: 74752   bits: 18/17
c ---[2728]---> Sorter-cost: 1192     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2726]---> Sorter-cost:  762     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2723]---> Adder-cost: 154   maxlim: 74752   bits: 18/17
c ---[2721]---> Adder-cost: 60   maxlim: 74752   bits: 18/17
c ---[2719]---> Adder-cost: 52   maxlim: 57344   bits: 17/16
c ---[2716]---> Adder-cost: 212   maxlim: 108544   bits: 18/17
c ---[2713]---> Adder-cost: 142   maxlim: 68608   bits: 18/17
c ---[2709]---> Adder-cost: 286   maxlim: 147456   bits: 19/18
c ---[2707]---> Adder-cost: 114   maxlim: 58368   bits: 17/16
c ---[2703]---> Adder-cost: 148   maxlim: 71680   bits: 18/17
c ---[2700]---> Sorter-cost: 1073     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2698]---> Sorter-cost:  971     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2695]---> Adder-cost: 48   maxlim: 58368   bits: 17/16
c ---[2692]---> Adder-cost: 272   maxlim: 133120   bits: 19/18
c ---[2688]---> Adder-cost: 248   maxlim: 125952   bits: 18/17
c ---[2684]---> Adder-cost: 238   maxlim: 118784   bits: 18/17
c ---[2682]---> Sorter-cost: 1223     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2680]---> Adder-cost: 98   maxlim: 53248   bits: 17/16
c ---[2676]---> Adder-cost: 274   maxlim: 135168   bits: 19/18
c ---[2674]---> Adder-cost: 176   maxlim: 89088   bits: 18/17
c ---[2670]---> Adder-cost: 276   maxlim: 143360   bits: 19/18
c ---[2666]---> Sorter-cost: 1117     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2664]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[2661]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[2659]---> Adder-cost: 88   maxlim: 55296   bits: 17/16
c ---[2657]---> Adder-cost: 168   maxlim: 82944   bits: 18/17
c ---[2653]---> Sorter-cost:  971     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2651]---> Adder-cost: 360   maxlim: 184320   bits: 19/18
c ---[2649]---> Adder-cost: 330   maxlim: 182272   bits: 19/18
c ---[2645]---> Adder-cost: 198   maxlim: 108544   bits: 18/17
c ---[2643]---> Adder-cost: 290   maxlim: 154624   bits: 19/18
c ---[2641]---> Adder-cost: 176   maxlim: 86016   bits: 18/17
c ---[2637]---> Adder-cost: 150   maxlim: 89088   bits: 18/17
c ---[2635]---> Sorter-cost:  831     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2631]---> Adder-cost: 238   maxlim: 118784   bits: 18/17
c ---[2628]---> Adder-cost: 124   maxlim: 62464   bits: 17/16
c ---[2626]---> Adder-cost: 48   maxlim: 62464   bits: 17/16
c ---[2622]---> Adder-cost: 118   maxlim: 61440   bits: 17/16
c ---[2620]---> Sorter-cost:  882     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2618]---> Adder-cost: 124   maxlim: 61440   bits: 17/16
c ---[2614]---> Adder-cost: 112   maxlim: 61440   bits: 17/16
c ---[2612]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2610]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2608]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2605]---> Sorter-cost:  845     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2603]---> Sorter-cost:  908     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2599]---> Adder-cost: 144   maxlim: 70656   bits: 18/17
c ---[2597]---> Adder-cost: 222   maxlim: 111616   bits: 18/17
c ---[2595]---> Adder-cost: 130   maxlim: 112640   bits: 18/17
c ---[2591]---> Adder-cost: 158   maxlim: 80896   bits: 18/17
c ---[2588]---> Sorter-cost:  787     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2585]---> Adder-cost: 106   maxlim: 52224   bits: 17/16
c ---[2583]---> Adder-cost: 274   maxlim: 137216   bits: 19/18
c ---[2581]---> Adder-cost: 140   maxlim: 138240   bits: 19/18
c ---[2577]---> Adder-cost: 184   maxlim: 90112   bits: 18/17
c ---[2573]---> Adder-cost: 264   maxlim: 138240   bits: 19/18
c ---[2571]---> Sorter-cost:  784     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2568]---> Adder-cost: 162   maxlim: 80896   bits: 18/17
c ---[2566]---> Adder-cost: 62   maxlim: 80896   bits: 18/17
c ---[2562]---> Adder-cost: 184   maxlim: 91136   bits: 18/17
c ---[2560]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2558]---> Sorter-cost:  227     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2556]---> Sorter-cost:  703     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2554]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2552]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2550]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2548]---> Sorter-cost:  593     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2546]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2544]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2541]---> Adder-cost: 122   maxlim: 61440   bits: 17/16
c ---[2539]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2537]---> Adder-cost: 98   maxlim: 60416   bits: 17/16
c ---[2534]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2532]---> Sorter-cost:  468     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2530]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2528]---> Sorter-cost:  669     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2526]---> Adder-cost: 278   maxlim: 146432   bits: 19/18
c ---[2524]---> Adder-cost: 88   maxlim: 146432   bits: 19/18
c ---[2520]---> Adder-cost: 148   maxlim: 74752   bits: 18/17
c ---[2516]---> Adder-cost: 176   maxlim: 88064   bits: 18/17
c ---[2514]---> Adder-cost: 184   maxlim: 90112   bits: 18/17
c ---[2512]---> Adder-cost: 72   maxlim: 90112   bits: 18/17
c ---[2510]---> Sorter-cost:  563     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2506]---> Adder-cost: 152   maxlim: 77824   bits: 18/17
c ---[2503]---> Adder-cost: 182   maxlim: 91136   bits: 18/17
c ---[2501]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2498]---> Adder-cost: 170   maxlim: 82944   bits: 18/17
c ---[2496]---> Adder-cost: 298   maxlim: 149504   bits: 19/18
c ---[2494]---> Adder-cost: 210   maxlim: 105472   bits: 18/17
c ---[2492]---> Sorter-cost: 1244     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2490]---> Sorter-cost:  818     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2486]---> Adder-cost: 290   maxlim: 149504   bits: 19/18
c ---[2484]---> Sorter-cost:  470     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2481]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2479]---> Sorter-cost:  785     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2477]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2475]---> Adder-cost: 74   maxlim: 105472   bits: 18/17
c ---[2473]---> Adder-cost: 204   maxlim: 102400   bits: 18/17
c ---[2471]---> Adder-cost: 134   maxlim: 78848   bits: 18/17
c ---[2469]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2467]---> Sorter-cost:  896     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2465]---> Sorter-cost:  623     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2463]---> Sorter-cost:  923     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2461]---> Adder-cost: 154   maxlim: 73728   bits: 18/17
c ---[2459]---> Adder-cost: 252   maxlim: 129024   bits: 18/17
c ---[2457]---> Adder-cost: 112   maxlim: 104448   bits: 18/17
c ---[2454]---> Adder-cost: 154   maxlim: 82944   bits: 18/17
c ---[2452]---> Adder-cost: 130   maxlim: 81920   bits: 18/17
c ---[2448]---> Sorter-cost: 1269     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2446]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2444]---> Adder-cost: 180   maxlim: 105472   bits: 18/17
c ---[2441]---> Adder-cost: 152   maxlim: 76800   bits: 18/17
c ---[2439]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2437]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2435]---> Sorter-cost:  908     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2433]---> Sorter-cost:  905     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2429]---> Sorter-cost: 1215     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2427]---> Adder-cost: 146   maxlim: 74752   bits: 18/17
c ---[2425]---> Sorter-cost: 1182     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2423]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2421]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2419]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2417]---> Sorter-cost:  584     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2415]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2413]---> Adder-cost: 130   maxlim: 72704   bits: 18/17
c ---[2411]---> Sorter-cost:  436     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2409]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2407]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2404]---> Sorter-cost: 1313     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2402]---> Sorter-cost: 1279     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2400]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2398]---> Adder-cost: 144   maxlim: 70656   bits: 18/17
c ---[2395]---> Adder-cost: 202   maxlim: 99328   bits: 18/17
c ---[2393]---> Adder-cost: 70   maxlim: 99328   bits: 18/17
c ---[2391]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2388]---> Adder-cost: 118   maxlim: 60416   bits: 17/16
c ---[2384]---> Adder-cost: 166   maxlim: 87040   bits: 18/17
c ---[2382]---> Adder-cost: 136   maxlim: 69632   bits: 18/17
c ---[2380]---> Adder-cost: 132   maxlim: 76800   bits: 18/17
c ---[2378]---> Adder-cost: 62   maxlim: 69632   bits: 18/17
c ---[2375]---> Adder-cost: 66   maxlim: 87040   bits: 18/17
c ---[2371]---> Sorter-cost: 1034     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2369]---> Sorter-cost:  639     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2367]---> Sorter-cost: 1138     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2365]---> Adder-cost: 136   maxlim: 70656   bits: 18/17
c ---[2363]---> Sorter-cost: 1143     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2361]---> Adder-cost: 122   maxlim: 61440   bits: 17/16
c ---[2359]---> Adder-cost: 138   maxlim: 67584   bits: 18/17
c ---[2356]---> Adder-cost: 92   maxlim: 62464   bits: 17/16
c ---[2354]---> Adder-cost: 84   maxlim: 71680   bits: 18/17
c ---[2352]---> Sorter-cost:  269     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2350]---> Adder-cost: 298   maxlim: 151552   bits: 19/18
c ---[2348]---> Adder-cost: 302   maxlim: 153600   bits: 19/18
c ---[2346]---> Adder-cost: 222   maxlim: 110592   bits: 18/17
c ---[2343]---> Adder-cost: 186   maxlim: 95232   bits: 18/17
c ---[2341]---> Adder-cost: 228   maxlim: 125952   bits: 18/17
c ---[2339]---> Sorter-cost:  412     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2337]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2335]---> Sorter-cost:  647     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2333]---> Adder-cost: 194   maxlim: 101376   bits: 18/17
c ---[2329]---> Sorter-cost: 1211     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2327]---> Adder-cost: 152   maxlim: 75776   bits: 18/17
c ---[2325]---> Adder-cost: 104   maxlim: 59392   bits: 17/16
c ---[2323]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2321]---> Sorter-cost: 1153     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2319]---> Adder-cost: 164   maxlim: 99328   bits: 18/17
c ---[2316]---> Adder-cost: 218   maxlim: 108544   bits: 18/17
c ---[2314]---> Adder-cost: 214   maxlim: 118784   bits: 18/17
c ---[2312]---> Adder-cost: 80   maxlim: 118784   bits: 18/17
c ---[2310]---> Adder-cost: 174   maxlim: 86016   bits: 18/17
c ---[2308]---> Adder-cost: 66   maxlim: 86016   bits: 18/17
c ---[2306]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2302]---> Adder-cost: 200   maxlim: 99328   bits: 18/17
c ---[2300]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2298]---> Sorter-cost: 1016     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2296]---> Sorter-cost:  677     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2294]---> Adder-cost: 184   maxlim: 90112   bits: 18/17
c ---[2292]---> Sorter-cost: 1311     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2290]---> Adder-cost: 126   maxlim: 63488   bits: 17/16
c ---[2288]---> Adder-cost: 252   maxlim: 136192   bits: 19/18
c ---[2285]---> Sorter-cost:  900     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2283]---> Adder-cost: 70   maxlim: 99328   bits: 18/17
c ---[2281]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2279]---> Sorter-cost: 1259     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2276]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2274]---> Adder-cost: 138   maxlim: 72704   bits: 18/17
c ---[2272]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2270]---> Adder-cost: 188   maxlim: 98304   bits: 18/17
c ---[2267]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2265]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2263]---> Adder-cost: 106   maxlim: 54272   bits: 17/16
c ---[2261]---> Sorter-cost:  985     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2257]---> Adder-cost: 108   maxlim: 97280   bits: 18/17
c ---[2255]---> Adder-cost: 168   maxlim: 86016   bits: 18/17
c ---[2253]---> Sorter-cost:  688     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2249]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2247]---> Sorter-cost:  520     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2245]---> Sorter-cost:  440     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2241]---> Adder-cost: 158   maxlim: 96256   bits: 18/17
c ---[2239]---> Sorter-cost: 1048     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2235]---> Sorter-cost:  779     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2233]---> Sorter-cost:  395     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2230]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2226]---> Adder-cost: 108   maxlim: 95232   bits: 18/17
c ---[2224]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2220]---> Adder-cost: 168   maxlim: 81920   bits: 18/17
c ---[2217]---> Adder-cost: 144   maxlim: 69632   bits: 18/17
c ---[2214]---> Adder-cost: 110   maxlim: 54272   bits: 17/16
c ---[2212]---> Adder-cost: 70   maxlim: 95232   bits: 18/17
c ---[2210]---> Adder-cost: 112   maxlim: 60416   bits: 17/16
c ---[2208]---> Adder-cost: 48   maxlim: 60416   bits: 17/16
c ---[2204]---> Adder-cost: 314   maxlim: 162816   bits: 19/18
c ---[2202]---> Adder-cost: 92   maxlim: 162816   bits: 19/18
c ---[2200]---> Adder-cost: 310   maxlim: 166912   bits: 19/18
c ---[2198]---> Adder-cost: 100   maxlim: 166912   bits: 19/18
c ---[2195]---> Adder-cost: 100   maxlim: 166912   bits: 19/18
c ---[2193]---> Adder-cost: 100   maxlim: 166912   bits: 19/18
c ---[2190]---> Sorter-cost:  619     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2188]---> Adder-cost: 112   maxlim: 56320   bits: 17/16
c ---[2186]---> Adder-cost: 92   maxlim: 54272   bits: 17/16
c ---[2184]---> Adder-cost: 78   maxlim: 51200   bits: 17/16
c ---[2182]---> Adder-cost: 278   maxlim: 141312   bits: 19/18
c ---[2178]---> Adder-cost: 128   maxlim: 68608   bits: 18/17
c ---[2176]---> Adder-cost: 96   maxlim: 66560   bits: 18/17
c ---[2174]---> Adder-cost: 136   maxlim: 65536   bits: 18/17
c ---[2170]---> Adder-cost: 86   maxlim: 53248   bits: 17/16
c ---[2168]---> Adder-cost: 364   maxlim: 184320   bits: 19/18
c ---[2166]---> Sorter-cost: 1219     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2162]---> Adder-cost: 178   maxlim: 89088   bits: 18/17
c ---[2160]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2157]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[2155]---> Adder-cost: 142   maxlim: 72704   bits: 18/17
c ---[2153]---> Adder-cost: 116   maxlim: 70656   bits: 18/17
c ---[2151]---> Adder-cost: 254   maxlim: 153600   bits: 19/18
c ---[2148]---> Adder-cost: 148   maxlim: 73728   bits: 18/17
c ---[2146]---> Adder-cost: 102   maxlim: 55296   bits: 17/16
c ---[2142]---> Adder-cost: 230   maxlim: 119808   bits: 18/17
c ---[2140]---> Adder-cost: 80   maxlim: 119808   bits: 18/17
c ---[2137]---> Sorter-cost:  460     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2134]---> Adder-cost: 168   maxlim: 152576   bits: 19/18
c ---[2131]---> Sorter-cost:  617     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2129]---> Sorter-cost:  548     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2127]---> Sorter-cost:  532     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2125]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2123]---> Sorter-cost:  544     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2121]---> Sorter-cost: 1178     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2119]---> Adder-cost: 118   maxlim: 58368   bits: 17/16
c ---[2116]---> Sorter-cost: 1183     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2114]---> Adder-cost: 146   maxlim: 155648   bits: 19/18
c ---[2110]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2106]---> Adder-cost: 124   maxlim: 61440   bits: 17/16
c ---[2104]---> Adder-cost: 50   maxlim: 61440   bits: 17/16
c ---[2102]---> Sorter-cost: 1053     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2100]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2098]---> Adder-cost: 96   maxlim: 155648   bits: 19/18
c ---[2096]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2092]---> Sorter-cost:  680     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2090]---> Adder-cost: 172   maxlim: 87040   bits: 18/17
c ---[2088]---> Adder-cost: 226   maxlim: 119808   bits: 18/17
c ---[2086]---> Adder-cost: 142   maxlim: 73728   bits: 18/17
c ---[2084]---> Adder-cost: 62   maxlim: 73728   bits: 18/17
c ---[2079]---> Sorter-cost:  554     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2075]---> Sorter-cost:  931     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2072]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2070]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2068]---> Adder-cost: 154   maxlim: 73728   bits: 18/17
c ---[2066]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2063]---> Sorter-cost: 1147     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2061]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[2057]---> Sorter-cost:  727     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2053]---> Sorter-cost:  363     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2051]---> Adder-cost: 88   maxlim: 73728   bits: 18/17
c ---[2048]---> Sorter-cost: 1084     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2045]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2043]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2041]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[2039]---> Sorter-cost:  534     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2036]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2034]---> Adder-cost: 108   maxlim: 61440   bits: 17/16
c ---[2032]---> Adder-cost: 186   maxlim: 93184   bits: 18/17
c ---[2030]---> Adder-cost: 84   maxlim: 93184   bits: 18/17
c ---[2027]---> Sorter-cost: 1157     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2025]---> Sorter-cost:  771     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2023]---> Sorter-cost:  408     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2021]---> Sorter-cost:  698     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2017]---> Adder-cost: 172   maxlim: 90112   bits: 18/17
c ---[2015]---> Sorter-cost:  997     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2012]---> Sorter-cost: 1074     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2010]---> Sorter-cost:  987     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2008]---> Adder-cost: 172   maxlim: 86016   bits: 18/17
c ---[2006]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2004]---> Sorter-cost:  466     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2002]---> Sorter-cost:  676     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[2000]---> Sorter-cost:  443     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1998]---> Sorter-cost:  245     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1996]---> Sorter-cost:  375     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1993]---> Sorter-cost: 1133     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1991]---> Adder-cost: 108   maxlim: 79872   bits: 18/17
c ---[1989]---> Sorter-cost:  269     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1987]---> Sorter-cost:  231     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1985]---> Sorter-cost:  720     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1983]---> Sorter-cost:  704     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1980]---> Sorter-cost:  624     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1978]---> Sorter-cost:  315     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1976]---> Adder-cost: 150   maxlim: 77824   bits: 18/17
c ---[1973]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1971]---> Adder-cost: 230   maxlim: 115712   bits: 18/17
c ---[1969]---> Adder-cost: 160   maxlim: 114688   bits: 18/17
c ---[1967]---> Adder-cost: 204   maxlim: 116736   bits: 18/17
c ---[1964]---> Sorter-cost:  468     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1962]---> Adder-cost: 64   maxlim: 77824   bits: 18/17
c ---[1959]---> Sorter-cost:  684     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1957]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1955]---> Sorter-cost:  589     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1951]---> Adder-cost: 204   maxlim: 104448   bits: 18/17
c ---[1949]---> Sorter-cost: 1155     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1947]---> Adder-cost: 104   maxlim: 51200   bits: 17/16
c ---[1943]---> Sorter-cost: 1289     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1940]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1938]---> Sorter-cost:  271     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1936]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1933]---> Sorter-cost:  267     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1931]---> Adder-cost: 44   maxlim: 51200   bits: 17/16
c ---[1929]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1926]---> Sorter-cost:  657     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1923]---> Sorter-cost:  733     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1920]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1917]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1915]---> Sorter-cost: 1246     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1913]---> Sorter-cost:  951     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1911]---> Sorter-cost: 1129     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1908]---> Sorter-cost: 1061     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1906]---> Sorter-cost:  671     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1903]---> Adder-cost: 114   maxlim: 59392   bits: 17/16
c ---[1901]---> Adder-cost: 50   maxlim: 59392   bits: 17/16
c ---[1899]---> Adder-cost: 90   maxlim: 58368   bits: 17/16
c ---[1896]---> Adder-cost: 108   maxlim: 55296   bits: 17/16
c ---[1894]---> Sorter-cost:  607     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1892]---> Sorter-cost:  411     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1890]---> Sorter-cost: 1265     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1888]---> Adder-cost: 102   maxlim: 58368   bits: 17/16
c ---[1886]---> Sorter-cost: 1229     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1884]---> Adder-cost: 136   maxlim: 73728   bits: 18/17
c ---[1881]---> Sorter-cost:  657     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1879]---> Sorter-cost: 1209     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1877]---> Sorter-cost:  706     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1875]---> Sorter-cost:  448     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1873]---> Adder-cost: 304   maxlim: 163840   bits: 19/18
c ---[1871]---> Adder-cost: 124   maxlim: 61440   bits: 17/16
c ---[1868]---> Sorter-cost:  314     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1865]---> Sorter-cost: 1271     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1863]---> Adder-cost: 152   maxlim: 82944   bits: 18/17
c ---[1861]---> Sorter-cost:  680     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1857]---> Adder-cost: 146   maxlim: 79872   bits: 18/17
c ---[1855]---> Sorter-cost: 1128     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1852]---> Adder-cost: 212   maxlim: 111616   bits: 18/17
c ---[1849]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1847]---> Sorter-cost:  697     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1845]---> Sorter-cost: 1287     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1843]---> Adder-cost: 132   maxlim: 75776   bits: 18/17
c ---[1839]---> Sorter-cost:  361     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1837]---> Sorter-cost:  653     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1834]---> Adder-cost: 106   maxlim: 52224   bits: 17/16
c ---[1831]---> Adder-cost: 44   maxlim: 52224   bits: 17/16
c ---[1828]---> Sorter-cost: 1178     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1825]---> Sorter-cost:  939     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1823]---> Sorter-cost: 1085     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1821]---> Sorter-cost: 1089     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1819]---> Sorter-cost:  577     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1817]---> Sorter-cost:  670     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1815]---> Sorter-cost:  883     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1813]---> Adder-cost: 218   maxlim: 110592   bits: 18/17
c ---[1811]---> Adder-cost: 192   maxlim: 101376   bits: 18/17
c ---[1809]---> Adder-cost: 114   maxlim: 57344   bits: 17/16
c ---[1806]---> Sorter-cost:  439     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1804]---> Sorter-cost:  450     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1802]---> Sorter-cost:  265     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1800]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1798]---> Sorter-cost: 1301     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1796]---> Sorter-cost:  363     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1794]---> Sorter-cost: 1246     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1792]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1790]---> Adder-cost: 174   maxlim: 89088   bits: 18/17
c ---[1788]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1786]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1784]---> Sorter-cost:  296     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1782]---> Sorter-cost:  581     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1780]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1778]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1774]---> Adder-cost: 124   maxlim: 62464   bits: 17/16
c ---[1772]---> Adder-cost: 174   maxlim: 108544   bits: 18/17
c ---[1770]---> Adder-cost: 164   maxlim: 82944   bits: 18/17
c ---[1767]---> Sorter-cost:  611     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1765]---> Sorter-cost:  305     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1763]---> Sorter-cost:  684     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1761]---> Sorter-cost:  991     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1759]---> Adder-cost: 242   maxlim: 123904   bits: 18/17
c ---[1757]---> Sorter-cost:  599     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1754]---> Sorter-cost:  657     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1752]---> Adder-cost: 110   maxlim: 55296   bits: 17/16
c ---[1748]---> Sorter-cost: 1248     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1746]---> Sorter-cost:  923     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1744]---> Adder-cost: 200   maxlim: 125952   bits: 18/17
c ---[1742]---> Adder-cost: 104   maxlim: 52224   bits: 17/16
c ---[1740]---> Adder-cost: 108   maxlim: 60416   bits: 17/16
c ---[1738]---> Adder-cost: 110   maxlim: 64512   bits: 17/16
c ---[1736]---> Adder-cost: 102   maxlim: 58368   bits: 17/16
c ---[1734]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1732]---> Sorter-cost:  963     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1730]---> Sorter-cost: 1159     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1728]---> Adder-cost: 268   maxlim: 134144   bits: 19/18
c ---[1726]---> Adder-cost: 110   maxlim: 53248   bits: 17/16
c ---[1722]---> Sorter-cost:  975     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1720]---> Sorter-cost: 1073     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1717]---> Adder-cost: 154   maxlim: 73728   bits: 18/17
c ---[1714]---> Adder-cost: 242   maxlim: 138240   bits: 19/18
c ---[1712]---> Sorter-cost:  464     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1710]---> Sorter-cost:  259     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1707]---> Sorter-cost:  991     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1704]---> Sorter-cost:  937     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1702]---> Adder-cost: 264   maxlim: 141312   bits: 19/18
c ---[1700]---> Sorter-cost: 1132     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1698]---> Sorter-cost: 1016     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1694]---> Adder-cost: 110   maxlim: 64512   bits: 17/16
c ---[1692]---> Sorter-cost:  313     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1690]---> Sorter-cost:  179     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1686]---> Sorter-cost:  636     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1683]---> Sorter-cost:  973     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1681]---> Sorter-cost:  668     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1678]---> Adder-cost: 160   maxlim: 78848   bits: 18/17
c ---[1676]---> Adder-cost: 60   maxlim: 78848   bits: 18/17
c ---[1674]---> Adder-cost: 110   maxlim: 56320   bits: 17/16
c ---[1672]---> Sorter-cost: 1275     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1669]---> Sorter-cost:  464     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1667]---> Adder-cost: 156   maxlim: 77824   bits: 18/17
c ---[1665]---> Adder-cost: 94   maxlim: 79872   bits: 18/17
c ---[1663]---> Adder-cost: 266   maxlim: 136192   bits: 19/18
c ---[1661]---> Adder-cost: 226   maxlim: 135168   bits: 19/18
c ---[1659]---> Adder-cost: 280   maxlim: 142336   bits: 19/18
c ---[1657]---> Adder-cost: 92   maxlim: 142336   bits: 19/18
c ---[1655]---> Sorter-cost:  559     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1652]---> Sorter-cost:  414     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1650]---> Sorter-cost:  904     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1648]---> Adder-cost: 140   maxlim: 65536   bits: 18/17
c ---[1646]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1644]---> Sorter-cost: 1082     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1641]---> Adder-cost: 244   maxlim: 128000   bits: 18/17
c ---[1639]---> Sorter-cost:  462     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1637]---> Adder-cost: 110   maxlim: 56320   bits: 17/16
c ---[1635]---> Sorter-cost: 1031     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1633]---> Adder-cost: 46   maxlim: 56320   bits: 17/16
c ---[1629]---> Sorter-cost:  581     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1627]---> Sorter-cost:  622     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1625]---> Sorter-cost:  476     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1623]---> Sorter-cost:  227     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1621]---> Sorter-cost:  221     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1618]---> Adder-cost: 180   maxlim: 91136   bits: 18/17
c ---[1616]---> Adder-cost: 104   maxlim: 52224   bits: 17/16
c ---[1614]---> Adder-cost: 158   maxlim: 84992   bits: 18/17
c ---[1611]---> Adder-cost: 142   maxlim: 67584   bits: 18/17
c ---[1609]---> Adder-cost: 200   maxlim: 99328   bits: 18/17
c ---[1607]---> Adder-cost: 70   maxlim: 99328   bits: 18/17
c ---[1603]---> Adder-cost: 124   maxlim: 62464   bits: 17/16
c ---[1599]---> Sorter-cost:  775     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1596]---> Sorter-cost: 1008     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1594]---> Sorter-cost:  967     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1592]---> Adder-cost: 152   maxlim: 90112   bits: 18/17
c ---[1589]---> Adder-cost: 282   maxlim: 159744   bits: 19/18
c ---[1587]---> Adder-cost: 106   maxlim: 58368   bits: 17/16
c ---[1585]---> Adder-cost: 84   maxlim: 59392   bits: 17/16
c ---[1583]---> Adder-cost: 108   maxlim: 61440   bits: 17/16
c ---[1580]---> Sorter-cost:  968     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1578]---> Sorter-cost:  613     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1576]---> Sorter-cost:  291     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1574]---> Sorter-cost: 1068     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1572]---> Adder-cost: 112   maxlim: 60416   bits: 17/16
c ---[1570]---> Sorter-cost:  873     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1568]---> Sorter-cost:  672     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1566]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1564]---> Sorter-cost:  495     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1562]---> Adder-cost: 108   maxlim: 53248   bits: 17/16
c ---[1560]---> Adder-cost: 48   maxlim: 53248   bits: 17/16
c ---[1556]---> Adder-cost: 104   maxlim: 64512   bits: 17/16
c ---[1553]---> Sorter-cost:  894     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1550]---> Adder-cost: 220   maxlim: 111616   bits: 18/17
c ---[1548]---> Sorter-cost:  664     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1546]---> Sorter-cost:  510     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1544]---> Sorter-cost: 1313     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1542]---> Sorter-cost: 1175     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1539]---> Sorter-cost:  655     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1537]---> Sorter-cost:  309     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1535]---> Sorter-cost: 1221     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1533]---> Sorter-cost:  791     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1529]---> Sorter-cost:  259     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[1527]---> Sorter-cost: 1057     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1525]---> Sorter-cost: 1103     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1523]---> Adder-cost: 236   maxlim: 122880   bits: 18/17
c ---[1521]---> Sorter-cost:  528     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1519]---> Adder-cost: 206   maxlim: 119808   bits: 18/17
c ---[1514]---> Sorter-cost: 1293     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1512]---> Adder-cost: 138   maxlim: 66560   bits: 18/17
c ---[1509]---> Sorter-cost:  448     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1507]---> Sorter-cost:  593     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1505]---> Sorter-cost:  811     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1502]---> Sorter-cost: 1069     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1500]---> Adder-cost: 122   maxlim: 67584   bits: 18/17
c ---[1498]---> Sorter-cost: 1183     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1496]---> Sorter-cost: 1281     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1494]---> Adder-cost: 124   maxlim: 61440   bits: 17/16
c ---[1492]---> Sorter-cost:  375     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1490]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1488]---> Adder-cost: 202   maxlim: 102400   bits: 18/17
c ---[1486]---> Adder-cost: 138   maxlim: 101376   bits: 18/17
c ---[1484]---> Sorter-cost:  999     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1482]---> Adder-cost: 170   maxlim: 89088   bits: 18/17
c ---[1480]---> Adder-cost: 146   maxlim: 72704   bits: 18/17
c ---[1478]---> Adder-cost: 318   maxlim: 159744   bits: 19/18
c ---[1476]---> Adder-cost: 114   maxlim: 58368   bits: 17/16
c ---[1474]---> Adder-cost: 86   maxlim: 52224   bits: 17/16
c ---[1472]---> Sorter-cost: 1091     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1470]---> Sorter-cost:  882     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1468]---> Adder-cost: 146   maxlim: 69632   bits: 18/17
c ---[1466]---> Adder-cost: 158   maxlim: 78848   bits: 18/17
c ---[1464]---> Adder-cost: 206   maxlim: 104448   bits: 18/17
c ---[1462]---> Sorter-cost: 1246     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1460]---> Adder-cost: 224   maxlim: 119808   bits: 18/17
c ---[1458]---> Adder-cost: 186   maxlim: 96256   bits: 18/17
c ---[1456]---> Adder-cost: 236   maxlim: 126976   bits: 18/17
c ---[1454]---> Adder-cost: 192   maxlim: 106496   bits: 18/17
c ---[1452]---> Adder-cost: 156   maxlim: 75776   bits: 18/17
c ---[1450]---> Adder-cost: 172   maxlim: 87040   bits: 18/17
c ---[1448]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1446]---> Adder-cost: 238   maxlim: 129024   bits: 18/17
c ---[1444]---> Sorter-cost: 1207     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1441]---> Sorter-cost:  553     Base: 2 2 2 2 2 2 2 2 2 2 7
c ---[1439]---> Adder-cost: 102   maxlim: 51200   bits: 17/16
c ---[1437]---> Adder-cost: 92   maxlim: 57344   bits: 17/16
c ---[1435]---> Adder-cost: 76   maxlim: 54272   bits: 17/16
c ---[1433]---> Adder-cost: 214   maxlim: 110592   bits: 18/17
c ---[1431]---> Adder-cost: 256   maxlim: 135168   bits: 19/18
c ---[1429]---> Adder-cost: 262   maxlim: 141312   bits: 19/18
c ---[1427]---> Adder-cost: 354   maxlim: 199680   bits: 19/18
c ---[1425]---> Adder-cost: 230   maxlim: 152576   bits: 19/18
c ---[1423]---> Adder-cost: 338   maxlim: 196608   bits: 19/18
c ---[1421]---> Adder-cost: 264   maxlim: 194560   bits: 19/18
c ---[1419]---> Adder-cost: 310   maxlim: 191488   bits: 19/18
c ---[1417]---> Adder-cost: 276   maxlim: 178176   bits: 19/18
c ---[1415]---> Adder-cost: 266   maxlim: 151552   bits: 19/18
c ---[1413]---> Adder-cost: 274   maxlim: 171008   bits: 19/18
c ---[1411]---> Adder-cost: 366   maxlim: 203776   bits: 19/18
c ---[1409]---> Adder-cost: 364   maxlim: 218112   bits: 19/18
c ---[1407]---> Adder-cost: 346   maxlim: 216064   bits: 19/18
c ---[1405]---> Adder-cost: 306   maxlim: 195584   bits: 19/18
c ---[1403]---> Adder-cost: 216   maxlim: 142336   bits: 19/18
c ---[1401]---> Adder-cost: 198   maxlim: 118784   bits: 18/17
c ---[1399]---> Adder-cost: 184   maxlim: 110592   bits: 18/17
c ---[1397]---> Adder-cost: 196   maxlim: 120832   bits: 18/17
c ---[1395]---> Adder-cost: 184   maxlim: 115712   bits: 18/17
c ---[1393]---> Adder-cost: 168   maxlim: 94208   bits: 18/17
c ---[1391]---> Adder-cost: 272   maxlim: 142336   bits: 19/18
c ---[1389]---> Adder-cost: 186   maxlim: 143360   bits: 19/18
c ---[1387]---> Adder-cost: 252   maxlim: 141312   bits: 19/18
c ---[1385]---> Adder-cost: 168   maxlim: 146432   bits: 19/18
c ---[1383]---> Adder-cost: 190   maxlim: 144384   bits: 19/18
c ---[1381]---> Adder-cost: 196   maxlim: 148480   bits: 19/18
c ---[1379]---> Adder-cost: 250   maxlim: 156672   bits: 19/18
c ---[1377]---> Adder-cost: 180   maxlim: 154624   bits: 19/18
c ---[1375]---> Adder-cost: 108   maxlim: 53248   bits: 17/16
c ---[1373]---> Adder-cost: 208   maxlim: 140288   bits: 19/18
c ---[1371]---> Adder-cost: 210   maxlim: 141312   bits: 19/18
c ---[1369]---> Adder-cost: 170   maxlim: 136192   bits: 19/18
c ---[1367]---> Adder-cost: 228   maxlim: 135168   bits: 19/18
c ---[1365]---> Adder-cost: 216   maxlim: 139264   bits: 19/18
c ---[1363]---> Adder-cost: 156   maxlim: 136192   bits: 19/18
c ---[1361]---> Adder-cost: 178   maxlim: 111616   bits: 18/17
c ---[1359]---> Adder-cost: 156   maxlim: 80896   bits: 18/17
c ---[1357]---> Adder-cost: 180   maxlim: 109568   bits: 18/17
c ---[1356]---> Adder-cost: 2306   maxlim: 1125375   bits: 22/21
c ---[1355]---> Adder-cost: 11112   maxlim: 5775359   bits: 23/23
c ---[1353]---> Adder-cost: 257   maxlim: 135167   bits: 19/18
c ---[1352]---> Adder-cost: 275   maxlim: 146431   bits: 19/18
c ---[1351]---> Adder-cost: 309   maxlim: 149503   bits: 19/18
c ---[1349]---> Adder-cost: 323   maxlim: 157695   bits: 19/18
c ---[1348]---> Adder-cost: 345   maxlim: 173055   bits: 19/18
c ---[1346]---> Adder-cost: 520   maxlim: 244735   bits: 19/18
c ---[1345]---> Adder-cost: 303   maxlim: 150527   bits: 19/18
c ---[1343]---> Adder-cost: 496   maxlim: 243711   bits: 19/18
c ---[1337]---> Adder-cost: 351   maxlim: 162815   bits: 19/18
c ---[1335]---> Adder-cost: 496   maxlim: 254975   bits: 19/18
c ---[1334]---> Adder-cost: 603   maxlim: 301055   bits: 20/19
c ---[1330]---> Adder-cost: 406   maxlim: 195583   bits: 19/18
c ---[1329]---> Adder-cost: 2972   maxlim: 1595391   bits: 22/21
c ---[1325]---> Adder-cost: 725   maxlim: 359423   bits: 20/19
c ---[1324]---> Adder-cost: 3446   maxlim: 1300479   bits: 21/21
c ---[13

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/31257/stat): 31257 (minisat+_script) R 31256 31257 9854 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796605218 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/31257/statm): 174 3 169 147 0 27 0
[pid=31257] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=31258
New process pid=31259
New process pid=31260
execve syscall for /bin/sed executable
One traced child (pid=31259) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=31260) exited with status: 0
One traced child (pid=31258) exited with status: 0
New process pid=31261
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-siena1.opb
One traced child (pid=31261) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=31262
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-20-10-siena1.opb

[startup+10.0039 s]
Raw data (loadavg): 0.93 0.97 0.99 1/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) T 31257 31257 9854 0 -1 0 4759 0 3 0 915 24 0 0 25 0 1 0 1796605239 23068672 4483 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31262/statm): 5632 4483 162 162 0 5470 0
[pid=31262] vsize: 22528
Current children cumulated CPU time (s) 9.53
Current children cumulated vsize (Kb) 24656

[startup+20.0046 s]
Raw data (loadavg): 1.02 0.99 0.99 1/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) T 31257 31257 9854 0 -1 0 8740 0 3 0 1872 43 0 0 25 0 1 0 1796605239 34795520 7256 4294967295 134512640 135167914 3221224448 3221222540 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31262/statm): 8495 7256 162 162 0 8333 0
[pid=31262] vsize: 33980
Current children cumulated CPU time (s) 19.29
Current children cumulated vsize (Kb) 36108

[startup+30.0054 s]
Raw data (loadavg): 1.02 0.99 0.99 1/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) T 31257 31257 9854 0 -1 0 12263 0 3 0 2831 61 0 0 25 0 1 0 1796605239 44007424 9469 4294967295 134512640 135167914 3221224448 3221222524 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31262/statm): 10744 9469 162 162 0 10582 0
[pid=31262] vsize: 42976
Current children cumulated CPU time (s) 29.06
Current children cumulated vsize (Kb) 45104

[startup+40.0062 s]
Raw data (loadavg): 1.02 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 16085 0 3 0 3791 80 0 0 25 0 1 0 1796605239 52584448 11589 4294967295 134512640 135167914 3221224448 3221222876 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 12838 11589 162 162 0 12676 0
[pid=31262] vsize: 51352
Current children cumulated CPU time (s) 38.85
Current children cumulated vsize (Kb) 53480

[startup+50.0071 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 16253 0 3 0 4790 80 0 0 25 0 1 0 1796605239 53272576 11757 4294967295 134512640 135167914 3221224448 3221221792 134849179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31262/statm): 13006 11757 162 162 0 12844 0
[pid=31262] vsize: 52024
Current children cumulated CPU time (s) 48.84
Current children cumulated vsize (Kb) 54152

[startup+60.0078 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 16918 0 3 0 5788 82 0 0 25 0 1 0 1796605239 55521280 12257 4294967295 134512640 135167914 3221224448 3221221808 134693566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 13555 12257 162 162 0 13393 0
[pid=31262] vsize: 54220
Current children cumulated CPU time (s) 58.84
Current children cumulated vsize (Kb) 56348

[startup+70.0086 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 18048 0 3 0 6783 85 0 0 25 0 1 0 1796605239 59564032 13057 4294967295 134512640 135167914 3221224448 3221220852 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 14542 13057 162 162 0 14380 0
[pid=31262] vsize: 58168
Current children cumulated CPU time (s) 68.82
Current children cumulated vsize (Kb) 60296

[startup+80.0104 s]
Raw data (loadavg): 1.01 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 18523 0 3 0 7779 87 0 0 25 0 1 0 1796605239 60792832 13532 4294967295 134512640 135167914 3221224448 3221222444 134723262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 14842 13532 162 162 0 14680 0
[pid=31262] vsize: 59368
Current children cumulated CPU time (s) 78.8
Current children cumulated vsize (Kb) 61496

[startup+90.0111 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 18933 0 3 0 8775 90 0 0 25 0 1 0 1796605239 64995328 13942 4294967295 134512640 135167914 3221224448 3221221964 134722225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 15868 13942 162 162 0 15706 0
[pid=31262] vsize: 63472
Current children cumulated CPU time (s) 88.79
Current children cumulated vsize (Kb) 65600

[startup+100.012 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 20651 0 3 0 9769 94 0 0 25 0 1 0 1796605239 68763648 15001 4294967295 134512640 135167914 3221224448 3221221904 134843010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31262/statm): 16788 15001 162 162 0 16626 0
[pid=31262] vsize: 67152
Current children cumulated CPU time (s) 98.77
Current children cumulated vsize (Kb) 69280

[startup+110.013 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 21168 0 3 0 10764 97 0 0 25 0 1 0 1796605239 70098944 15518 4294967295 134512640 135167914 3221224448 3221222496 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 17114 15518 162 162 0 16952 0
[pid=31262] vsize: 68456
Current children cumulated CPU time (s) 108.75
Current children cumulated vsize (Kb) 70584

[startup+120.014 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 21725 0 3 0 11759 100 0 0 25 0 1 0 1796605239 71532544 16075 4294967295 134512640 135167914 3221224448 3221221260 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 17464 16075 162 162 0 17302 0
[pid=31262] vsize: 69856
Current children cumulated CPU time (s) 118.73
Current children cumulated vsize (Kb) 71984

[startup+130.014 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 22457 0 3 0 12753 102 0 0 25 0 1 0 1796605239 79720448 16807 4294967295 134512640 135167914 3221224448 3221223036 134722656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 19463 16807 162 162 0 19301 0
[pid=31262] vsize: 77852
Current children cumulated CPU time (s) 128.69
Current children cumulated vsize (Kb) 79980

[startup+140.015 s]
Raw data (loadavg): 1.00 0.99 0.99 1/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) T 31257 31257 9854 0 -1 0 22840 0 3 0 13751 104 0 0 25 0 1 0 1796605239 80711680 17190 4294967295 134512640 135167914 3221224448 3221200652 134934490 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31262/statm): 19705 17190 162 162 0 19543 0
[pid=31262] vsize: 78820
Current children cumulated CPU time (s) 138.69
Current children cumulated vsize (Kb) 80948

[startup+150.016 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 30440 0 3 0 14708 127 0 0 25 0 1 0 1796605239 112123904 23138 4294967295 134512640 135167914 3221224448 3221222932 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 27374 23138 162 162 0 27212 0
[pid=31262] vsize: 109496
Current children cumulated CPU time (s) 148.49
Current children cumulated vsize (Kb) 111624

[startup+160.017 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 30486 0 3 0 15709 127 0 0 25 0 1 0 1796605239 112304128 23184 4294967295 134512640 135167914 3221224448 3220553636 134624831 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 27418 23184 162 162 0 27256 0
[pid=31262] vsize: 109672
Current children cumulated CPU time (s) 158.5
Current children cumulated vsize (Kb) 111800

[startup+170.016 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 31628 0 3 0 16703 131 0 0 25 0 1 0 1796605239 115765248 24326 4294967295 134512640 135167914 3221224448 3219277120 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 28263 24326 162 162 0 28101 0
[pid=31262] vsize: 113052
Current children cumulated CPU time (s) 168.48
Current children cumulated vsize (Kb) 115180

[startup+180.017 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 32495 0 3 0 17697 134 0 0 25 0 1 0 1796605239 117551104 24747 4294967295 134512640 135167914 3221224448 3221223036 134722660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 28699 24747 162 162 0 28537 0
[pid=31262] vsize: 114796
Current children cumulated CPU time (s) 178.45
Current children cumulated vsize (Kb) 116924

[startup+190.018 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 42840 0 3 0 18650 165 0 0 25 0 1 0 1796605239 141987840 32455 4294967295 134512640 135167914 3221224448 3220773892 134849060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34665 32455 162 162 0 34503 0
[pid=31262] vsize: 138660
Current children cumulated CPU time (s) 188.29
Current children cumulated vsize (Kb) 140788

[startup+200.019 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43969 0 3 0 19642 168 0 0 25 0 1 0 1796605239 142884864 32659 4294967295 134512640 135167914 3221224448 3221220320 134696697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32659 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 198.24
Current children cumulated vsize (Kb) 141664

[startup+210.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 20642 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221220540 134845882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 208.24
Current children cumulated vsize (Kb) 141664

[startup+220.02 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 21643 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221220384 134849187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 218.25
Current children cumulated vsize (Kb) 141664

[startup+230.021 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 22643 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221220880 134722527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 228.25
Current children cumulated vsize (Kb) 141664

[startup+240.022 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 23643 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221220884 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 238.25
Current children cumulated vsize (Kb) 141664

[startup+250.023 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 24643 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221220688 134696256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 248.25
Current children cumulated vsize (Kb) 141664

[startup+260.024 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 25644 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221220356 134843000 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 258.26
Current children cumulated vsize (Kb) 141664

[startup+270.024 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 26644 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221220728 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 268.26
Current children cumulated vsize (Kb) 141664

[startup+280.025 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 27644 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221220896 134843118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 278.26
Current children cumulated vsize (Kb) 141664

[startup+290.026 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 28644 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221024 134843153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 288.26
Current children cumulated vsize (Kb) 141664

[startup+300.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 29645 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221220800 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 298.27
Current children cumulated vsize (Kb) 141664

[startup+310.027 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 30645 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221232 134845937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 308.27
Current children cumulated vsize (Kb) 141664

[startup+320.028 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 31645 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221116 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 318.27
Current children cumulated vsize (Kb) 141664

[startup+330.03 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 32646 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221220352 134720491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 328.28
Current children cumulated vsize (Kb) 141664

[startup+340.031 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 33646 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221104 134522197 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 338.28
Current children cumulated vsize (Kb) 141664

[startup+350.032 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 34646 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221240 134842997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 348.28
Current children cumulated vsize (Kb) 141664

[startup+360.032 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 35646 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221300 134629088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 358.28
Current children cumulated vsize (Kb) 141664

[startup+370.033 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 36647 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221440 134843036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 368.29
Current children cumulated vsize (Kb) 141664

[startup+380.034 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 37647 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221220704 134718193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 378.29
Current children cumulated vsize (Kb) 141664

[startup+390.035 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 38647 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221756 134722218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 388.29
Current children cumulated vsize (Kb) 141664

[startup+400.036 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 39647 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221816 134694481 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 398.29
Current children cumulated vsize (Kb) 141664

[startup+410.036 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 40648 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221392 134849153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 408.3
Current children cumulated vsize (Kb) 141664

[startup+420.037 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 41648 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221712 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 418.3
Current children cumulated vsize (Kb) 141664

[startup+430.039 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 42648 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221448 134722657 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 428.3
Current children cumulated vsize (Kb) 141664

[startup+440.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 43648 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221296 134630893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 438.3
Current children cumulated vsize (Kb) 141664

[startup+450.041 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 44649 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221904 134843107 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 448.31
Current children cumulated vsize (Kb) 141664

[startup+460.041 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 45649 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221640 134693553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 458.31
Current children cumulated vsize (Kb) 141664

[startup+470.041 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 46649 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221480 134629265 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 468.31
Current children cumulated vsize (Kb) 141664

[startup+480.042 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 47649 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221280 134693570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 478.31
Current children cumulated vsize (Kb) 141664

[startup+490.043 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 48650 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221222096 134696236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 488.32
Current children cumulated vsize (Kb) 141664

[startup+500.043 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 49650 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221984 134849066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 498.32
Current children cumulated vsize (Kb) 141664

[startup+510.044 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 50650 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221728 134844706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 508.32
Current children cumulated vsize (Kb) 141664

[startup+520.045 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 51650 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221222124 134845876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 518.32
Current children cumulated vsize (Kb) 141664

[startup+530.046 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 52650 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221440 134849096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 528.32
Current children cumulated vsize (Kb) 141664

[startup+540.047 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 53651 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221504 134845913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 538.33
Current children cumulated vsize (Kb) 141664

[startup+550.048 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 54651 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221222256 134844694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 548.33
Current children cumulated vsize (Kb) 141664

[startup+560.049 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 55651 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221968 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 558.33
Current children cumulated vsize (Kb) 141664

[startup+570.05 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 56652 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221222348 134693792 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 568.34
Current children cumulated vsize (Kb) 141664

[startup+580.052 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 57652 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221376 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 578.34
Current children cumulated vsize (Kb) 141664

[startup+590.053 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 58652 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221776 134522834 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 588.34
Current children cumulated vsize (Kb) 141664

[startup+600.053 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 59652 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221944 134845877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 598.34
Current children cumulated vsize (Kb) 141664

[startup+610.054 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 60653 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221904 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 608.35
Current children cumulated vsize (Kb) 141664

[startup+620.055 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 61653 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221222320 134849082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 618.35
Current children cumulated vsize (Kb) 141664

[startup+630.056 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 62653 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221312 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 628.35
Current children cumulated vsize (Kb) 141664

[startup+640.057 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 63653 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221664 134844668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 638.35
Current children cumulated vsize (Kb) 141664

[startup+650.057 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 64654 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221222480 134722521 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 648.36
Current children cumulated vsize (Kb) 141664

[startup+660.058 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 65654 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221222500 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 658.36
Current children cumulated vsize (Kb) 141664

[startup+670.059 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 66654 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221920 134723229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 668.36
Current children cumulated vsize (Kb) 141664

[startup+680.06 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 67654 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221222616 134845939 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 678.36
Current children cumulated vsize (Kb) 141664

[startup+690.06 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 68655 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221221840 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 688.37
Current children cumulated vsize (Kb) 141664

[startup+700.062 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 69655 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221222160 134849196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 698.37
Current children cumulated vsize (Kb) 141664

[startup+710.063 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43977 0 3 0 70655 168 0 0 25 0 1 0 1796605239 142884864 32667 4294967295 134512640 135167914 3221224448 3221222432 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34884 32667 162 162 0 34722 0
[pid=31262] vsize: 139536
Current children cumulated CPU time (s) 708.37
Current children cumulated vsize (Kb) 141664

[startup+720.063 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 71655 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221074240 134696113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 718.37
Current children cumulated vsize (Kb) 140068

[startup+730.065 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 72656 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221220712 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 728.38
Current children cumulated vsize (Kb) 140068

[startup+740.065 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 73656 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221220832 134844672 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 738.38
Current children cumulated vsize (Kb) 140068

[startup+750.066 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 74656 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221024 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 748.38
Current children cumulated vsize (Kb) 140068

[startup+760.067 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 75656 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221604 134849147 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 758.38
Current children cumulated vsize (Kb) 140068

[startup+770.067 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 76656 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221664 134844653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 768.38
Current children cumulated vsize (Kb) 140068

[startup+780.067 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 77657 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221222080 134844731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 778.39
Current children cumulated vsize (Kb) 140068

[startup+790.068 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 78657 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221964 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 788.39
Current children cumulated vsize (Kb) 140068

[startup+800.069 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 79657 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221222524 134843033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 798.39
Current children cumulated vsize (Kb) 140068

[startup+810.07 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 80658 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221222384 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 808.4
Current children cumulated vsize (Kb) 140068

[startup+820.071 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 81658 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221220320 134696773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 818.4
Current children cumulated vsize (Kb) 140068

[startup+830.071 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 82658 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221220320 134843400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 828.4
Current children cumulated vsize (Kb) 140068

[startup+840.072 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 83658 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221220580 134843031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 838.4
Current children cumulated vsize (Kb) 140068

[startup+850.072 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 84658 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221220608 134629114 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 848.4
Current children cumulated vsize (Kb) 140068

[startup+860.073 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 85659 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221220656 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 858.41
Current children cumulated vsize (Kb) 140068

[startup+870.073 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 86659 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221220864 134843402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 868.41
Current children cumulated vsize (Kb) 140068

[startup+880.073 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 87659 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221220496 134843113 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 878.41
Current children cumulated vsize (Kb) 140068

[startup+890.074 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 88659 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221220524 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 888.41
Current children cumulated vsize (Kb) 140068

[startup+900.075 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 89660 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221524 134844636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 898.42
Current children cumulated vsize (Kb) 140068

[startup+910.076 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 90660 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221220784 134844647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 908.42
Current children cumulated vsize (Kb) 140068

[startup+920.077 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 91660 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221056 134693573 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 918.42
Current children cumulated vsize (Kb) 140068

[startup+930.077 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 92660 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221052 134722227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 928.42
Current children cumulated vsize (Kb) 140068

[startup+940.078 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 93660 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221024 134844725 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 938.42
Current children cumulated vsize (Kb) 140068

[startup+950.078 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 94661 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221544 134844674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 948.43
Current children cumulated vsize (Kb) 140068

[startup+960.079 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 95661 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221216 134843001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 958.43
Current children cumulated vsize (Kb) 140068

[startup+970.079 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 96661 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221760 134722527 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 968.43
Current children cumulated vsize (Kb) 140068

[startup+980.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 97661 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221468 134522235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 978.43
Current children cumulated vsize (Kb) 140068

[startup+990.081 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 98662 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221232 134845881 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 988.44
Current children cumulated vsize (Kb) 140068

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 99662 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221240 134844633 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 998.44
Current children cumulated vsize (Kb) 140068

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 100662 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221056 134844637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1008.44
Current children cumulated vsize (Kb) 140068

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 101662 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221600 134843123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1018.44
Current children cumulated vsize (Kb) 140068

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 102663 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221264 134694407 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1028.45
Current children cumulated vsize (Kb) 140068

[startup+1040.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 103663 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221468 134694368 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1038.45
Current children cumulated vsize (Kb) 140068

[startup+1050.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 104663 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221408 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1048.45
Current children cumulated vsize (Kb) 140068

[startup+1060.08 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 105663 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221980 134843002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1058.45
Current children cumulated vsize (Kb) 140068

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 106663 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221632 134696565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1068.45
Current children cumulated vsize (Kb) 140068

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 107664 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221980 134722542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1078.46
Current children cumulated vsize (Kb) 140068

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 108664 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221984 134693566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1088.46
Current children cumulated vsize (Kb) 140068

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 109664 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221728 134845888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1098.46
Current children cumulated vsize (Kb) 140068

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 110664 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221568 134723229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1108.46
Current children cumulated vsize (Kb) 140068

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 111665 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221222140 134722512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1118.47
Current children cumulated vsize (Kb) 140068

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 112665 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221904 134844708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1128.47
Current children cumulated vsize (Kb) 140068

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 113665 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221904 134844728 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1138.47
Current children cumulated vsize (Kb) 140068

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 114665 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221221904 134696376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1148.47
Current children cumulated vsize (Kb) 140068

[startup+1160.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 115666 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221222256 134844736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1158.48
Current children cumulated vsize (Kb) 140068

[startup+1170.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 116666 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221222264 134693629 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1168.48
Current children cumulated vsize (Kb) 140068

[startup+1180.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 117666 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221222468 134845938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1178.48
Current children cumulated vsize (Kb) 140068

[startup+1190.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 118666 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221222256 134844715 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1188.48
Current children cumulated vsize (Kb) 140068

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43984 0 3 0 119667 168 0 0 25 0 1 0 1796605239 141250560 32275 4294967295 134512640 135167914 3221224448 3221222144 134843406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32275 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1198.49
Current children cumulated vsize (Kb) 140068

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43985 0 3 0 120667 168 0 0 25 0 1 0 1796605239 141250560 32276 4294967295 134512640 135167914 3221224448 3221222848 134843026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32276 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1208.49
Current children cumulated vsize (Kb) 140068



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.99 2/57 31262
Raw data (/proc/31257/stat): 31257 (minisat+_script) S 31256 31257 9854 0 -1 0 314 758 0 0 0 1 9 4 17 0 1 0 1796605218 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31257/statm): 532 234 485 147 0 385 0
[pid=31257] vsize: 2128
Raw data (/proc/31262/stat): 31262 (minisat+_bignum) R 31257 31257 9854 0 -1 0 43985 0 3 0 120667 168 0 0 25 0 1 0 1796605239 141250560 32276 4294967295 134512640 135167914 3221224448 3221222784 134844644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31262/statm): 34485 32276 162 162 0 34323 0
[pid=31262] vsize: 137940
Current children cumulated CPU time (s) 1208.49
Current children cumulated vsize (Kb) 140068

Sending SIGTERM to -31257
Sleeping 2 seconds
One traced child (pid=31257) ended because it received signal 15 (SIGTERM)
One traced child (pid=31262) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.42
CPU user time (s): 1206.67
CPU system time (s): 1.74473
CPU usage (%): 99.8561
Max. virtual memory (cumulated for all children) (Kb): 141664

Verifier Data

ERROR: no interpretation found !