Some explanations

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

General information on the benchmark

Namemps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-pp08aCUTS.opb
MD5SUMd9b143d593d6c40f70d01400b968fa76
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 3424
Biggest coefficient in the objective function 1073741824
Number of bits for the biggest coefficient in the objective function 31
Sum of the numbers in the objective function 180407058264
Number of bits of the sum of numbers in the objective function 38
Biggest number in a constraint 1073741824
Number of bits of the biggest number in a constraint 31
Biggest sum of numbers in a constraint 180407058264
Number of bits of the biggest sum of numbers38
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables4600
Total number of constraints374
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)64
Number of constraints which are nor clauses,nor cardinality constraints310
Minimum length of a constraint1
Maximum length of a constraint147

Trace number 3935

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        864940 kB
Buffers:         37000 kB
Cached:         105640 kB
SwapCached:        228 kB
Active:          68160 kB
Inactive:        77460 kB
HighTotal:      131008 kB
HighFree:        56336 kB
LowTotal:       903652 kB
LowFree:        808604 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6272 kB
Slab:            18480 kB
Committed_AS:    64128 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 04:10:31 (client local time) WITH STATUS 0 IN 1208.83 SECONDS
stats: 2935 7 1208.83 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:   18
c ---[ 500]---> BDD-cost:   18
c ---[ 499]---> BDD-cost:   18
c ---[ 498]---> BDD-cost:   18
c ---[ 497]---> BDD-cost:   18
c ---[ 496]---> BDD-cost:   18
c ---[ 495]---> BDD-cost:   18
c ---[ 494]---> BDD-cost:   18
c ---[ 485]---> BDD-cost:   18
c ---[ 484]---> BDD-cost:   18
c ---[ 483]---> BDD-cost:   18
c ---[ 482]---> BDD-cost:   18
c ---[ 481]---> BDD-cost:   18
c ---[ 480]---> BDD-cost:   18
c ---[ 479]---> BDD-cost:   18
c ---[ 477]---> BDD-cost:   18
c ---[ 476]---> BDD-cost:   18
c ---[ 475]---> BDD-cost:   18
c ---[ 474]---> BDD-cost:   18
c ---[ 473]---> BDD-cost:   18
c ---[ 472]---> BDD-cost:   18
c ---[ 471]---> BDD-cost:   18
c ---[ 469]---> BDD-cost:   17
c ---[ 468]---> BDD-cost:   17
c ---[ 467]---> BDD-cost:   17
c ---[ 466]---> BDD-cost:   17
c ---[ 465]---> BDD-cost:   17
c ---[ 464]---> BDD-cost:   17
c ---[ 463]---> BDD-cost:   17
c ---[ 462]---> BDD-cost:   17
c ---[ 461]---> BDD-cost:   18
c ---[ 460]---> BDD-cost:   18
c ---[ 459]---> BDD-cost:   18
c ---[ 458]---> BDD-cost:   18
c ---[ 457]---> BDD-cost:   18
c ---[ 456]---> BDD-cost:   18
c ---[ 455]---> BDD-cost:   18
c ---[ 454]---> BDD-cost:   18
c ---[ 445]---> BDD-cost:   16
c ---[ 444]---> BDD-cost:   16
c ---[ 443]---> BDD-cost:   16
c ---[ 442]---> BDD-cost:   16
c ---[ 441]---> BDD-cost:   16
c ---[ 440]---> BDD-cost:   16
c ---[ 439]---> BDD-cost:   16
c ---[ 438]---> BDD-cost:   16
c ---[ 436]---> BDD-cost:  220
c ---[ 434]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> BDD-cost:    6
c ---[ 432]---> BDD-cost:    6
c ---[ 431]---> BDD-cost:    6
c ---[ 430]---> BDD-cost:    6
c ---[ 429]---> BDD-cost:   26
c ---[ 428]---> BDD-cost:    4
c ---[ 427]---> BDD-cost:    4
c ---[ 426]---> BDD-cost:    4
c ---[ 425]---> BDD-cost:    4
c ---[ 424]---> BDD-cost:    4
c ---[ 422]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 421]---> BDD-cost:    4
c ---[ 420]---> BDD-cost:    4
c ---[ 419]---> BDD-cost:    4
c ---[ 418]---> BDD-cost:    9
c ---[ 417]---> BDD-cost:    9
c ---[ 416]---> BDD-cost:    9
c ---[ 415]---> BDD-cost:    6
c ---[ 414]---> BDD-cost:    6
c ---[ 413]---> BDD-cost:    6
c ---[ 412]---> BDD-cost:    6
c ---[ 410]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 409]---> BDD-cost:    6
c ---[ 408]---> BDD-cost:   22
c ---[ 407]---> BDD-cost:   22
c ---[ 406]---> BDD-cost:   22
c ---[ 405]---> BDD-cost:   22
c ---[ 404]---> BDD-cost:   22
c ---[ 403]---> BDD-cost:   22
c ---[ 402]---> BDD-cost:   22
c ---[ 401]---> BDD-cost:   22
c ---[ 400]---> BDD-cost:    6
c ---[ 398]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    6
c ---[ 394]---> BDD-cost:    6
c ---[ 393]---> BDD-cost:    6
c ---[ 392]---> BDD-cost:    6
c ---[ 391]---> BDD-cost:    6
c ---[ 386]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> BDD-cost:  220
c ---[ 253]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 249]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 247]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 243]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 241]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 239]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 237]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 235]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 233]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 231]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 229]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 227]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 225]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 219]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 217]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 213]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 211]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 203]---> BDD-cost:  216
c ---[ 201]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 191]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost: 1687     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost: 1668     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 1668     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost: 1668     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 1668     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost: 1668     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost: 1668     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  586     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 2360     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost: 2360     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost: 2360     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost: 2360     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 2360     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost: 1706     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost: 2360     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost: 2360     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost: 2360     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    6
c ---[ 154]---> BDD-cost:    6
c ---[ 153]---> BDD-cost:    6
c ---[ 152]---> BDD-cost:    6
c ---[ 150]---> Sorter-cost:  604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> BDD-cost:    8
c ---[ 148]---> BDD-cost:   22
c ---[ 147]---> BDD-cost:   22
c ---[ 146]---> BDD-cost:   22
c ---[ 145]---> BDD-cost:   22
c ---[ 144]---> BDD-cost:   22
c ---[ 143]---> BDD-cost:   22
c ---[ 142]---> BDD-cost:   22
c ---[ 141]---> BDD-cost:   22
c ---[ 140]---> BDD-cost:    9
c ---[ 138]---> Sorter-cost:  595     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> BDD-cost:    9
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:    6
c ---[ 134]---> BDD-cost:    6
c ---[ 133]---> BDD-cost:    6
c ---[ 132]---> BDD-cost:    6
c ---[ 131]---> BDD-cost:   26
c ---[ 130]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:    9
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:    1
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:    1
c ---[ 122]---> BDD-cost:    1
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:    1
c ---[ 118]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:    1
c ---[ 110]---> BDD-cost:    1
c ---[ 109]---> BDD-cost:   59
c ---[ 108]---> BDD-cost:  230
c ---[ 107]---> BDD-cost:   54
c ---[ 106]---> BDD-cost:  221
c ---[ 105]---> BDD-cost:   57
c ---[ 104]---> BDD-cost:  218
c ---[ 103]---> BDD-cost:   47
c ---[ 102]---> BDD-cost:  200
c ---[ 101]---> BDD-cost:   53
c ---[ 100]---> BDD-cost:  194
c ---[  99]---> BDD-cost:    5
c ---[  98]---> BDD-cost:   82
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:   71
c ---[  95]---> BDD-cost:   50
c ---[  94]---> BDD-cost:  185
c ---[  93]---> BDD-cost:   54
c ---[  92]---> BDD-cost:  209
c ---[  91]---> BDD-cost:   49
c ---[  90]---> BDD-cost:  200
c ---[  89]---> BDD-cost:   44
c ---[  88]---> BDD-cost:  191
c ---[  87]---> BDD-cost:   50
c ---[  86]---> BDD-cost:  185
c ---[  85]---> BDD-cost:    5
c ---[  84]---> BDD-cost:   79
c ---[  83]---> BDD-cost:    3
c ---[  82]---> BDD-cost:   74
c ---[  81]---> BDD-cost:   54
c ---[  80]---> BDD-cost:  221
c ---[  79]---> BDD-cost:   57
c ---[  78]---> BDD-cost:  218
c ---[  77]---> BDD-cost:   50
c ---[  76]---> BDD-cost:  197
c ---[  75]---> BDD-cost:   53
c ---[  74]---> BDD-cost:  194
c ---[  73]---> BDD-cost:   59
c ---[  72]---> BDD-cost:  230
c ---[  71]---> BDD-cost:    3
c ---[  70]---> BDD-cost:   70
c ---[  69]---> BDD-cost:   57
c ---[  68]---> BDD-cost:  218
c ---[  67]---> BDD-cost:   57
c ---[  66]---> BDD-cost:  218
c ---[  65]---> BDD-cost:   64
c ---[  64]---> BDD-cost:  236
c ---[  63]---> BDD-cost:   56
c ---[  62]---> BDD-cost:  188
c ---[  61]---> BDD-cost:   59
c ---[  60]---> BDD-cost:  230
c ---[  59]---> BDD-cost:   57
c ---[  58]---> BDD-cost:  218
c ---[  57]---> BDD-cost:    5
c ---[  56]---> BDD-cost:   82
c ---[  55]---> BDD-cost:    5
c ---[  54]---> BDD-cost:   79
c ---[  53]---> BDD-cost:   47
c ---[  52]---> BDD-cost:  188
c ---[  51]---> BDD-cost:   50
c ---[  50]---> BDD-cost:  185
c ---[  49]---> BDD-cost:   44
c ---[  48]---> BDD-cost:  191
c ---[  47]---> BDD-cost:   44
c ---[  46]---> BDD-cost:  191
c ---[  45]---> BDD-cost:   47
c ---[  44]---> BDD-cost:  188
c ---[  43]---> BDD-cost:    3
c ---[  42]---> BDD-cost:   73
c ---[  41]---> BDD-cost:    6
c ---[  40]---> BDD-cost:   87
c ---[  39]---> BDD-cost:   50
c ---[  38]---> BDD-cost:  197
c ---[  37]---> BDD-cost:   50
c ---[  36]---> BDD-cost:  197
c ---[  35]---> BDD-cost:   50
c ---[  34]---> BDD-cost:  197
c ---[  33]---> BDD-cost:   57
c ---[  32]---> BDD-cost:  218
c ---[  31]---> BDD-cost:   47
c ---[  30]---> BDD-cost:  200
c ---[  29]---> BDD-cost:   50
c ---[  28]---> BDD-cost:  197
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:   84
c ---[  25]---> BDD-cost:   47
c ---[  24]---> BDD-cost:  188
c ---[  23]---> BDD-cost:   54
c ---[  22]---> BDD-cost:  209
c ---[  21]---> BDD-cost:   44
c ---[  20]---> BDD-cost:  191
c ---[  19]---> BDD-cost:   47
c ---[  18]---> BDD-cost:  188
c ---[  17]---> BDD-cost:   52
c ---[  16]---> BDD-cost:  197
c ---[  15]---> BDD-cost:   50
c ---[  14]---> BDD-cost:  185
c ---[  13]---> BDD-cost:    3
c ---[  12]---> BDD-cost:   69
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:   68
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:  176
c ---[   7]---> BDD-cost:   44
c ---[   6]---> BDD-cost:  179
c ---[   5]---> BDD-cost:   44
c ---[   4]---> BDD-cost:  179
c ---[   3]---> BDD-cost:   47
c ---[   2]---> BDD-cost:  176
c ---[   1]---> BDD-cost:    4
c ---[   0]---> BDD-cost:   71
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  293828   708752 |   97942       0        0     nan |  0.000 % |
c |       102 |  293828   708752 |  107736     102     1729    17.0 |  5.437 % |
c |       252 |  293580   708205 |  118509     205     2048    10.0 |  5.506 % |
c |       477 |  293283   707547 |  130360     379     2708     7.1 |  5.588 % |
c |       814 |  292918   706734 |  143396     663     3741     5.6 |  5.685 % |
c |      1320 |  292567   705955 |  157736    1112     5656     5.1 |  5.778 % |
c |      2079 |  292264   705281 |  173510    1823     8280     4.5 |  5.859 % |
c |      3218 |  291104   702687 |  190861    2795    11659     4.2 |  6.160 % |
c |      4926 |  290177   700612 |  209947    4382    17505     4.0 |  6.400 % |
c |      7488 |  289431   698939 |  230942    6835    28361     4.1 |  6.590 % |
c |     11332 |  288000   695744 |  254036   10480    45363     4.3 |  6.961 % |
c |     17098 |  285661   690509 |  279439   15921    69297     4.4 |  7.565 % |
c |     25747 |  284320   687510 |  307383   24371   121941     5.0 |  7.913 % |
c |     38721 |  282947   684426 |  338122   37163   203491     5.5 |  8.263 % |
c |     58182 |  281504   681186 |  371934   56426   329775     5.8 |  8.630 % |
c |     87375 |  280774   679550 |  409128   85513   594418     7.0 |  8.818 % |
c |    131164 |  280133   678112 |  450040  129227  1122688     8.7 |  8.980 % |
c |    196849 |  279930   677656 |  495044  194867  2298140    11.8 |  9.037 % |
c |    295375 |  279694   677128 |  544549  293374  4559670    15.5 |  9.097 % |

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/3247/stat): 3247 (minisat+_script) R 3246 3247 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788597116 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/3247/statm): 174 3 169 147 0 27 0
[pid=3247] 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=3248
New process pid=3249
New process pid=3250
execve syscall for /bin/sed executable
One traced child (pid=3249) 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=3250) exited with status: 0
One traced child (pid=3248) exited with status: 0
New process pid=3251
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-pp08aCUTS.opb

[startup+10.0032 s]
Raw data (loadavg): 0.93 0.95 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9171 0 0 0 924 37 0 0 25 0 1 0 1788597121 39129088 8835 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 9553 8835 145 145 0 9408 0
[pid=3251] vsize: 38212
Current children cumulated CPU time (s) 9.62
Current children cumulated vsize (Kb) 40336

[startup+20.0037 s]
Raw data (loadavg): 0.94 0.95 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9215 0 0 0 1922 38 0 0 25 0 1 0 1788597121 39305216 8879 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9596 8879 145 145 0 9451 0
[pid=3251] vsize: 38384
Current children cumulated CPU time (s) 19.61
Current children cumulated vsize (Kb) 40508

[startup+30.0043 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9221 0 0 0 2922 38 0 0 25 0 1 0 1788597121 39325696 8885 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 9601 8885 145 145 0 9456 0
[pid=3251] vsize: 38404
Current children cumulated CPU time (s) 29.61
Current children cumulated vsize (Kb) 40528

[startup+40.0049 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9253 0 0 0 3922 38 0 0 25 0 1 0 1788597121 39448576 8917 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9631 8917 145 145 0 9486 0
[pid=3251] vsize: 38524
Current children cumulated CPU time (s) 39.61
Current children cumulated vsize (Kb) 40648

[startup+50.0054 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9287 0 0 0 4921 39 0 0 25 0 1 0 1788597121 39596032 8951 4294967295 134512640 135094434 3221224432 3221223136 134559017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9667 8951 145 145 0 9522 0
[pid=3251] vsize: 38668
Current children cumulated CPU time (s) 49.61
Current children cumulated vsize (Kb) 40792

[startup+60.006 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9309 0 0 0 5920 39 0 0 25 0 1 0 1788597121 39645184 8973 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9679 8973 145 145 0 9534 0
[pid=3251] vsize: 38716
Current children cumulated CPU time (s) 59.6
Current children cumulated vsize (Kb) 40840

[startup+70.0066 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9327 0 0 0 6919 39 0 0 25 0 1 0 1788597121 39694336 8991 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9691 8991 145 145 0 9546 0
[pid=3251] vsize: 38764
Current children cumulated CPU time (s) 69.59
Current children cumulated vsize (Kb) 40888

[startup+80.0081 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9351 0 0 0 7919 40 0 0 25 0 1 0 1788597121 39776256 9015 4294967295 134512640 135094434 3221224432 3221223044 134563030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9711 9015 145 145 0 9566 0
[pid=3251] vsize: 38844
Current children cumulated CPU time (s) 79.6
Current children cumulated vsize (Kb) 40968

[startup+90.0087 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9373 0 0 0 8919 40 0 0 25 0 1 0 1788597121 39849984 9037 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9729 9037 145 145 0 9584 0
[pid=3251] vsize: 38916
Current children cumulated CPU time (s) 89.6
Current children cumulated vsize (Kb) 41040

[startup+100.008 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9403 0 0 0 9918 40 0 0 25 0 1 0 1788597121 39993344 9067 4294967295 134512640 135094434 3221224432 3221223056 134557565 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9764 9067 145 145 0 9619 0
[pid=3251] vsize: 39056
Current children cumulated CPU time (s) 99.59
Current children cumulated vsize (Kb) 41180

[startup+110.009 s]
Raw data (loadavg): 1.06 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9436 0 0 0 10918 41 0 0 25 0 1 0 1788597121 40116224 9100 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9794 9100 145 145 0 9649 0
[pid=3251] vsize: 39176
Current children cumulated CPU time (s) 109.6
Current children cumulated vsize (Kb) 41300

[startup+120.009 s]
Raw data (loadavg): 1.05 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9471 0 0 0 11918 41 0 0 25 0 1 0 1788597121 40251392 9135 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9827 9135 145 145 0 9682 0
[pid=3251] vsize: 39308
Current children cumulated CPU time (s) 119.6
Current children cumulated vsize (Kb) 41432

[startup+130.01 s]
Raw data (loadavg): 1.04 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9510 0 0 0 12917 41 0 0 25 0 1 0 1788597121 40398848 9174 4294967295 134512640 135094434 3221224432 3221223072 134562070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9863 9174 145 145 0 9718 0
[pid=3251] vsize: 39452
Current children cumulated CPU time (s) 129.59
Current children cumulated vsize (Kb) 41576

[startup+140.01 s]
Raw data (loadavg): 1.04 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9535 0 0 0 13917 41 0 0 25 0 1 0 1788597121 40488960 9199 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9885 9199 145 145 0 9740 0
[pid=3251] vsize: 39540
Current children cumulated CPU time (s) 139.59
Current children cumulated vsize (Kb) 41664

[startup+150.011 s]
Raw data (loadavg): 1.03 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9563 0 0 0 14916 42 0 0 25 0 1 0 1788597121 40595456 9227 4294967295 134512640 135094434 3221224432 3221223044 134563087 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9911 9227 145 145 0 9766 0
[pid=3251] vsize: 39644
Current children cumulated CPU time (s) 149.59
Current children cumulated vsize (Kb) 41768

[startup+160.012 s]
Raw data (loadavg): 1.03 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9612 0 0 0 15916 42 0 0 25 0 1 0 1788597121 40919040 9276 4294967295 134512640 135094434 3221224432 3221223072 134562068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 9990 9276 145 145 0 9845 0
[pid=3251] vsize: 39960
Current children cumulated CPU time (s) 159.59
Current children cumulated vsize (Kb) 42084

[startup+170.012 s]
Raw data (loadavg): 1.02 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9632 0 0 0 16916 42 0 0 25 0 1 0 1788597121 40988672 9296 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10007 9296 145 145 0 9862 0
[pid=3251] vsize: 40028
Current children cumulated CPU time (s) 169.59
Current children cumulated vsize (Kb) 42152

[startup+180.013 s]
Raw data (loadavg): 1.02 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9665 0 0 0 17916 43 0 0 25 0 1 0 1788597121 41115648 9329 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10038 9329 145 145 0 9893 0
[pid=3251] vsize: 40152
Current children cumulated CPU time (s) 179.6
Current children cumulated vsize (Kb) 42276

[startup+190.013 s]
Raw data (loadavg): 1.01 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9698 0 0 0 18915 43 0 0 25 0 1 0 1788597121 41238528 9362 4294967295 134512640 135094434 3221224432 3221223044 134563059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10068 9362 145 145 0 9923 0
[pid=3251] vsize: 40272
Current children cumulated CPU time (s) 189.59
Current children cumulated vsize (Kb) 42396

[startup+200.014 s]
Raw data (loadavg): 1.01 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9724 0 0 0 19914 44 0 0 25 0 1 0 1788597121 41336832 9388 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10092 9388 145 145 0 9947 0
[pid=3251] vsize: 40368
Current children cumulated CPU time (s) 199.59
Current children cumulated vsize (Kb) 42492

[startup+210.014 s]
Raw data (loadavg): 1.01 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9756 0 0 0 20913 44 0 0 25 0 1 0 1788597121 41447424 9420 4294967295 134512640 135094434 3221224432 3221223044 134563121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10119 9420 145 145 0 9974 0
[pid=3251] vsize: 40476
Current children cumulated CPU time (s) 209.58
Current children cumulated vsize (Kb) 42600

[startup+220.015 s]
Raw data (loadavg): 1.01 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9783 0 0 0 21913 44 0 0 25 0 1 0 1788597121 41549824 9447 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10144 9447 145 145 0 9999 0
[pid=3251] vsize: 40576
Current children cumulated CPU time (s) 219.58
Current children cumulated vsize (Kb) 42700

[startup+230.016 s]
Raw data (loadavg): 1.01 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9822 0 0 0 22913 45 0 0 25 0 1 0 1788597121 41693184 9486 4294967295 134512640 135094434 3221224432 3221223136 134559005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10179 9486 145 145 0 10034 0
[pid=3251] vsize: 40716
Current children cumulated CPU time (s) 229.59
Current children cumulated vsize (Kb) 42840

[startup+240.016 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9861 0 0 0 23913 45 0 0 25 0 1 0 1788597121 41844736 9525 4294967295 134512640 135094434 3221224432 3221223088 134558164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10216 9525 145 145 0 10071 0
[pid=3251] vsize: 40864
Current children cumulated CPU time (s) 239.59
Current children cumulated vsize (Kb) 42988

[startup+250.016 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9887 0 0 0 24912 45 0 0 25 0 1 0 1788597121 41943040 9551 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10240 9551 145 145 0 10095 0
[pid=3251] vsize: 40960
Current children cumulated CPU time (s) 249.58
Current children cumulated vsize (Kb) 43084

[startup+260.016 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9916 0 0 0 25911 46 0 0 25 0 1 0 1788597121 42053632 9580 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10267 9580 145 145 0 10122 0
[pid=3251] vsize: 41068
Current children cumulated CPU time (s) 259.58
Current children cumulated vsize (Kb) 43192

[startup+270.017 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9947 0 0 0 26911 46 0 0 25 0 1 0 1788597121 42172416 9611 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10296 9611 145 145 0 10151 0
[pid=3251] vsize: 41184
Current children cumulated CPU time (s) 269.58
Current children cumulated vsize (Kb) 43308

[startup+280.017 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 9974 0 0 0 27911 46 0 0 25 0 1 0 1788597121 42274816 9638 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10321 9638 145 145 0 10176 0
[pid=3251] vsize: 41284
Current children cumulated CPU time (s) 279.58
Current children cumulated vsize (Kb) 43408

[startup+290.018 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10005 0 0 0 28911 46 0 0 25 0 1 0 1788597121 42393600 9669 4294967295 134512640 135094434 3221224432 3221223136 134554538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10350 9669 145 145 0 10205 0
[pid=3251] vsize: 41400
Current children cumulated CPU time (s) 289.58
Current children cumulated vsize (Kb) 43524

[startup+300.017 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10039 0 0 0 29910 47 0 0 25 0 1 0 1788597121 42786816 9703 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10446 9703 145 145 0 10301 0
[pid=3251] vsize: 41784
Current children cumulated CPU time (s) 299.58
Current children cumulated vsize (Kb) 43908

[startup+310.018 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10071 0 0 0 30910 47 0 0 25 0 1 0 1788597121 42909696 9735 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10476 9735 145 145 0 10331 0
[pid=3251] vsize: 41904
Current children cumulated CPU time (s) 309.58
Current children cumulated vsize (Kb) 44028

[startup+320.019 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10107 0 0 0 31909 47 0 0 25 0 1 0 1788597121 43044864 9771 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10509 9771 145 145 0 10364 0
[pid=3251] vsize: 42036
Current children cumulated CPU time (s) 319.57
Current children cumulated vsize (Kb) 44160

[startup+330.02 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10154 0 0 0 32909 47 0 0 25 0 1 0 1788597121 43229184 9818 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10554 9818 145 145 0 10409 0
[pid=3251] vsize: 42216
Current children cumulated CPU time (s) 329.57
Current children cumulated vsize (Kb) 44340

[startup+340.021 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10212 0 0 0 33908 48 0 0 25 0 1 0 1788597121 43454464 9876 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10609 9876 145 145 0 10464 0
[pid=3251] vsize: 42436
Current children cumulated CPU time (s) 339.57
Current children cumulated vsize (Kb) 44560

[startup+350.021 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10268 0 0 0 34907 48 0 0 25 0 1 0 1788597121 43671552 9932 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10662 9932 145 145 0 10517 0
[pid=3251] vsize: 42648
Current children cumulated CPU time (s) 349.56
Current children cumulated vsize (Kb) 44772

[startup+360.022 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10348 0 0 0 35905 49 0 0 25 0 1 0 1788597121 43982848 10012 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10738 10012 145 145 0 10593 0
[pid=3251] vsize: 42952
Current children cumulated CPU time (s) 359.55
Current children cumulated vsize (Kb) 45076

[startup+370.021 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10384 0 0 0 36905 49 0 0 25 0 1 0 1788597121 44122112 10048 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10772 10048 145 145 0 10627 0
[pid=3251] vsize: 43088
Current children cumulated CPU time (s) 369.55
Current children cumulated vsize (Kb) 45212

[startup+380.023 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10474 0 0 0 37904 50 0 0 25 0 1 0 1788597121 44478464 10138 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10859 10138 145 145 0 10714 0
[pid=3251] vsize: 43436
Current children cumulated CPU time (s) 379.55
Current children cumulated vsize (Kb) 45560

[startup+390.024 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10520 0 0 0 38903 50 0 0 25 0 1 0 1788597121 44650496 10184 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10901 10184 145 145 0 10756 0
[pid=3251] vsize: 43604
Current children cumulated CPU time (s) 389.54
Current children cumulated vsize (Kb) 45728

[startup+400.024 s]
Raw data (loadavg): 1.00 0.98 0.98 1/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) T 3247 3247 22582 0 -1 0 10557 0 0 0 39902 50 0 0 25 0 1 0 1788597121 44793856 10221 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10936 10221 145 145 0 10791 0
[pid=3251] vsize: 43744
Current children cumulated CPU time (s) 399.53
Current children cumulated vsize (Kb) 45868

[startup+410.025 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10600 0 0 0 40902 51 0 0 25 0 1 0 1788597121 44957696 10264 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 10976 10264 145 145 0 10831 0
[pid=3251] vsize: 43904
Current children cumulated CPU time (s) 409.54
Current children cumulated vsize (Kb) 46028

[startup+420.024 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10660 0 0 0 41901 51 0 0 25 0 1 0 1788597121 45191168 10324 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11033 10324 145 145 0 10888 0
[pid=3251] vsize: 44132
Current children cumulated CPU time (s) 419.53
Current children cumulated vsize (Kb) 46256

[startup+430.025 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10698 0 0 0 42900 52 0 0 25 0 1 0 1788597121 45338624 10362 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11069 10362 145 145 0 10924 0
[pid=3251] vsize: 44276
Current children cumulated CPU time (s) 429.53
Current children cumulated vsize (Kb) 46400

[startup+440.025 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10751 0 0 0 43899 52 0 0 25 0 1 0 1788597121 45543424 10415 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11119 10415 145 145 0 10974 0
[pid=3251] vsize: 44476
Current children cumulated CPU time (s) 439.52
Current children cumulated vsize (Kb) 46600

[startup+450.026 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10792 0 0 0 44898 52 0 0 25 0 1 0 1788597121 45699072 10456 4294967295 134512640 135094434 3221224432 3221223044 134563069 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11157 10456 145 145 0 11012 0
[pid=3251] vsize: 44628
Current children cumulated CPU time (s) 449.51
Current children cumulated vsize (Kb) 46752

[startup+460.026 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10830 0 0 0 45898 52 0 0 25 0 1 0 1788597121 45846528 10494 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11193 10494 145 145 0 11048 0
[pid=3251] vsize: 44772
Current children cumulated CPU time (s) 459.51
Current children cumulated vsize (Kb) 46896

[startup+470.027 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10882 0 0 0 46897 53 0 0 25 0 1 0 1788597121 46047232 10546 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11242 10546 145 145 0 11097 0
[pid=3251] vsize: 44968
Current children cumulated CPU time (s) 469.51
Current children cumulated vsize (Kb) 47092

[startup+480.028 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 10948 0 0 0 47896 53 0 0 25 0 1 0 1788597121 46305280 10612 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11305 10612 145 145 0 11160 0
[pid=3251] vsize: 45220
Current children cumulated CPU time (s) 479.5
Current children cumulated vsize (Kb) 47344

[startup+490.028 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11022 0 0 0 48895 54 0 0 25 0 1 0 1788597121 46600192 10686 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11377 10686 145 145 0 11232 0
[pid=3251] vsize: 45508
Current children cumulated CPU time (s) 489.5
Current children cumulated vsize (Kb) 47632

[startup+500.029 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11076 0 0 0 49894 54 0 0 25 0 1 0 1788597121 46809088 10740 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11428 10740 145 145 0 11283 0
[pid=3251] vsize: 45712
Current children cumulated CPU time (s) 499.49
Current children cumulated vsize (Kb) 47836

[startup+510.029 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11121 0 0 0 50892 55 0 0 25 0 1 0 1788597121 46985216 10785 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11471 10785 145 145 0 11326 0
[pid=3251] vsize: 45884
Current children cumulated CPU time (s) 509.48
Current children cumulated vsize (Kb) 48008

[startup+520.03 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11221 0 0 0 51891 56 0 0 25 0 1 0 1788597121 47378432 10885 4294967295 134512640 135094434 3221224432 3221223088 134558298 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11567 10885 145 145 0 11422 0
[pid=3251] vsize: 46268
Current children cumulated CPU time (s) 519.48
Current children cumulated vsize (Kb) 48392

[startup+530.03 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11282 0 0 0 52890 56 0 0 25 0 1 0 1788597121 47616000 10946 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11625 10946 145 145 0 11480 0
[pid=3251] vsize: 46500
Current children cumulated CPU time (s) 529.47
Current children cumulated vsize (Kb) 48624

[startup+540.031 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11332 0 0 0 53890 56 0 0 25 0 1 0 1788597121 47812608 10996 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 11673 10996 145 145 0 11528 0
[pid=3251] vsize: 46692
Current children cumulated CPU time (s) 539.47
Current children cumulated vsize (Kb) 48816

[startup+550.032 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11376 0 0 0 54889 57 0 0 25 0 1 0 1788597121 48508928 11040 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11843 11040 145 145 0 11698 0
[pid=3251] vsize: 47372
Current children cumulated CPU time (s) 549.47
Current children cumulated vsize (Kb) 49496

[startup+560.032 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11439 0 0 0 55888 57 0 0 25 0 1 0 1788597121 48754688 11103 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11903 11103 145 145 0 11758 0
[pid=3251] vsize: 47612
Current children cumulated CPU time (s) 559.46
Current children cumulated vsize (Kb) 49736

[startup+570.033 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11529 0 0 0 56887 57 0 0 25 0 1 0 1788597121 49111040 11193 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 11990 11193 145 145 0 11845 0
[pid=3251] vsize: 47960
Current children cumulated CPU time (s) 569.45
Current children cumulated vsize (Kb) 50084

[startup+580.033 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11585 0 0 0 57886 58 0 0 25 0 1 0 1788597121 49328128 11249 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12043 11249 145 145 0 11898 0
[pid=3251] vsize: 48172
Current children cumulated CPU time (s) 579.45
Current children cumulated vsize (Kb) 50296

[startup+590.034 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11634 0 0 0 58885 58 0 0 25 0 1 0 1788597121 49520640 11298 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12090 11298 145 145 0 11945 0
[pid=3251] vsize: 48360
Current children cumulated CPU time (s) 589.44
Current children cumulated vsize (Kb) 50484

[startup+600.034 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11706 0 0 0 59884 59 0 0 25 0 1 0 1788597121 49803264 11370 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12159 11370 145 145 0 12014 0
[pid=3251] vsize: 48636
Current children cumulated CPU time (s) 599.44
Current children cumulated vsize (Kb) 50760

[startup+610.035 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11833 0 0 0 60883 59 0 0 25 0 1 0 1788597121 50307072 11497 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12282 11497 145 145 0 12137 0
[pid=3251] vsize: 49128
Current children cumulated CPU time (s) 609.43
Current children cumulated vsize (Kb) 51252

[startup+620.035 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11889 0 0 0 61881 61 0 0 25 0 1 0 1788597121 50528256 11553 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12336 11553 145 145 0 12191 0
[pid=3251] vsize: 49344
Current children cumulated CPU time (s) 619.43
Current children cumulated vsize (Kb) 51468

[startup+630.036 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 11977 0 0 0 62880 62 0 0 25 0 1 0 1788597121 50876416 11641 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12421 11641 145 145 0 12276 0
[pid=3251] vsize: 49684
Current children cumulated CPU time (s) 629.43
Current children cumulated vsize (Kb) 51808

[startup+640.037 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12054 0 0 0 63879 62 0 0 25 0 1 0 1788597121 51179520 11718 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12495 11718 145 145 0 12350 0
[pid=3251] vsize: 49980
Current children cumulated CPU time (s) 639.42
Current children cumulated vsize (Kb) 52104

[startup+650.037 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12120 0 0 0 64877 63 0 0 25 0 1 0 1788597121 51441664 11784 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12559 11784 145 145 0 12414 0
[pid=3251] vsize: 50236
Current children cumulated CPU time (s) 649.41
Current children cumulated vsize (Kb) 52360

[startup+660.038 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12213 0 0 0 65875 64 0 0 25 0 1 0 1788597121 51810304 11877 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12649 11877 145 145 0 12504 0
[pid=3251] vsize: 50596
Current children cumulated CPU time (s) 659.4
Current children cumulated vsize (Kb) 52720

[startup+670.038 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12278 0 0 0 66874 65 0 0 25 0 1 0 1788597121 52064256 11942 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12711 11942 145 145 0 12566 0
[pid=3251] vsize: 50844
Current children cumulated CPU time (s) 669.4
Current children cumulated vsize (Kb) 52968

[startup+680.039 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12356 0 0 0 67872 66 0 0 25 0 1 0 1788597121 52371456 12020 4294967295 134512640 135094434 3221224432 3221223044 134563154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12786 12020 145 145 0 12641 0
[pid=3251] vsize: 51144
Current children cumulated CPU time (s) 679.39
Current children cumulated vsize (Kb) 53268

[startup+690.039 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12435 0 0 0 68870 67 0 0 25 0 1 0 1788597121 52682752 12099 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12862 12099 145 145 0 12717 0
[pid=3251] vsize: 51448
Current children cumulated CPU time (s) 689.38
Current children cumulated vsize (Kb) 53572

[startup+700.039 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12556 0 0 0 69869 67 0 0 25 0 1 0 1788597121 53161984 12220 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 12979 12220 145 145 0 12834 0
[pid=3251] vsize: 51916
Current children cumulated CPU time (s) 699.37
Current children cumulated vsize (Kb) 54040

[startup+710.04 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12607 0 0 0 70868 68 0 0 25 0 1 0 1788597121 53362688 12271 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 13028 12271 145 145 0 12883 0
[pid=3251] vsize: 52112
Current children cumulated CPU time (s) 709.37
Current children cumulated vsize (Kb) 54236

[startup+720.04 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12675 0 0 0 71867 68 0 0 25 0 1 0 1788597121 53633024 12339 4294967295 134512640 135094434 3221224432 3221223088 134558420 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 13094 12339 145 145 0 12949 0
[pid=3251] vsize: 52376
Current children cumulated CPU time (s) 719.36
Current children cumulated vsize (Kb) 54500

[startup+730.041 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 12781 0 0 0 72865 69 0 0 25 0 1 0 1788597121 54050816 12445 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 13196 12445 145 145 0 13051 0
[pid=3251] vsize: 52784
Current children cumulated CPU time (s) 729.35
Current children cumulated vsize (Kb) 54908

[startup+740.041 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13116 0 0 0 73858 72 0 0 25 0 1 0 1788597121 55390208 12780 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 13523 12780 145 145 0 13378 0
[pid=3251] vsize: 54092
Current children cumulated CPU time (s) 739.31
Current children cumulated vsize (Kb) 56216

[startup+750.042 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13235 0 0 0 74857 73 0 0 25 0 1 0 1788597121 55861248 12899 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 13638 12899 145 145 0 13493 0
[pid=3251] vsize: 54552
Current children cumulated CPU time (s) 749.31
Current children cumulated vsize (Kb) 56676

[startup+760.042 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13297 0 0 0 75855 74 0 0 25 0 1 0 1788597121 56107008 12961 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 13698 12961 145 145 0 13553 0
[pid=3251] vsize: 54792
Current children cumulated CPU time (s) 759.3
Current children cumulated vsize (Kb) 56916

[startup+770.043 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13350 0 0 0 76854 75 0 0 25 0 1 0 1788597121 56315904 13014 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 13749 13014 145 145 0 13604 0
[pid=3251] vsize: 54996
Current children cumulated CPU time (s) 769.3
Current children cumulated vsize (Kb) 57120

[startup+780.044 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13497 0 0 0 77850 77 0 0 25 0 1 0 1788597121 56905728 13161 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 13893 13161 145 145 0 13748 0
[pid=3251] vsize: 55572
Current children cumulated CPU time (s) 779.28
Current children cumulated vsize (Kb) 57696

[startup+790.045 s]
Raw data (loadavg): 1.00 0.98 0.98 1/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) T 3247 3247 22582 0 -1 0 13604 0 0 0 78853 78 0 0 25 0 1 0 1788597121 57331712 13268 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/3251/statm): 13997 13268 145 145 0 13852 0
[pid=3251] vsize: 55988
Current children cumulated CPU time (s) 789.32
Current children cumulated vsize (Kb) 58112

[startup+800.646 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13650 0 0 0 79852 78 0 0 25 0 1 0 1788597121 57511936 13314 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 14041 13314 145 145 0 13896 0
[pid=3251] vsize: 56164
Current children cumulated CPU time (s) 799.31
Current children cumulated vsize (Kb) 58288

[startup+810.648 s]
Raw data (loadavg): 1.00 0.98 0.98 3/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13712 0 0 0 80850 79 0 0 25 0 1 0 1788597121 57757696 13376 4294967295 134512640 135094434 3221224432 3221223088 134561460 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 14101 13376 145 145 0 13956 0
[pid=3251] vsize: 56404
Current children cumulated CPU time (s) 809.3
Current children cumulated vsize (Kb) 58528

[startup+820.648 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13798 0 0 0 81849 80 0 0 25 0 1 0 1788597121 58093568 13462 4294967295 134512640 135094434 3221224432 3221223080 134558258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 14183 13462 145 145 0 14038 0
[pid=3251] vsize: 56732
Current children cumulated CPU time (s) 819.3
Current children cumulated vsize (Kb) 58856

[startup+830.65 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13869 0 0 0 82847 81 0 0 25 0 1 0 1788597121 58376192 13533 4294967295 134512640 135094434 3221224432 3221222976 134562082 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 14252 13533 145 145 0 14107 0
[pid=3251] vsize: 57008
Current children cumulated CPU time (s) 829.29
Current children cumulated vsize (Kb) 59132

[startup+840.651 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 13981 0 0 0 83844 83 0 0 25 0 1 0 1788597121 58822656 13645 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 14361 13645 145 145 0 14216 0
[pid=3251] vsize: 57444
Current children cumulated CPU time (s) 839.28
Current children cumulated vsize (Kb) 59568

[startup+850.65 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14204 0 0 0 84839 85 0 0 25 0 1 0 1788597121 59715584 13868 4294967295 134512640 135094434 3221224432 3221223088 134558254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 14579 13868 145 145 0 14434 0
[pid=3251] vsize: 58316
Current children cumulated CPU time (s) 849.25
Current children cumulated vsize (Kb) 60440

[startup+860.651 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14343 0 0 0 85836 86 0 0 25 0 1 0 1788597121 60264448 14007 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 14713 14007 145 145 0 14568 0
[pid=3251] vsize: 58852
Current children cumulated CPU time (s) 859.23
Current children cumulated vsize (Kb) 60976

[startup+870.652 s]
Raw data (loadavg): 1.00 0.98 0.98 3/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14423 0 0 0 86834 87 0 0 25 0 1 0 1788597121 60579840 14087 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 14790 14087 145 145 0 14645 0
[pid=3251] vsize: 59160
Current children cumulated CPU time (s) 869.22
Current children cumulated vsize (Kb) 61284

[startup+880.653 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14483 0 0 0 87834 87 0 0 25 0 1 0 1788597121 60817408 14147 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 14848 14147 145 145 0 14703 0
[pid=3251] vsize: 59392
Current children cumulated CPU time (s) 879.22
Current children cumulated vsize (Kb) 61516

[startup+890.653 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14540 0 0 0 88833 88 0 0 25 0 1 0 1788597121 61042688 14204 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 14903 14204 145 145 0 14758 0
[pid=3251] vsize: 59612
Current children cumulated CPU time (s) 889.22
Current children cumulated vsize (Kb) 61736

[startup+900.654 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14609 0 0 0 89832 88 0 0 25 0 1 0 1788597121 61313024 14273 4294967295 134512640 135094434 3221224432 3221223120 134554726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 14969 14273 145 145 0 14824 0
[pid=3251] vsize: 59876
Current children cumulated CPU time (s) 899.21
Current children cumulated vsize (Kb) 62000

[startup+910.654 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14700 0 0 0 90830 89 0 0 25 0 1 0 1788597121 61665280 14364 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 15055 14364 145 145 0 14910 0
[pid=3251] vsize: 60220
Current children cumulated CPU time (s) 909.2
Current children cumulated vsize (Kb) 62344

[startup+920.655 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14768 0 0 0 91829 90 0 0 25 0 1 0 1788597121 61935616 14432 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 15121 14432 145 145 0 14976 0
[pid=3251] vsize: 60484
Current children cumulated CPU time (s) 919.2
Current children cumulated vsize (Kb) 62608

[startup+930.657 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14832 0 0 0 92828 90 0 0 25 0 1 0 1788597121 62189568 14496 4294967295 134512640 135094434 3221224432 3221223072 134562088 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 15183 14496 145 145 0 15038 0
[pid=3251] vsize: 60732
Current children cumulated CPU time (s) 929.19
Current children cumulated vsize (Kb) 62856

[startup+940.657 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14929 0 0 0 93826 91 0 0 25 0 1 0 1788597121 62574592 14593 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 15277 14593 145 145 0 15132 0
[pid=3251] vsize: 61108
Current children cumulated CPU time (s) 939.18
Current children cumulated vsize (Kb) 63232

[startup+950.658 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 14975 0 0 0 94826 92 0 0 25 0 1 0 1788597121 62754816 14639 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 15321 14639 145 145 0 15176 0
[pid=3251] vsize: 61284
Current children cumulated CPU time (s) 949.19
Current children cumulated vsize (Kb) 63408

[startup+960.658 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15031 0 0 0 95824 92 0 0 25 0 1 0 1788597121 62976000 14695 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 15375 14695 145 145 0 15230 0
[pid=3251] vsize: 61500
Current children cumulated CPU time (s) 959.17
Current children cumulated vsize (Kb) 63624

[startup+970.659 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15127 0 0 0 96824 93 0 0 25 0 1 0 1788597121 63356928 14791 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 15468 14791 145 145 0 15323 0
[pid=3251] vsize: 61872
Current children cumulated CPU time (s) 969.18
Current children cumulated vsize (Kb) 63996

[startup+980.659 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15250 0 0 0 97821 95 0 0 25 0 1 0 1788597121 63844352 14914 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 15587 14914 145 145 0 15442 0
[pid=3251] vsize: 62348
Current children cumulated CPU time (s) 979.17
Current children cumulated vsize (Kb) 64472

[startup+990.66 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15317 0 0 0 98820 95 0 0 25 0 1 0 1788597121 65159168 14981 4294967295 134512640 135094434 3221224432 3221223104 134554891 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 15908 14981 145 145 0 15763 0
[pid=3251] vsize: 63632
Current children cumulated CPU time (s) 989.16
Current children cumulated vsize (Kb) 65756

[startup+1000.66 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15375 0 0 0 99819 95 0 0 25 0 1 0 1788597121 65388544 15039 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 15964 15039 145 145 0 15819 0
[pid=3251] vsize: 63856
Current children cumulated CPU time (s) 999.15
Current children cumulated vsize (Kb) 65980

[startup+1010.66 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15483 0 0 0 100817 97 0 0 25 0 1 0 1788597121 65814528 15147 4294967295 134512640 135094434 3221224432 3221223076 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 16068 15147 145 145 0 15923 0
[pid=3251] vsize: 64272
Current children cumulated CPU time (s) 1009.15
Current children cumulated vsize (Kb) 66396

[startup+1020.66 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15609 0 0 0 101815 97 0 0 25 0 1 0 1788597121 66314240 15273 4294967295 134512640 135094434 3221224432 3221223120 134784967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 16190 15273 145 145 0 16045 0
[pid=3251] vsize: 64760
Current children cumulated CPU time (s) 1019.13
Current children cumulated vsize (Kb) 66884

[startup+1030.66 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15828 0 0 0 102810 100 0 0 25 0 1 0 1788597121 67190784 15492 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 16404 15492 145 145 0 16259 0
[pid=3251] vsize: 65616
Current children cumulated CPU time (s) 1029.11
Current children cumulated vsize (Kb) 67740

[startup+1040.66 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 15893 0 0 0 103809 100 0 0 25 0 1 0 1788597121 67444736 15557 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 16466 15557 145 145 0 16321 0
[pid=3251] vsize: 65864
Current children cumulated CPU time (s) 1039.1
Current children cumulated vsize (Kb) 67988

[startup+1050.66 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 16312 0 0 0 104802 103 0 0 25 0 1 0 1788597121 69132288 15976 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3251/statm): 16878 15976 145 145 0 16733 0
[pid=3251] vsize: 67512
Current children cumulated CPU time (s) 1049.06
Current children cumulated vsize (Kb) 69636

[startup+1060.66 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 16569 0 0 0 105797 106 0 0 25 0 1 0 1788597121 70168576 16233 4294967295 134512640 135094434 3221224432 3221223000 134538517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 17131 16233 145 145 0 16986 0
[pid=3251] vsize: 68524
Current children cumulated CPU time (s) 1059.04
Current children cumulated vsize (Kb) 70648

[startup+1070.66 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 16687 0 0 0 106795 107 0 0 25 0 1 0 1788597121 70635520 16351 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 17245 16351 145 145 0 17100 0
[pid=3251] vsize: 68980
Current children cumulated CPU time (s) 1069.03
Current children cumulated vsize (Kb) 71104

[startup+1080.66 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 17037 0 0 0 107789 110 0 0 25 0 1 0 1788597121 72044544 16701 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 17589 16701 145 145 0 17444 0
[pid=3251] vsize: 70356
Current children cumulated CPU time (s) 1079
Current children cumulated vsize (Kb) 72480

[startup+1090.67 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 17316 0 0 0 108782 113 0 0 25 0 1 0 1788597121 73162752 16980 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 17862 16980 145 145 0 17717 0
[pid=3251] vsize: 71448
Current children cumulated CPU time (s) 1088.96
Current children cumulated vsize (Kb) 73572

[startup+1100.67 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 17490 0 0 0 109779 114 0 0 25 0 1 0 1788597121 73867264 17154 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 18034 17154 145 145 0 17889 0
[pid=3251] vsize: 72136
Current children cumulated CPU time (s) 1098.94
Current children cumulated vsize (Kb) 74260

[startup+1110.67 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 17675 0 0 0 110776 116 0 0 25 0 1 0 1788597121 74608640 17339 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 18215 17339 145 145 0 18070 0
[pid=3251] vsize: 72860
Current children cumulated CPU time (s) 1108.93
Current children cumulated vsize (Kb) 74984

[startup+1120.67 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 17740 0 0 0 111774 117 0 0 25 0 1 0 1788597121 74858496 17404 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 18276 17404 145 145 0 18131 0
[pid=3251] vsize: 73104
Current children cumulated CPU time (s) 1118.92
Current children cumulated vsize (Kb) 75228

[startup+1130.67 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 17886 0 0 0 112771 119 0 0 25 0 1 0 1788597121 75444224 17550 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 18419 17550 145 145 0 18274 0
[pid=3251] vsize: 73676
Current children cumulated CPU time (s) 1128.91
Current children cumulated vsize (Kb) 75800

[startup+1140.67 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18103 0 0 0 113767 120 0 0 25 0 1 0 1788597121 76316672 17767 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 18632 17767 145 145 0 18487 0
[pid=3251] vsize: 74528
Current children cumulated CPU time (s) 1138.88
Current children cumulated vsize (Kb) 76652

[startup+1150.67 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18171 0 0 0 114765 121 0 0 25 0 1 0 1788597121 76582912 17835 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 18697 17835 145 145 0 18552 0
[pid=3251] vsize: 74788
Current children cumulated CPU time (s) 1148.87
Current children cumulated vsize (Kb) 76912

[startup+1160.67 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18298 0 0 0 115763 123 0 0 25 0 1 0 1788597121 77090816 17962 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 18821 17962 145 145 0 18676 0
[pid=3251] vsize: 75284
Current children cumulated CPU time (s) 1158.87
Current children cumulated vsize (Kb) 77408

[startup+1170.67 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18449 0 0 0 116760 125 0 0 25 0 1 0 1788597121 77692928 18113 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 18968 18113 145 145 0 18823 0
[pid=3251] vsize: 75872
Current children cumulated CPU time (s) 1168.86
Current children cumulated vsize (Kb) 77996

[startup+1180.67 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18590 0 0 0 117756 127 0 0 25 0 1 0 1788597121 78262272 18254 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 19107 18254 145 145 0 18962 0
[pid=3251] vsize: 76428
Current children cumulated CPU time (s) 1178.84
Current children cumulated vsize (Kb) 78552

[startup+1190.68 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18713 0 0 0 118753 129 0 0 25 0 1 0 1788597121 78749696 18377 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 19226 18377 145 145 0 19081 0
[pid=3251] vsize: 76904
Current children cumulated CPU time (s) 1188.83
Current children cumulated vsize (Kb) 79028

[startup+1200.68 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18828 0 0 0 119749 130 0 0 25 0 1 0 1788597121 79208448 18492 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 19338 18492 145 145 0 19193 0
[pid=3251] vsize: 77352
Current children cumulated CPU time (s) 1198.8
Current children cumulated vsize (Kb) 79476

[startup+1210.68 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18965 0 0 0 120746 132 0 0 25 0 1 0 1788597121 79753216 18629 4294967295 134512640 135094434 3221224432 3221223056 134557606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 19471 18629 145 145 0 19326 0
[pid=3251] vsize: 77884
Current children cumulated CPU time (s) 1208.79
Current children cumulated vsize (Kb) 80008



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.68 s]
Raw data (loadavg): 1.00 0.98 0.98 2/57 3251
Raw data (/proc/3247/stat): 3247 (minisat+_script) S 3246 3247 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788597116 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3247/statm): 531 226 485 147 0 384 0
[pid=3247] vsize: 2124
Raw data (/proc/3251/stat): 3251 (minisat+_64-bit) R 3247 3247 22582 0 -1 0 18965 0 0 0 120746 132 0 0 25 0 1 0 1788597121 79753216 18629 4294967295 134512640 135094434 3221224432 3221223056 134557606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3251/statm): 19471 18629 145 145 0 19326 0
[pid=3251] vsize: 77884
Current children cumulated CPU time (s) 1208.79
Current children cumulated vsize (Kb) 80008

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

Child status: 0
Real time (s): 1210.72
CPU time (s): 1208.83
CPU user time (s): 1207.47
CPU system time (s): 1.36179
CPU usage (%): 99.8438
Max. virtual memory (cumulated for all children) (Kb): 80008

Verifier Data

ERROR: no interpretation found !