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/miplib3/normalized-mps-v2-13-7-pp08aCUTS.opb
MD5SUMfa6454a9831f2da4180d8bfab7c0a21b
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 constraints310
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints310
Minimum length of a constraint14
Maximum length of a constraint123

Trace number 6237

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        913760 kB
Buffers:         21360 kB
Cached:          70156 kB
SwapCached:        692 kB
Active:          26232 kB
Inactive:        67840 kB
HighTotal:      131008 kB
HighFree:        58548 kB
LowTotal:       903652 kB
LowFree:        855212 kB
SwapTotal:     2097892 kB
SwapFree:      2096628 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            21052 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 05:03:54 (client local time) WITH STATUS 0 IN 1208.21 SECONDS
stats: 3403 7 1208.21 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 ---[ 437]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 436]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 435]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 434]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 432]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 431]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 428]---> BDD-cost:  158
c ---[ 426]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 420]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 418]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 416]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 414]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 412]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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 ---[ 408]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 406]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 404]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 398]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 392]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 390]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 388]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 382]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> BDD-cost:  158
c ---[ 378]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 376]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 364]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 360]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 358]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 354]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 352]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 348]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 346]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 344]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 342]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 340]---> Sorter-cost: 1179     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 ---[ 336]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 334]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> BDD-cost:  154
c ---[ 330]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 301]---> BDD-cost:    9
c ---[ 300]---> BDD-cost:    9
c ---[ 299]---> BDD-cost:    9
c ---[ 298]---> BDD-cost:    6
c ---[ 297]---> BDD-cost:    6
c ---[ 296]---> BDD-cost:    6
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    8
c ---[ 293]---> BDD-cost:   19
c ---[ 292]---> BDD-cost:   19
c ---[ 291]---> BDD-cost:   19
c ---[ 290]---> BDD-cost:   19
c ---[ 289]---> BDD-cost:   19
c ---[ 288]---> BDD-cost:   19
c ---[ 287]---> BDD-cost:   19
c ---[ 286]---> BDD-cost:   19
c ---[ 285]---> BDD-cost:    9
c ---[ 284]---> BDD-cost:    9
c ---[ 283]---> BDD-cost:    9
c ---[ 282]---> BDD-cost:    6
c ---[ 281]---> BDD-cost:    6
c ---[ 280]---> BDD-cost:    6
c ---[ 279]---> BDD-cost:    6
c ---[ 278]---> BDD-cost:   23
c ---[ 277]---> BDD-cost:    9
c ---[ 276]---> BDD-cost:    9
c ---[ 275]---> BDD-cost:    9
c ---[ 274]---> BDD-cost:    6
c ---[ 273]---> BDD-cost:    6
c ---[ 272]---> BDD-cost:    6
c ---[ 271]---> BDD-cost:    6
c ---[ 270]---> BDD-cost:   23
c ---[ 269]---> BDD-cost:    4
c ---[ 268]---> BDD-cost:    4
c ---[ 267]---> BDD-cost:    4
c ---[ 266]---> BDD-cost:    4
c ---[ 265]---> BDD-cost:    4
c ---[ 264]---> BDD-cost:    4
c ---[ 263]---> BDD-cost:    4
c ---[ 262]---> BDD-cost:    4
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:    9
c ---[ 258]---> BDD-cost:    6
c ---[ 257]---> BDD-cost:    6
c ---[ 256]---> BDD-cost:    6
c ---[ 255]---> BDD-cost:    6
c ---[ 254]---> BDD-cost:    6
c ---[ 253]---> BDD-cost:   19
c ---[ 252]---> BDD-cost:   19
c ---[ 251]---> BDD-cost:   19
c ---[ 250]---> BDD-cost:   19
c ---[ 249]---> BDD-cost:   19
c ---[ 248]---> BDD-cost:   19
c ---[ 247]---> BDD-cost:   19
c ---[ 246]---> BDD-cost:   19
c ---[ 245]---> BDD-cost:    6
c ---[ 244]---> BDD-cost:    6
c ---[ 243]---> BDD-cost:    6
c ---[ 242]---> BDD-cost:    6
c ---[ 241]---> BDD-cost:    6
c ---[ 240]---> BDD-cost:    6
c ---[ 239]---> BDD-cost:    6
c ---[ 238]---> BDD-cost:    6
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:  167
c ---[ 107]---> BDD-cost:   59
c ---[ 106]---> BDD-cost:   38
c ---[ 105]---> BDD-cost:  149
c ---[ 104]---> BDD-cost:   35
c ---[ 103]---> BDD-cost:  152
c ---[ 102]---> BDD-cost:   35
c ---[ 101]---> BDD-cost:  152
c ---[ 100]---> BDD-cost:   38
c ---[  99]---> BDD-cost:  149
c ---[  98]---> BDD-cost:    4
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:   62
c ---[  95]---> BDD-cost:   73
c ---[  94]---> BDD-cost:    3
c ---[  93]---> BDD-cost:   62
c ---[  92]---> BDD-cost:   41
c ---[  91]---> BDD-cost:  158
c ---[  90]---> BDD-cost:   45
c ---[  89]---> BDD-cost:  182
c ---[  88]---> BDD-cost:   40
c ---[  87]---> BDD-cost:  203
c ---[  86]---> BDD-cost:  173
c ---[  85]---> BDD-cost:   35
c ---[  84]---> BDD-cost:  164
c ---[  83]---> BDD-cost:   41
c ---[  82]---> BDD-cost:  158
c ---[  81]---> BDD-cost:    5
c ---[  80]---> BDD-cost:   70
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:   65
c ---[  77]---> BDD-cost:   45
c ---[  76]---> BDD-cost:   45
c ---[  75]---> BDD-cost:  194
c ---[  74]---> BDD-cost:   48
c ---[  73]---> BDD-cost:  191
c ---[  72]---> BDD-cost:   41
c ---[  71]---> BDD-cost:  170
c ---[  70]---> BDD-cost:   44
c ---[  69]---> BDD-cost:  167
c ---[  68]---> BDD-cost:   50
c ---[  67]---> BDD-cost:  203
c ---[  66]---> BDD-cost:    3
c ---[  65]---> BDD-cost:  194
c ---[  64]---> BDD-cost:   61
c ---[  63]---> BDD-cost:   48
c ---[  62]---> BDD-cost:  191
c ---[  61]---> BDD-cost:   48
c ---[  60]---> BDD-cost:  191
c ---[  59]---> BDD-cost:   55
c ---[  58]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> BDD-cost:   47
c ---[  56]---> BDD-cost:  161
c ---[  55]---> BDD-cost:   50
c ---[  54]---> BDD-cost:   48
c ---[  53]---> BDD-cost:  203
c ---[  52]---> BDD-cost:   48
c ---[  51]---> BDD-cost:  191
c ---[  50]---> BDD-cost:    5
c ---[  49]---> BDD-cost:   73
c ---[  48]---> BDD-cost:    5
c ---[  47]---> BDD-cost:   70
c ---[  46]---> BDD-cost:   38
c ---[  45]---> BDD-cost:  161
c ---[  44]---> BDD-cost:   41
c ---[  43]---> BDD-cost:  191
c ---[  42]---> BDD-cost:  158
c ---[  41]---> BDD-cost:   35
c ---[  40]---> BDD-cost:  164
c ---[  39]---> BDD-cost:   35
c ---[  38]---> BDD-cost:  164
c ---[  37]---> BDD-cost:   38
c ---[  36]---> BDD-cost:  161
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:   64
c ---[  33]---> BDD-cost:    6
c ---[  32]---> BDD-cost:   38
c ---[  31]---> BDD-cost:   78
c ---[  30]---> BDD-cost:   41
c ---[  29]---> BDD-cost:  170
c ---[  28]---> BDD-cost:   41
c ---[  27]---> BDD-cost:  170
c ---[  26]---> BDD-cost:   41
c ---[  25]---> BDD-cost:  170
c ---[  24]---> BDD-cost:   48
c ---[  23]---> BDD-cost:  191
c ---[  22]---> BDD-cost:   38
c ---[  21]---> BDD-cost:  173
c ---[  20]---> BDD-cost:  173
c ---[  19]---> BDD-cost:   41
c ---[  18]---> BDD-cost:  170
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:   75
c ---[  15]---> BDD-cost:   38
c ---[  14]---> BDD-cost:  161
c ---[  13]---> BDD-cost:   45
c ---[  12]---> BDD-cost:  182
c ---[  11]---> BDD-cost:   35
c ---[  10]---> BDD-cost:   44
c ---[   9]---> BDD-cost:  164
c ---[   8]---> BDD-cost:   38
c ---[   7]---> BDD-cost:  161
c ---[   6]---> BDD-cost:   43
c ---[   5]---> BDD-cost:  170
c ---[   4]---> BDD-cost:   41
c ---[   3]---> BDD-cost:  158
c ---[   2]---> BDD-cost:    3
c ---[   1]---> BDD-cost:   60
c ---[   0]---> BDD-cost:    3
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 |       100 |  215317   519326 |   78993      85      297     3.5 |  4.798 % |
c |       252 |  215250   519177 |   86892     230     1279     5.6 |  4.822 % |
c |       477 |  215017   518658 |   95581     419     1998     4.8 |  4.904 % |
c |       814 |  214690   517929 |  105139     706     3191     4.5 |  5.022 % |
c |      1320 |  214206   516851 |  115653    1147     4686     4.1 |  5.197 % |
c |      2081 |  213777   515892 |  127219    1851     7475     4.0 |  5.346 % |
c |      3220 |  213265   514751 |  139941    2913    13437     4.6 |  5.528 % |
c |      4928 |  212597   513260 |  153935    4530    19792     4.4 |  5.766 % |
c |      7491 |  211927   511762 |  169328    7017    31746     4.5 |  6.002 % |
c |     11335 |  210797   509228 |  186261   10729    52175     4.9 |  6.392 % |
c |     17102 |  209752   506890 |  204888   16365    92151     5.6 |  6.757 % |
c |     25751 |  208643   504413 |  225376   24862   148831     6.0 |  7.149 % |
c |     38725 |  208052   503090 |  247914   37757   317212     8.4 |  7.355 % |
c |     58188 |  207566   501999 |  272705   57154   747689    13.1 |  7.526 % |
c |     87380 |  206308   499177 |  299976   86159  1393567    16.2 |  7.970 % |
c |    131171 |  206005   498499 |  329974  129904  2588408    19.9 |  8.077 % |
c |    196857 |  205794   498026 |  362971  195554  4238870    21.7 |  8.152 % |
c |    295383 |  205426   497203 |  399268  294027  7129688    24.2 |  8.284 % |

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

[startup+10.005 s]
Raw data (loadavg): 0.93 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 7053 0 0 0 939 28 0 0 25 0 1 0 1855734170 31723520 6691 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 7745 6691 145 145 0 7600 0
[pid=28242] vsize: 30980
Current children cumulated CPU time (s) 9.67
Current children cumulated vsize (Kb) 33104

[startup+20.0068 s]
Raw data (loadavg): 0.94 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 7091 0 0 0 1938 29 0 0 25 0 1 0 1855734170 31870976 6729 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 7781 6729 145 145 0 7636 0
[pid=28242] vsize: 31124
Current children cumulated CPU time (s) 19.67
Current children cumulated vsize (Kb) 33248

[startup+30.0076 s]
Raw data (loadavg): 0.95 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 7137 0 0 0 2937 29 0 0 25 0 1 0 1855734170 32014336 6775 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 7816 6775 145 145 0 7671 0
[pid=28242] vsize: 31264
Current children cumulated CPU time (s) 29.66
Current children cumulated vsize (Kb) 33388

[startup+40.0084 s]
Raw data (loadavg): 0.95 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 7169 0 0 0 3936 29 0 0 25 0 1 0 1855734170 32161792 6807 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 7852 6807 145 145 0 7707 0
[pid=28242] vsize: 31408
Current children cumulated CPU time (s) 39.65
Current children cumulated vsize (Kb) 33532

[startup+50.0093 s]
Raw data (loadavg): 0.96 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 7218 0 0 0 4935 29 0 0 25 0 1 0 1855734170 32337920 6856 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 7895 6856 145 145 0 7750 0
[pid=28242] vsize: 31580
Current children cumulated CPU time (s) 49.64
Current children cumulated vsize (Kb) 33704

[startup+60.0101 s]
Raw data (loadavg): 0.97 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 7279 0 0 0 5935 30 0 0 25 0 1 0 1855734170 32616448 6917 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 7963 6917 145 145 0 7818 0
[pid=28242] vsize: 31852
Current children cumulated CPU time (s) 59.65
Current children cumulated vsize (Kb) 33976

[startup+70.0109 s]
Raw data (loadavg): 0.97 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 7330 0 0 0 6934 30 0 0 25 0 1 0 1855734170 32808960 6968 4294967295 134512640 135094434 3221224432 3221223072 134562128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 8010 6968 145 145 0 7865 0
[pid=28242] vsize: 32040
Current children cumulated CPU time (s) 69.64
Current children cumulated vsize (Kb) 34164

[startup+80.0117 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 7359 0 0 0 7933 31 0 0 25 0 1 0 1855734170 32915456 6997 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 8036 6997 145 145 0 7891 0
[pid=28242] vsize: 32144
Current children cumulated CPU time (s) 79.64
Current children cumulated vsize (Kb) 34268

[startup+90.0126 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 7434 0 0 0 8932 31 0 0 25 0 1 0 1855734170 33202176 7072 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 8106 7072 145 145 0 7961 0
[pid=28242] vsize: 32424
Current children cumulated CPU time (s) 89.63
Current children cumulated vsize (Kb) 34548

[startup+100.013 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 7485 0 0 0 9932 31 0 0 25 0 1 0 1855734170 33394688 7123 4294967295 134512640 135094434 3221224432 3221223044 134563110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 8153 7123 145 145 0 8008 0
[pid=28242] vsize: 32612
Current children cumulated CPU time (s) 99.63
Current children cumulated vsize (Kb) 34736

[startup+110.015 s]
Raw data (loadavg): 0.98 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 7631 0 0 0 10930 33 0 0 25 0 1 0 1855734170 34103296 7269 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 8326 7269 145 145 0 8181 0
[pid=28242] vsize: 33304
Current children cumulated CPU time (s) 109.63
Current children cumulated vsize (Kb) 35428

[startup+120.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 7762 0 0 0 11928 34 0 0 25 0 1 0 1855734170 34619392 7400 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 8452 7400 145 145 0 8307 0
[pid=28242] vsize: 33808
Current children cumulated CPU time (s) 119.62
Current children cumulated vsize (Kb) 35932

[startup+130.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 8051 0 0 0 12922 36 0 0 25 0 1 0 1855734170 35770368 7689 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 8733 7689 145 145 0 8588 0
[pid=28242] vsize: 34932
Current children cumulated CPU time (s) 129.58
Current children cumulated vsize (Kb) 37056

[startup+140.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 8287 0 0 0 13919 37 0 0 25 0 1 0 1855734170 36708352 7925 4294967295 134512640 135094434 3221224432 3221223072 134562076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 8962 7925 145 145 0 8817 0
[pid=28242] vsize: 35848
Current children cumulated CPU time (s) 139.56
Current children cumulated vsize (Kb) 37972

[startup+150.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 8568 0 0 0 14913 39 0 0 25 0 1 0 1855734170 37830656 8206 4294967295 134512640 135094434 3221224432 3221223088 134550385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 9236 8206 145 145 0 9091 0
[pid=28242] vsize: 36944
Current children cumulated CPU time (s) 149.52
Current children cumulated vsize (Kb) 39068

[startup+160.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 8634 0 0 0 15911 40 0 0 25 0 1 0 1855734170 38350848 8272 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 9363 8272 145 145 0 9218 0
[pid=28242] vsize: 37452
Current children cumulated CPU time (s) 159.51
Current children cumulated vsize (Kb) 39576

[startup+170.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 8729 0 0 0 16909 41 0 0 25 0 1 0 1855734170 38727680 8367 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 9455 8367 145 145 0 9310 0
[pid=28242] vsize: 37820
Current children cumulated CPU time (s) 169.5
Current children cumulated vsize (Kb) 39944

[startup+180.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 8868 0 0 0 17907 42 0 0 25 0 1 0 1855734170 39272448 8506 4294967295 134512640 135094434 3221224432 3221223056 134557593 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 9588 8506 145 145 0 9443 0
[pid=28242] vsize: 38352
Current children cumulated CPU time (s) 179.49
Current children cumulated vsize (Kb) 40476

[startup+190.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 9029 0 0 0 18905 43 0 0 25 0 1 0 1855734170 39899136 8667 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 9741 8667 145 145 0 9596 0
[pid=28242] vsize: 38964
Current children cumulated CPU time (s) 189.48
Current children cumulated vsize (Kb) 41088

[startup+200.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 9157 0 0 0 19903 44 0 0 25 0 1 0 1855734170 40411136 8795 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 9866 8795 145 145 0 9721 0
[pid=28242] vsize: 39464
Current children cumulated CPU time (s) 199.47
Current children cumulated vsize (Kb) 41588

[startup+210.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 9344 0 0 0 20899 46 0 0 25 0 1 0 1855734170 41160704 8982 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 10049 8982 145 145 0 9904 0
[pid=28242] vsize: 40196
Current children cumulated CPU time (s) 209.45
Current children cumulated vsize (Kb) 42320

[startup+220.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 9445 0 0 0 21897 47 0 0 25 0 1 0 1855734170 41558016 9083 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 10146 9083 145 145 0 10001 0
[pid=28242] vsize: 40584
Current children cumulated CPU time (s) 219.44
Current children cumulated vsize (Kb) 42708

[startup+230.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 9641 0 0 0 22892 49 0 0 25 0 1 0 1855734170 42340352 9279 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 10337 9279 145 145 0 10192 0
[pid=28242] vsize: 41348
Current children cumulated CPU time (s) 229.41
Current children cumulated vsize (Kb) 43472

[startup+240.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 9783 0 0 0 23891 50 0 0 25 0 1 0 1855734170 42901504 9421 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 10474 9421 145 145 0 10329 0
[pid=28242] vsize: 41896
Current children cumulated CPU time (s) 239.41
Current children cumulated vsize (Kb) 44020

[startup+250.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 9994 0 0 0 24886 52 0 0 25 0 1 0 1855734170 43745280 9632 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 10680 9632 145 145 0 10535 0
[pid=28242] vsize: 42720
Current children cumulated CPU time (s) 249.38
Current children cumulated vsize (Kb) 44844

[startup+260.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 10069 0 0 0 25886 52 0 0 25 0 1 0 1855734170 44040192 9707 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 10752 9707 145 145 0 10607 0
[pid=28242] vsize: 43008
Current children cumulated CPU time (s) 259.38
Current children cumulated vsize (Kb) 45132

[startup+270.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 10298 0 0 0 26881 55 0 0 25 0 1 0 1855734170 44957696 9936 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 10976 9936 145 145 0 10831 0
[pid=28242] vsize: 43904
Current children cumulated CPU time (s) 269.36
Current children cumulated vsize (Kb) 46028

[startup+280.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 10530 0 0 0 27877 56 0 0 25 0 1 0 1855734170 45895680 10168 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 11205 10168 145 145 0 11060 0
[pid=28242] vsize: 44820
Current children cumulated CPU time (s) 279.33
Current children cumulated vsize (Kb) 46944

[startup+290.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 10691 0 0 0 28874 57 0 0 25 0 1 0 1855734170 46542848 10329 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 11363 10329 145 145 0 11218 0
[pid=28242] vsize: 45452
Current children cumulated CPU time (s) 289.31
Current children cumulated vsize (Kb) 47576

[startup+300.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 10825 0 0 0 29872 59 0 0 25 0 1 0 1855734170 47075328 10463 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 11493 10463 145 145 0 11348 0
[pid=28242] vsize: 45972
Current children cumulated CPU time (s) 299.31
Current children cumulated vsize (Kb) 48096

[startup+310.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 10915 0 0 0 30871 59 0 0 25 0 1 0 1855734170 47955968 10553 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 11708 10553 145 145 0 11563 0
[pid=28242] vsize: 46832
Current children cumulated CPU time (s) 309.3
Current children cumulated vsize (Kb) 48956

[startup+320.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 11041 0 0 0 31868 61 0 0 25 0 1 0 1855734170 48467968 10679 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 11833 10679 145 145 0 11688 0
[pid=28242] vsize: 47332
Current children cumulated CPU time (s) 319.29
Current children cumulated vsize (Kb) 49456

[startup+330.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 11151 0 0 0 32866 62 0 0 25 0 1 0 1855734170 48885760 10789 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 11935 10789 145 145 0 11790 0
[pid=28242] vsize: 47740
Current children cumulated CPU time (s) 329.28
Current children cumulated vsize (Kb) 49864

[startup+340.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 11276 0 0 0 33864 63 0 0 25 0 1 0 1855734170 49393664 10914 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 12059 10914 145 145 0 11914 0
[pid=28242] vsize: 48236
Current children cumulated CPU time (s) 339.27
Current children cumulated vsize (Kb) 50360

[startup+350.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 11418 0 0 0 34862 64 0 0 25 0 1 0 1855734170 49983488 11056 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 12203 11056 145 145 0 12058 0
[pid=28242] vsize: 48812
Current children cumulated CPU time (s) 349.26
Current children cumulated vsize (Kb) 50936

[startup+360.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 11555 0 0 0 35860 65 0 0 25 0 1 0 1855734170 50556928 11193 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 12343 11193 145 145 0 12198 0
[pid=28242] vsize: 49372
Current children cumulated CPU time (s) 359.25
Current children cumulated vsize (Kb) 51496

[startup+370.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 11668 0 0 0 36858 66 0 0 25 0 1 0 1855734170 51027968 11306 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 12458 11306 145 145 0 12313 0
[pid=28242] vsize: 49832
Current children cumulated CPU time (s) 369.24
Current children cumulated vsize (Kb) 51956

[startup+380.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 11754 0 0 0 37857 66 0 0 25 0 1 0 1855734170 51359744 11392 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 12539 11392 145 145 0 12394 0
[pid=28242] vsize: 50156
Current children cumulated CPU time (s) 379.23
Current children cumulated vsize (Kb) 52280

[startup+390.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 11855 0 0 0 38857 67 0 0 25 0 1 0 1855734170 51765248 11493 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 12638 11493 145 145 0 12493 0
[pid=28242] vsize: 50552
Current children cumulated CPU time (s) 389.24
Current children cumulated vsize (Kb) 52676

[startup+400.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 12001 0 0 0 39854 68 0 0 25 0 1 0 1855734170 52355072 11639 4294967295 134512640 135094434 3221224432 3221223088 134558295 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 12782 11639 145 145 0 12637 0
[pid=28242] vsize: 51128
Current children cumulated CPU time (s) 399.22
Current children cumulated vsize (Kb) 53252

[startup+410.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 12080 0 0 0 40853 68 0 0 25 0 1 0 1855734170 52670464 11718 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 12859 11718 145 145 0 12714 0
[pid=28242] vsize: 51436
Current children cumulated CPU time (s) 409.21
Current children cumulated vsize (Kb) 53560

[startup+420.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 12146 0 0 0 41851 69 0 0 25 0 1 0 1855734170 52928512 11784 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 12922 11784 145 145 0 12777 0
[pid=28242] vsize: 51688
Current children cumulated CPU time (s) 419.2
Current children cumulated vsize (Kb) 53812

[startup+430.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 12218 0 0 0 42851 69 0 0 25 0 1 0 1855734170 53207040 11856 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 12990 11856 145 145 0 12845 0
[pid=28242] vsize: 51960
Current children cumulated CPU time (s) 429.2
Current children cumulated vsize (Kb) 54084

[startup+440.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 12289 0 0 0 43849 70 0 0 25 0 1 0 1855734170 53485568 11927 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 13058 11927 145 145 0 12913 0
[pid=28242] vsize: 52232
Current children cumulated CPU time (s) 439.19
Current children cumulated vsize (Kb) 54356

[startup+450.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 12463 0 0 0 44846 71 0 0 25 0 1 0 1855734170 54206464 12101 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 13234 12101 145 145 0 13089 0
[pid=28242] vsize: 52936
Current children cumulated CPU time (s) 449.17
Current children cumulated vsize (Kb) 55060

[startup+460.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 12602 0 0 0 45845 72 0 0 25 0 1 0 1855734170 54771712 12240 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 13372 12240 145 145 0 13227 0
[pid=28242] vsize: 53488
Current children cumulated CPU time (s) 459.17
Current children cumulated vsize (Kb) 55612

[startup+470.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 12736 0 0 0 46842 73 0 0 25 0 1 0 1855734170 55291904 12374 4294967295 134512640 135094434 3221224432 3221223104 134556485 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 13499 12374 145 145 0 13354 0
[pid=28242] vsize: 53996
Current children cumulated CPU time (s) 469.15
Current children cumulated vsize (Kb) 56120

[startup+480.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 12985 0 0 0 47839 75 0 0 25 0 1 0 1855734170 56299520 12623 4294967295 134512640 135094434 3221224432 3221223024 134557419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 13745 12623 145 145 0 13600 0
[pid=28242] vsize: 54980
Current children cumulated CPU time (s) 479.14
Current children cumulated vsize (Kb) 57104

[startup+490.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 13124 0 0 0 48836 76 0 0 25 0 1 0 1855734170 56848384 12762 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 13879 12762 145 145 0 13734 0
[pid=28242] vsize: 55516
Current children cumulated CPU time (s) 489.12
Current children cumulated vsize (Kb) 57640

[startup+500.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 13184 0 0 0 49835 76 0 0 25 0 1 0 1855734170 57077760 12822 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 13935 12822 145 145 0 13790 0
[pid=28242] vsize: 55740
Current children cumulated CPU time (s) 499.11
Current children cumulated vsize (Kb) 57864

[startup+510.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 13302 0 0 0 50833 77 0 0 25 0 1 0 1855734170 57561088 12940 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 14053 12940 145 145 0 13908 0
[pid=28242] vsize: 56212
Current children cumulated CPU time (s) 509.1
Current children cumulated vsize (Kb) 58336

[startup+520.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 13408 0 0 0 51832 78 0 0 25 0 1 0 1855734170 57982976 13046 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 14156 13046 145 145 0 14011 0
[pid=28242] vsize: 56624
Current children cumulated CPU time (s) 519.1
Current children cumulated vsize (Kb) 58748

[startup+530.053 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 13498 0 0 0 52829 80 0 0 25 0 1 0 1855734170 58347520 13136 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 14245 13136 145 145 0 14100 0
[pid=28242] vsize: 56980
Current children cumulated CPU time (s) 529.09
Current children cumulated vsize (Kb) 59104

[startup+540.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 13610 0 0 0 53827 82 0 0 25 0 1 0 1855734170 58810368 13248 4294967295 134512640 135094434 3221224432 3221223088 134558135 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 14358 13248 145 145 0 14213 0
[pid=28242] vsize: 57432
Current children cumulated CPU time (s) 539.09
Current children cumulated vsize (Kb) 59556

[startup+550.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 13717 0 0 0 54825 83 0 0 25 0 1 0 1855734170 59273216 13355 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 14471 13355 145 145 0 14326 0
[pid=28242] vsize: 57884
Current children cumulated CPU time (s) 549.08
Current children cumulated vsize (Kb) 60008

[startup+560.056 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 13780 0 0 0 55824 83 0 0 25 0 1 0 1855734170 59514880 13418 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 14530 13418 145 145 0 14385 0
[pid=28242] vsize: 58120
Current children cumulated CPU time (s) 559.07
Current children cumulated vsize (Kb) 60244

[startup+570.057 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 13910 0 0 0 56822 84 0 0 25 0 1 0 1855734170 60039168 13548 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 14658 13548 145 145 0 14513 0
[pid=28242] vsize: 58632
Current children cumulated CPU time (s) 569.06
Current children cumulated vsize (Kb) 60756

[startup+580.058 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 14064 0 0 0 57819 86 0 0 25 0 1 0 1855734170 60653568 13702 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 14808 13702 145 145 0 14663 0
[pid=28242] vsize: 59232
Current children cumulated CPU time (s) 579.05
Current children cumulated vsize (Kb) 61356

[startup+590.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 14212 0 0 0 58817 87 0 0 25 0 1 0 1855734170 61313024 13850 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 14969 13850 145 145 0 14824 0
[pid=28242] vsize: 59876
Current children cumulated CPU time (s) 589.04
Current children cumulated vsize (Kb) 62000

[startup+600.061 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 14324 0 0 0 59815 88 0 0 25 0 1 0 1855734170 61751296 13962 4294967295 134512640 135094434 3221224432 3221223056 134557662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 15076 13962 145 145 0 14931 0
[pid=28242] vsize: 60304
Current children cumulated CPU time (s) 599.03
Current children cumulated vsize (Kb) 62428

[startup+610.061 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 14394 0 0 0 60814 89 0 0 25 0 1 0 1855734170 62050304 14032 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 15149 14032 145 145 0 15004 0
[pid=28242] vsize: 60596
Current children cumulated CPU time (s) 609.03
Current children cumulated vsize (Kb) 62720

[startup+620.063 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 14468 0 0 0 61814 89 0 0 25 0 1 0 1855734170 62341120 14106 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 15220 14106 145 145 0 15075 0
[pid=28242] vsize: 60880
Current children cumulated CPU time (s) 619.03
Current children cumulated vsize (Kb) 63004

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 14646 0 0 0 62811 90 0 0 25 0 1 0 1855734170 63053824 14284 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 15394 14284 145 145 0 15249 0
[pid=28242] vsize: 61576
Current children cumulated CPU time (s) 629.01
Current children cumulated vsize (Kb) 63700

[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 14863 0 0 0 63806 92 0 0 25 0 1 0 1855734170 63918080 14501 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 15605 14501 145 145 0 15460 0
[pid=28242] vsize: 62420
Current children cumulated CPU time (s) 638.98
Current children cumulated vsize (Kb) 64544

[startup+650.065 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 15126 0 0 0 64801 94 0 0 25 0 1 0 1855734170 64962560 14764 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 15860 14764 145 145 0 15715 0
[pid=28242] vsize: 63440
Current children cumulated CPU time (s) 648.95
Current children cumulated vsize (Kb) 65564

[startup+660.067 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 15252 0 0 0 65800 95 0 0 25 0 1 0 1855734170 65478656 14890 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 15986 14890 145 145 0 15841 0
[pid=28242] vsize: 63944
Current children cumulated CPU time (s) 658.95
Current children cumulated vsize (Kb) 66068

[startup+670.067 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 15358 0 0 0 66798 95 0 0 25 0 1 0 1855734170 65896448 14996 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 16088 14996 145 145 0 15943 0
[pid=28242] vsize: 64352
Current children cumulated CPU time (s) 668.93
Current children cumulated vsize (Kb) 66476

[startup+680.068 s]
Raw data (loadavg): 0.99 0.97 0.92 3/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 15470 0 0 0 67797 96 0 0 25 0 1 0 1855734170 66342912 15108 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 16197 15108 145 145 0 16052 0
[pid=28242] vsize: 64788
Current children cumulated CPU time (s) 678.93
Current children cumulated vsize (Kb) 66912

[startup+690.069 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 15556 0 0 0 68796 97 0 0 25 0 1 0 1855734170 67776512 15194 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 16547 15194 145 145 0 16402 0
[pid=28242] vsize: 66188
Current children cumulated CPU time (s) 688.93
Current children cumulated vsize (Kb) 68312

[startup+700.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 15698 0 0 0 69794 98 0 0 25 0 1 0 1855734170 68313088 15336 4294967295 134512640 135094434 3221224432 3221223056 134562149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 16678 15336 145 145 0 16533 0
[pid=28242] vsize: 66712
Current children cumulated CPU time (s) 698.92
Current children cumulated vsize (Kb) 68836

[startup+710.071 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 15792 0 0 0 70792 99 0 0 25 0 1 0 1855734170 68710400 15430 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 16775 15430 145 145 0 16630 0
[pid=28242] vsize: 67100
Current children cumulated CPU time (s) 708.91
Current children cumulated vsize (Kb) 69224

[startup+720.072 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 15898 0 0 0 71791 99 0 0 25 0 1 0 1855734170 69128192 15536 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 16877 15536 145 145 0 16732 0
[pid=28242] vsize: 67508
Current children cumulated CPU time (s) 718.9
Current children cumulated vsize (Kb) 69632

[startup+730.072 s]
Raw data (loadavg): 1.07 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 16064 0 0 0 72788 100 0 0 25 0 1 0 1855734170 69799936 15702 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 17041 15702 145 145 0 16896 0
[pid=28242] vsize: 68164
Current children cumulated CPU time (s) 728.88
Current children cumulated vsize (Kb) 70288

[startup+740.073 s]
Raw data (loadavg): 1.06 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 16236 0 0 0 73786 101 0 0 25 0 1 0 1855734170 70479872 15874 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 17207 15874 145 145 0 17062 0
[pid=28242] vsize: 68828
Current children cumulated CPU time (s) 738.87
Current children cumulated vsize (Kb) 70952

[startup+750.074 s]
Raw data (loadavg): 1.05 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 16400 0 0 0 74785 102 0 0 25 0 1 0 1855734170 71172096 16038 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 17376 16038 145 145 0 17231 0
[pid=28242] vsize: 69504
Current children cumulated CPU time (s) 748.87
Current children cumulated vsize (Kb) 71628

[startup+760.076 s]
Raw data (loadavg): 1.04 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 16565 0 0 0 75783 104 0 0 25 0 1 0 1855734170 71847936 16203 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 17541 16203 145 145 0 17396 0
[pid=28242] vsize: 70164
Current children cumulated CPU time (s) 758.87
Current children cumulated vsize (Kb) 72288

[startup+770.077 s]
Raw data (loadavg): 1.03 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 16739 0 0 0 76780 105 0 0 25 0 1 0 1855734170 72683520 16377 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 17745 16377 145 145 0 17600 0
[pid=28242] vsize: 70980
Current children cumulated CPU time (s) 768.85
Current children cumulated vsize (Kb) 73104

[startup+780.077 s]
Raw data (loadavg): 1.03 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 16879 0 0 0 77779 105 0 0 25 0 1 0 1855734170 73220096 16517 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 17876 16517 145 145 0 17731 0
[pid=28242] vsize: 71504
Current children cumulated CPU time (s) 778.84
Current children cumulated vsize (Kb) 73628

[startup+790.078 s]
Raw data (loadavg): 1.02 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 16967 0 0 0 78778 106 0 0 25 0 1 0 1855734170 73613312 16605 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 17972 16605 145 145 0 17827 0
[pid=28242] vsize: 71888
Current children cumulated CPU time (s) 788.84
Current children cumulated vsize (Kb) 74012

[startup+800.079 s]
Raw data (loadavg): 1.02 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 17153 0 0 0 79775 107 0 0 25 0 1 0 1855734170 74362880 16791 4294967295 134512640 135094434 3221224432 3221223088 134561757 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 18155 16791 145 145 0 18010 0
[pid=28242] vsize: 72620
Current children cumulated CPU time (s) 798.82
Current children cumulated vsize (Kb) 74744

[startup+810.08 s]
Raw data (loadavg): 1.02 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 17211 0 0 0 80774 108 0 0 25 0 1 0 1855734170 74588160 16849 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 18210 16849 145 145 0 18065 0
[pid=28242] vsize: 72840
Current children cumulated CPU time (s) 808.82
Current children cumulated vsize (Kb) 74964

[startup+820.081 s]
Raw data (loadavg): 1.01 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 17391 0 0 0 81771 109 0 0 25 0 1 0 1855734170 75309056 17029 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 18386 17029 145 145 0 18241 0
[pid=28242] vsize: 73544
Current children cumulated CPU time (s) 818.8
Current children cumulated vsize (Kb) 75668

[startup+830.082 s]
Raw data (loadavg): 1.01 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 17477 0 0 0 82770 109 0 0 25 0 1 0 1855734170 75640832 17115 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 18467 17115 145 145 0 18322 0
[pid=28242] vsize: 73868
Current children cumulated CPU time (s) 828.79
Current children cumulated vsize (Kb) 75992

[startup+840.082 s]
Raw data (loadavg): 1.01 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 17568 0 0 0 83769 110 0 0 25 0 1 0 1855734170 76001280 17206 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 18555 17206 145 145 0 18410 0
[pid=28242] vsize: 74220
Current children cumulated CPU time (s) 838.79
Current children cumulated vsize (Kb) 76344

[startup+850.083 s]
Raw data (loadavg): 1.01 0.99 0.93 1/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) T 28238 28238 28974 0 -1 0 17701 0 0 0 84767 110 0 0 25 0 1 0 1855734170 76525568 17339 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/28242/statm): 18683 17339 145 145 0 18538 0
[pid=28242] vsize: 74732
Current children cumulated CPU time (s) 848.77
Current children cumulated vsize (Kb) 76856

[startup+860.085 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 17777 0 0 0 85766 111 0 0 25 0 1 0 1855734170 76824576 17415 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 18756 17415 145 145 0 18611 0
[pid=28242] vsize: 75024
Current children cumulated CPU time (s) 858.77
Current children cumulated vsize (Kb) 77148

[startup+870.086 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 17922 0 0 0 86764 112 0 0 25 0 1 0 1855734170 77434880 17560 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 18905 17560 145 145 0 18760 0
[pid=28242] vsize: 75620
Current children cumulated CPU time (s) 868.76
Current children cumulated vsize (Kb) 77744

[startup+880.087 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 18058 0 0 0 87761 113 0 0 25 0 1 0 1855734170 77946880 17696 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 19030 17696 145 145 0 18885 0
[pid=28242] vsize: 76120
Current children cumulated CPU time (s) 878.74
Current children cumulated vsize (Kb) 78244

[startup+890.089 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 18184 0 0 0 88759 114 0 0 25 0 1 0 1855734170 78430208 17822 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 19148 17822 145 145 0 19003 0
[pid=28242] vsize: 76592
Current children cumulated CPU time (s) 888.73
Current children cumulated vsize (Kb) 78716

[startup+900.089 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 18304 0 0 0 89757 115 0 0 25 0 1 0 1855734170 78880768 17942 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 19258 17942 145 145 0 19113 0
[pid=28242] vsize: 77032
Current children cumulated CPU time (s) 898.72
Current children cumulated vsize (Kb) 79156

[startup+910.09 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 18415 0 0 0 90756 115 0 0 25 0 1 0 1855734170 79310848 18053 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 19363 18053 145 145 0 19218 0
[pid=28242] vsize: 77452
Current children cumulated CPU time (s) 908.71
Current children cumulated vsize (Kb) 79576

[startup+920.092 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 18584 0 0 0 91753 117 0 0 25 0 1 0 1855734170 79998976 18222 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 19531 18222 145 145 0 19386 0
[pid=28242] vsize: 78124
Current children cumulated CPU time (s) 918.7
Current children cumulated vsize (Kb) 80248

[startup+930.092 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 18766 0 0 0 92749 118 0 0 25 0 1 0 1855734170 80732160 18404 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 19710 18404 145 145 0 19565 0
[pid=28242] vsize: 78840
Current children cumulated CPU time (s) 928.67
Current children cumulated vsize (Kb) 80964

[startup+940.093 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 18933 0 0 0 93746 120 0 0 25 0 1 0 1855734170 81412096 18571 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 19876 18571 145 145 0 19731 0
[pid=28242] vsize: 79504
Current children cumulated CPU time (s) 938.66
Current children cumulated vsize (Kb) 81628

[startup+950.093 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 19173 0 0 0 94742 121 0 0 25 0 1 0 1855734170 82370560 18811 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 20110 18811 145 145 0 19965 0
[pid=28242] vsize: 80440
Current children cumulated CPU time (s) 948.63
Current children cumulated vsize (Kb) 82564

[startup+960.094 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 19672 0 0 0 95733 125 0 0 25 0 1 0 1855734170 84393984 19310 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 20604 19310 145 145 0 20459 0
[pid=28242] vsize: 82416
Current children cumulated CPU time (s) 958.58
Current children cumulated vsize (Kb) 84540

[startup+970.095 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 20001 0 0 0 96727 128 0 0 25 0 1 0 1855734170 85725184 19639 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 20929 19639 145 145 0 20784 0
[pid=28242] vsize: 83716
Current children cumulated CPU time (s) 968.55
Current children cumulated vsize (Kb) 85840

[startup+980.096 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 20117 0 0 0 97725 128 0 0 25 0 1 0 1855734170 86171648 19755 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 21038 19755 145 145 0 20893 0
[pid=28242] vsize: 84152
Current children cumulated CPU time (s) 978.53
Current children cumulated vsize (Kb) 86276

[startup+990.097 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 20252 0 0 0 98723 129 0 0 25 0 1 0 1855734170 86708224 19890 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 21169 19890 145 145 0 21024 0
[pid=28242] vsize: 84676
Current children cumulated CPU time (s) 988.52
Current children cumulated vsize (Kb) 86800

[startup+1000.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 20338 0 0 0 99721 130 0 0 25 0 1 0 1855734170 87076864 19976 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 21259 19976 145 145 0 21114 0
[pid=28242] vsize: 85036
Current children cumulated CPU time (s) 998.51
Current children cumulated vsize (Kb) 87160

[startup+1010.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 20462 0 0 0 100719 131 0 0 25 0 1 0 1855734170 87625728 20100 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 21393 20100 145 145 0 21248 0
[pid=28242] vsize: 85572
Current children cumulated CPU time (s) 1008.5
Current children cumulated vsize (Kb) 87696

[startup+1020.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 20553 0 0 0 101717 132 0 0 25 0 1 0 1855734170 87986176 20191 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 21481 20191 145 145 0 21336 0
[pid=28242] vsize: 85924
Current children cumulated CPU time (s) 1018.49
Current children cumulated vsize (Kb) 88048

[startup+1030.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 20613 0 0 0 102716 133 0 0 25 0 1 0 1855734170 88223744 20251 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/28242/statm): 21539 20251 145 145 0 21394 0
[pid=28242] vsize: 86156
Current children cumulated CPU time (s) 1028.49
Current children cumulated vsize (Kb) 88280

[startup+1040.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 20732 0 0 0 103714 133 0 0 25 0 1 0 1855734170 88694784 20370 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 21654 20370 145 145 0 21509 0
[pid=28242] vsize: 86616
Current children cumulated CPU time (s) 1038.47
Current children cumulated vsize (Kb) 88740

[startup+1050.1 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 20885 0 0 0 104710 135 0 0 25 0 1 0 1855734170 89305088 20523 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 21803 20523 145 145 0 21658 0
[pid=28242] vsize: 87212
Current children cumulated CPU time (s) 1048.45
Current children cumulated vsize (Kb) 89336

[startup+1060.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 21179 0 0 0 105704 138 0 0 25 0 1 0 1855734170 90484736 20817 4294967295 134512640 135094434 3221224432 3221223104 134556502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 22091 20817 145 145 0 21946 0
[pid=28242] vsize: 88364
Current children cumulated CPU time (s) 1058.42
Current children cumulated vsize (Kb) 90488

[startup+1070.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 21270 0 0 0 106702 139 0 0 25 0 1 0 1855734170 90845184 20908 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 22179 20908 145 145 0 22034 0
[pid=28242] vsize: 88716
Current children cumulated CPU time (s) 1068.41
Current children cumulated vsize (Kb) 90840

[startup+1080.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 21412 0 0 0 107699 140 0 0 25 0 1 0 1855734170 91410432 21050 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 22317 21050 145 145 0 22172 0
[pid=28242] vsize: 89268
Current children cumulated CPU time (s) 1078.39
Current children cumulated vsize (Kb) 91392

[startup+1090.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 21529 0 0 0 108696 142 0 0 25 0 1 0 1855734170 91873280 21167 4294967295 134512640 135094434 3221224432 3221223104 134556111 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 22430 21167 145 145 0 22285 0
[pid=28242] vsize: 89720
Current children cumulated CPU time (s) 1088.38
Current children cumulated vsize (Kb) 91844

[startup+1100.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 21941 0 0 0 109689 145 0 0 25 0 1 0 1855734170 93536256 21579 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 22836 21579 145 145 0 22691 0
[pid=28242] vsize: 91344
Current children cumulated CPU time (s) 1098.34
Current children cumulated vsize (Kb) 93468

[startup+1110.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 22408 0 0 0 110681 148 0 0 25 0 1 0 1855734170 95428608 22046 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 23298 22046 145 145 0 23153 0
[pid=28242] vsize: 93192
Current children cumulated CPU time (s) 1108.29
Current children cumulated vsize (Kb) 95316

[startup+1120.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 22853 0 0 0 111671 152 0 0 25 0 1 0 1855734170 97243136 22491 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 23741 22491 145 145 0 23596 0
[pid=28242] vsize: 94964
Current children cumulated CPU time (s) 1118.23
Current children cumulated vsize (Kb) 97088

[startup+1130.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 23259 0 0 0 112664 155 0 0 25 0 1 0 1855734170 98889728 22897 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 24143 22897 145 145 0 23998 0
[pid=28242] vsize: 96572
Current children cumulated CPU time (s) 1128.19
Current children cumulated vsize (Kb) 98696

[startup+1140.11 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 23675 0 0 0 113656 159 0 0 25 0 1 0 1855734170 100585472 23313 4294967295 134512640 135094434 3221224432 3221222384 134562843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 24557 23313 145 145 0 24412 0
[pid=28242] vsize: 98228
Current children cumulated CPU time (s) 1138.15
Current children cumulated vsize (Kb) 100352

[startup+1150.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 23675 0 0 0 114655 160 0 0 25 0 1 0 1855734170 100585472 23313 4294967295 134512640 135094434 3221224432 3221222824 134782747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 24557 23313 145 145 0 24412 0
[pid=28242] vsize: 98228
Current children cumulated CPU time (s) 1148.15
Current children cumulated vsize (Kb) 100352

[startup+1160.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 23675 0 0 0 115655 160 0 0 25 0 1 0 1855734170 100585472 23313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 24557 23313 145 145 0 24412 0
[pid=28242] vsize: 98228
Current children cumulated CPU time (s) 1158.15
Current children cumulated vsize (Kb) 100352

[startup+1170.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 23675 0 0 0 116655 161 0 0 25 0 1 0 1855734170 100585472 23313 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 24557 23313 145 145 0 24412 0
[pid=28242] vsize: 98228
Current children cumulated CPU time (s) 1168.16
Current children cumulated vsize (Kb) 100352

[startup+1180.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 23675 0 0 0 117654 161 0 0 25 0 1 0 1855734170 100585472 23313 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 24557 23313 145 145 0 24412 0
[pid=28242] vsize: 98228
Current children cumulated CPU time (s) 1178.15
Current children cumulated vsize (Kb) 100352

[startup+1190.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 23675 0 0 0 118654 162 0 0 25 0 1 0 1855734170 100585472 23313 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 24557 23313 145 145 0 24412 0
[pid=28242] vsize: 98228
Current children cumulated CPU time (s) 1188.16
Current children cumulated vsize (Kb) 100352

[startup+1200.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 23675 0 0 0 119654 162 0 0 25 0 1 0 1855734170 100585472 23313 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 24557 23313 145 145 0 24412 0
[pid=28242] vsize: 98228
Current children cumulated CPU time (s) 1198.16
Current children cumulated vsize (Kb) 100352

[startup+1210.12 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 23675 0 0 0 120653 163 0 0 25 0 1 0 1855734170 100585472 23313 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 24557 23313 145 145 0 24412 0
[pid=28242] vsize: 98228
Current children cumulated CPU time (s) 1208.16
Current children cumulated vsize (Kb) 100352



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 1.00 0.99 0.93 2/57 28242
Raw data (/proc/28238/stat): 28238 (minisat+_script) S 28237 28238 28974 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855734165 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/28238/statm): 531 226 485 147 0 384 0
[pid=28238] vsize: 2124
Raw data (/proc/28242/stat): 28242 (minisat+_64-bit) R 28238 28238 28974 0 -1 0 23675 0 0 0 120653 163 0 0 25 0 1 0 1855734170 100585472 23313 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/28242/statm): 24557 23313 145 145 0 24412 0
[pid=28242] vsize: 98228
Current children cumulated CPU time (s) 1208.16
Current children cumulated vsize (Kb) 100352

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

Child status: 0
Real time (s): 1210.17
CPU time (s): 1208.21
CPU user time (s): 1206.54
CPU system time (s): 1.67474
CPU usage (%): 99.8381
Max. virtual memory (cumulated for all children) (Kb): 100352

Verifier Data

ERROR: no interpretation found !