Some explanations

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

General information on the benchmark

Namemps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-greenbeb.opb
MD5SUM376d4643e7856d57cc9cab321f965d04
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 14882
Biggest coefficient in the objective function 536870912000000
Number of bits for the biggest coefficient in the objective function 49
Sum of the numbers in the objective function 12491747892670016
Number of bits of the sum of numbers in the objective function 54
Biggest number in a constraint 536870912000000
Number of bits of the biggest number in a constraint 49
Biggest sum of numbers in a constraint 24454743822989865
Number of bits of the biggest sum of numbers55
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables155020
Total number of constraints2676
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 constraints2676
Minimum length of a constraint11
Maximum length of a constraint7172

Trace number 2645

Launcher Data

LAUNCH ON wulflinc12 THE 2005-09-18 20:18:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2780 boxname=wulflinc12 idbench=436 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  376d4643e7856d57cc9cab321f965d04  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-greenbeb.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-greenbeb.opb
IDLAUNCH: 2780
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        869864 kB
Buffers:         38764 kB
Cached:          85404 kB
SwapCached:        544 kB
Active:          93244 kB
Inactive:        43152 kB
HighTotal:      131008 kB
HighFree:        45556 kB
LowTotal:       903652 kB
LowFree:        824308 kB
SwapTotal:     2097136 kB
SwapFree:      2096072 kB
Dirty:              44 kB
Writeback:           0 kB
Mapped:           5884 kB
Slab:            22780 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 20:38:43 (client local time) WITH STATUS 0 IN 1207.72 SECONDS
stats: 2780 7 1207.72 0

Solver Data

c Parsing PB file...
c PARSE ERROR! [line 5409] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 4201 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[4250]---> BDD-cost:   20
c ---[4245]---> BDD-cost:   18
c ---[4244]---> BDD-cost:   17
c ---[4243]---> BDD-cost:   21
c ---[4242]---> BDD-cost:   18
c ---[4240]---> BDD-cost:   17
c ---[4239]---> BDD-cost:   19
c ---[4238]---> BDD-cost:   16
c ---[4237]---> BDD-cost:   16
c ---[4233]---> BDD-cost:   16
c ---[4231]---> BDD-cost:   13
c ---[4230]---> BDD-cost:   15
c ---[4229]---> BDD-cost:   11
c ---[4228]---> BDD-cost:   15
c ---[4227]---> BDD-cost:   15
c ---[4226]---> BDD-cost:   12
c ---[4224]---> BDD-cost:   16
c ---[4221]---> BDD-cost:   18
c ---[4218]---> BDD-cost:   12
c ---[4217]---> BDD-cost:   19
c ---[4216]---> BDD-cost:   15
c ---[4215]---> BDD-cost:   16
c ---[4214]---> BDD-cost:   17
c ---[4213]---> BDD-cost:   15
c ---[4212]---> BDD-cost:   18
c ---[4211]---> BDD-cost:   15
c ---[4209]---> BDD-cost:   12
c ---[4207]---> BDD-cost:   15
c ---[4206]---> BDD-cost:   14
c ---[4205]---> BDD-cost:   14
c ---[4204]---> BDD-cost:   15
c ---[4203]---> BDD-cost:   17
c ---[4200]---> BDD-cost:   22
c ---[4199]---> BDD-cost:   15
c ---[4198]---> BDD-cost:   19
c ---[4196]---> BDD-cost:   19
c ---[4195]---> BDD-cost:   13
c ---[4194]---> BDD-cost:   20
c ---[4193]---> BDD-cost:   17
c ---[4192]---> BDD-cost:   17
c ---[4190]---> BDD-cost:   20
c ---[4189]---> BDD-cost:   18
c ---[4188]---> BDD-cost:   19
c ---[4187]---> BDD-cost:   17
c ---[4186]---> BDD-cost:   16
c ---[4185]---> BDD-cost:   10
c ---[4184]---> BDD-cost:   14
c ---[4182]---> BDD-cost:   10
c ---[4181]---> BDD-cost:   16
c ---[4180]---> BDD-cost:   15
c ---[4179]---> BDD-cost:   12
c ---[4177]---> BDD-cost:   16
c ---[4176]---> BDD-cost:   15
c ---[4175]---> BDD-cost:   18
c ---[4174]---> BDD-cost:   20
c ---[4173]---> BDD-cost:   23
c ---[4172]---> BDD-cost:   17
c ---[4171]---> BDD-cost:   16
c ---[4170]---> BDD-cost:   20
c ---[4168]---> BDD-cost:   12
c ---[4167]---> BDD-cost:   20
c ---[4166]---> BDD-cost:   14
c ---[4165]---> BDD-cost:   21
c ---[4164]---> BDD-cost:   18
c ---[4162]---> BDD-cost:   19
c ---[4161]---> BDD-cost:   19
c ---[4160]---> BDD-cost:   18
c ---[4159]---> BDD-cost:   20
c ---[4156]---> BDD-cost:   10
c ---[4155]---> BDD-cost:   14
c ---[4153]---> BDD-cost:   10
c ---[4152]---> BDD-cost:   17
c ---[4151]---> BDD-cost:   16
c ---[4150]---> BDD-cost:   11
c ---[4149]---> BDD-cost:   16
c ---[4148]---> BDD-cost:   17
c ---[4147]---> BDD-cost:   16
c ---[4146]---> BDD-cost:   17
c ---[4145]---> BDD-cost:   16
c ---[4144]---> BDD-cost:   17
c ---[4143]---> BDD-cost:   18
c ---[4142]---> BDD-cost:   22
c ---[4141]---> BDD-cost:   19
c ---[4140]---> BDD-cost:   19
c ---[4138]---> BDD-cost:   18
c ---[4137]---> BDD-cost:   20
c ---[4136]---> BDD-cost:   16
c ---[4135]---> BDD-cost:   19
c ---[4134]---> BDD-cost:   19
c ---[4133]---> BDD-cost:   19
c ---[4132]---> BDD-cost:   18
c ---[4131]---> BDD-cost:   19
c ---[4129]---> BDD-cost:   18
c ---[4128]---> BDD-cost:   19
c ---[4126]---> BDD-cost:   15
c ---[4125]---> BDD-cost:   19
c ---[4124]---> BDD-cost:   18
c ---[4123]---> BDD-cost:   16
c ---[4122]---> BDD-cost:   15
c ---[4121]---> BDD-cost:   14
c ---[4120]---> BDD-cost:   14
c ---[4119]---> BDD-cost:   15
c ---[4118]---> BDD-cost:   14
c ---[4117]---> BDD-cost:   15
c ---[4116]---> BDD-cost:   14
c ---[4115]---> BDD-cost:   15
c ---[4114]---> BDD-cost:   14
c ---[4113]---> BDD-cost:   14
c ---[4112]---> BDD-cost:   15
c ---[4111]---> BDD-cost:   15
c ---[4109]---> BDD-cost:   21
c ---[4106]---> BDD-cost:   17
c ---[4105]---> BDD-cost:   18
c ---[4102]---> BDD-cost:   19
c ---[4101]---> BDD-cost:   16
c ---[4100]---> BDD-cost:   18
c ---[4099]---> BDD-cost:   19
c ---[4098]---> BDD-cost:   20
c ---[4096]---> BDD-cost:   16
c ---[4095]---> BDD-cost:   15
c ---[4093]---> BDD-cost:   13
c ---[4092]---> BDD-cost:   15
c ---[4090]---> BDD-cost:   14
c ---[4088]---> BDD-cost:   15
c ---[4087]---> BDD-cost:   17
c ---[4086]---> BDD-cost:   16
c ---[4083]---> BDD-cost:   15
c ---[4082]---> BDD-cost:   12
c ---[4078]---> BDD-cost:   13
c ---[4073]---> BDD-cost:   15
c ---[4072]---> BDD-cost:   19
c ---[4071]---> BDD-cost:   20
c ---[4070]---> BDD-cost:   17
c ---[4068]---> BDD-cost:   16
c ---[4067]---> BDD-cost:   18
c ---[4066]---> BDD-cost:   19
c ---[4065]---> BDD-cost:   13
c ---[4064]---> BDD-cost:   20
c ---[4062]---> BDD-cost:   19
c ---[4061]---> BDD-cost:   19
c ---[4059]---> BDD-cost:   16
c ---[4058]---> BDD-cost:   21
c ---[4057]---> BDD-cost:   17
c ---[4056]---> BDD-cost:   15
c ---[4055]---> BDD-cost:   15
c ---[4054]---> BDD-cost:   16
c ---[4053]---> BDD-cost:   10
c ---[4051]---> BDD-cost:   16
c ---[4050]---> BDD-cost:   12
c ---[4049]---> BDD-cost:   12
c ---[4048]---> BDD-cost:   16
c ---[4047]---> BDD-cost:   15
c ---[4046]---> BDD-cost:   20
c ---[4045]---> BDD-cost:   17
c ---[4044]---> BDD-cost:   14
c ---[4042]---> BDD-cost:   18
c ---[4041]---> BDD-cost:   22
c ---[4040]---> BDD-cost:   23
c ---[4038]---> BDD-cost:   18
c ---[4037]---> BDD-cost:   19
c ---[4036]---> BDD-cost:   21
c ---[4034]---> BDD-cost:   21
c ---[4033]---> BDD-cost:   16
c ---[4031]---> BDD-cost:   21
c ---[4030]---> BDD-cost:   18
c ---[4028]---> BDD-cost:   18
c ---[4027]---> BDD-cost:   18
c ---[4025]---> BDD-cost:   20
c ---[4024]---> BDD-cost:   17
c ---[4023]---> BDD-cost:   16
c ---[4021]---> BDD-cost:   10
c ---[4020]---> BDD-cost:   18
c ---[4019]---> BDD-cost:   16
c ---[4018]---> BDD-cost:   15
c ---[4017]---> BDD-cost:   15
c ---[4016]---> BDD-cost:   17
c ---[4015]---> BDD-cost:   15
c ---[4014]---> BDD-cost:   22
c ---[4013]---> BDD-cost:   20
c ---[4010]---> BDD-cost:   19
c ---[4009]---> BDD-cost:   21
c ---[4008]---> BDD-cost:   17
c ---[4007]---> BDD-cost:   18
c ---[4006]---> BDD-cost:   18
c ---[4005]---> BDD-cost:   19
c ---[4003]---> BDD-cost:   19
c ---[4001]---> BDD-cost:   18
c ---[4000]---> BDD-cost:   18
c ---[3997]---> BDD-cost:   16
c ---[3996]---> BDD-cost:   20
c ---[3994]---> BDD-cost:   14
c ---[3993]---> BDD-cost:   15
c ---[3992]---> BDD-cost:   13
c ---[3991]---> BDD-cost:   10
c ---[3990]---> BDD-cost:   16
c ---[3989]---> BDD-cost:   14
c ---[3988]---> BDD-cost:   10
c ---[3987]---> BDD-cost:   12
c ---[3986]---> BDD-cost:   15
c ---[3985]---> BDD-cost:   15
c ---[3982]---> BDD-cost:   14
c ---[3980]---> BDD-cost:   16
c ---[3979]---> BDD-cost:   20
c ---[3978]---> BDD-cost:   16
c ---[3976]---> BDD-cost:   14
c ---[3975]---> BDD-cost:   18
c ---[3974]---> BDD-cost:   16
c ---[3973]---> BDD-cost:   14
c ---[3972]---> BDD-cost:   10
c ---[3971]---> BDD-cost:   11
c ---[3970]---> BDD-cost:   16
c ---[3969]---> BDD-cost:   17
c ---[3968]---> BDD-cost:   14
c ---[3965]---> BDD-cost:   13
c ---[3964]---> BDD-cost:   11
c ---[3962]---> BDD-cost:   16
c ---[3960]---> BDD-cost:   19
c ---[3958]---> Sorter-cost: 2385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3956]---> Adder-cost: 657   maxlim: 1480704   bits: 22/21
c ---[3954]---> Adder-cost: 1205   maxlim: 1075380223   bits: 32/31
c ---[3952]---> Adder-cost: 657   maxlim: 1157120   bits: 22/21
c ---[3950]---> Adder-cost: 354   maxlim: 617472   bits: 21/20
c ---[3948]---> Adder-cost: 625   maxlim: 665600   bits: 21/20
c ---[3946]---> Sorter-cost: 3621     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3944]---> Sorter-cost: 2519     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3942]---> Adder-cost: 336   maxlim: 414720   bits: 20/19
c ---[3940]---> Adder-cost: 354   maxlim: 566272   bits: 21/20
c ---[3938]---> BDD-cost:  205
c ---[3936]---> Adder-cost: 336   maxlim: 513024   bits: 20/19
c ---[3934]---> Sorter-cost:  419     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3932]---> BDD-cost:   80
c ---[3930]---> Adder-cost: 336   maxlim: 488448   bits: 20/19
c ---[3928]---> Adder-cost: 689   maxlim: 3509248   bits: 23/22
c ---[3926]---> Adder-cost: 689   maxlim: 2531328   bits: 23/22
c ---[3924]---> BDD-cost:   70
c ---[3922]---> Sorter-cost: 1823     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3920]---> Adder-cost: 657   maxlim: 1408000   bits: 22/21
c ---[3918]---> Sorter-cost: 1215     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3916]---> Adder-cost: 657   maxlim: 1760256   bits: 22/21
c ---[3912]---> Sorter-cost: 3570     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3910]---> Adder-cost: 372   maxlim: 1319936   bits: 22/21
c ---[3908]---> Sorter-cost: 3593     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3906]---> Adder-cost: 354   maxlim: 870400   bits: 21/20
c ---[3904]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3902]---> Adder-cost: 447   maxlim: 481280   bits: 20/19
c ---[3900]---> BDD-cost:   90
c ---[3898]---> Adder-cost: 354   maxlim: 1003520   bits: 21/20
c ---[3896]---> Sorter-cost: 1282     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3894]---> Sorter-cost: 1649     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3892]---> Sorter-cost: 2520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3890]---> BDD-cost:   90
c ---[3888]---> Sorter-cost: 2170     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3886]---> Sorter-cost: 2171     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3884]---> BDD-cost:  201
c ---[3882]---> BDD-cost:   70
c ---[3880]---> BDD-cost:   70
c ---[3878]---> Adder-cost: 353   maxlim: 222208   bits: 19/18
c ---[3876]---> BDD-cost:  314
c ---[3874]---> BDD-cost:  314
c ---[3864]---> BDD-cost:  167
c ---[3862]---> BDD-cost:  568
c ---[3860]---> BDD-cost:  314
c ---[3858]---> BDD-cost:   90
c ---[3856]---> BDD-cost:   90
c ---[3854]---> BDD-cost:   50
c ---[3852]---> BDD-cost:   50
c ---[3842]---> BDD-cost:  167
c ---[3840]---> BDD-cost:  568
c ---[3838]---> BDD-cost:  314
c ---[3830]---> Sorter-cost: 2367     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 2
c ---[3828]---> Adder-cost: 622   maxlim: 60129542032   bits: 37/36
c ---[3826]---> Adder-cost: 628   maxlim: 60129542032   bits: 37/36
c ---[3824]---> Adder-cost: 634   maxlim: 60129542032   bits: 37/36
c ---[3822]---> Adder-cost: 566   maxlim: 3758096272   bits: 33/32
c ---[3818]---> Sorter-cost: 3652     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[3810]---> Sorter-cost: 3618     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 7 2 2 2
c ---[3808]---> Sorter-cost: 5337     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3806]---> Sorter-cost: 5367     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3804]---> Sorter-cost: 5321     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 ---[3802]---> Sorter-cost: 5321     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 ---[3798]---> Sorter-cost: 4580     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2
c ---[3790]---> Sorter-cost: 1797     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 2
c ---[3788]---> Sorter-cost: 3584     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3786]---> Sorter-cost: 3614     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3784]---> Sorter-cost: 3566     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3782]---> Sorter-cost: 3566     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3778]---> Sorter-cost: 2092     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2
c ---[3770]---> Sorter-cost: 3540     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 5 7 2 2 2
c ---[3768]---> Sorter-cost: 6245     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2
c ---[3766]---> Sorter-cost: 6275     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2
c ---[3764]---> Sorter-cost: 6227     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2
c ---[3762]---> Sorter-cost: 6227     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2
c ---[3758]---> Sorter-cost: 4911     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 5 2 7 2 2
c ---[3750]---> Sorter-cost: 3618     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 7 2 2 2
c ---[3748]---> Sorter-cost: 4987     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3746]---> Sorter-cost: 5017     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3744]---> Sorter-cost: 4969     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3742]---> Sorter-cost: 4969     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3738]---> Sorter-cost: 4174     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2
c ---[3728]---> BDD-cost:  461
c ---[3726]---> BDD-cost:  461
c ---[3722]---> Sorter-cost: 2284     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 2 2
c ---[3720]---> Sorter-cost: 3952     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3718]---> Sorter-cost: 3982     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3716]---> Sorter-cost: 3936     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3714]---> Sorter-cost: 3936     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3710]---> Sorter-cost: 2698     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 7 2 2
c ---[3702]---> Sorter-cost: 3222     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2 2
c ---[3700]---> Sorter-cost: 8280     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 2 2 2 2 2 2 7

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/26053/stat): 26053 (minisat+_script) R 26052 26053 8263 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785837613 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/26053/statm): 174 3 169 147 0 27 0
[pid=26053] 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=26054
New process pid=26055
New process pid=26056
execve syscall for /bin/sed executable
One traced child (pid=26055) 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=26056) exited with status: 0
One traced child (pid=26054) exited with status: 0
New process pid=26057
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-greenbeb.opb
One traced child (pid=26057) exited with status: 5
open syscall for file /oldhome/oroussel/solvers/
New process pid=26058
execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-greenbeb.opb

[startup+10.0041 s]
Raw data (loadavg): 1.01 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) T 26053 26053 8263 0 -1 0 5214 0 3 0 927 25 0 0 25 0 1 0 1785837621 23777280 4898 4294967295 134512640 135167914 3221224448 3221223288 134865821 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26058/statm): 5805 4898 162 162 0 5643 0
[pid=26058] vsize: 23220
Current children cumulated CPU time (s) 9.55
Current children cumulated vsize (Kb) 25348

[startup+20.0059 s]
Raw data (loadavg): 1.01 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 8090 0 3 0 1885 47 0 0 25 0 1 0 1785837621 34279424 7774 4294967295 134512640 135167914 3221224448 3221222300 134581245 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26058/statm): 8369 7774 162 162 0 8207 0
[pid=26058] vsize: 33476
Current children cumulated CPU time (s) 19.35
Current children cumulated vsize (Kb) 35604

[startup+30.0068 s]
Raw data (loadavg): 1.01 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 10779 0 3 0 2851 64 0 0 25 0 1 0 1785837621 44052480 10463 4294967295 134512640 135167914 3221224448 3221222780 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 10755 10463 162 162 0 10593 0
[pid=26058] vsize: 43020
Current children cumulated CPU time (s) 29.18
Current children cumulated vsize (Kb) 45148

[startup+40.0076 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) T 26053 26053 8263 0 -1 0 13357 0 3 0 3819 79 0 0 25 0 1 0 1785837621 62459904 13009 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26058/statm): 15249 13009 162 162 0 15087 0
[pid=26058] vsize: 60996
Current children cumulated CPU time (s) 39.01
Current children cumulated vsize (Kb) 63124

[startup+50.0084 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 15683 0 3 0 4783 95 0 0 22 0 1 0 1785837621 71675904 15335 4294967295 134512640 135167914 3221224448 3221222780 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 17499 15335 162 162 0 17337 0
[pid=26058] vsize: 69996
Current children cumulated CPU time (s) 48.81
Current children cumulated vsize (Kb) 72124

[startup+60.0093 s]
Raw data (loadavg): 1.00 0.97 0.91 1/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) T 26053 26053 8263 0 -1 0 17948 0 3 0 5746 111 0 0 25 0 1 0 1785837621 80605184 17567 4294967295 134512640 135167914 3221224448 3221222524 134934490 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26058/statm): 19679 17567 162 162 0 19517 0
[pid=26058] vsize: 78716
Current children cumulated CPU time (s) 58.6
Current children cumulated vsize (Kb) 80844

[startup+70.0101 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 19936 0 3 0 6705 130 0 0 25 0 1 0 1785837621 87855104 19346 4294967295 134512640 135167914 3221224448 3221222784 134694450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 21449 19346 162 162 0 21287 0
[pid=26058] vsize: 85796
Current children cumulated CPU time (s) 68.38
Current children cumulated vsize (Kb) 87924

[startup+80.0109 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) T 26053 26053 8263 0 -1 0 21887 0 3 0 7664 148 0 0 25 0 1 0 1785837621 95182848 21164 4294967295 134512640 135167914 3221224448 3221223336 134865821 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/26058/statm): 23238 21164 162 162 0 23076 0
[pid=26058] vsize: 92952
Current children cumulated CPU time (s) 78.15
Current children cumulated vsize (Kb) 95080

[startup+90.0108 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 24754 0 3 0 8640 160 0 0 25 0 1 0 1785837621 106614784 23969 4294967295 134512640 135167914 3221224448 3221223216 134691221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26058/statm): 26029 23969 162 162 0 25867 0
[pid=26058] vsize: 104116
Current children cumulated CPU time (s) 88.03
Current children cumulated vsize (Kb) 106244

[startup+100.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 24756 0 3 0 9639 161 0 0 25 0 1 0 1785837621 106614784 23971 4294967295 134512640 135167914 3221224448 3221223216 134691376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26029 23971 162 162 0 25867 0
[pid=26058] vsize: 104116
Current children cumulated CPU time (s) 98.03
Current children cumulated vsize (Kb) 106244

[startup+110.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 24758 0 3 0 10639 161 0 0 25 0 1 0 1785837621 106614784 23973 4294967295 134512640 135167914 3221224448 3221223268 134522188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26029 23973 162 162 0 25867 0
[pid=26058] vsize: 104116
Current children cumulated CPU time (s) 108.03
Current children cumulated vsize (Kb) 106244

[startup+120.013 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 24765 0 3 0 11639 161 0 0 25 0 1 0 1785837621 106614784 23980 4294967295 134512640 135167914 3221224448 3221223216 134691329 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26029 23980 162 162 0 25867 0
[pid=26058] vsize: 104116
Current children cumulated CPU time (s) 118.03
Current children cumulated vsize (Kb) 106244

[startup+130.014 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 24767 0 3 0 12639 161 0 0 25 0 1 0 1785837621 106618880 23982 4294967295 134512640 135167914 3221224448 3221223216 134691332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26030 23982 162 162 0 25868 0
[pid=26058] vsize: 104120
Current children cumulated CPU time (s) 128.03
Current children cumulated vsize (Kb) 106248

[startup+140.015 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 24768 0 3 0 13639 161 0 0 25 0 1 0 1785837621 106618880 23983 4294967295 134512640 135167914 3221224448 3221223268 134691204 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26030 23983 162 162 0 25868 0
[pid=26058] vsize: 104120
Current children cumulated CPU time (s) 138.03
Current children cumulated vsize (Kb) 106248

[startup+150.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 24769 0 3 0 14640 161 0 0 25 0 1 0 1785837621 106618880 23984 4294967295 134512640 135167914 3221224448 3221223216 134691226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26030 23984 162 162 0 25868 0
[pid=26058] vsize: 104120
Current children cumulated CPU time (s) 148.04
Current children cumulated vsize (Kb) 106248

[startup+160.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 24819 0 3 0 15639 162 0 0 25 0 1 0 1785837621 103034880 23125 4294967295 134512640 135167914 3221224448 3221222432 134845895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26058/statm): 25155 23125 162 162 0 24993 0
[pid=26058] vsize: 100620
Current children cumulated CPU time (s) 158.04
Current children cumulated vsize (Kb) 102748

[startup+170.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 24870 0 3 0 16638 162 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221216880 134843406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 168.03
Current children cumulated vsize (Kb) 102952

[startup+180.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25302 0 3 0 17635 164 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221215584 134696126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 178.02
Current children cumulated vsize (Kb) 102952

[startup+190.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 18634 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221219132 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 188.02
Current children cumulated vsize (Kb) 102952

[startup+200.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 19634 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221219344 134849099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 198.02
Current children cumulated vsize (Kb) 102952

[startup+210.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 20634 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221221068 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 208.02
Current children cumulated vsize (Kb) 102952

[startup+220.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 21635 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220384 134694439 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 218.03
Current children cumulated vsize (Kb) 102952

[startup+230.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 22635 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221219664 134849148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 228.03
Current children cumulated vsize (Kb) 102952

[startup+240.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 23635 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220940 134693585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 238.03
Current children cumulated vsize (Kb) 102952

[startup+250.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 24636 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220576 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 248.04
Current children cumulated vsize (Kb) 102952

[startup+260.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 25636 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220188 134845876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 258.04
Current children cumulated vsize (Kb) 102952

[startup+270.026 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 26636 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220376 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 268.04
Current children cumulated vsize (Kb) 102952

[startup+280.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 27636 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221219100 134723262 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 278.04
Current children cumulated vsize (Kb) 102952

[startup+290.027 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 28636 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221219820 134693600 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 288.04
Current children cumulated vsize (Kb) 102952

[startup+300.028 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 29637 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220400 134849110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 298.05
Current children cumulated vsize (Kb) 102952

[startup+310.029 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 30637 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221221104 134849071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 308.05
Current children cumulated vsize (Kb) 102952

[startup+320.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 31637 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220496 134844736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 318.05
Current children cumulated vsize (Kb) 102952

[startup+330.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 32637 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221219840 134849153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 328.05
Current children cumulated vsize (Kb) 102952

[startup+340.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 33638 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221221104 134693570 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 338.06
Current children cumulated vsize (Kb) 102952

[startup+350.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 34638 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220760 134696561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 348.06
Current children cumulated vsize (Kb) 102952

[startup+360.031 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 35638 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221219328 134849099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 358.06
Current children cumulated vsize (Kb) 102952

[startup+370.032 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 36638 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221219664 134722539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 368.06
Current children cumulated vsize (Kb) 102952

[startup+380.033 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 37639 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220384 134843026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 378.07
Current children cumulated vsize (Kb) 102952

[startup+390.034 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 38639 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221221376 134843404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 388.07
Current children cumulated vsize (Kb) 102952

[startup+400.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 39639 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220384 134849061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 398.07
Current children cumulated vsize (Kb) 102952

[startup+410.035 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 40639 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221221056 134722521 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 408.07
Current children cumulated vsize (Kb) 102952

[startup+420.036 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 41639 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220960 134630803 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 418.07
Current children cumulated vsize (Kb) 102952

[startup+430.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 42640 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220220 134696406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 428.08
Current children cumulated vsize (Kb) 102952

[startup+440.037 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 43640 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221220412 134693552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 438.08
Current children cumulated vsize (Kb) 102952

[startup+450.038 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 44640 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221221104 134843001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 448.08
Current children cumulated vsize (Kb) 102952

[startup+460.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 45640 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221221788 134845940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 458.08
Current children cumulated vsize (Kb) 102952

[startup+470.039 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 46641 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221221772 134844632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 468.09
Current children cumulated vsize (Kb) 102952

[startup+480.04 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 47641 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221221356 134844638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 478.09
Current children cumulated vsize (Kb) 102952

[startup+490.041 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25734 0 3 0 48641 165 0 0 25 0 1 0 1785837621 103243776 23176 4294967295 134512640 135167914 3221224448 3221222124 134845940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25206 23176 162 162 0 25044 0
[pid=26058] vsize: 100824
Current children cumulated CPU time (s) 488.09
Current children cumulated vsize (Kb) 102952

[startup+500.042 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25929 0 3 0 49641 165 0 0 25 0 1 0 1785837621 104816640 23371 4294967295 134512640 135167914 3221224448 3221220336 134849082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25590 23371 162 162 0 25428 0
[pid=26058] vsize: 102360
Current children cumulated CPU time (s) 498.09
Current children cumulated vsize (Kb) 104488

[startup+510.043 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25929 0 3 0 50641 165 0 0 25 0 1 0 1785837621 104816640 23371 4294967295 134512640 135167914 3221224448 3221220320 134844700 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25590 23371 162 162 0 25428 0
[pid=26058] vsize: 102360
Current children cumulated CPU time (s) 508.09
Current children cumulated vsize (Kb) 104488

[startup+520.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25945 0 3 0 51641 165 0 0 25 0 1 0 1785837621 104816640 23387 4294967295 134512640 135167914 3221224448 3221220592 134628673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25590 23387 162 162 0 25428 0
[pid=26058] vsize: 102360
Current children cumulated CPU time (s) 518.09
Current children cumulated vsize (Kb) 104488

[startup+530.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25945 0 3 0 52642 165 0 0 25 0 1 0 1785837621 104816640 23387 4294967295 134512640 135167914 3221224448 3221221568 134723225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25590 23387 162 162 0 25428 0
[pid=26058] vsize: 102360
Current children cumulated CPU time (s) 528.1
Current children cumulated vsize (Kb) 104488

[startup+540.044 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25961 0 3 0 53642 165 0 0 25 0 1 0 1785837621 104816640 23403 4294967295 134512640 135167914 3221224448 3221220744 134849057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25590 23403 162 162 0 25428 0
[pid=26058] vsize: 102360
Current children cumulated CPU time (s) 538.1
Current children cumulated vsize (Kb) 104488

[startup+550.045 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25961 0 3 0 54642 165 0 0 25 0 1 0 1785837621 104816640 23403 4294967295 134512640 135167914 3221224448 3221221264 134843026 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25590 23403 162 162 0 25428 0
[pid=26058] vsize: 102360
Current children cumulated CPU time (s) 548.1
Current children cumulated vsize (Kb) 104488

[startup+560.046 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25976 0 3 0 55642 165 0 0 25 0 1 0 1785837621 104816640 23418 4294967295 134512640 135167914 3221224448 3221219680 134694511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25590 23418 162 162 0 25428 0
[pid=26058] vsize: 102360
Current children cumulated CPU time (s) 558.1
Current children cumulated vsize (Kb) 104488

[startup+570.047 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25976 0 3 0 56642 165 0 0 25 0 1 0 1785837621 104816640 23418 4294967295 134512640 135167914 3221224448 3221222168 134694366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25590 23418 162 162 0 25428 0
[pid=26058] vsize: 102360
Current children cumulated CPU time (s) 568.1
Current children cumulated vsize (Kb) 104488

[startup+580.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 25976 0 3 0 57643 165 0 0 25 0 1 0 1785837621 104816640 23418 4294967295 134512640 135167914 3221224448 3221220840 134844633 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25590 23418 162 162 0 25428 0
[pid=26058] vsize: 102360
Current children cumulated CPU time (s) 578.11
Current children cumulated vsize (Kb) 104488

[startup+590.048 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26321 0 3 0 58642 166 0 0 25 0 1 0 1785837621 106168320 23763 4294967295 134512640 135167914 3221224448 3221220848 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23763 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 588.11
Current children cumulated vsize (Kb) 105808

[startup+600.049 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26321 0 3 0 59642 166 0 0 25 0 1 0 1785837621 106168320 23763 4294967295 134512640 135167914 3221224448 3221221568 134696653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23763 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 598.11
Current children cumulated vsize (Kb) 105808

[startup+610.05 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26339 0 3 0 60643 166 0 0 25 0 1 0 1785837621 106168320 23781 4294967295 134512640 135167914 3221224448 3221221436 134722512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23781 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 608.12
Current children cumulated vsize (Kb) 105808

[startup+620.051 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26360 0 3 0 61643 166 0 0 25 0 1 0 1785837621 106168320 23802 4294967295 134512640 135167914 3221224448 3221222496 134849196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23802 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 618.12
Current children cumulated vsize (Kb) 105808

[startup+630.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26388 0 3 0 62643 166 0 0 25 0 1 0 1785837621 106168320 23830 4294967295 134512640 135167914 3221224448 3221220672 134843160 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23830 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 628.12
Current children cumulated vsize (Kb) 105808

[startup+640.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26388 0 3 0 63643 166 0 0 25 0 1 0 1785837621 106168320 23830 4294967295 134512640 135167914 3221224448 3221221968 134843036 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23830 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 638.12
Current children cumulated vsize (Kb) 105808

[startup+650.052 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26399 0 3 0 64643 166 0 0 25 0 1 0 1785837621 106168320 23841 4294967295 134512640 135167914 3221224448 3221219608 134844674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23841 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 648.12
Current children cumulated vsize (Kb) 105808

[startup+660.053 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26399 0 3 0 65643 166 0 0 25 0 1 0 1785837621 106168320 23841 4294967295 134512640 135167914 3221224448 3221221056 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23841 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 658.12
Current children cumulated vsize (Kb) 105808

[startup+670.054 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26399 0 3 0 66644 166 0 0 25 0 1 0 1785837621 106168320 23841 4294967295 134512640 135167914 3221224448 3221221248 134722532 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23841 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 668.13
Current children cumulated vsize (Kb) 105808

[startup+680.055 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26399 0 3 0 67644 166 0 0 25 0 1 0 1785837621 106168320 23841 4294967295 134512640 135167914 3221224448 3221221376 134844706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23841 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 678.13
Current children cumulated vsize (Kb) 105808

[startup+690.056 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26418 0 3 0 68644 167 0 0 25 0 1 0 1785837621 106168320 23860 4294967295 134512640 135167914 3221224448 3221219728 134630786 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23860 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 688.14
Current children cumulated vsize (Kb) 105808

[startup+700.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26418 0 3 0 69644 167 0 0 25 0 1 0 1785837621 106168320 23860 4294967295 134512640 135167914 3221224448 3221220336 134843064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23860 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 698.14
Current children cumulated vsize (Kb) 105808

[startup+710.057 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26418 0 3 0 70645 167 0 0 25 0 1 0 1785837621 106168320 23860 4294967295 134512640 135167914 3221224448 3221220184 134845939 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23860 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 708.15
Current children cumulated vsize (Kb) 105808

[startup+720.058 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26418 0 3 0 71645 167 0 0 25 0 1 0 1785837621 106168320 23860 4294967295 134512640 135167914 3221224448 3221221552 134844650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23860 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 718.15
Current children cumulated vsize (Kb) 105808

[startup+730.059 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26436 0 3 0 72645 167 0 0 25 0 1 0 1785837621 106168320 23878 4294967295 134512640 135167914 3221224448 3221219532 134694551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23878 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 728.15
Current children cumulated vsize (Kb) 105808

[startup+740.06 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26436 0 3 0 73645 167 0 0 25 0 1 0 1785837621 106168320 23878 4294967295 134512640 135167914 3221224448 3221220880 134845881 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23878 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 738.15
Current children cumulated vsize (Kb) 105808

[startup+750.061 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26436 0 3 0 74645 167 0 0 25 0 1 0 1785837621 106168320 23878 4294967295 134512640 135167914 3221224448 3221221552 134843123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23878 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 748.15
Current children cumulated vsize (Kb) 105808

[startup+760.062 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26436 0 3 0 75646 167 0 0 25 0 1 0 1785837621 106168320 23878 4294967295 134512640 135167914 3221224448 3221220592 134630898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23878 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 758.16
Current children cumulated vsize (Kb) 105808

[startup+770.063 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26436 0 3 0 76646 167 0 0 25 0 1 0 1785837621 106168320 23878 4294967295 134512640 135167914 3221224448 3221221792 134849092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 25920 23878 162 162 0 25758 0
[pid=26058] vsize: 103680
Current children cumulated CPU time (s) 768.16
Current children cumulated vsize (Kb) 105808

[startup+780.064 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26454 0 3 0 77646 167 0 0 25 0 1 0 1785837621 107741184 23896 4294967295 134512640 135167914 3221224448 3221219116 134844638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23896 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 778.16
Current children cumulated vsize (Kb) 107344

[startup+790.064 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26454 0 3 0 78646 167 0 0 25 0 1 0 1785837621 107741184 23896 4294967295 134512640 135167914 3221224448 3221220012 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23896 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 788.16
Current children cumulated vsize (Kb) 107344

[startup+800.065 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26454 0 3 0 79647 167 0 0 25 0 1 0 1785837621 107741184 23896 4294967295 134512640 135167914 3221224448 3221221440 134694444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23896 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 798.17
Current children cumulated vsize (Kb) 107344

[startup+810.066 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26454 0 3 0 80647 167 0 0 25 0 1 0 1785837621 107741184 23896 4294967295 134512640 135167914 3221224448 3221220656 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23896 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 808.17
Current children cumulated vsize (Kb) 107344

[startup+820.067 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26471 0 3 0 81647 167 0 0 25 0 1 0 1785837621 107741184 23913 4294967295 134512640 135167914 3221224448 3221220848 134844644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23913 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 818.17
Current children cumulated vsize (Kb) 107344

[startup+830.067 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26471 0 3 0 82647 167 0 0 25 0 1 0 1785837621 107741184 23913 4294967295 134512640 135167914 3221224448 3221220960 134844689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23913 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 828.17
Current children cumulated vsize (Kb) 107344

[startup+840.068 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26471 0 3 0 83647 167 0 0 25 0 1 0 1785837621 107741184 23913 4294967295 134512640 135167914 3221224448 3221221376 134845921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23913 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 838.17
Current children cumulated vsize (Kb) 107344

[startup+850.069 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26471 0 3 0 84648 167 0 0 25 0 1 0 1785837621 107741184 23913 4294967295 134512640 135167914 3221224448 3221221724 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23913 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 848.18
Current children cumulated vsize (Kb) 107344

[startup+860.07 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26485 0 3 0 85648 167 0 0 25 0 1 0 1785837621 107741184 23927 4294967295 134512640 135167914 3221224448 3221221104 134693576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23927 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 858.18
Current children cumulated vsize (Kb) 107344

[startup+870.072 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26497 0 3 0 86648 167 0 0 25 0 1 0 1785837621 107741184 23939 4294967295 134512640 135167914 3221224448 3221220576 134694338 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23939 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 868.18
Current children cumulated vsize (Kb) 107344

[startup+880.072 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26502 0 3 0 87648 167 0 0 25 0 1 0 1785837621 107741184 23944 4294967295 134512640 135167914 3221224448 3221221472 134523161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23944 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 878.18
Current children cumulated vsize (Kb) 107344

[startup+890.072 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26512 0 3 0 88648 167 0 0 25 0 1 0 1785837621 107741184 23954 4294967295 134512640 135167914 3221224448 3221220576 134849163 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23954 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 888.18
Current children cumulated vsize (Kb) 107344

[startup+900.073 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26527 0 3 0 89649 167 0 0 25 0 1 0 1785837621 107741184 23969 4294967295 134512640 135167914 3221224448 3221219856 134694495 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23969 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 898.19
Current children cumulated vsize (Kb) 107344

[startup+910.074 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26527 0 3 0 90649 167 0 0 25 0 1 0 1785837621 107741184 23969 4294967295 134512640 135167914 3221224448 3221221904 134844728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23969 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 908.19
Current children cumulated vsize (Kb) 107344

[startup+920.075 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26541 0 3 0 91649 167 0 0 25 0 1 0 1785837621 107741184 23983 4294967295 134512640 135167914 3221224448 3221220516 134723216 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23983 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 918.19
Current children cumulated vsize (Kb) 107344

[startup+930.076 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26541 0 3 0 92649 167 0 0 25 0 1 0 1785837621 107741184 23983 4294967295 134512640 135167914 3221224448 3221221760 134849071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23983 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 928.19
Current children cumulated vsize (Kb) 107344

[startup+940.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26555 0 3 0 93650 167 0 0 25 0 1 0 1785837621 107741184 23997 4294967295 134512640 135167914 3221224448 3221219712 134629231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23997 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 938.2
Current children cumulated vsize (Kb) 107344

[startup+950.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 26555 0 3 0 94650 167 0 0 25 0 1 0 1785837621 107741184 23997 4294967295 134512640 135167914 3221224448 3221220560 134694504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 26304 23997 162 162 0 26142 0
[pid=26058] vsize: 105216
Current children cumulated CPU time (s) 948.2
Current children cumulated vsize (Kb) 107344

[startup+960.077 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 30951 0 3 0 95615 183 0 0 25 0 1 0 1785837621 123002880 27733 4294967295 134512640 135167914 3221224448 3221211476 134849255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26058/statm): 30030 27733 162 162 0 29868 0
[pid=26058] vsize: 120120
Current children cumulated CPU time (s) 958.01
Current children cumulated vsize (Kb) 122248

[startup+970.078 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 36535 0 3 0 96567 203 0 0 25 0 1 0 1785837621 143171584 32658 4294967295 134512640 135167914 3221224448 3221223200 134849102 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26058/statm): 34954 32658 162 162 0 34792 0
[pid=26058] vsize: 139816
Current children cumulated CPU time (s) 967.73
Current children cumulated vsize (Kb) 141944

[startup+980.079 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 36535 0 3 0 97565 204 0 0 25 0 1 0 1785837621 137773056 31340 4294967295 134512640 135167914 3221224448 3221209980 134722660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26058/statm): 33636 31340 162 162 0 33474 0
[pid=26058] vsize: 134544
Current children cumulated CPU time (s) 977.72
Current children cumulated vsize (Kb) 136672

[startup+990.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37857 0 3 0 98551 208 0 0 25 0 1 0 1785837621 143179776 32662 4294967295 134512640 135167914 3221224448 3221220096 134844703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32662 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 987.62
Current children cumulated vsize (Kb) 141952

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37876 0 3 0 99552 208 0 0 25 0 1 0 1785837621 143179776 32681 4294967295 134512640 135167914 3221224448 3221221552 134844713 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32681 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 997.63
Current children cumulated vsize (Kb) 141952

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37900 0 3 0 100552 208 0 0 25 0 1 0 1785837621 143179776 32705 4294967295 134512640 135167914 3221224448 3221222108 134722225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32705 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1007.63
Current children cumulated vsize (Kb) 141952

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37919 0 3 0 101552 208 0 0 25 0 1 0 1785837621 143179776 32724 4294967295 134512640 135167914 3221224448 3221220912 134849187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32724 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1017.63
Current children cumulated vsize (Kb) 141952

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37919 0 3 0 102552 208 0 0 25 0 1 0 1785837621 143179776 32724 4294967295 134512640 135167914 3221224448 3221220848 134696400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32724 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1027.63
Current children cumulated vsize (Kb) 141952

[startup+1040.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37931 0 3 0 103553 208 0 0 25 0 1 0 1785837621 143179776 32736 4294967295 134512640 135167914 3221224448 3221219616 134696718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32736 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1037.64
Current children cumulated vsize (Kb) 141952

[startup+1050.08 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37931 0 3 0 104553 208 0 0 25 0 1 0 1785837621 143179776 32736 4294967295 134512640 135167914 3221224448 3221219804 134843002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32736 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1047.64
Current children cumulated vsize (Kb) 141952

[startup+1060.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37931 0 3 0 105553 208 0 0 25 0 1 0 1785837621 143179776 32736 4294967295 134512640 135167914 3221224448 3221220364 134844675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32736 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1057.64
Current children cumulated vsize (Kb) 141952

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37931 0 3 0 106554 208 0 0 25 0 1 0 1785837621 143179776 32736 4294967295 134512640 135167914 3221224448 3221220048 134693582 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32736 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1067.65
Current children cumulated vsize (Kb) 141952

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37931 0 3 0 107554 208 0 0 25 0 1 0 1785837621 143179776 32736 4294967295 134512640 135167914 3221224448 3221221088 134843015 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32736 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1077.65
Current children cumulated vsize (Kb) 141952

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37931 0 3 0 108554 208 0 0 25 0 1 0 1785837621 143179776 32736 4294967295 134512640 135167914 3221224448 3221220176 134693566 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32736 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1087.65
Current children cumulated vsize (Kb) 141952

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37931 0 3 0 109554 208 0 0 25 0 1 0 1785837621 143179776 32736 4294967295 134512640 135167914 3221224448 3221220396 134849056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32736 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1097.65
Current children cumulated vsize (Kb) 141952

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37931 0 3 0 110554 208 0 0 25 0 1 0 1785837621 143179776 32736 4294967295 134512640 135167914 3221224448 3221220952 134630742 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32736 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1107.65
Current children cumulated vsize (Kb) 141952

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37931 0 3 0 111555 208 0 0 25 0 1 0 1785837621 143179776 32736 4294967295 134512640 135167914 3221224448 3221220496 134844676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32736 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1117.66
Current children cumulated vsize (Kb) 141952

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37931 0 3 0 112555 208 0 0 25 0 1 0 1785837621 143179776 32736 4294967295 134512640 135167914 3221224448 3221220320 134844723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32736 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1127.66
Current children cumulated vsize (Kb) 141952

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37931 0 3 0 113555 208 0 0 25 0 1 0 1785837621 143179776 32736 4294967295 134512640 135167914 3221224448 3221220864 134843153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32736 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1137.66
Current children cumulated vsize (Kb) 141952

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37952 0 3 0 114555 209 0 0 25 0 1 0 1785837621 143179776 32757 4294967295 134512640 135167914 3221224448 3221209300 134697377 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26058/statm): 34956 32757 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1147.67
Current children cumulated vsize (Kb) 141952

[startup+1160.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37955 0 3 0 115555 209 0 0 25 0 1 0 1785837621 143179776 32760 4294967295 134512640 135167914 3221224448 3221219600 134845888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32760 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1157.67
Current children cumulated vsize (Kb) 141952

[startup+1170.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37955 0 3 0 116555 209 0 0 25 0 1 0 1785837621 143179776 32760 4294967295 134512640 135167914 3221224448 3221218144 134844733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32760 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1167.67
Current children cumulated vsize (Kb) 141952

[startup+1180.09 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37955 0 3 0 117555 209 0 0 25 0 1 0 1785837621 143179776 32760 4294967295 134512640 135167914 3221224448 3221218764 134843033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32760 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1177.67
Current children cumulated vsize (Kb) 141952

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37955 0 3 0 118555 209 0 0 25 0 1 0 1785837621 143179776 32760 4294967295 134512640 135167914 3221224448 3221220736 134843107 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32760 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1187.67
Current children cumulated vsize (Kb) 141952

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37955 0 3 0 119556 209 0 0 25 0 1 0 1785837621 143179776 32760 4294967295 134512640 135167914 3221224448 3221221036 134723246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32760 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1197.68
Current children cumulated vsize (Kb) 141952

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37955 0 3 0 120556 209 0 0 25 0 1 0 1785837621 143179776 32760 4294967295 134512640 135167914 3221224448 3221220364 134842996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32760 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1207.68
Current children cumulated vsize (Kb) 141952



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.97 0.91 2/57 26058
Raw data (/proc/26053/stat): 26053 (minisat+_script) S 26052 26053 8263 0 -1 0 314 332 0 0 0 0 1 2 21 0 1 0 1785837613 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/26053/statm): 532 234 485 147 0 385 0
[pid=26053] vsize: 2128
Raw data (/proc/26058/stat): 26058 (minisat+_bignum) R 26053 26053 8263 0 -1 0 37955 0 3 0 120556 209 0 0 25 0 1 0 1785837621 143179776 32760 4294967295 134512640 135167914 3221224448 3221220200 134845877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26058/statm): 34956 32760 162 162 0 34794 0
[pid=26058] vsize: 139824
Current children cumulated CPU time (s) 1207.68
Current children cumulated vsize (Kb) 141952

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1207.72
CPU user time (s): 1205.56
CPU system time (s): 2.15467
CPU usage (%): 99.7981
Max. virtual memory (cumulated for all children) (Kb): 141952

Verifier Data

ERROR: no interpretation found !