Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-pp08aCUTS.opb
MD5SUMd1b87efc35bcd73acfc5183bbe3df4f0
Bench Categoryoptimization, medium integers (OPTMEDINT)
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 2304
Biggest coefficient in the objective function 1048576
Number of bits for the biggest coefficient in the objective function 21
Sum of the numbers in the objective function 178464600
Number of bits of the sum of numbers in the objective function 28
Biggest number in a constraint 1048576
Number of bits of the biggest number in a constraint 21
Biggest sum of numbers in a constraint 178464600
Number of bits of the biggest sum of numbers28
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables3288
Total number of constraints374
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)64
Number of constraints which are nor clauses,nor cardinality constraints310
Minimum length of a constraint1
Maximum length of a constraint123

Trace number 6155

Launcher Data

LAUNCH ON wulflinc23 THE 2005-09-20 03:52:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3319 boxname=wulflinc23 idbench=975 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d1b87efc35bcd73acfc5183bbe3df4f0  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-pp08aCUTS.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-pp08aCUTS.opb
IDLAUNCH: 3319
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        910388 kB
Buffers:         15668 kB
Cached:          81072 kB
SwapCached:        840 kB
Active:          28132 kB
Inactive:        71256 kB
HighTotal:      131008 kB
HighFree:        48776 kB
LowTotal:       903652 kB
LowFree:        861612 kB
SwapTotal:     2097136 kB
SwapFree:      2095788 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5668 kB
Slab:            19312 kB
Committed_AS:    64152 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:12:13 (client local time) WITH STATUS 0 IN 1208.76 SECONDS
stats: 3319 7 1208.76 0

Solver Data

c Parsing PB file...
c Converting 374 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[ 501]---> BDD-cost:   15
c ---[ 500]---> BDD-cost:   15
c ---[ 499]---> BDD-cost:   15
c ---[ 498]---> BDD-cost:   15
c ---[ 497]---> BDD-cost:   15
c ---[ 496]---> BDD-cost:   15
c ---[ 495]---> BDD-cost:   15
c ---[ 494]---> BDD-cost:   15
c ---[ 485]---> BDD-cost:   15
c ---[ 484]---> BDD-cost:   15
c ---[ 483]---> BDD-cost:   15
c ---[ 482]---> BDD-cost:   15
c ---[ 481]---> BDD-cost:   15
c ---[ 480]---> BDD-cost:   15
c ---[ 479]---> BDD-cost:   15
c ---[ 477]---> BDD-cost:   15
c ---[ 476]---> BDD-cost:   15
c ---[ 475]---> BDD-cost:   15
c ---[ 474]---> BDD-cost:   15
c ---[ 473]---> BDD-cost:   15
c ---[ 472]---> BDD-cost:   15
c ---[ 471]---> BDD-cost:   15
c ---[ 469]---> BDD-cost:   14
c ---[ 468]---> BDD-cost:   14
c ---[ 467]---> BDD-cost:   14
c ---[ 466]---> BDD-cost:   14
c ---[ 465]---> BDD-cost:   14
c ---[ 464]---> BDD-cost:   14
c ---[ 463]---> BDD-cost:   14
c ---[ 462]---> BDD-cost:   14
c ---[ 461]---> BDD-cost:   15
c ---[ 460]---> BDD-cost:   15
c ---[ 459]---> BDD-cost:   15
c ---[ 458]---> BDD-cost:   15
c ---[ 457]---> BDD-cost:   15
c ---[ 456]---> BDD-cost:   15
c ---[ 455]---> BDD-cost:   15
c ---[ 454]---> BDD-cost:   15
c ---[ 445]---> BDD-cost:   13
c ---[ 444]---> BDD-cost:   13
c ---[ 443]---> BDD-cost:   13
c ---[ 442]---> BDD-cost:   13
c ---[ 441]---> BDD-cost:   13
c ---[ 440]---> BDD-cost:   13
c ---[ 439]---> BDD-cost:   13
c ---[ 438]---> BDD-cost:   13
c ---[ 436]---> BDD-cost:  158
c ---[ 434]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> BDD-cost:    6
c ---[ 432]---> BDD-cost:    6
c ---[ 431]---> BDD-cost:    6
c ---[ 430]---> BDD-cost:    6
c ---[ 429]---> BDD-cost:   23
c ---[ 428]---> BDD-cost:    4
c ---[ 427]---> BDD-cost:    4
c ---[ 426]---> BDD-cost:    4
c ---[ 425]---> BDD-cost:    4
c ---[ 424]---> BDD-cost:    4
c ---[ 422]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 421]---> BDD-cost:    4
c ---[ 420]---> BDD-cost:    4
c ---[ 419]---> BDD-cost:    4
c ---[ 418]---> BDD-cost:    9
c ---[ 417]---> BDD-cost:    9
c ---[ 416]---> BDD-cost:    9
c ---[ 415]---> BDD-cost:    6
c ---[ 414]---> BDD-cost:    6
c ---[ 413]---> BDD-cost:    6
c ---[ 412]---> BDD-cost:    6
c ---[ 410]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 409]---> BDD-cost:    6
c ---[ 408]---> BDD-cost:   19
c ---[ 407]---> BDD-cost:   19
c ---[ 406]---> BDD-cost:   19
c ---[ 405]---> BDD-cost:   19
c ---[ 404]---> BDD-cost:   19
c ---[ 403]---> BDD-cost:   19
c ---[ 402]---> BDD-cost:   19
c ---[ 401]---> BDD-cost:   19
c ---[ 400]---> BDD-cost:    6
c ---[ 398]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    6
c ---[ 394]---> BDD-cost:    6
c ---[ 393]---> BDD-cost:    6
c ---[ 392]---> BDD-cost:    6
c ---[ 391]---> BDD-cost:    6
c ---[ 386]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> BDD-cost:  158
c ---[ 253]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 249]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 247]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 243]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 241]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 239]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 237]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 235]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 233]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 231]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 229]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 227]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 225]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 219]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 217]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 213]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 211]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 203]---> BDD-cost:  154
c ---[ 201]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 191]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    6
c ---[ 154]---> BDD-cost:    6
c ---[ 153]---> BDD-cost:    6
c ---[ 152]---> BDD-cost:    6
c ---[ 150]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> BDD-cost:    8
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:   19
c ---[ 146]---> BDD-cost:   19
c ---[ 145]---> BDD-cost:   19
c ---[ 144]---> BDD-cost:   19
c ---[ 143]---> BDD-cost:   19
c ---[ 142]---> BDD-cost:   19
c ---[ 141]---> BDD-cost:   19
c ---[ 140]---> BDD-cost:    9
c ---[ 138]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> BDD-cost:    9
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:    6
c ---[ 134]---> BDD-cost:    6
c ---[ 133]---> BDD-cost:    6
c ---[ 132]---> BDD-cost:    6
c ---[ 131]---> BDD-cost:   23
c ---[ 130]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:    9
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:    1
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:    1
c ---[ 122]---> BDD-cost:    1
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:    1
c ---[ 118]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:    1
c ---[ 110]---> BDD-cost:    1
c ---[ 109]---> BDD-cost:   50
c ---[ 108]---> BDD-cost:  203
c ---[ 107]---> BDD-cost:   45
c ---[ 106]---> BDD-cost:  194
c ---[ 105]---> BDD-cost:   48
c ---[ 104]---> BDD-cost:  191
c ---[ 103]---> BDD-cost:   38
c ---[ 102]---> BDD-cost:  173
c ---[ 101]---> BDD-cost:   44
c ---[ 100]---> BDD-cost:  167
c ---[  99]---> BDD-cost:    5
c ---[  98]---> BDD-cost:   73
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:   62
c ---[  95]---> BDD-cost:   41
c ---[  94]---> BDD-cost:  158
c ---[  93]---> BDD-cost:   45
c ---[  92]---> BDD-cost:  182
c ---[  91]---> BDD-cost:   40
c ---[  90]---> BDD-cost:  173
c ---[  89]---> BDD-cost:   35
c ---[  88]---> BDD-cost:  164
c ---[  87]---> BDD-cost:   41
c ---[  86]---> BDD-cost:  158
c ---[  85]---> BDD-cost:    5
c ---[  84]---> BDD-cost:   70
c ---[  83]---> BDD-cost:    3
c ---[  82]---> BDD-cost:   65
c ---[  81]---> BDD-cost:   45
c ---[  80]---> BDD-cost:  194
c ---[  79]---> BDD-cost:   48
c ---[  78]---> BDD-cost:  191
c ---[  77]---> BDD-cost:   41
c ---[  76]---> BDD-cost:  170
c ---[  75]---> BDD-cost:   44
c ---[  74]---> BDD-cost:  167
c ---[  73]---> BDD-cost:   50
c ---[  72]---> BDD-cost:  203
c ---[  71]---> BDD-cost:    3
c ---[  70]---> BDD-cost:   61
c ---[  69]---> BDD-cost:   48
c ---[  68]---> BDD-cost:  191
c ---[  67]---> BDD-cost:   48
c ---[  66]---> BDD-cost:  191
c ---[  65]---> BDD-cost:   55
c ---[  64]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> BDD-cost:   47
c ---[  62]---> BDD-cost:  161
c ---[  61]---> BDD-cost:   50
c ---[  60]---> BDD-cost:  203
c ---[  59]---> BDD-cost:   48
c ---[  58]---> BDD-cost:  191
c ---[  57]---> BDD-cost:    5
c ---[  56]---> BDD-cost:   73
c ---[  55]---> BDD-cost:    5
c ---[  54]---> BDD-cost:   70
c ---[  53]---> BDD-cost:   38
c ---[  52]---> BDD-cost:  161
c ---[  51]---> BDD-cost:   41
c ---[  50]---> BDD-cost:  158
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:  164
c ---[  47]---> BDD-cost:   35
c ---[  46]---> BDD-cost:  164
c ---[  45]---> BDD-cost:   38
c ---[  44]---> BDD-cost:  161
c ---[  43]---> BDD-cost:    3
c ---[  42]---> BDD-cost:   64
c ---[  41]---> BDD-cost:    6
c ---[  40]---> BDD-cost:   78
c ---[  39]---> BDD-cost:   41
c ---[  38]---> BDD-cost:  170
c ---[  37]---> BDD-cost:   41
c ---[  36]---> BDD-cost:  170
c ---[  35]---> BDD-cost:   41
c ---[  34]---> BDD-cost:  170
c ---[  33]---> BDD-cost:   48
c ---[  32]---> BDD-cost:  191
c ---[  31]---> BDD-cost:   38
c ---[  30]---> BDD-cost:  173
c ---[  29]---> BDD-cost:   41
c ---[  28]---> BDD-cost:  170
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:   75
c ---[  25]---> BDD-cost:   38
c ---[  24]---> BDD-cost:  161
c ---[  23]---> BDD-cost:   45
c ---[  22]---> BDD-cost:  182
c ---[  21]---> BDD-cost:   35
c ---[  20]---> BDD-cost:  164
c ---[  19]---> BDD-cost:   38
c ---[  18]---> BDD-cost:  161
c ---[  17]---> BDD-cost:   43
c ---[  16]---> BDD-cost:  170
c ---[  15]---> BDD-cost:   41
c ---[  14]---> BDD-cost:  158
c ---[  13]---> BDD-cost:    3
c ---[  12]---> BDD-cost:   60
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:   59
c ---[   9]---> BDD-cost:   38
c ---[   8]---> BDD-cost:  149
c ---[   7]---> BDD-cost:   35
c ---[   6]---> BDD-cost:  152
c ---[   5]---> BDD-cost:   35
c ---[   4]---> BDD-cost:  152
c ---[   3]---> BDD-cost:   38
c ---[   2]---> BDD-cost:  149
c ---[   1]---> BDD-cost:    4
c ---[   0]---> BDD-cost:   62
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  215438   519594 |   71812       0        0     nan |  0.000 % |
c |       101 |  215326   519346 |   78993      79      271     3.4 |  4.796 % |
c |       251 |  215165   518988 |   86892     203      739     3.6 |  4.854 % |
c |       476 |  215013   518651 |   95581     405     1451     3.6 |  4.912 % |
c |       814 |  214882   518363 |  105139     718     2555     3.6 |  4.964 % |
c |      1320 |  214188   516814 |  115653    1138     3953     3.5 |  5.212 % |
c |      2079 |  213603   515514 |  127219    1804     6333     3.5 |  5.426 % |
c |      3218 |  213209   514630 |  139941    2898    10656     3.7 |  5.562 % |
c |      4926 |  212696   513482 |  153935    4545    17723     3.9 |  5.742 % |
c |      7488 |  211648   511137 |  169328    6973    28093     4.0 |  6.108 % |
c |     11332 |  210588   508770 |  186261   10695    45175     4.2 |  6.481 % |
c |     17098 |  208970   505150 |  204888   16237    70107     4.3 |  7.050 % |
c |     25747 |  207655   502206 |  225376   24727   121042     4.9 |  7.504 % |
c |     38721 |  206711   500085 |  247914   37579   208692     5.6 |  7.832 % |
c |     58183 |  206122   498761 |  272705   56950   373165     6.6 |  8.033 % |
c |     87375 |  206065   498634 |  299976   86132  1052463    12.2 |  8.053 % |
c |    131164 |  205853   498158 |  329974  129888  2014357    15.5 |  8.128 % |
c |    196848 |  205590   497567 |  362971  195540  3544352    18.1 |  8.217 % |
c |    295374 |  205512   497392 |  399268  294054  6084326    20.7 |  8.247 % |
c |    443164 |  205325   496976 |  439195   68442   994490    14.5 |  8.316 % |

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/27245/stat): 27245 (minisat+_script) R 27244 27245 5299 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855450281 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/27245/statm): 174 3 169 147 0 27 0
[pid=27245] 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=27246
New process pid=27247
New process pid=27248
execve syscall for /bin/sed executable
One traced child (pid=27247) 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=27248) exited with status: 0
One traced child (pid=27246) exited with status: 0
New process pid=27249
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-pp08aCUTS.opb

[startup+10.004 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7025 0 0 0 939 30 0 0 25 0 1 0 1855450286 31629312 6668 4294967295 134512640 135094434 3221224432 3221223116 134553432 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 7722 6668 145 145 0 7577 0
[pid=27249] vsize: 30888
Current children cumulated CPU time (s) 9.71
Current children cumulated vsize (Kb) 33012

[startup+20.0046 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7049 0 0 0 1938 30 0 0 25 0 1 0 1855450286 31727616 6692 4294967295 134512640 135094434 3221224432 3221223088 134561502 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 7746 6692 145 145 0 7601 0
[pid=27249] vsize: 30984
Current children cumulated CPU time (s) 19.7
Current children cumulated vsize (Kb) 33108

[startup+30.0053 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7085 0 0 0 2937 30 0 0 25 0 1 0 1855450286 31862784 6728 4294967295 134512640 135094434 3221224432 3221223044 134563089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27249/statm): 7779 6728 145 145 0 7634 0
[pid=27249] vsize: 31116
Current children cumulated CPU time (s) 29.69
Current children cumulated vsize (Kb) 33240

[startup+40.0059 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7121 0 0 0 3936 31 0 0 25 0 1 0 1855450286 32002048 6764 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 7813 6764 145 145 0 7668 0
[pid=27249] vsize: 31252
Current children cumulated CPU time (s) 39.69
Current children cumulated vsize (Kb) 33376

[startup+50.0066 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7152 0 0 0 4936 31 0 0 25 0 1 0 1855450286 32096256 6795 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 7836 6795 145 145 0 7691 0
[pid=27249] vsize: 31344
Current children cumulated CPU time (s) 49.69
Current children cumulated vsize (Kb) 33468

[startup+60.0072 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7174 0 0 0 5936 31 0 0 25 0 1 0 1855450286 32169984 6817 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 7854 6817 145 145 0 7709 0
[pid=27249] vsize: 31416
Current children cumulated CPU time (s) 59.69
Current children cumulated vsize (Kb) 33540

[startup+70.0079 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7226 0 0 0 6935 32 0 0 25 0 1 0 1855450286 32415744 6869 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 7914 6869 145 145 0 7769 0
[pid=27249] vsize: 31656
Current children cumulated CPU time (s) 69.69
Current children cumulated vsize (Kb) 33780

[startup+80.0085 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7250 0 0 0 7935 32 0 0 25 0 1 0 1855450286 32501760 6893 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 7935 6893 145 145 0 7790 0
[pid=27249] vsize: 31740
Current children cumulated CPU time (s) 79.69
Current children cumulated vsize (Kb) 33864

[startup+90.0091 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7277 0 0 0 8935 32 0 0 25 0 1 0 1855450286 32595968 6920 4294967295 134512640 135094434 3221224432 3221223056 134557604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 7958 6920 145 145 0 7813 0
[pid=27249] vsize: 31832
Current children cumulated CPU time (s) 89.69
Current children cumulated vsize (Kb) 33956

[startup+100.01 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7307 0 0 0 9935 32 0 0 25 0 1 0 1855450286 32698368 6950 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 7983 6950 145 145 0 7838 0
[pid=27249] vsize: 31932
Current children cumulated CPU time (s) 99.69
Current children cumulated vsize (Kb) 34056

[startup+110.011 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7332 0 0 0 10933 33 0 0 25 0 1 0 1855450286 32792576 6975 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8006 6975 145 145 0 7861 0
[pid=27249] vsize: 32024
Current children cumulated CPU time (s) 109.68
Current children cumulated vsize (Kb) 34148

[startup+120.012 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7365 0 0 0 11933 33 0 0 25 0 1 0 1855450286 32915456 7008 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8036 7008 145 145 0 7891 0
[pid=27249] vsize: 32144
Current children cumulated CPU time (s) 119.68
Current children cumulated vsize (Kb) 34268

[startup+130.013 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7399 0 0 0 12932 34 0 0 25 0 1 0 1855450286 33042432 7042 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8067 7042 145 145 0 7922 0
[pid=27249] vsize: 32268
Current children cumulated CPU time (s) 129.68
Current children cumulated vsize (Kb) 34392

[startup+140.013 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7441 0 0 0 13932 34 0 0 25 0 1 0 1855450286 33337344 7084 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8139 7084 145 145 0 7994 0
[pid=27249] vsize: 32556
Current children cumulated CPU time (s) 139.68
Current children cumulated vsize (Kb) 34680

[startup+150.014 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7473 0 0 0 14931 35 0 0 25 0 1 0 1855450286 33456128 7116 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8168 7116 145 145 0 8023 0
[pid=27249] vsize: 32672
Current children cumulated CPU time (s) 149.68
Current children cumulated vsize (Kb) 34796

[startup+160.015 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27249
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7517 0 0 0 15930 35 0 0 25 0 1 0 1855450286 33624064 7160 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8209 7160 145 145 0 8064 0
[pid=27249] vsize: 32836
Current children cumulated CPU time (s) 159.67
Current children cumulated vsize (Kb) 34960

[startup+170.015 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7558 0 0 0 16930 36 0 0 25 0 1 0 1855450286 33771520 7201 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8245 7201 145 145 0 8100 0
[pid=27249] vsize: 32980
Current children cumulated CPU time (s) 169.68
Current children cumulated vsize (Kb) 35104

[startup+180.016 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7594 0 0 0 17930 36 0 0 25 0 1 0 1855450286 33910784 7237 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8279 7237 145 145 0 8134 0
[pid=27249] vsize: 33116
Current children cumulated CPU time (s) 179.68
Current children cumulated vsize (Kb) 35240

[startup+190.017 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7660 0 0 0 18929 36 0 0 25 0 1 0 1855450286 34164736 7303 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8341 7303 145 145 0 8196 0
[pid=27249] vsize: 33364
Current children cumulated CPU time (s) 189.67
Current children cumulated vsize (Kb) 35488

[startup+200.016 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7694 0 0 0 19928 37 0 0 25 0 1 0 1855450286 34295808 7337 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8373 7337 145 145 0 8228 0
[pid=27249] vsize: 33492
Current children cumulated CPU time (s) 199.67
Current children cumulated vsize (Kb) 35616

[startup+210.018 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7736 0 0 0 20928 37 0 0 25 0 1 0 1855450286 34459648 7379 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8413 7379 145 145 0 8268 0
[pid=27249] vsize: 33652
Current children cumulated CPU time (s) 209.67
Current children cumulated vsize (Kb) 35776

[startup+220.018 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 7827 0 0 0 21927 37 0 0 25 0 1 0 1855450286 34811904 7470 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8499 7470 145 145 0 8354 0
[pid=27249] vsize: 33996
Current children cumulated CPU time (s) 219.66
Current children cumulated vsize (Kb) 36120

[startup+230.018 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 8207 0 0 0 22921 39 0 0 25 0 1 0 1855450286 36577280 7850 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 8930 7850 145 145 0 8785 0
[pid=27249] vsize: 35720
Current children cumulated CPU time (s) 229.62
Current children cumulated vsize (Kb) 37844

[startup+240.019 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 8712 0 0 0 23913 42 0 0 25 0 1 0 1855450286 38608896 8355 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 9426 8355 145 145 0 9281 0
[pid=27249] vsize: 37704
Current children cumulated CPU time (s) 239.57
Current children cumulated vsize (Kb) 39828

[startup+250.019 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 8922 0 0 0 24910 44 0 0 25 0 1 0 1855450286 39456768 8565 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 9633 8565 145 145 0 9488 0
[pid=27249] vsize: 38532
Current children cumulated CPU time (s) 249.56
Current children cumulated vsize (Kb) 40656

[startup+260.02 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 9067 0 0 0 25908 44 0 0 25 0 1 0 1855450286 40034304 8710 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 9774 8710 145 145 0 9629 0
[pid=27249] vsize: 39096
Current children cumulated CPU time (s) 259.54
Current children cumulated vsize (Kb) 41220

[startup+270.021 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 9144 0 0 0 26905 45 0 0 25 0 1 0 1855450286 40333312 8787 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 9847 8787 145 145 0 9702 0
[pid=27249] vsize: 39388
Current children cumulated CPU time (s) 269.52
Current children cumulated vsize (Kb) 41512

[startup+280.021 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 9270 0 0 0 27903 46 0 0 25 0 1 0 1855450286 40837120 8913 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 9970 8913 145 145 0 9825 0
[pid=27249] vsize: 39880
Current children cumulated CPU time (s) 279.51
Current children cumulated vsize (Kb) 42004

[startup+290.022 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 9490 0 0 0 28898 48 0 0 25 0 1 0 1855450286 41721856 9133 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 10186 9133 145 145 0 10041 0
[pid=27249] vsize: 40744
Current children cumulated CPU time (s) 289.48
Current children cumulated vsize (Kb) 42868

[startup+300.023 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 9588 0 0 0 29897 49 0 0 25 0 1 0 1855450286 42110976 9231 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 10281 9231 145 145 0 10136 0
[pid=27249] vsize: 41124
Current children cumulated CPU time (s) 299.48
Current children cumulated vsize (Kb) 43248

[startup+310.023 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 9714 0 0 0 30895 49 0 0 25 0 1 0 1855450286 42610688 9357 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 10403 9357 145 145 0 10258 0
[pid=27249] vsize: 41612
Current children cumulated CPU time (s) 309.46
Current children cumulated vsize (Kb) 43736

[startup+320.024 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10011 0 0 0 31889 52 0 0 25 0 1 0 1855450286 43798528 9654 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 10693 9654 145 145 0 10548 0
[pid=27249] vsize: 42772
Current children cumulated CPU time (s) 319.43
Current children cumulated vsize (Kb) 44896

[startup+330.024 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10140 0 0 0 32886 53 0 0 25 0 1 0 1855450286 44318720 9783 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 10820 9783 145 145 0 10675 0
[pid=27249] vsize: 43280
Current children cumulated CPU time (s) 329.41
Current children cumulated vsize (Kb) 45404

[startup+340.025 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10282 0 0 0 33883 55 0 0 25 0 1 0 1855450286 45408256 9925 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 11086 9925 145 145 0 10941 0
[pid=27249] vsize: 44344
Current children cumulated CPU time (s) 339.4
Current children cumulated vsize (Kb) 46468

[startup+350.025 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10422 0 0 0 34881 56 0 0 25 0 1 0 1855450286 45965312 10065 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 11222 10065 145 145 0 11077 0
[pid=27249] vsize: 44888
Current children cumulated CPU time (s) 349.39
Current children cumulated vsize (Kb) 47012

[startup+360.025 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10621 0 0 0 35877 58 0 0 25 0 1 0 1855450286 46800896 10264 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 11426 10264 145 145 0 11281 0
[pid=27249] vsize: 45704
Current children cumulated CPU time (s) 359.37
Current children cumulated vsize (Kb) 47828

[startup+370.026 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10699 0 0 0 36876 58 0 0 25 0 1 0 1855450286 47128576 10342 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 11506 10342 145 145 0 11361 0
[pid=27249] vsize: 46024
Current children cumulated CPU time (s) 369.36
Current children cumulated vsize (Kb) 48148

[startup+380.026 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10831 0 0 0 37874 60 0 0 25 0 1 0 1855450286 47669248 10474 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 11638 10474 145 145 0 11493 0
[pid=27249] vsize: 46552
Current children cumulated CPU time (s) 379.36
Current children cumulated vsize (Kb) 48676

[startup+390.029 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 10973 0 0 0 38871 62 0 0 25 0 1 0 1855450286 48234496 10616 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 11776 10616 145 145 0 11631 0
[pid=27249] vsize: 47104
Current children cumulated CPU time (s) 389.35
Current children cumulated vsize (Kb) 49228

[startup+400.03 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11079 0 0 0 39869 63 0 0 25 0 1 0 1855450286 48664576 10722 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 11881 10722 145 145 0 11736 0
[pid=27249] vsize: 47524
Current children cumulated CPU time (s) 399.34
Current children cumulated vsize (Kb) 49648

[startup+410.031 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11247 0 0 0 40866 65 0 0 25 0 1 0 1855450286 49336320 10890 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 12045 10890 145 145 0 11900 0
[pid=27249] vsize: 48180
Current children cumulated CPU time (s) 409.33
Current children cumulated vsize (Kb) 50304

[startup+420.031 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11402 0 0 0 41863 67 0 0 25 0 1 0 1855450286 49954816 11045 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 12196 11045 145 145 0 12051 0
[pid=27249] vsize: 48784
Current children cumulated CPU time (s) 419.32
Current children cumulated vsize (Kb) 50908

[startup+430.032 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11485 0 0 0 42861 68 0 0 25 0 1 0 1855450286 50282496 11128 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 12276 11128 145 145 0 12131 0
[pid=27249] vsize: 49104
Current children cumulated CPU time (s) 429.31
Current children cumulated vsize (Kb) 51228

[startup+440.033 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11547 0 0 0 43861 68 0 0 25 0 1 0 1855450286 50548736 11190 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 12341 11190 145 145 0 12196 0
[pid=27249] vsize: 49364
Current children cumulated CPU time (s) 439.31
Current children cumulated vsize (Kb) 51488

[startup+450.033 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11629 0 0 0 44860 69 0 0 25 0 1 0 1855450286 50876416 11272 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 12421 11272 145 145 0 12276 0
[pid=27249] vsize: 49684
Current children cumulated CPU time (s) 449.31
Current children cumulated vsize (Kb) 51808

[startup+460.034 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11709 0 0 0 45859 69 0 0 25 0 1 0 1855450286 51187712 11352 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 12497 11352 145 145 0 12352 0
[pid=27249] vsize: 49988
Current children cumulated CPU time (s) 459.3
Current children cumulated vsize (Kb) 52112

[startup+470.034 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11841 0 0 0 46856 71 0 0 25 0 1 0 1855450286 51703808 11484 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 12623 11484 145 145 0 12478 0
[pid=27249] vsize: 50492
Current children cumulated CPU time (s) 469.29
Current children cumulated vsize (Kb) 52616

[startup+480.035 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 11954 0 0 0 47854 72 0 0 25 0 1 0 1855450286 52154368 11597 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 12733 11597 145 145 0 12588 0
[pid=27249] vsize: 50932
Current children cumulated CPU time (s) 479.28
Current children cumulated vsize (Kb) 53056

[startup+490.036 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12119 0 0 0 48852 73 0 0 25 0 1 0 1855450286 52801536 11762 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 12891 11762 145 145 0 12746 0
[pid=27249] vsize: 51564
Current children cumulated CPU time (s) 489.27
Current children cumulated vsize (Kb) 53688

[startup+500.035 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12245 0 0 0 49849 75 0 0 25 0 1 0 1855450286 53329920 11888 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 13020 11888 145 145 0 12875 0
[pid=27249] vsize: 52080
Current children cumulated CPU time (s) 499.26
Current children cumulated vsize (Kb) 54204

[startup+510.037 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12336 0 0 0 50847 76 0 0 25 0 1 0 1855450286 53686272 11979 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 13107 11979 145 145 0 12962 0
[pid=27249] vsize: 52428
Current children cumulated CPU time (s) 509.25
Current children cumulated vsize (Kb) 54552

[startup+520.038 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12434 0 0 0 51844 76 0 0 25 0 1 0 1855450286 54067200 12077 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 13200 12077 145 145 0 13055 0
[pid=27249] vsize: 52800
Current children cumulated CPU time (s) 519.22
Current children cumulated vsize (Kb) 54924

[startup+530.037 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12501 0 0 0 52842 78 0 0 25 0 1 0 1855450286 54333440 12144 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 13265 12144 145 145 0 13120 0
[pid=27249] vsize: 53060
Current children cumulated CPU time (s) 529.22
Current children cumulated vsize (Kb) 55184

[startup+540.038 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12563 0 0 0 53842 78 0 0 25 0 1 0 1855450286 54571008 12206 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 13323 12206 145 145 0 13178 0
[pid=27249] vsize: 53292
Current children cumulated CPU time (s) 539.22
Current children cumulated vsize (Kb) 55416

[startup+550.039 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12665 0 0 0 54839 79 0 0 25 0 1 0 1855450286 54976512 12308 4294967295 134512640 135094434 3221224432 3221223088 134557984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 13422 12308 145 145 0 13277 0
[pid=27249] vsize: 53688
Current children cumulated CPU time (s) 549.2
Current children cumulated vsize (Kb) 55812

[startup+560.039 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12718 0 0 0 55838 79 0 0 25 0 1 0 1855450286 55181312 12361 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 13472 12361 145 145 0 13327 0
[pid=27249] vsize: 53888
Current children cumulated CPU time (s) 559.19
Current children cumulated vsize (Kb) 56012

[startup+570.04 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12792 0 0 0 56837 80 0 0 25 0 1 0 1855450286 55472128 12435 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 13543 12435 145 145 0 13398 0
[pid=27249] vsize: 54172
Current children cumulated CPU time (s) 569.19
Current children cumulated vsize (Kb) 56296

[startup+580.04 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 12933 0 0 0 57833 81 0 0 25 0 1 0 1855450286 56037376 12576 4294967295 134512640 135094434 3221224432 3221223044 134563163 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 13681 12576 145 145 0 13536 0
[pid=27249] vsize: 54724
Current children cumulated CPU time (s) 579.16
Current children cumulated vsize (Kb) 56848

[startup+590.041 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13054 0 0 0 58832 83 0 0 25 0 1 0 1855450286 56516608 12697 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 13798 12697 145 145 0 13653 0
[pid=27249] vsize: 55192
Current children cumulated CPU time (s) 589.17
Current children cumulated vsize (Kb) 57316

[startup+600.042 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13223 0 0 0 59829 84 0 0 25 0 1 0 1855450286 57167872 12866 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 13957 12866 145 145 0 13812 0
[pid=27249] vsize: 55828
Current children cumulated CPU time (s) 599.15
Current children cumulated vsize (Kb) 57952

[startup+610.043 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13340 0 0 0 60827 85 0 0 25 0 1 0 1855450286 57651200 12983 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 14075 12983 145 145 0 13930 0
[pid=27249] vsize: 56300
Current children cumulated CPU time (s) 609.14
Current children cumulated vsize (Kb) 58424

[startup+620.044 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13445 0 0 0 61826 86 0 0 25 0 1 0 1855450286 58060800 13088 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 14175 13088 145 145 0 14030 0
[pid=27249] vsize: 56700
Current children cumulated CPU time (s) 619.14
Current children cumulated vsize (Kb) 58824

[startup+630.045 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13550 0 0 0 62825 86 0 0 25 0 1 0 1855450286 58466304 13193 4294967295 134512640 135094434 3221224432 3221223044 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 14274 13193 145 145 0 14129 0
[pid=27249] vsize: 57096
Current children cumulated CPU time (s) 629.13
Current children cumulated vsize (Kb) 59220

[startup+640.045 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13691 0 0 0 63822 87 0 0 25 0 1 0 1855450286 59031552 13334 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 14412 13334 145 145 0 14267 0
[pid=27249] vsize: 57648
Current children cumulated CPU time (s) 639.11
Current children cumulated vsize (Kb) 59772

[startup+650.046 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13783 0 0 0 64821 87 0 0 25 0 1 0 1855450286 59404288 13426 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 14503 13426 145 145 0 14358 0
[pid=27249] vsize: 58012
Current children cumulated CPU time (s) 649.1
Current children cumulated vsize (Kb) 60136

[startup+660.047 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13871 0 0 0 65819 89 0 0 25 0 1 0 1855450286 59748352 13514 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 14587 13514 145 145 0 14442 0
[pid=27249] vsize: 58348
Current children cumulated CPU time (s) 659.1
Current children cumulated vsize (Kb) 60472

[startup+670.047 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 13959 0 0 0 66817 89 0 0 25 0 1 0 1855450286 60092416 13602 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 14671 13602 145 145 0 14526 0
[pid=27249] vsize: 58684
Current children cumulated CPU time (s) 669.08
Current children cumulated vsize (Kb) 60808

[startup+680.048 s]
Raw data (loadavg): 1.00 0.97 0.96 1/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) T 27245 27245 5299 0 -1 0 14068 0 0 0 67816 90 0 0 25 0 1 0 1855450286 60563456 13711 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27249/statm): 14786 13711 145 145 0 14641 0
[pid=27249] vsize: 59144
Current children cumulated CPU time (s) 679.08
Current children cumulated vsize (Kb) 61268

[startup+690.049 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 14172 0 0 0 68814 91 0 0 25 0 1 0 1855450286 60973056 13815 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 14886 13815 145 145 0 14741 0
[pid=27249] vsize: 59544
Current children cumulated CPU time (s) 689.07
Current children cumulated vsize (Kb) 61668

[startup+700.049 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 14283 0 0 0 69812 92 0 0 25 0 1 0 1855450286 61411328 13926 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 14993 13926 145 145 0 14848 0
[pid=27249] vsize: 59972
Current children cumulated CPU time (s) 699.06
Current children cumulated vsize (Kb) 62096

[startup+710.05 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 14480 0 0 0 70809 93 0 0 25 0 1 0 1855450286 62197760 14123 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 15185 14123 145 145 0 15040 0
[pid=27249] vsize: 60740
Current children cumulated CPU time (s) 709.04
Current children cumulated vsize (Kb) 62864

[startup+720.051 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 14544 0 0 0 71808 94 0 0 25 0 1 0 1855450286 63496192 14187 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 15502 14187 145 145 0 15357 0
[pid=27249] vsize: 62008
Current children cumulated CPU time (s) 719.04
Current children cumulated vsize (Kb) 64132

[startup+730.051 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 14646 0 0 0 72806 94 0 0 25 0 1 0 1855450286 63901696 14289 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 15601 14289 145 145 0 15456 0
[pid=27249] vsize: 62404
Current children cumulated CPU time (s) 729.02
Current children cumulated vsize (Kb) 64528

[startup+740.052 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 15154 0 0 0 73799 98 0 0 25 0 1 0 1855450286 65949696 14797 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 16101 14797 145 145 0 15956 0
[pid=27249] vsize: 64404
Current children cumulated CPU time (s) 738.99
Current children cumulated vsize (Kb) 66528

[startup+750.052 s]
Raw data (loadavg): 1.00 0.97 0.96 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 15493 0 0 0 74793 101 0 0 25 0 1 0 1855450286 67317760 15136 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 16435 15136 145 145 0 16290 0
[pid=27249] vsize: 65740
Current children cumulated CPU time (s) 748.96
Current children cumulated vsize (Kb) 67864

[startup+760.053 s]
Raw data (loadavg): 1.08 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) T 27245 27245 5299 0 -1 0 15563 0 0 0 75811 101 0 0 25 0 1 0 1855450286 67596288 15206 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/27249/statm): 16503 15206 145 145 0 16358 0
[pid=27249] vsize: 66012
Current children cumulated CPU time (s) 759.14
Current children cumulated vsize (Kb) 68136

[startup+771.337 s]
Raw data (loadavg): 1.07 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 15670 0 0 0 76809 102 0 0 25 0 1 0 1855450286 68022272 15313 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 16607 15313 145 145 0 16462 0
[pid=27249] vsize: 66428
Current children cumulated CPU time (s) 769.13
Current children cumulated vsize (Kb) 68552

[startup+781.338 s]
Raw data (loadavg): 1.06 0.99 0.97 3/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 15856 0 0 0 77806 104 0 0 25 0 1 0 1855450286 68767744 15499 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 16789 15499 145 145 0 16644 0
[pid=27249] vsize: 67156
Current children cumulated CPU time (s) 779.12
Current children cumulated vsize (Kb) 69280

[startup+791.339 s]
Raw data (loadavg): 1.05 0.99 0.97 3/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 15966 0 0 0 78803 105 0 0 25 0 1 0 1855450286 69201920 15609 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27249/statm): 16895 15609 145 145 0 16750 0
[pid=27249] vsize: 67580
Current children cumulated CPU time (s) 789.1
Current children cumulated vsize (Kb) 69704

[startup+801.339 s]
Raw data (loadavg): 1.04 0.99 0.97 3/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16130 0 0 0 79800 106 0 0 25 0 1 0 1855450286 69857280 15773 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 17055 15773 145 145 0 16910 0
[pid=27249] vsize: 68220
Current children cumulated CPU time (s) 799.08
Current children cumulated vsize (Kb) 70344

[startup+811.341 s]
Raw data (loadavg): 1.03 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16233 0 0 0 80799 107 0 0 25 0 1 0 1855450286 70262784 15876 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 17154 15876 145 145 0 17009 0
[pid=27249] vsize: 68616
Current children cumulated CPU time (s) 809.08
Current children cumulated vsize (Kb) 70740

[startup+821.341 s]
Raw data (loadavg): 1.03 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16345 0 0 0 81797 108 0 0 25 0 1 0 1855450286 70709248 15988 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 17263 15988 145 145 0 17118 0
[pid=27249] vsize: 69052
Current children cumulated CPU time (s) 819.07
Current children cumulated vsize (Kb) 71176

[startup+831.342 s]
Raw data (loadavg): 1.02 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16441 0 0 0 82795 109 0 0 25 0 1 0 1855450286 71090176 16084 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 17356 16084 145 145 0 17211 0
[pid=27249] vsize: 69424
Current children cumulated CPU time (s) 829.06
Current children cumulated vsize (Kb) 71548

[startup+841.343 s]
Raw data (loadavg): 1.02 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16518 0 0 0 83793 110 0 0 25 0 1 0 1855450286 71393280 16161 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 17430 16161 145 145 0 17285 0
[pid=27249] vsize: 69720
Current children cumulated CPU time (s) 839.05
Current children cumulated vsize (Kb) 71844

[startup+851.343 s]
Raw data (loadavg): 1.02 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16790 0 0 0 84789 112 0 0 25 0 1 0 1855450286 72482816 16433 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 17696 16433 145 145 0 17551 0
[pid=27249] vsize: 70784
Current children cumulated CPU time (s) 849.03
Current children cumulated vsize (Kb) 72908

[startup+861.344 s]
Raw data (loadavg): 1.01 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 16910 0 0 0 85786 113 0 0 25 0 1 0 1855450286 72957952 16553 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 17812 16553 145 145 0 17667 0
[pid=27249] vsize: 71248
Current children cumulated CPU time (s) 859.01
Current children cumulated vsize (Kb) 73372

[startup+871.345 s]
Raw data (loadavg): 1.01 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17034 0 0 0 86784 114 0 0 25 0 1 0 1855450286 73453568 16677 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27249/statm): 17933 16677 145 145 0 17788 0
[pid=27249] vsize: 71732
Current children cumulated CPU time (s) 869
Current children cumulated vsize (Kb) 73856

[startup+881.345 s]
Raw data (loadavg): 1.01 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17148 0 0 0 87781 115 0 0 25 0 1 0 1855450286 73904128 16791 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27249/statm): 18043 16791 145 145 0 17898 0
[pid=27249] vsize: 72172
Current children cumulated CPU time (s) 878.98
Current children cumulated vsize (Kb) 74296

[startup+891.347 s]
Raw data (loadavg): 1.01 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17246 0 0 0 88778 117 0 0 25 0 1 0 1855450286 74293248 16889 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27249/statm): 18138 16889 145 145 0 17993 0
[pid=27249] vsize: 72552
Current children cumulated CPU time (s) 888.97
Current children cumulated vsize (Kb) 74676

[startup+901.348 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17348 0 0 0 89776 117 0 0 25 0 1 0 1855450286 74698752 16991 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 18237 16991 145 145 0 18092 0
[pid=27249] vsize: 72948
Current children cumulated CPU time (s) 898.95
Current children cumulated vsize (Kb) 75072

[startup+911.348 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17423 0 0 0 90775 118 0 0 25 0 1 0 1855450286 74993664 17066 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 18309 17066 145 145 0 18164 0
[pid=27249] vsize: 73236
Current children cumulated CPU time (s) 908.95
Current children cumulated vsize (Kb) 75360

[startup+921.349 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17491 0 0 0 91774 119 0 0 25 0 1 0 1855450286 75264000 17134 4294967295 134512640 135094434 3221224432 3221223056 134557665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 18375 17134 145 145 0 18230 0
[pid=27249] vsize: 73500
Current children cumulated CPU time (s) 918.95
Current children cumulated vsize (Kb) 75624

[startup+931.35 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17631 0 0 0 92771 120 0 0 25 0 1 0 1855450286 75821056 17274 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 18511 17274 145 145 0 18366 0
[pid=27249] vsize: 74044
Current children cumulated CPU time (s) 928.93
Current children cumulated vsize (Kb) 76168

[startup+941.35 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17727 0 0 0 93770 120 0 0 25 0 1 0 1855450286 76197888 17370 4294967295 134512640 135094434 3221224432 3221223044 134563077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 18603 17370 145 145 0 18458 0
[pid=27249] vsize: 74412
Current children cumulated CPU time (s) 938.92
Current children cumulated vsize (Kb) 76536

[startup+951.351 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 17914 0 0 0 94766 122 0 0 25 0 1 0 1855450286 76947456 17557 4294967295 134512640 135094434 3221224432 3221223088 134557978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 18786 17557 145 145 0 18641 0
[pid=27249] vsize: 75144
Current children cumulated CPU time (s) 948.9
Current children cumulated vsize (Kb) 77268

[startup+961.352 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18114 0 0 0 95764 123 0 0 25 0 1 0 1855450286 77742080 17757 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 18980 17757 145 145 0 18835 0
[pid=27249] vsize: 75920
Current children cumulated CPU time (s) 958.89
Current children cumulated vsize (Kb) 78044

[startup+971.353 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18263 0 0 0 96762 124 0 0 25 0 1 0 1855450286 78336000 17906 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 19125 17906 145 145 0 18980 0
[pid=27249] vsize: 76500
Current children cumulated CPU time (s) 968.88
Current children cumulated vsize (Kb) 78624

[startup+981.354 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18413 0 0 0 97758 126 0 0 25 0 1 0 1855450286 78942208 18056 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 19273 18056 145 145 0 19128 0
[pid=27249] vsize: 77092
Current children cumulated CPU time (s) 978.86
Current children cumulated vsize (Kb) 79216

[startup+991.355 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18545 0 0 0 98753 129 0 0 25 0 1 0 1855450286 79450112 18188 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 19397 18188 145 145 0 19252 0
[pid=27249] vsize: 77588
Current children cumulated CPU time (s) 988.84
Current children cumulated vsize (Kb) 79712

[startup+1001.36 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18684 0 0 0 99751 130 0 0 25 0 1 0 1855450286 80048128 18327 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 19543 18327 145 145 0 19398 0
[pid=27249] vsize: 78172
Current children cumulated CPU time (s) 998.83
Current children cumulated vsize (Kb) 80296

[startup+1011.36 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18816 0 0 0 100749 131 0 0 25 0 1 0 1855450286 80625664 18459 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 19684 18459 145 145 0 19539 0
[pid=27249] vsize: 78736
Current children cumulated CPU time (s) 1008.82
Current children cumulated vsize (Kb) 80860

[startup+1021.36 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 18964 0 0 0 101748 132 0 0 25 0 1 0 1855450286 81268736 18607 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 19841 18607 145 145 0 19696 0
[pid=27249] vsize: 79364
Current children cumulated CPU time (s) 1018.82
Current children cumulated vsize (Kb) 81488

[startup+1031.36 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 19095 0 0 0 102745 134 0 0 25 0 1 0 1855450286 81797120 18738 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 19970 18738 145 145 0 19825 0
[pid=27249] vsize: 79880
Current children cumulated CPU time (s) 1028.81
Current children cumulated vsize (Kb) 82004

[startup+1041.36 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 19220 0 0 0 103742 135 0 0 25 0 1 0 1855450286 82292736 18863 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 20091 18863 145 145 0 19946 0
[pid=27249] vsize: 80364
Current children cumulated CPU time (s) 1038.79
Current children cumulated vsize (Kb) 82488

[startup+1051.36 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 19377 0 0 0 104740 136 0 0 25 0 1 0 1855450286 82952192 19020 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 20252 19020 145 145 0 20107 0
[pid=27249] vsize: 81008
Current children cumulated CPU time (s) 1048.78
Current children cumulated vsize (Kb) 83132

[startup+1061.36 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 19534 0 0 0 105738 137 0 0 25 0 1 0 1855450286 83582976 19177 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 20406 19177 145 145 0 20261 0
[pid=27249] vsize: 81624
Current children cumulated CPU time (s) 1058.77
Current children cumulated vsize (Kb) 83748

[startup+1071.36 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 19643 0 0 0 106736 138 0 0 25 0 1 0 1855450286 84013056 19286 4294967295 134512640 135094434 3221224432 3221223088 134558181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 20511 19286 145 145 0 20366 0
[pid=27249] vsize: 82044
Current children cumulated CPU time (s) 1068.76
Current children cumulated vsize (Kb) 84168

[startup+1081.36 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 19732 0 0 0 107734 138 0 0 25 0 1 0 1855450286 84365312 19375 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 20597 19375 145 145 0 20452 0
[pid=27249] vsize: 82388
Current children cumulated CPU time (s) 1078.74
Current children cumulated vsize (Kb) 84512

[startup+1091.36 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20014 0 0 0 108728 141 0 0 21 0 1 0 1855450286 85508096 19657 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 20876 19657 145 145 0 20731 0
[pid=27249] vsize: 83504
Current children cumulated CPU time (s) 1088.71
Current children cumulated vsize (Kb) 85628

[startup+1101.36 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 109726 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223024 134551465 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1098.71
Current children cumulated vsize (Kb) 86288

[startup+1111.37 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 110726 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223072 134562149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1108.71
Current children cumulated vsize (Kb) 86288

[startup+1121.37 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 111726 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1118.71
Current children cumulated vsize (Kb) 86288

[startup+1131.37 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 112726 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1128.71
Current children cumulated vsize (Kb) 86288

[startup+1141.37 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 113726 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1138.71
Current children cumulated vsize (Kb) 86288

[startup+1151.37 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 114727 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1148.72
Current children cumulated vsize (Kb) 86288

[startup+1161.37 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 115727 143 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1158.72
Current children cumulated vsize (Kb) 86288

[startup+1171.37 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 116727 144 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1168.73
Current children cumulated vsize (Kb) 86288

[startup+1181.37 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 117727 144 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1178.73
Current children cumulated vsize (Kb) 86288

[startup+1191.37 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 118727 144 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223056 134557568 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1188.73
Current children cumulated vsize (Kb) 86288

[startup+1201.37 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 119727 144 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1198.73
Current children cumulated vsize (Kb) 86288

[startup+1211.37 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 120727 144 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1208.73
Current children cumulated vsize (Kb) 86288



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1211.37 s]
Raw data (loadavg): 1.00 0.99 0.97 2/57 27251
Raw data (/proc/27245/stat): 27245 (minisat+_script) S 27244 27245 5299 0 -1 0 289 239 0 0 0 1 0 1 21 0 1 0 1855450281 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/27245/statm): 531 226 485 147 0 384 0
[pid=27245] vsize: 2124
Raw data (/proc/27249/stat): 27249 (minisat+_64-bit) R 27245 27245 5299 0 -1 0 20182 0 0 0 120727 144 0 0 25 0 1 0 1855450286 86183936 19825 4294967295 134512640 135094434 3221224432 3221223088 134558033 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/27249/statm): 21041 19825 145 145 0 20896 0
[pid=27249] vsize: 84164
Current children cumulated CPU time (s) 1208.73
Current children cumulated vsize (Kb) 86288

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

Child status: 0
Real time (s): 1211.65
CPU time (s): 1208.76
CPU user time (s): 1207.27
CPU system time (s): 1.48477
CPU usage (%): 99.7609
Max. virtual memory (cumulated for all children) (Kb): 86288

Verifier Data

ERROR: no interpretation found !