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-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-greenbea.opb
MD5SUM44cf829c3f56aa0e06d9c19014e5de34
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 10788
Biggest coefficient in the objective function 524288000000
Number of bits for the biggest coefficient in the objective function 39
Sum of the numbers in the objective function 20280599220360
Number of bits of the sum of numbers in the objective function 45
Biggest number in a constraint 524288000000
Number of bits of the biggest number in a constraint 39
Biggest sum of numbers in a constraint 23881563011625
Number of bits of the biggest sum of numbers45
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables104437
Total number of constraints2675
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints2675
Minimum length of a constraint8
Maximum length of a constraint4913

Trace number 6032

Launcher Data

LAUNCH ON wulflinc29 THE 2005-09-20 02:46:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3163 boxname=wulflinc29 idbench=819 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  44cf829c3f56aa0e06d9c19014e5de34  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-greenbea.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-greenbea.opb
IDLAUNCH: 3163
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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	: 3
cpu MHz		: 451.020
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:        860332 kB
Buffers:         36412 kB
Cached:         105848 kB
SwapCached:        676 kB
Active:          40280 kB
Inactive:       104444 kB
HighTotal:      131008 kB
HighFree:        25928 kB
LowTotal:       903652 kB
LowFree:        834404 kB
SwapTotal:     2097892 kB
SwapFree:      2096528 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5664 kB
Slab:            23944 kB
Committed_AS:    64140 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:06:55 (client local time) WITH STATUS 0 IN 1208.6 SECONDS
stats: 3163 7 1208.6 0

Solver Data

c Parsing PB file...
c Converting 4200 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssss
c ---[4247]---> BDD-cost:   17
c ---[4242]---> BDD-cost:   15
c ---[4241]---> BDD-cost:   14
c ---[4240]---> BDD-cost:   18
c ---[4239]---> BDD-cost:   15
c ---[4237]---> BDD-cost:   14
c ---[4236]---> BDD-cost:   16
c ---[4235]---> BDD-cost:   13
c ---[4234]---> BDD-cost:   13
c ---[4233]---> BDD-cost:   11
c ---[4232]---> BDD-cost:   13
c ---[4230]---> BDD-cost:   13
c ---[4229]---> BDD-cost:   14
c ---[4227]---> BDD-cost:   12
c ---[4226]---> BDD-cost:    8
c ---[4225]---> BDD-cost:   12
c ---[4224]---> BDD-cost:   12
c ---[4223]---> BDD-cost:    9
c ---[4221]---> BDD-cost:   13
c ---[4218]---> BDD-cost:   10
c ---[4217]---> BDD-cost:   15
c ---[4214]---> BDD-cost:    9
c ---[4213]---> BDD-cost:   16
c ---[4212]---> BDD-cost:   12
c ---[4211]---> BDD-cost:   14
c ---[4210]---> BDD-cost:   14
c ---[4209]---> BDD-cost:   12
c ---[4208]---> BDD-cost:   15
c ---[4207]---> BDD-cost:   12
c ---[4206]---> BDD-cost:   13
c ---[4205]---> BDD-cost:    8
c ---[4203]---> BDD-cost:   12
c ---[4202]---> BDD-cost:   11
c ---[4201]---> BDD-cost:   10
c ---[4200]---> BDD-cost:   12
c ---[4199]---> BDD-cost:   14
c ---[4196]---> BDD-cost:   19
c ---[4195]---> BDD-cost:   13
c ---[4194]---> BDD-cost:   16
c ---[4192]---> BDD-cost:   16
c ---[4190]---> BDD-cost:   17
c ---[4189]---> BDD-cost:   15
c ---[4188]---> BDD-cost:   15
c ---[4187]---> BDD-cost:   13
c ---[4186]---> BDD-cost:   17
c ---[4185]---> BDD-cost:   16
c ---[4184]---> BDD-cost:   16
c ---[4183]---> BDD-cost:   15
c ---[4182]---> BDD-cost:   14
c ---[4181]---> BDD-cost:    7
c ---[4180]---> BDD-cost:   11
c ---[4179]---> BDD-cost:   15
c ---[4178]---> BDD-cost:    7
c ---[4177]---> BDD-cost:   12
c ---[4176]---> BDD-cost:   12
c ---[4175]---> BDD-cost:    8
c ---[4174]---> BDD-cost:   11
c ---[4173]---> BDD-cost:   14
c ---[4170]---> BDD-cost:   17
c ---[4169]---> BDD-cost:   20
c ---[4168]---> BDD-cost:   14
c ---[4167]---> BDD-cost:   13
c ---[4166]---> BDD-cost:   17
c ---[4164]---> BDD-cost:    9
c ---[4163]---> BDD-cost:   17
c ---[4162]---> BDD-cost:   11
c ---[4161]---> BDD-cost:   18
c ---[4160]---> BDD-cost:   15
c ---[4159]---> BDD-cost:   16
c ---[4158]---> BDD-cost:   16
c ---[4157]---> BDD-cost:   16
c ---[4155]---> BDD-cost:   17
c ---[4154]---> BDD-cost:   15
c ---[4153]---> BDD-cost:   15
c ---[4152]---> BDD-cost:    7
c ---[4151]---> BDD-cost:   11
c ---[4149]---> BDD-cost:    7
c ---[4148]---> BDD-cost:   14
c ---[4147]---> BDD-cost:   13
c ---[4146]---> BDD-cost:    7
c ---[4145]---> BDD-cost:   12
c ---[4142]---> BDD-cost:   14
c ---[4141]---> BDD-cost:   15
c ---[4140]---> BDD-cost:   19
c ---[4139]---> BDD-cost:   16
c ---[4138]---> BDD-cost:   16
c ---[4136]---> BDD-cost:   15
c ---[4135]---> BDD-cost:   17
c ---[4134]---> BDD-cost:   11
c ---[4133]---> BDD-cost:   16
c ---[4132]---> BDD-cost:   16
c ---[4130]---> BDD-cost:   15
c ---[4128]---> BDD-cost:   15
c ---[4127]---> BDD-cost:   15
c ---[4126]---> BDD-cost:   16
c ---[4125]---> BDD-cost:   16
c ---[4124]---> BDD-cost:   12
c ---[4123]---> BDD-cost:   16
c ---[4122]---> BDD-cost:   15
c ---[4121]---> BDD-cost:   12
c ---[4120]---> BDD-cost:   12
c ---[4119]---> BDD-cost:   11
c ---[4117]---> BDD-cost:   12
c ---[4116]---> BDD-cost:   11
c ---[4115]---> BDD-cost:   12
c ---[4114]---> BDD-cost:   11
c ---[4113]---> BDD-cost:   12
c ---[4112]---> BDD-cost:   12
c ---[4111]---> BDD-cost:   12
c ---[4110]---> BDD-cost:   13
c ---[4109]---> BDD-cost:   12
c ---[4108]---> BDD-cost:   15
c ---[4107]---> BDD-cost:   19
c ---[4104]---> BDD-cost:   15
c ---[4103]---> BDD-cost:   15
c ---[4100]---> BDD-cost:   16
c ---[4099]---> BDD-cost:   15
c ---[4098]---> BDD-cost:   16
c ---[4097]---> BDD-cost:   16
c ---[4096]---> BDD-cost:   17
c ---[4094]---> BDD-cost:   14
c ---[4093]---> BDD-cost:   13
c ---[4092]---> BDD-cost:   14
c ---[4091]---> BDD-cost:   12
c ---[4089]---> BDD-cost:   11
c ---[4087]---> BDD-cost:   12
c ---[4086]---> BDD-cost:   14
c ---[4085]---> BDD-cost:   13
c ---[4084]---> BDD-cost:   12
c ---[4083]---> BDD-cost:   15
c ---[4082]---> BDD-cost:   12
c ---[4080]---> BDD-cost:   11
c ---[4079]---> BDD-cost:   11
c ---[4077]---> BDD-cost:   10
c ---[4072]---> BDD-cost:   12
c ---[4071]---> BDD-cost:   16
c ---[4069]---> BDD-cost:   14
c ---[4067]---> BDD-cost:   13
c ---[4066]---> BDD-cost:   15
c ---[4064]---> BDD-cost:   16
c ---[4063]---> BDD-cost:   10
c ---[4061]---> BDD-cost:   16
c ---[4060]---> BDD-cost:   16
c ---[4059]---> BDD-cost:   16
c ---[4057]---> BDD-cost:   13
c ---[4056]---> BDD-cost:   18
c ---[4055]---> BDD-cost:   14
c ---[4054]---> BDD-cost:   12
c ---[4053]---> BDD-cost:   11
c ---[4052]---> BDD-cost:   13
c ---[4051]---> BDD-cost:    7
c ---[4050]---> BDD-cost:   14
c ---[4049]---> BDD-cost:   13
c ---[4048]---> BDD-cost:    9
c ---[4047]---> BDD-cost:    9
c ---[4046]---> BDD-cost:   13
c ---[4045]---> BDD-cost:   14
c ---[4044]---> BDD-cost:   17
c ---[4042]---> BDD-cost:   11
c ---[4041]---> BDD-cost:   12
c ---[4040]---> BDD-cost:   15
c ---[4039]---> BDD-cost:   19
c ---[4036]---> BDD-cost:   15
c ---[4035]---> BDD-cost:   16
c ---[4034]---> BDD-cost:   18
c ---[4032]---> BDD-cost:   18
c ---[4031]---> BDD-cost:   13
c ---[4030]---> BDD-cost:   18
c ---[4027]---> BDD-cost:   16
c ---[4026]---> BDD-cost:   15
c ---[4025]---> BDD-cost:   18
c ---[4024]---> BDD-cost:   17
c ---[4022]---> BDD-cost:   12
c ---[4021]---> BDD-cost:   15
c ---[4020]---> BDD-cost:    7
c ---[4019]---> BDD-cost:   15
c ---[4018]---> BDD-cost:   13
c ---[4017]---> BDD-cost:   12
c ---[4016]---> BDD-cost:   11
c ---[4015]---> BDD-cost:   13
c ---[4014]---> BDD-cost:   19
c ---[4013]---> BDD-cost:   16
c ---[4010]---> BDD-cost:   16
c ---[4009]---> BDD-cost:   18
c ---[4008]---> BDD-cost:   14
c ---[4007]---> BDD-cost:   15
c ---[4006]---> BDD-cost:   15
c ---[4005]---> BDD-cost:   16
c ---[4003]---> BDD-cost:   16
c ---[4002]---> BDD-cost:   10
c ---[4001]---> BDD-cost:   15
c ---[4000]---> BDD-cost:   15
c ---[3998]---> BDD-cost:   12
c ---[3997]---> BDD-cost:   13
c ---[3996]---> BDD-cost:   17
c ---[3994]---> BDD-cost:   11
c ---[3993]---> BDD-cost:   11
c ---[3992]---> BDD-cost:   10
c ---[3991]---> BDD-cost:    7
c ---[3990]---> BDD-cost:   13
c ---[3989]---> BDD-cost:   11
c ---[3988]---> BDD-cost:    8
c ---[3987]---> BDD-cost:    9
c ---[3986]---> BDD-cost:   11
c ---[3980]---> BDD-cost:   17
c ---[3979]---> BDD-cost:   13
c ---[3977]---> BDD-cost:   12
c ---[3975]---> BDD-cost:   15
c ---[3973]---> BDD-cost:   11
c ---[3972]---> BDD-cost:    7
c ---[3971]---> BDD-cost:    8
c ---[3970]---> BDD-cost:   13
c ---[3969]---> BDD-cost:   11
c ---[3968]---> BDD-cost:   14
c ---[3966]---> BDD-cost:   11
c ---[3965]---> BDD-cost:   10
c ---[3963]---> BDD-cost:    9
c ---[3961]---> BDD-cost:   13
c ---[3958]---> BDD-cost:   17
c ---[3956]---> Sorter-cost: 1853     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3954]---> Adder-cost: 593   maxlim: 310528   bits: 20/19
c ---[3952]---> Adder-cost: 926   maxlim: 1250687   bits: 22/21
c ---[3950]---> Adder-cost: 593   maxlim: 297600   bits: 20/19
c ---[3948]---> Sorter-cost: 3378     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3946]---> Adder-cost: 529   maxlim: 108800   bits: 18/17
c ---[3944]---> Sorter-cost: 3248     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3942]---> Sorter-cost: 2120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3940]---> Sorter-cost: 3164     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3938]---> Adder-cost: 300   maxlim: 97664   bits: 18/17
c ---[3936]---> BDD-cost:  172
c ---[3934]---> Adder-cost: 300   maxlim: 78976   bits: 18/17
c ---[3932]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3930]---> BDD-cost:   70
c ---[3928]---> Sorter-cost: 3164     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3926]---> Adder-cost: 593   maxlim: 453888   bits: 20/19
c ---[3924]---> Adder-cost: 593   maxlim: 299136   bits: 20/19
c ---[3922]---> BDD-cost:   58
c ---[3920]---> Sorter-cost: 1562     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3918]---> Adder-cost: 561   maxlim: 248192   bits: 19/18
c ---[3916]---> Sorter-cost: 1087     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3914]---> Adder-cost: 593   maxlim: 321152   bits: 20/19
c ---[3912]---> BDD-cost:   85
c ---[3910]---> Sorter-cost: 2874     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3908]---> Adder-cost: 353   maxlim: 219648   bits: 19/18
c ---[3906]---> Sorter-cost: 2946     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3904]---> Sorter-cost: 3380     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3902]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3900]---> Adder-cost: 375   maxlim: 60160   bits: 17/16
c ---[3898]---> BDD-cost:   75
c ---[3896]---> Adder-cost: 318   maxlim: 131712   bits: 19/18
c ---[3894]---> Sorter-cost: 1087     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3892]---> Sorter-cost: 1385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3890]---> Sorter-cost: 2120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3888]---> BDD-cost:   75
c ---[3886]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3884]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3882]---> BDD-cost:  170
c ---[3880]---> BDD-cost:   58
c ---[3878]---> BDD-cost:   58
c ---[3876]---> Adder-cost: 293   maxlim: 20224   bits: 16/15
c ---[3874]---> BDD-cost:   50
c ---[3872]---> BDD-cost:  314
c ---[3862]---> BDD-cost:  167
c ---[3860]---> BDD-cost:  314
c ---[3858]---> BDD-cost:  314
c ---[3856]---> BDD-cost:   90
c ---[3854]---> BDD-cost:   90
c ---[3852]---> BDD-cost:   50
c ---[3850]---> BDD-cost:   50
c ---[3840]---> Adder-cost: 404   maxlim: 2557996273   bits: 33/32
c ---[3838]---> Adder-cost: 404   maxlim: 2557996273   bits: 33/32
c ---[3836]---> Adder-cost: 404   maxlim: 2557996273   bits: 33/32
c ---[3828]---> Sorter-cost: 1999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 2
c ---[3826]---> Sorter-cost: 4718     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3824]---> Sorter-cost: 4748     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3822]---> Sorter-cost: 4702     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3820]---> Sorter-cost: 4702     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3816]---> Sorter-cost: 2732     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[3808]---> Sorter-cost: 3056     Base: 2 2 2 2 2 5 5 5 2 2 2 2 7 2 2 2
c ---[3806]---> Sorter-cost: 4317     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3804]---> Sorter-cost: 4269     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3802]---> Sorter-cost: 4269     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3800]---> Sorter-cost: 4269     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3796]---> Sorter-cost: 3658     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3788]---> Sorter-cost: 1577     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 2
c ---[3786]---> Sorter-cost: 3148     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3784]---> Sorter-cost: 3178     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3782]---> Sorter-cost: 3130     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3780]---> Sorter-cost: 3130     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3776]---> Sorter-cost: 1872     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2
c ---[3768]---> Sorter-cost: 2957     Base: 2 2 2 2 5 5 2 2 2 2 2 2 5 7 2 2 2
c ---[3766]---> Sorter-cost: 4645     Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2
c ---[3764]---> Sorter-cost: 4597     Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 2
c ---[3762]---> Sorter-cost: 4597     Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 2
c ---[3760]---> Sorter-cost: 4597     Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 2
c ---[3756]---> Sorter-cost: 3580     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 5 2 7 2 2
c ---[3748]---> Sorter-cost: 3056     Base: 2 2 2 2 2 5 5 5 2 2 2 2 7 2 2 2
c ---[3746]---> Sorter-cost: 4287     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3744]---> Sorter-cost: 4317     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3742]---> Sorter-cost: 4269     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3740]---> Sorter-cost: 4269     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3736]---> Sorter-cost: 3658     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3726]---> BDD-cost:   53
c ---[3724]---> BDD-cost:   53
c ---[3720]---> Sorter-cost: 2016     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 2 2
c ---[3718]---> Sorter-cost: 3242     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3716]---> Sorter-cost: 3196     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3714]---> Sorter-cost: 3196     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3712]---> Sorter-cost: 3196     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3708]---> Sorter-cost: 2296     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 7 2 2
c ---[3700]---> BDD-cost:  595
c ---[3698]---> Sorter-cost: 3899     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3696]---> Sorter-cost: 3929     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3694]---> Sorter-cost: 3881     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3692]---> Sorter-cost: 3881     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3688]---> Sorter-cost: 3755     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[3680]---> Sorter-cost: 2658     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3678]---> Sorter-cost: 4342     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3676]---> Sorter-cost: 4362     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3674]---> Sorter-cost: 4362     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3672]---> Sorter-cost: 4362     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3668]---> Sorter-cost: 3084     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3660]---> Sorter-cost: 2861     Base: 2 2 2 2 2 2 2 2 2 5 2 2 3 7 2 2 2 2 2 2
c ---[3658]---> Sorter-cost: 4620     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[3656]---> Sorter-cost: 4640     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[3654]---> Sorter-cost: 4640     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[3652]---> Sorter-cost: 4640     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[3648]---> Sorter-cost: 3187     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3640]---> BDD-cost:  596
c ---[3638]---> Sorter-cost: 3506     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3636]---> Sorter-cost: 3458     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3634]---> Sorter-cost: 3458     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3632]---> Sorter-cost: 3458     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3628]---> Sorter-cost: 3165     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 7
c ---[3620]---> Sorter-cost: 2658     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3618]---> Sorter-cost: 4342     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3616]---> Sorter-cost: 4362     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3614]---> Sorter-cost: 4362     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3612]---> Sorter-cost: 4362     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3608]---> Sorter-cost: 3084     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3600]---> Sorter-cost: 2705     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3598]---> BDD-cost:  148
c ---[3594]---> Sorter-cost: 2627     Base: 2 2 2 2 2 2 2 2 2 3 3 3 2 2 2 2 2 2 2
c ---[3592]---> Sorter-cost: 4226     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3590]---> Sorter-cost: 4226     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3588]---> Sorter-cost: 4226     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3586]---> Sorter-cost: 4226     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3582]---> Sorter-cost: 2999     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3574]---> Sorter-cost: 4674     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 3 2 3 11 2 2 2
c ---[3572]---> Adder-cost: 548   maxlim: 163444290   bits: 29/28
c ---[3570]---> Adder-cost: 666   maxlim: 2615146050   bits: 32/32
c ---[3568]---> Adder-cost: 666   maxlim: 2615146050   bits: 32/32
c ---[3566]---> Adder-cost: 468   maxlim: 1307573025   bits: 32/31
c ---[3564]---> Sorter-cost: 4674     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 3 2 3 11 2 2 2
c ---[3562]---> BDD-cost:  447
c ---[3560]---> Adder-cost: 516   maxlim: 140770970   bits: 29/28
c ---[3558]---> Adder-cost: 544   maxlim: 375389850   bits: 30/29
c ---[3556]---> Adder-cost: 516   maxlim: 140770970   bits: 29/28
c ---[3554]---> BDD-cost:  254
c ---[3552]---> Sorter-cost: 1999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[3550]---> Sorter-cost: 1999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[3548]---> Sorter-cost: 1999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[3546]---> Adder-cost: 390   maxlim: 1301281575   bits: 32/31
c ---[3544]---> Adder-cost: 456   maxlim: 162657870   bits: 29/28
c ---[3542]---> Adder-cost: 560   maxlim: 2602563150   bits: 32/32
c ---[3540]---> Adder-cost: 560   maxlim: 2602563150   bits: 32/32
c ---[3538]---> Adder-cost: 390   maxlim: 1301281575   bits: 32/31
c ---[3536]---> Adder-cost: 370   maxlim: 650640167   bits: 31/30
c ---[3534]---> BDD-cost:  450
c ---[3532]---> Adder-cost: 358   maxlim: 161480550   bits: 28/28
c ---[3530]---> Adder-cost: 358   maxlim: 161480550   bits: 28/28
c ---[3528]---> Adder-cost: 358   maxlim: 161480550   bits: 28/28
c ---[3526]---> Adder-cost: 330   maxlim: 162659111   bits: 29/28
c ---[3524]---> Sorter-cost: 5540     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2
c ---[3522]---> BDD-cost:  181
c ---[3520]---> Sorter-cost: 3779     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[3518]---> Sorter-cost: 3779     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[3516]---> BDD-cost:  615
c ---[3512]---> BDD-cost:  154
c ---[3510]---> Sorter-cost: 3405     Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3508]---> Sorter-cost: 3405     Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3506]---> Sorter-cost: 3114     Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3502]---> Sorter-cost: 5380     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[3500]---> BDD-cost:  154
c ---[3498]---> Sorter-cost: 3650     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2
c ---[3496]---> Sorter-cost: 3650     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2
c ---[3494]---> Sorter-cost: 3650     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2
c ---[3492]---> Sorter-cost: 3650     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2
c ---[3490]---> BDD-cost:  288
c ---[3488]---> Sorter-cost: 3502     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2
c ---[3486]---> Sorter-cost: 4188     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[3484]---> BDD-cost:  278
c ---[3482]---> Sorter-cost: 4188     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[3480]---> Sorter-cost: 4188     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[3478]---> Sorter-cost: 4188     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[3476]---> BDD-cost:  463
c ---[3474]---> Sorter-cost: 3748     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[3472]---> Sorter-cost: 2140     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3470]---> Sorter-cost: 3598     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 2
c ---[3468]---> Sorter-cost: 4750     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3466]---> Sorter-cost: 4946     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 3 2 2
c ---[3464]---> Sorter-cost: 2140     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3462]---> Sorter-cost: 2140     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3460]---> Sorter-cost: 1814     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3458]---> Sorter-cost: 1604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3450]---> Sorter-cost: 3521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 3 3 2 2
c ---[3448]---> Adder-cost: 392   maxlim: 15007286   bits: 25/24
c ---[3446]---> Adder-cost: 510   maxlim: 480247350   bits: 30/29
c ---[3444]---> Adder-cost: 510   maxlim: 480247350   bits: 30/29
c ---[3442]---> Sorter-cost: 3521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 3 3 2 2
c ---[3440]---> Sorter-cost: 3264     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3438]---> Sorter-cost: 2793     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 3 3 2 2
c ---[3436]---> Sorter-cost: 2778     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3434]---> Sorter-cost: 1368     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2
c ---[3432]---> Sorter-cost: 1368     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2
c ---[3430]---> Sorter-cost: 1368     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2
c ---[3428]---> Sorter-cost: 5758     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2
c ---[3426]---> BDD-cost:  173
c ---[3424]---> Adder-cost: 406   maxlim: 2778196813   bits: 33/32
c ---[3422]---> Adder-cost: 406   maxlim: 2778196813   bits: 33/32
c ---[3420]---> BDD-cost:  607
c ---[3416]---> BDD-cost:  172
c ---[3412]---> Sorter-cost: 6191     Base: 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3410]---> BDD-cost:  286
c ---[3408]---> Adder-cost: 490   maxlim: 1601174025   bits: 32/31
c ---[3406]---> Adder-cost: 490   maxlim: 1601174025   bits: 32/31
c ---[3404]---> Adder-cost: 490   maxlim: 1601174025   bits: 32/31
c ---[3402]---> Adder-cost: 490   maxlim: 1601174025   bits: 32/31
c ---[3400]---> BDD-cost:  421
c ---[3398]---> Sorter-cost: 5086     Base: 2 2 2 2 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2
c ---[3396]---> Sorter-cost: 3252     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2
c ---[3394]---> BDD-cost:  451
c ---[3392]---> Sorter-cost: 3252     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2
c ---[3390]---> Sorter-cost: 3252     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2
c ---[3388]---> Sorter-cost: 3252     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2
c ---[3386]---> Sorter-cost: 2610     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2
c ---[3384]---> Sorter-cost: 3036     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2
c ---[3382]---> Sorter-cost: 3602     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 3
c ---[3380]---> Adder-cost: 598   maxlim: 14032030650   bits: 35/34
c ---[3378]---> Adder-cost: 598   maxlim: 14032030650   bits: 35/34
c ---[3376]---> Sorter-cost: 4093     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2 2 2
c ---[3374]---> Sorter-cost: 3849     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2 2 2
c ---[3372]---> BDD-cost:  131
c ---[3370]---> Sorter-cost: 3210     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2
c ---[3368]---> Sorter-cost: 3524     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2
c ---[3366]---> Sorter-cost: 3210     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2
c ---[3364]---> BDD-cost:  105
c ---[3356]---> Adder-cost: 384   maxlim: 7049569725   bits: 34/33
c ---[3354]---> Adder-cost: 634   maxlim: 14099139450   bits: 35/34
c ---[3352]---> Adder-cost: 634   maxlim: 14099139450   bits: 35/34
c ---[3350]---> Adder-cost: 384   maxlim: 7049569725   bits: 34/33
c ---[3348]---> Adder-cost: 364   maxlim: 3524781501   bits: 33/32
c ---[3346]---> BDD-cost:  131
c ---[3344]---> Sorter-cost: 5682     Base: 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3342]---> Sorter-cost: 5682     Base: 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3340]---> Sorter-cost: 5682     Base: 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3338]---> BDD-cost:  340
c ---[3336]---> Sorter-cost: 6568     Base: 2 2 2 2 2 5 5 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3334]---> Sorter-cost: 3886     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[3332]---> Sorter-cost: 3886     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[3330]---> Sorter-cost: 3456     Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[3328]---> BDD-cost:  152
c ---[3326]---> BDD-cost:  373
c ---[3324]---> Sorter-cost: 4232     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2
c ---[3322]---> Sorter-cost: 4232     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2
c ---[3320]---> Sorter-cost: 3956     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2
c ---[3316]---> Adder-cost: 514   maxlim: 488635950   bits: 30/29
c ---[3314]---> Adder-cost: 514   maxlim: 488635950   bits: 30/29
c ---[3312]---> Adder-cost: 514   maxlim: 488635950   bits: 30/29
c ---[3310]---> Sorter-cost: 2118     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3308]---> Sorter-cost: 2118     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3306]---> Sorter-cost: 2118     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3304]---> BDD-cost:  758
c ---[3302]---> BDD-cost:  754
c ---[3300]---> Sorter-cost: 2265     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[3298]---> Sorter-cost: 2265     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[3296]---> Sorter-cost: 2265     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[3294]---> Sorter-cost: 2491     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 7 2 2
c ---[3292]---> Sorter-cost: 2491     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 7 2 2
c ---[3290]---> Sorter-cost: 2491     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 7 2 2
c ---[3288]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3286]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3284]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3282]---> Sorter-cost: 4366     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3280]---> Sorter-cost: 3277     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2
c ---[3278]---> Sorter-cost: 3277     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2
c ---[3276]---> Sorter-cost: 3501     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2
c ---[3274]---> Sorter-cost: 3277     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2
c ---[3272]---> Sorter-cost: 3277     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2
c ---[3270]---> BDD-cost:  595
c ---[3268]---> BDD-cost:  530
c ---[3266]---> Sorter-cost: 3151     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3264]---> Sorter-cost: 1392     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[3262]---> Sorter-cost: 1478     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[3260]---> Sorter-cost: 1535     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[3258]---> Sorter-cost: 1478     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[3256]---> Sorter-cost: 1535     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[3254]---> Sorter-cost: 1134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[3252]---> Sorter-cost: 1191     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[3250]---> Sorter-cost: 5317     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3248]---> Sorter-cost: 4100     Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 7 2 2 2
c ---[3246]---> Sorter-cost: 4142     Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3244]---> Sorter-cost: 4142     Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3242]---> Sorter-cost: 3745     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3240]---> Sorter-cost: 3745     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3238]---> BDD-cost:  581
c ---[3236]---> BDD-cost:  529
c ---[3234]---> Sorter-cost: 3523     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3232]---> Sorter-cost: 2102     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3
c ---[3230]---> Sorter-cost: 2210     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3
c ---[3228]---> Sorter-cost: 2234     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[3226]---> Sorter-cost: 2210     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3
c ---[3224]---> Sorter-cost: 2234     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[3222]---> Sorter-cost: 1778     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3
c ---[3220]---> Sorter-cost: 1802     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[3218]---> Sorter-cost: 4684     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3216]---> Sorter-cost: 2644     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3214]---> Sorter-cost: 2644     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3212]---> Sorter-cost: 2879     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3210]---> Sorter-cost: 2644     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3208]---> Sorter-cost: 2644     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3206]---> Sorter-cost: 2039     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3204]---> Sorter-cost: 1871     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3202]---> Sorter-cost: 6062     Base: 2 2 2 2 2 2 2 2 2 5 2 5 2 2 5 2 2 2 2 2 2 2 2 2
c ---[3200]---> Sorter-cost: 3284     Base: 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 3
c ---[3198]---> Sorter-cost: 3561     Base: 2 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 3
c ---[3196]---> Sorter-cost: 3832     Base: 2 2 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 2
c ---[3194]---> Sorter-cost: 3561     Base: 2 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 3
c ---[3192]---> Sorter-cost: 3832     Base: 2 2 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 2
c ---[3190]---> Sorter-cost: 2300     Base: 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 3
c ---[3188]---> Sorter-cost: 2756     Base: 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 2
c ---[3186]---> Sorter-cost: 5559     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3184]---> Sorter-cost: 3987     Base: 2 2 2 2 2 2 2 2 2 5 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3182]---> Sorter-cost: 4024     Base: 2 2 2 2 2 2 2 2 2 5 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3180]---> Sorter-cost: 4024     Base: 2 2 2 2 2 2 2 2 2 5 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3178]---> Sorter-cost: 3727     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3176]---> Sorter-cost: 3727     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3174]---> Sorter-cost: 3052     Base: 2 2 2 2 2 2 5 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3172]---> Sorter-cost: 2776     Base: 2 2 2 2 2 2 5 2 2 5 2 2 2 2 2 2 2 2 2
c ---[3170]---> Sorter-cost: 6731     Base: 2 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3168]---> Sorter-cost: 3761     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 3
c ---[3166]---> Sorter-cost: 4035     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 3
c ---[3164]---> Sorter-cost: 4126     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 2 2
c ---[3162]---> Sorter-cost: 4035     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 3
c ---[3160]---> Sorter-cost: 4126     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 2 2
c ---[3158]---> Sorter-cost: 2939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 3
c ---[3156]---> Sorter-cost: 3030     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 2 2
c ---[3154]---> Sorter-cost: 3706     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3152]---> Sorter-cost: 3706     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3150]---> Sorter-cost: 3706     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3148]---> Sorter-cost: 3580     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3146]---> Sorter-cost: 3580     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3144]---> Sorter-cost: 3580     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3142]---> Sorter-cost: 3798     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2
c ---[3140]---> Sorter-cost: 3798     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2
c ---[3138]---> Sorter-cost: 3798     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2
c ---[3136]---> Sorter-cost: 4211     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3134]---> Sorter-cost: 4211     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3132]---> Sorter-cost: 4211     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3130]---> Sorter-cost: 5069     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3128]---> Sorter-cost: 3088     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3126]---> Sorter-cost: 3389     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3124]---> Sorter-cost: 3088     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3122]---> Sorter-cost: 3696     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3120]---> Sorter-cost: 3696     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3118]---> Sorter-cost: 3696     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3116]---> Sorter-cost: 3172     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2 2 2
c ---[3114]---> Sorter-cost: 1456     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3112]---> Sorter-cost: 1456     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3110]---> Sorter-cost: 1370     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3108]---> Sorter-cost: 2101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2
c ---[3106]---> Sorter-cost: 2101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2
c ---[3104]---> Sorter-cost: 2101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2
c ---[3102]---> Sorter-cost: 3791     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[3100]---> Sorter-cost: 2107     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5
c ---[3098]---> Sorter-cost: 2101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2
c ---[3096]---> Sorter-cost: 2107     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5
c ---[3094]---> Sorter-cost: 1542     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3092]---> Sorter-cost: 1542     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3090]---> Sorter-cost: 1542     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3088]---> Sorter-cost: 5054     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3086]---> Sorter-cost: 2867     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 3 2 2 2 3
c ---[3084]---> Sorter-cost: 2935     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[3082]---> Sorter-cost: 2867     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 3 2 2 2 3
c ---[3080]---> Sorter-cost: 2935     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[3078]---> Sorter-cost: 2935     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[3076]---> Sorter-cost: 2935     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[3074]---> Adder-cost: 1048   maxlim: 22769277786   bits: 35/35
c ---[3072]---> Adder-cost: 1048   maxlim: 22769277786   bits: 35/35
c ---[3070]---> Adder-cost: 1048   maxlim: 22769277786   bits: 35/35
c ---[3068]---> Adder-cost: 1868   maxlim: 1273684285   bits: 32/31
c ---[3066]---> Adder-cost: 2325   maxlim: 1783847576   bits: 32/31
c ---[3064]---> Adder-cost: 2055   maxlim: 1724964795   bits: 32/31
c ---[3062]---> Sorter-cost: 2144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3060]---> Sorter-cost: 6043     Base: 11 11 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 3
c ---[3058]---> Adder-cost: 544   maxlim: 761265450   bits: 31/30
c ---[3056]---> Sorter-cost: 6043     Base: 11 11 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 3
c ---[3054]---> Adder-cost: 544   maxlim: 761265450   bits: 31/30
c ---[3052]---> Adder-cost: 544   maxlim: 761265450   bits: 31/30
c ---[3050]---> Adder-cost: 544   maxlim: 761265450   bits: 31/30
c ---[3048]---> Adder-cost: 346   maxlim: 80740198   bits: 28/27
c ---[3046]---> Sorter-cost: 4195     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 3 2
c ---[3044]---> Adder-cost: 364   maxlim: 161480550   bits: 29/28
c ---[3042]---> Adder-cost: 364   maxlim: 161480550   bits: 29/28
c ---[3040]---> Adder-cost: 364   maxlim: 161480550   bits: 29/28
c ---[3038]---> Sorter-cost: 3199     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 11 2 2 2 2
c ---[3036]---> Adder-cost: 307   maxlim: 122158871   bits: 28/27
c ---[3034]---> Adder-cost: 325   maxlim: 244317975   bits: 29/28
c ---[3032]---> Adder-cost: 307   maxlim: 122158871   bits: 28/27
c ---[3030]---> Adder-cost: 325   maxlim: 244317975   bits: 29/28
c ---[3028]---> Adder-cost: 325   maxlim: 244317975   bits: 29/28
c ---[3026]---> Adder-cost: 325   maxlim: 244317975   bits: 29/28
c ---[3024]---> Sorter-cost: 2602     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3022]---> Sorter-cost: 2602     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3020]---> Sorter-cost: 2602     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3018]---> Sorter-cost: 3051     Base: 2 2 2 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3016]---> Sorter-cost: 3584     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 3 2 2 2
c ---[3006]---> Sorter-cost: 3810     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[3004]---> Sorter-cost: 4239     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[3002]---> Sorter-cost: 4239     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[3000]---> BDD-cost:  388
c ---[2998]---> BDD-cost:  388
c ---[2988]---> BDD-cost:  212
c ---[2986]---> BDD-cost:  212
c ---[2976]---> Sorter-cost: 4072     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2974]---> Sorter-cost: 4163     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2972]---> Sorter-cost: 4163     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2970]---> Sorter-cost: 2881     Base: 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2
c ---[2968]---> Sorter-cost: 3830     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3
c ---[2966]---> Sorter-cost: 3844     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2964]---> Sorter-cost: 3844     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2962]---> Sorter-cost: 3817     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3
c ---[2960]---> Sorter-cost: 3844     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2958]---> Sorter-cost: 3844     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2956]---> Sorter-cost: 4249     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2954]---> Sorter-cost: 3817     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3
c ---[2952]---> Sorter-cost: 3844     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2950]---> Sorter-cost: 3844     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2948]---> Sorter-cost: 6254     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2946]---> Sorter-cost: 2693     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2944]---> Sorter-cost: 3888     Base: 2 2 5 5 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2942]---> Sorter-cost: 6254     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2940]---> Sorter-cost: 3461     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3
c ---[2938]---> Sorter-cost: 3473     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2936]---> Sorter-cost: 3473     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2934]---> BDD-cost:  389
c ---[2932]---> Sorter-cost: 4239     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2908]---> Sorter-cost: 5511     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2906]---> Sorter-cost: 5339     Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2
c ---[2904]---> Sorter-cost: 5480     Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 3 5 2
c ---[2894]---> Sorter-cost: 2986     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2892]---> Sorter-cost: 3420     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2890]---> Sorter-cost: 2929     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2888]---> Sorter-cost: 3817     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2886]---> Sorter-cost: 3934     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2884]---> Sorter-cost: 3365     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2882]---> Sorter-cost: 3263     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 5 2
c ---[2880]---> BDD-cost:  370
c ---[2878]---> Sorter-cost: 3866     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 5 2 2 2 2 2 2
c ---[2876]---> Sorter-cost: 3866     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 5 2 2 2 2 2 2
c ---[2874]---> Sorter-cost: 3684     Base: 2 2 2 2 5 5 5 2 2 2 2 2 5 2 2 2 2 2 2
c ---[2870]---> BDD-cost:  133
c ---[2866]---> Sorter-cost: 3117     Base: 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2864]---> Sorter-cost: 1880     Base: 2 5 5 5 2 2 2 2 2 2 2
c ---[2862]---> Sorter-cost: 2828     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[2860]---> Sorter-cost: 3165     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2858]---> Sorter-cost: 1339     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2
c ---[2856]---> Sorter-cost: 2247     Base: 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2854]---> Sorter-cost: 2075     Base: 2 5 5 5 2 2 2 2 2 2 2
c ---[2852]---> Sorter-cost: 1880     Base: 2 5 5 5 2 2 2 2 2 2 2
c ---[2850]---> Sorter-cost: 2828     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[2848]---> Sorter-cost: 3165     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2846]---> Sorter-cost: 2806     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[2844]---> Sorter-cost: 5284     Base: 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2
c ---[2842]---> BDD-cost:  171
c ---[2840]---> Sorter-cost: 3874     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2
c ---[2838]---> Sorter-cost: 3874     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2
c ---[2836]---> Sorter-cost: 2253     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2
c ---[2834]---> Sorter-cost: 3129     Base: 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[2832]---> Sorter-cost: 3587     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2830]---> BDD-cost:  171
c ---[2828]---> Sorter-cost: 3874     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2
c ---[2826]---> Sorter-cost: 3874     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2
c ---[2824]---> Sorter-cost: 3864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2
c ---[2822]---> Sorter-cost: 1420     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ---[2820]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 5 2
c ---[2818]---> Adder-cost: 280   maxlim: 17301471   bits: 26/25
c ---[2816]---> Adder-cost: 280   maxlim: 17301471   bits: 26/25
c ---[2814]---> Sorter-cost: 2727     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 5 2
c ---[2

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/4588/stat): 4588 (minisat+_script) R 4587 4588 19818 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855037271 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/4588/statm): 174 3 169 147 0 27 0
[pid=4588] 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=4589
New process pid=4590
New process pid=4591
execve syscall for /bin/sed executable
One traced child (pid=4590) 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=4591) exited with status: 0
One traced child (pid=4589) exited with status: 0
New process pid=4592
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-greenbea.opb

[startup+10.0035 s]
Raw data (loadavg): 0.84 0.94 0.90 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 13980 0 0 0 841 76 0 0 25 0 1 0 1855037276 60293120 13677 4294967295 134512640 135094434 3221224432 3221223248 134580024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 14720 13677 145 145 0 14575 0
[pid=4592] vsize: 58880
Current children cumulated CPU time (s) 9.18
Current children cumulated vsize (Kb) 61004

[startup+20.0043 s]
Raw data (loadavg): 0.87 0.94 0.90 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 14547 0 0 0 1838 78 0 0 25 0 1 0 1855037276 57880576 13110 4294967295 134512640 135094434 3221224432 3221220752 134677284 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4592/statm): 14131 13110 145 145 0 13986 0
[pid=4592] vsize: 56524
Current children cumulated CPU time (s) 19.17
Current children cumulated vsize (Kb) 58648

[startup+30.0051 s]
Raw data (loadavg): 0.89 0.94 0.90 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 14988 0 0 0 2835 79 0 0 25 0 1 0 1855037276 57942016 13125 4294967295 134512640 135094434 3221224432 3221220988 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4592/statm): 14146 13125 145 145 0 14001 0
[pid=4592] vsize: 56584
Current children cumulated CPU time (s) 29.15
Current children cumulated vsize (Kb) 58708

[startup+40.0059 s]
Raw data (loadavg): 0.90 0.94 0.90 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 15419 0 0 0 3833 81 0 0 25 0 1 0 1855037276 57966592 13131 4294967295 134512640 135094434 3221224432 3221220928 134676532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4592/statm): 14152 13131 145 145 0 14007 0
[pid=4592] vsize: 56608
Current children cumulated CPU time (s) 39.15
Current children cumulated vsize (Kb) 58732

[startup+50.0066 s]
Raw data (loadavg): 0.92 0.95 0.90 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 15419 0 0 0 4833 81 0 0 25 0 1 0 1855037276 57966592 13131 4294967295 134512640 135094434 3221224432 3221221104 134600175 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4592/statm): 14152 13131 145 145 0 14007 0
[pid=4592] vsize: 56608
Current children cumulated CPU time (s) 49.15
Current children cumulated vsize (Kb) 58732

[startup+60.0074 s]
Raw data (loadavg): 0.93 0.95 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 15701 0 0 0 5832 82 0 0 25 0 1 0 1855037276 59539456 13413 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4592/statm): 14536 13413 145 145 0 14391 0
[pid=4592] vsize: 58144
Current children cumulated CPU time (s) 59.15
Current children cumulated vsize (Kb) 60268

[startup+70.0082 s]
Raw data (loadavg): 0.94 0.95 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 15849 0 0 0 6831 83 0 0 25 0 1 0 1855037276 61112320 13519 4294967295 134512640 135094434 3221224432 3221220832 134676328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4592/statm): 14920 13519 145 145 0 14775 0
[pid=4592] vsize: 59680
Current children cumulated CPU time (s) 69.15
Current children cumulated vsize (Kb) 61804

[startup+80.009 s]
Raw data (loadavg): 0.95 0.95 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 16010 0 0 0 7831 84 0 0 25 0 1 0 1855037276 61308928 13638 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 14968 13638 145 145 0 14823 0
[pid=4592] vsize: 59872
Current children cumulated CPU time (s) 79.16
Current children cumulated vsize (Kb) 61996

[startup+90.0098 s]
Raw data (loadavg): 0.96 0.95 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18294 0 0 0 8821 91 0 0 25 0 1 0 1855037276 66363392 14972 4294967295 134512640 135094434 3221224432 3221222512 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 16202 14972 145 145 0 16057 0
[pid=4592] vsize: 64808
Current children cumulated CPU time (s) 89.13
Current children cumulated vsize (Kb) 66932

[startup+100.011 s]
Raw data (loadavg): 0.96 0.95 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18359 0 0 0 9821 91 0 0 25 0 1 0 1855037276 66363392 15037 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 16202 15037 145 145 0 16057 0
[pid=4592] vsize: 64808
Current children cumulated CPU time (s) 99.13
Current children cumulated vsize (Kb) 66932

[startup+110.011 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18415 0 0 0 10821 91 0 0 25 0 1 0 1855037276 66363392 15093 4294967295 134512640 135094434 3221224432 3221221072 134518677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 16202 15093 145 145 0 16057 0
[pid=4592] vsize: 64808
Current children cumulated CPU time (s) 109.13
Current children cumulated vsize (Kb) 66932

[startup+120.012 s]
Raw data (loadavg): 0.97 0.95 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18468 0 0 0 11821 91 0 0 25 0 1 0 1855037276 66363392 15146 4294967295 134512640 135094434 3221224432 3221220960 134783376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 16202 15146 145 145 0 16057 0
[pid=4592] vsize: 64808
Current children cumulated CPU time (s) 119.13
Current children cumulated vsize (Kb) 66932

[startup+130.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18538 0 0 0 12821 91 0 0 25 0 1 0 1855037276 69509120 15216 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 16970 15216 145 145 0 16825 0
[pid=4592] vsize: 67880
Current children cumulated CPU time (s) 129.13
Current children cumulated vsize (Kb) 70004

[startup+140.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18709 0 0 0 13821 92 0 0 25 0 1 0 1855037276 69509120 15304 4294967295 134512640 135094434 3221224432 3221221888 134676328 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 16970 15304 145 145 0 16825 0
[pid=4592] vsize: 67880
Current children cumulated CPU time (s) 139.14
Current children cumulated vsize (Kb) 70004

[startup+150.014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 18838 0 0 0 14821 92 0 0 25 0 1 0 1855037276 69509120 15350 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 16970 15350 145 145 0 16825 0
[pid=4592] vsize: 67880
Current children cumulated CPU time (s) 149.14
Current children cumulated vsize (Kb) 70004

[startup+160.015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 19663 0 0 0 15816 95 0 0 25 0 1 0 1855037276 70254592 15563 4294967295 134512640 135094434 3221224432 3221220576 134600232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 17152 15563 145 145 0 17007 0
[pid=4592] vsize: 68608
Current children cumulated CPU time (s) 159.12
Current children cumulated vsize (Kb) 70732

[startup+170.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 19663 0 0 0 16816 95 0 0 25 0 1 0 1855037276 70254592 15563 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 17152 15563 145 145 0 17007 0
[pid=4592] vsize: 68608
Current children cumulated CPU time (s) 169.12
Current children cumulated vsize (Kb) 70732

[startup+180.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 20007 0 0 0 17815 95 0 0 25 0 1 0 1855037276 70311936 15585 4294967295 134512640 135094434 3221224432 3221220992 134677086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 17166 15585 145 145 0 17021 0
[pid=4592] vsize: 68664
Current children cumulated CPU time (s) 179.11
Current children cumulated vsize (Kb) 70788

[startup+190.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 20136 0 0 0 18815 96 0 0 25 0 1 0 1855037276 70311936 15589 4294967295 134512640 135094434 3221224432 3221219344 134677239 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 17166 15589 145 145 0 17021 0
[pid=4592] vsize: 68664
Current children cumulated CPU time (s) 189.12
Current children cumulated vsize (Kb) 70788

[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 20261 0 0 0 19815 96 0 0 25 0 1 0 1855037276 70311936 15589 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 17166 15589 145 145 0 17021 0
[pid=4592] vsize: 68664
Current children cumulated CPU time (s) 199.12
Current children cumulated vsize (Kb) 70788

[startup+210.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 21718 0 0 0 20812 99 0 0 25 0 1 0 1855037276 73011200 16262 4294967295 134512640 135094434 3221224432 3221220672 134677065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 17825 16262 145 145 0 17680 0
[pid=4592] vsize: 71300
Current children cumulated CPU time (s) 209.12
Current children cumulated vsize (Kb) 73424

[startup+220.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 22650 0 0 0 21808 102 0 0 25 0 1 0 1855037276 72998912 16287 4294967295 134512640 135094434 3221224432 3221220576 134677284 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 17822 16287 145 145 0 17677 0
[pid=4592] vsize: 71288
Current children cumulated CPU time (s) 219.11
Current children cumulated vsize (Kb) 73412

[startup+230.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 23181 0 0 0 22806 104 0 0 25 0 1 0 1855037276 72912896 16275 4294967295 134512640 135094434 3221224432 3221222864 134600186 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 17801 16275 145 145 0 17656 0
[pid=4592] vsize: 71204
Current children cumulated CPU time (s) 229.11
Current children cumulated vsize (Kb) 73328

[startup+240.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 25941 0 0 0 23790 113 0 0 25 0 1 0 1855037276 72953856 16293 4294967295 134512640 135094434 3221224432 3221220564 134600238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4592/statm): 17811 16293 145 145 0 17666 0
[pid=4592] vsize: 71244
Current children cumulated CPU time (s) 239.04
Current children cumulated vsize (Kb) 73368

[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 27293 0 0 0 24783 117 0 0 25 0 1 0 1855037276 75235328 16860 4294967295 134512640 135094434 3221224432 3221220576 134676586 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 18368 16860 145 145 0 18223 0
[pid=4592] vsize: 73472
Current children cumulated CPU time (s) 249.01
Current children cumulated vsize (Kb) 75596

[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 27818 0 0 0 25781 118 0 0 25 0 1 0 1855037276 75313152 16890 4294967295 134512640 135094434 3221224432 3221220576 134600151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 18387 16890 145 145 0 18242 0
[pid=4592] vsize: 73548
Current children cumulated CPU time (s) 259
Current children cumulated vsize (Kb) 75672

[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 29181 0 0 0 26777 122 0 0 25 0 1 0 1855037276 75313152 16932 4294967295 134512640 135094434 3221224432 3221220220 134600233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4592/statm): 18387 16932 145 145 0 18242 0
[pid=4592] vsize: 73548
Current children cumulated CPU time (s) 269
Current children cumulated vsize (Kb) 75672

[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 29528 0 0 0 27777 123 0 0 25 0 1 0 1855037276 75313152 16948 4294967295 134512640 135094434 3221224432 3221221340 134677378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 18387 16948 145 145 0 18242 0
[pid=4592] vsize: 73548
Current children cumulated CPU time (s) 279.01
Current children cumulated vsize (Kb) 75672

[startup+290.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 30045 0 0 0 28776 124 0 0 25 0 1 0 1855037276 75313152 16969 4294967295 134512640 135094434 3221224432 3221219872 134600269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 18387 16969 145 145 0 18242 0
[pid=4592] vsize: 73548
Current children cumulated CPU time (s) 289.01
Current children cumulated vsize (Kb) 75672

[startup+300.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 30304 0 0 0 29775 125 0 0 25 0 1 0 1855037276 75313152 16980 4294967295 134512640 135094434 3221224432 3221221280 134600267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 18387 16980 145 145 0 18242 0
[pid=4592] vsize: 73548
Current children cumulated CPU time (s) 299.01
Current children cumulated vsize (Kb) 75672

[startup+310.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 30919 0 0 0 30774 126 0 0 25 0 1 0 1855037276 75313152 17015 4294967295 134512640 135094434 3221224432 3221220080 134780815 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 18387 17015 145 145 0 18242 0
[pid=4592] vsize: 73548
Current children cumulated CPU time (s) 309.01
Current children cumulated vsize (Kb) 75672

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 31109 0 0 0 31774 126 0 0 25 0 1 0 1855037276 75313152 17039 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 18387 17039 145 145 0 18242 0
[pid=4592] vsize: 73548
Current children cumulated CPU time (s) 319.01
Current children cumulated vsize (Kb) 75672

[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 31368 0 0 0 32773 127 0 0 25 0 1 0 1855037276 75313152 17132 4294967295 134512640 135094434 3221224432 3221220740 134600238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 18387 17132 145 145 0 18242 0
[pid=4592] vsize: 73548
Current children cumulated CPU time (s) 329.01
Current children cumulated vsize (Kb) 75672

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 31421 0 0 0 33773 127 0 0 25 0 1 0 1855037276 75313152 17185 4294967295 134512640 135094434 3221224432 3221221152 134677233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 18387 17185 145 145 0 18242 0
[pid=4592] vsize: 73548
Current children cumulated CPU time (s) 339.01
Current children cumulated vsize (Kb) 75672

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34003 0 0 0 34761 135 0 0 25 0 1 0 1855037276 79347712 18200 4294967295 134512640 135094434 3221224432 3221220120 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 19372 18200 145 145 0 19227 0
[pid=4592] vsize: 77488
Current children cumulated CPU time (s) 348.97
Current children cumulated vsize (Kb) 79612

[startup+360.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34344 0 0 0 35760 135 0 0 25 0 1 0 1855037276 79347712 18211 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 19372 18211 145 145 0 19227 0
[pid=4592] vsize: 77488
Current children cumulated CPU time (s) 358.96
Current children cumulated vsize (Kb) 79612

[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34677 0 0 0 36760 136 0 0 25 0 1 0 1855037276 79347712 18214 4294967295 134512640 135094434 3221224432 3221219400 134676461 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 19372 18214 145 145 0 19227 0
[pid=4592] vsize: 77488
Current children cumulated CPU time (s) 368.97
Current children cumulated vsize (Kb) 79612

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34691 0 0 0 37760 136 0 0 25 0 1 0 1855037276 79347712 18228 4294967295 134512640 135094434 3221224432 3221220912 134600241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 19372 18228 145 145 0 19227 0
[pid=4592] vsize: 77488
Current children cumulated CPU time (s) 378.97
Current children cumulated vsize (Kb) 79612

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34704 0 0 0 38760 136 0 0 25 0 1 0 1855037276 79347712 18241 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 19372 18241 145 145 0 19227 0
[pid=4592] vsize: 77488
Current children cumulated CPU time (s) 388.97
Current children cumulated vsize (Kb) 79612

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34704 0 0 0 39760 136 0 0 25 0 1 0 1855037276 79347712 18241 4294967295 134512640 135094434 3221224432 3221220560 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 19372 18241 145 145 0 19227 0
[pid=4592] vsize: 77488
Current children cumulated CPU time (s) 398.97
Current children cumulated vsize (Kb) 79612

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34707 0 0 0 40761 136 0 0 25 0 1 0 1855037276 79347712 18244 4294967295 134512640 135094434 3221224432 3221221632 134677340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 19372 18244 145 145 0 19227 0
[pid=4592] vsize: 77488
Current children cumulated CPU time (s) 408.98
Current children cumulated vsize (Kb) 79612

[startup+420.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34710 0 0 0 41761 136 0 0 25 0 1 0 1855037276 79347712 18247 4294967295 134512640 135094434 3221224432 3221220732 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 19372 18247 145 145 0 19227 0
[pid=4592] vsize: 77488
Current children cumulated CPU time (s) 418.98
Current children cumulated vsize (Kb) 79612

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34713 0 0 0 42761 136 0 0 25 0 1 0 1855037276 79347712 18250 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 19372 18250 145 145 0 19227 0
[pid=4592] vsize: 77488
Current children cumulated CPU time (s) 428.98
Current children cumulated vsize (Kb) 79612

[startup+440.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 34738 0 0 0 43761 136 0 0 25 0 1 0 1855037276 79347712 18275 4294967295 134512640 135094434 3221224432 3221221176 134677084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4592/statm): 19372 18275 145 145 0 19227 0
[pid=4592] vsize: 77488
Current children cumulated CPU time (s) 438.98
Current children cumulated vsize (Kb) 79612

[startup+450.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 36601 0 0 0 44753 141 0 0 25 0 1 0 1855037276 81379328 18819 4294967295 134512640 135094434 3221224432 3221219344 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 19868 18819 145 145 0 19723 0
[pid=4592] vsize: 79472
Current children cumulated CPU time (s) 448.95
Current children cumulated vsize (Kb) 81596

[startup+460.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 38303 0 0 0 45749 145 0 0 25 0 1 0 1855037276 81502208 18872 4294967295 134512640 135094434 3221224432 3221221632 134676503 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 19898 18872 145 145 0 19753 0
[pid=4592] vsize: 79592
Current children cumulated CPU time (s) 458.95
Current children cumulated vsize (Kb) 81716

[startup+470.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 39660 0 0 0 46746 148 0 0 25 0 1 0 1855037276 87793664 18909 4294967295 134512640 135094434 3221224432 3221221104 134600301 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21434 18909 145 145 0 21289 0
[pid=4592] vsize: 85736
Current children cumulated CPU time (s) 468.95
Current children cumulated vsize (Kb) 87860

[startup+480.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 40921 0 0 0 47742 152 0 0 25 0 1 0 1855037276 87797760 18920 4294967295 134512640 135094434 3221224432 3221220192 134676245 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21435 18920 145 145 0 21290 0
[pid=4592] vsize: 85740
Current children cumulated CPU time (s) 478.95
Current children cumulated vsize (Kb) 87864

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 40921 0 0 0 48742 152 0 0 25 0 1 0 1855037276 87797760 18920 4294967295 134512640 135094434 3221224432 3221221964 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21435 18920 145 145 0 21290 0
[pid=4592] vsize: 85740
Current children cumulated CPU time (s) 488.95
Current children cumulated vsize (Kb) 87864

[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 42198 0 0 0 49739 155 0 0 25 0 1 0 1855037276 87732224 18915 4294967295 134512640 135094434 3221224432 3221220848 134677056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21419 18915 145 145 0 21274 0
[pid=4592] vsize: 85676
Current children cumulated CPU time (s) 498.95
Current children cumulated vsize (Kb) 87800

[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 42198 0 0 0 50739 155 0 0 25 0 1 0 1855037276 87732224 18915 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21419 18915 145 145 0 21274 0
[pid=4592] vsize: 85676
Current children cumulated CPU time (s) 508.95
Current children cumulated vsize (Kb) 87800

[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 42696 0 0 0 51738 156 0 0 25 0 1 0 1855037276 87732224 18918 4294967295 134512640 135094434 3221224432 3221221104 134676598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21419 18918 145 145 0 21274 0
[pid=4592] vsize: 85676
Current children cumulated CPU time (s) 518.95
Current children cumulated vsize (Kb) 87800

[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 43191 0 0 0 52737 157 0 0 25 0 1 0 1855037276 87732224 18918 4294967295 134512640 135094434 3221224432 3221220144 134676376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21419 18918 145 145 0 21274 0
[pid=4592] vsize: 85676
Current children cumulated CPU time (s) 528.95
Current children cumulated vsize (Kb) 87800

[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 43365 0 0 0 53737 157 0 0 25 0 1 0 1855037276 87732224 18927 4294967295 134512640 135094434 3221224432 3221220752 134677327 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21419 18927 145 145 0 21274 0
[pid=4592] vsize: 85676
Current children cumulated CPU time (s) 538.95
Current children cumulated vsize (Kb) 87800

[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 44060 0 0 0 54735 159 0 0 25 0 1 0 1855037276 87732224 18962 4294967295 134512640 135094434 3221224432 3221220320 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21419 18962 145 145 0 21274 0
[pid=4592] vsize: 85676
Current children cumulated CPU time (s) 548.95
Current children cumulated vsize (Kb) 87800

[startup+560.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 44078 0 0 0 55735 159 0 0 25 0 1 0 1855037276 87732224 18980 4294967295 134512640 135094434 3221224432 3221221260 134677150 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21419 18980 145 145 0 21274 0
[pid=4592] vsize: 85676
Current children cumulated CPU time (s) 558.95
Current children cumulated vsize (Kb) 87800

[startup+570.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 44090 0 0 0 56736 159 0 0 25 0 1 0 1855037276 87732224 18992 4294967295 134512640 135094434 3221224432 3221221012 134677077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21419 18992 145 145 0 21274 0
[pid=4592] vsize: 85676
Current children cumulated CPU time (s) 568.96
Current children cumulated vsize (Kb) 87800

[startup+580.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 44101 0 0 0 57736 159 0 0 25 0 1 0 1855037276 87732224 19003 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21419 19003 145 145 0 21274 0
[pid=4592] vsize: 85676
Current children cumulated CPU time (s) 578.96
Current children cumulated vsize (Kb) 87800

[startup+590.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 44137 0 0 0 58736 159 0 0 25 0 1 0 1855037276 87732224 19039 4294967295 134512640 135094434 3221224432 3221220928 134676510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 21419 19039 145 145 0 21274 0
[pid=4592] vsize: 85676
Current children cumulated CPU time (s) 588.96
Current children cumulated vsize (Kb) 87800

[startup+600.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) T 4588 4588 19818 0 -1 0 45328 0 0 0 59733 162 0 0 25 0 1 0 1855037276 90431488 19735 4294967295 134512640 135094434 3221224432 3221209308 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/4592/statm): 22078 19735 145 145 0 21933 0
[pid=4592] vsize: 88312
Current children cumulated CPU time (s) 598.96
Current children cumulated vsize (Kb) 90436

[startup+610.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 69602 0 0 0 60599 241 0 0 25 0 1 0 1855037276 122236928 27506 4294967295 134512640 135094434 3221224432 3221221456 134599950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4592/statm): 29843 27506 145 145 0 29698 0
[pid=4592] vsize: 119372
Current children cumulated CPU time (s) 608.41
Current children cumulated vsize (Kb) 121496

[startup+620.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 69687 0 0 0 61599 241 0 0 25 0 1 0 1855037276 122236928 27591 4294967295 134512640 135094434 3221224432 3221221376 134519050 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 29843 27591 145 145 0 29698 0
[pid=4592] vsize: 119372
Current children cumulated CPU time (s) 618.41
Current children cumulated vsize (Kb) 121496

[startup+630.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 69771 0 0 0 62599 241 0 0 25 0 1 0 1855037276 122236928 27675 4294967295 134512640 135094434 3221224432 3221220032 134600241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 29843 27675 145 145 0 29698 0
[pid=4592] vsize: 119372
Current children cumulated CPU time (s) 628.41
Current children cumulated vsize (Kb) 121496

[startup+640.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 69808 0 0 0 63599 241 0 0 25 0 1 0 1855037276 122236928 27712 4294967295 134512640 135094434 3221224432 3221220636 134677228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 29843 27712 145 145 0 29698 0
[pid=4592] vsize: 119372
Current children cumulated CPU time (s) 638.41
Current children cumulated vsize (Kb) 121496

[startup+650.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72524 0 0 0 64592 248 0 0 25 0 1 0 1855037276 127639552 29110 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29110 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 648.41
Current children cumulated vsize (Kb) 126772

[startup+660.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72605 0 0 0 65593 248 0 0 25 0 1 0 1855037276 127639552 29191 4294967295 134512640 135094434 3221224432 3221220672 134677138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29191 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 658.42
Current children cumulated vsize (Kb) 126772

[startup+670.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72625 0 0 0 66593 248 0 0 25 0 1 0 1855037276 127639552 29211 4294967295 134512640 135094434 3221224432 3221220024 134676989 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29211 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 668.42
Current children cumulated vsize (Kb) 126772

[startup+680.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72636 0 0 0 67593 248 0 0 25 0 1 0 1855037276 127639552 29222 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29222 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 678.42
Current children cumulated vsize (Kb) 126772

[startup+690.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72664 0 0 0 68593 249 0 0 25 0 1 0 1855037276 127639552 29250 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29250 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 688.43
Current children cumulated vsize (Kb) 126772

[startup+700.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72689 0 0 0 69593 249 0 0 25 0 1 0 1855037276 127639552 29275 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29275 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 698.43
Current children cumulated vsize (Kb) 126772

[startup+710.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72724 0 0 0 70593 249 0 0 25 0 1 0 1855037276 127639552 29310 4294967295 134512640 135094434 3221224432 3221221104 134600151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29310 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 708.43
Current children cumulated vsize (Kb) 126772

[startup+720.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72764 0 0 0 71593 249 0 0 25 0 1 0 1855037276 127639552 29350 4294967295 134512640 135094434 3221224432 3221221600 134518676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29350 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 718.43
Current children cumulated vsize (Kb) 126772

[startup+730.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72794 0 0 0 72593 249 0 0 25 0 1 0 1855037276 127639552 29380 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29380 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 728.43
Current children cumulated vsize (Kb) 126772

[startup+740.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72818 0 0 0 73594 249 0 0 25 0 1 0 1855037276 127639552 29404 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29404 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 738.44
Current children cumulated vsize (Kb) 126772

[startup+750.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72850 0 0 0 74594 249 0 0 25 0 1 0 1855037276 127639552 29436 4294967295 134512640 135094434 3221224432 3221220576 134600215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29436 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 748.44
Current children cumulated vsize (Kb) 126772

[startup+760.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72913 0 0 0 75594 249 0 0 25 0 1 0 1855037276 127639552 29499 4294967295 134512640 135094434 3221224432 3221218288 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29499 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 758.44
Current children cumulated vsize (Kb) 126772

[startup+770.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 72969 0 0 0 76594 249 0 0 25 0 1 0 1855037276 127639552 29555 4294967295 134512640 135094434 3221224432 3221220672 134676321 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29555 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 768.44
Current children cumulated vsize (Kb) 126772

[startup+780.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73027 0 0 0 77594 250 0 0 25 0 1 0 1855037276 127639552 29613 4294967295 134512640 135094434 3221224432 3221220736 134600162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29613 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 778.45
Current children cumulated vsize (Kb) 126772

[startup+790.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73132 0 0 0 78594 250 0 0 25 0 1 0 1855037276 127639552 29718 4294967295 134512640 135094434 3221224432 3221221456 134677366 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29718 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 788.45
Current children cumulated vsize (Kb) 126772

[startup+800.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73193 0 0 0 79594 250 0 0 25 0 1 0 1855037276 127639552 29779 4294967295 134512640 135094434 3221224432 3221221000 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29779 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 798.45
Current children cumulated vsize (Kb) 126772

[startup+810.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73221 0 0 0 80594 250 0 0 25 0 1 0 1855037276 127639552 29807 4294967295 134512640 135094434 3221224432 3221220472 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29807 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 808.45
Current children cumulated vsize (Kb) 126772

[startup+820.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73221 0 0 0 81594 250 0 0 25 0 1 0 1855037276 127639552 29807 4294967295 134512640 135094434 3221224432 3221220652 134676331 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29807 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 818.45
Current children cumulated vsize (Kb) 126772

[startup+830.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73221 0 0 0 82595 250 0 0 25 0 1 0 1855037276 127639552 29807 4294967295 134512640 135094434 3221224432 3221221952 134676245 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29807 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 828.46
Current children cumulated vsize (Kb) 126772

[startup+840.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73221 0 0 0 83595 250 0 0 25 0 1 0 1855037276 127639552 29807 4294967295 134512640 135094434 3221224432 3221222160 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29807 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 838.46
Current children cumulated vsize (Kb) 126772

[startup+850.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73249 0 0 0 84595 250 0 0 25 0 1 0 1855037276 127639552 29835 4294967295 134512640 135094434 3221224432 3221220048 134677354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29835 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 848.46
Current children cumulated vsize (Kb) 126772

[startup+860.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73249 0 0 0 85595 250 0 0 25 0 1 0 1855037276 127639552 29835 4294967295 134512640 135094434 3221224432 3221220672 134676999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29835 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 858.46
Current children cumulated vsize (Kb) 126772

[startup+870.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73249 0 0 0 86596 250 0 0 25 0 1 0 1855037276 127639552 29835 4294967295 134512640 135094434 3221224432 3221221200 134677021 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29835 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 868.47
Current children cumulated vsize (Kb) 126772

[startup+880.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73254 0 0 0 87596 250 0 0 25 0 1 0 1855037276 127639552 29840 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29840 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 878.47
Current children cumulated vsize (Kb) 126772

[startup+890.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73254 0 0 0 88596 250 0 0 25 0 1 0 1855037276 127639552 29840 4294967295 134512640 135094434 3221224432 3221220320 134676273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29840 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 888.47
Current children cumulated vsize (Kb) 126772

[startup+900.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73254 0 0 0 89596 250 0 0 25 0 1 0 1855037276 127639552 29840 4294967295 134512640 135094434 3221224432 3221221088 134600246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29840 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 898.47
Current children cumulated vsize (Kb) 126772

[startup+910.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73254 0 0 0 90597 250 0 0 25 0 1 0 1855037276 127639552 29840 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29840 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 908.48
Current children cumulated vsize (Kb) 126772

[startup+920.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73259 0 0 0 91597 250 0 0 25 0 1 0 1855037276 127639552 29845 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29845 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 918.48
Current children cumulated vsize (Kb) 126772

[startup+930.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73293 0 0 0 92597 250 0 0 25 0 1 0 1855037276 127639552 29879 4294967295 134512640 135094434 3221224432 3221221808 134600267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29879 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 928.48
Current children cumulated vsize (Kb) 126772

[startup+940.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73314 0 0 0 93597 250 0 0 25 0 1 0 1855037276 127639552 29900 4294967295 134512640 135094434 3221224432 3221220144 134677065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29900 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 938.48
Current children cumulated vsize (Kb) 126772

[startup+950.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73314 0 0 0 94598 250 0 0 25 0 1 0 1855037276 127639552 29900 4294967295 134512640 135094434 3221224432 3221221808 134600232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29900 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 948.49
Current children cumulated vsize (Kb) 126772

[startup+960.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 95598 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221220556 134676988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 958.49
Current children cumulated vsize (Kb) 126772

[startup+970.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 96598 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221219616 134677059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 968.49
Current children cumulated vsize (Kb) 126772

[startup+980.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 97598 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221221808 134677248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 978.49
Current children cumulated vsize (Kb) 126772

[startup+990.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 98599 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221219968 134676273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 988.5
Current children cumulated vsize (Kb) 126772

[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 99599 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 998.5
Current children cumulated vsize (Kb) 126772

[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 100599 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221221924 134784900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 1008.5
Current children cumulated vsize (Kb) 126772

[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73319 0 0 0 101599 250 0 0 25 0 1 0 1855037276 127639552 29905 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29905 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 1018.5
Current children cumulated vsize (Kb) 126772

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73321 0 0 0 102600 250 0 0 25 0 1 0 1855037276 127639552 29907 4294967295 134512640 135094434 3221224432 3221220288 134676336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29907 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 1028.51
Current children cumulated vsize (Kb) 126772

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73321 0 0 0 103600 250 0 0 25 0 1 0 1855037276 127639552 29907 4294967295 134512640 135094434 3221224432 3221221632 134600232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29907 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 1038.51
Current children cumulated vsize (Kb) 126772

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73348 0 0 0 104600 250 0 0 25 0 1 0 1855037276 127639552 29934 4294967295 134512640 135094434 3221224432 3221221280 134676471 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29934 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 1048.51
Current children cumulated vsize (Kb) 126772

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73385 0 0 0 105600 250 0 0 25 0 1 0 1855037276 127639552 29971 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 29971 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 1058.51
Current children cumulated vsize (Kb) 126772

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73460 0 0 0 106600 250 0 0 25 0 1 0 1855037276 127639552 30046 4294967295 134512640 135094434 3221224432 3221220108 134676460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 30046 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 1068.51
Current children cumulated vsize (Kb) 126772

[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73549 0 0 0 107601 250 0 0 25 0 1 0 1855037276 127639552 30135 4294967295 134512640 135094434 3221224432 3221221096 134600234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 31162 30135 145 145 0 31017 0
[pid=4592] vsize: 124648
Current children cumulated CPU time (s) 1078.52
Current children cumulated vsize (Kb) 126772

[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73595 0 0 0 108599 251 0 0 25 0 1 0 1855037276 140222464 30181 4294967295 134512640 135094434 3221224432 3221220752 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/4592/statm): 34234 30181 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1088.51
Current children cumulated vsize (Kb) 139060

[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73632 0 0 0 109598 252 0 0 25 0 1 0 1855037276 140222464 30218 4294967295 134512640 135094434 3221224432 3221222336 134677300 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30218 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1098.51
Current children cumulated vsize (Kb) 139060

[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73726 0 0 0 110598 252 0 0 25 0 1 0 1855037276 140222464 30312 4294967295 134512640 135094434 3221224432 3221221080 134600694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30312 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1108.51
Current children cumulated vsize (Kb) 139060

[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73801 0 0 0 111598 253 0 0 25 0 1 0 1855037276 140222464 30387 4294967295 134512640 135094434 3221224432 3221220848 134677035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30387 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1118.52
Current children cumulated vsize (Kb) 139060

[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 73835 0 0 0 112598 253 0 0 25 0 1 0 1855037276 140222464 30421 4294967295 134512640 135094434 3221224432 3221221256 134677149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30421 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1128.52
Current children cumulated vsize (Kb) 139060

[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74002 0 0 0 113598 253 0 0 25 0 1 0 1855037276 140222464 30588 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30588 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1138.52
Current children cumulated vsize (Kb) 139060

[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74065 0 0 0 114597 254 0 0 25 0 1 0 1855037276 140222464 30651 4294967295 134512640 135094434 3221224432 3221220752 134677248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30651 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1148.52
Current children cumulated vsize (Kb) 139060

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74081 0 0 0 115598 254 0 0 25 0 1 0 1855037276 140222464 30667 4294967295 134512640 135094434 3221224432 3221222512 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30667 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1158.53
Current children cumulated vsize (Kb) 139060

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74125 0 0 0 116598 254 0 0 25 0 1 0 1855037276 140222464 30711 4294967295 134512640 135094434 3221224432 3221220648 134676334 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30711 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1168.53
Current children cumulated vsize (Kb) 139060

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74141 0 0 0 117598 254 0 0 25 0 1 0 1855037276 140222464 30727 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30727 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1178.53
Current children cumulated vsize (Kb) 139060

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74167 0 0 0 118598 254 0 0 25 0 1 0 1855037276 140222464 30753 4294967295 134512640 135094434 3221224432 3221221072 134518662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30753 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1188.53
Current children cumulated vsize (Kb) 139060

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74223 0 0 0 119599 254 0 0 25 0 1 0 1855037276 140222464 30809 4294967295 134512640 135094434 3221224432 3221221104 134676552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30809 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1198.54
Current children cumulated vsize (Kb) 139060

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74273 0 0 0 120599 254 0 0 25 0 1 0 1855037276 140222464 30859 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30859 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1208.54
Current children cumulated vsize (Kb) 139060



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 4592
Raw data (/proc/4588/stat): 4588 (minisat+_script) S 4587 4588 19818 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1855037271 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/4588/statm): 531 226 485 147 0 384 0
[pid=4588] vsize: 2124
Raw data (/proc/4592/stat): 4592 (minisat+_64-bit) R 4588 4588 19818 0 -1 0 74273 0 0 0 120599 254 0 0 25 0 1 0 1855037276 140222464 30859 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/4592/statm): 34234 30859 145 145 0 34089 0
[pid=4592] vsize: 136936
Current children cumulated CPU time (s) 1208.54
Current children cumulated vsize (Kb) 139060

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1208.6
CPU user time (s): 1205.99
CPU system time (s): 2.6076
CPU usage (%): 99.8712
Max. virtual memory (cumulated for all children) (Kb): 139060

Verifier Data

ERROR: no interpretation found !