Some explanations

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

General information on the benchmark

Namemps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-standata.opb
MD5SUMd5b771efe8f3bc863eeca85beb6d9cd6
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 140
Biggest coefficient in the objective function 52428800
Number of bits for the biggest coefficient in the objective function 26
Sum of the numbers in the objective function 318766800
Number of bits of the sum of numbers in the objective function 29
Biggest number in a constraint 75573493760
Number of bits of the biggest number in a constraint 37
Biggest sum of numbers in a constraint 2374370081400
Number of bits of the biggest sum of numbers42
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables20142
Total number of constraints462
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints462
Minimum length of a constraint8
Maximum length of a constraint14900

Trace number 6061

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        888476 kB
Buffers:         16992 kB
Cached:         100324 kB
SwapCached:        868 kB
Active:          38832 kB
Inactive:        81168 kB
HighTotal:      131008 kB
HighFree:        28252 kB
LowTotal:       903652 kB
LowFree:        860224 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5704 kB
Slab:            20356 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:16:32 (client local time) WITH STATUS 0 IN 1209 SECONDS
stats: 3208 7 1209 0

Solver Data

c Parsing PB file...
c Converting 596 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssss
c ---[ 607]---> BDD-cost:   13
c ---[ 606]---> BDD-cost:   12
c ---[ 605]---> BDD-cost:   12
c ---[ 604]---> BDD-cost:   10
c ---[ 603]---> BDD-cost:   10
c ---[ 602]---> BDD-cost:   14
c ---[ 601]---> BDD-cost:   13
c ---[ 600]---> BDD-cost:   12
c ---[ 599]---> BDD-cost:   12
c ---[ 598]---> BDD-cost:   10
c ---[ 597]---> BDD-cost:   10
c ---[ 596]---> BDD-cost:   14
c ---[ 595]---> BDD-cost:   13
c ---[ 594]---> BDD-cost:   12
c ---[ 593]---> BDD-cost:   12
c ---[ 592]---> BDD-cost:   10
c ---[ 591]---> BDD-cost:   10
c ---[ 590]---> BDD-cost:   14
c ---[ 589]---> BDD-cost:   13
c ---[ 588]---> BDD-cost:   12
c ---[ 587]---> BDD-cost:   12
c ---[ 586]---> BDD-cost:   10
c ---[ 585]---> BDD-cost:   10
c ---[ 584]---> BDD-cost:   14
c ---[ 583]---> BDD-cost:   13
c ---[ 582]---> BDD-cost:   12
c ---[ 581]---> BDD-cost:   12
c ---[ 580]---> BDD-cost:   10
c ---[ 579]---> BDD-cost:   10
c ---[ 578]---> BDD-cost:   14
c ---[ 577]---> BDD-cost:   13
c ---[ 576]---> BDD-cost:   12
c ---[ 575]---> BDD-cost:   12
c ---[ 574]---> BDD-cost:   10
c ---[ 573]---> BDD-cost:   10
c ---[ 572]---> BDD-cost:   14
c ---[ 571]---> BDD-cost:   10
c ---[ 570]---> BDD-cost:   10
c ---[ 569]---> BDD-cost:   10
c ---[ 565]---> BDD-cost:   10
c ---[ 564]---> BDD-cost:   10
c ---[ 563]---> BDD-cost:   10
c ---[ 559]---> BDD-cost:    7
c ---[ 557]---> BDD-cost:    7
c ---[ 556]---> BDD-cost:    7
c ---[ 554]---> BDD-cost:    7
c ---[ 553]---> BDD-cost:    7
c ---[ 552]---> BDD-cost:    7
c ---[ 550]---> BDD-cost:    7
c ---[ 549]---> BDD-cost:    7
c ---[ 548]---> BDD-cost:    7
c ---[ 547]---> BDD-cost:    7
c ---[ 545]---> BDD-cost:    7
c ---[ 544]---> BDD-cost:    7
c ---[ 543]---> BDD-cost:    7
c ---[ 542]---> BDD-cost:    7
c ---[ 541]---> BDD-cost:    7
c ---[ 540]---> BDD-cost:    7
c ---[ 539]---> BDD-cost:    7
c ---[ 538]---> BDD-cost:    7
c ---[ 537]---> BDD-cost:    7
c ---[ 536]---> BDD-cost:    7
c ---[ 535]---> BDD-cost:    7
c ---[ 534]---> BDD-cost:    7
c ---[ 533]---> BDD-cost:    7
c ---[ 532]---> BDD-cost:    7
c ---[ 530]---> BDD-cost:    7
c ---[ 529]---> BDD-cost:    7
c ---[ 528]---> BDD-cost:    7
c ---[ 526]---> BDD-cost:    7
c ---[ 525]---> BDD-cost:    7
c ---[ 524]---> BDD-cost:    7
c ---[ 522]---> BDD-cost:    7
c ---[ 521]---> BDD-cost:    7
c ---[ 520]---> BDD-cost:    7
c ---[ 519]---> BDD-cost:    7
c ---[ 517]---> BDD-cost:    7
c ---[ 516]---> BDD-cost:    7
c ---[ 515]---> BDD-cost:    7
c ---[ 514]---> BDD-cost:    7
c ---[ 513]---> BDD-cost:    7
c ---[ 512]---> BDD-cost:    7
c ---[ 511]---> BDD-cost:    7
c ---[ 510]---> BDD-cost:    7
c ---[ 509]---> BDD-cost:    7
c ---[ 508]---> BDD-cost:    7
c ---[ 507]---> BDD-cost:    7
c ---[ 506]---> BDD-cost:    7
c ---[ 505]---> BDD-cost:    7
c ---[ 504]---> BDD-cost:    7
c ---[ 502]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 500]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost:  807     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost:  807     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost:  807     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost:  807     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> Sorter-cost:  807     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost:  807     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> Adder-cost: 382   maxlim: 32767   bits: 16/15
c ---[ 476]---> Adder-cost: 382   maxlim: 32767   bits: 16/15
c ---[ 474]---> Adder-cost: 276   maxlim: 65534   bits: 17/16
c ---[ 472]---> Adder-cost: 295   maxlim: 65534   bits: 17/16
c ---[ 470]---> Adder-cost: 276   maxlim: 65534   bits: 17/16
c ---[ 468]---> Adder-cost: 295   maxlim: 65534   bits: 17/16
c ---[ 466]---> Adder-cost: 408   maxlim: 65535   bits: 17/16
c ---[ 464]---> Adder-cost: 405   maxlim: 65535   bits: 17/16
c ---[ 462]---> Adder-cost: 298   maxlim: 133117   bits: 18/18
c ---[ 460]---> Adder-cost: 318   maxlim: 135165   bits: 18/18
c ---[ 458]---> Adder-cost: 298   maxlim: 133117   bits: 18/18
c ---[ 456]---> Adder-cost: 318   maxlim: 135165   bits: 18/18
c ---[ 454]---> Adder-cost: 382   maxlim: 32767   bits: 16/15
c ---[ 452]---> Adder-cost: 382   maxlim: 32767   bits: 16/15
c ---[ 450]---> Adder-cost: 294   maxlim: 67581   bits: 17/17
c ---[ 448]---> Adder-cost: 338   maxlim: 69629   bits: 18/17
c ---[ 446]---> Adder-cost: 294   maxlim: 67581   bits: 17/17
c ---[ 444]---> Adder-cost: 338   maxlim: 69629   bits: 18/17
c ---[ 442]---> Adder-cost: 408   maxlim: 65535   bits: 17/16
c ---[ 440]---> Adder-cost: 405   maxlim: 65535   bits: 17/16
c ---[ 438]---> Adder-cost: 298   maxlim: 133117   bits: 18/18
c ---[ 436]---> Adder-cost: 344   maxlim: 147453   bits: 19/18
c ---[ 434]---> Adder-cost: 298   maxlim: 133117   bits: 18/18
c ---[ 432]---> Adder-cost: 344   maxlim: 147453   bits: 19/18
c ---[ 430]---> Adder-cost: 382   maxlim: 32767   bits: 16/15
c ---[ 428]---> Adder-cost: 382   maxlim: 32767   bits: 16/15
c ---[ 426]---> Adder-cost: 294   maxlim: 67581   bits: 17/17
c ---[ 424]---> Adder-cost: 360   maxlim: 81917   bits: 18/17
c ---[ 422]---> Adder-cost: 294   maxlim: 67581   bits: 17/17
c ---[ 420]---> Adder-cost: 360   maxlim: 81917   bits: 18/17
c ---[ 418]---> Adder-cost: 408   maxlim: 65535   bits: 17/16
c ---[ 416]---> Adder-cost: 405   maxlim: 65535   bits: 17/16
c ---[ 414]---> Adder-cost: 298   maxlim: 133117   bits: 18/18
c ---[ 412]---> Adder-cost: 362   maxlim: 163837   bits: 19/18
c ---[ 410]---> Adder-cost: 298   maxlim: 133117   bits: 18/18
c ---[ 408]---> Adder-cost: 362   maxlim: 163837   bits: 19/18
c ---[ 406]---> Adder-cost: 382   maxlim: 32767   bits: 16/15
c ---[ 404]---> Adder-cost: 382   maxlim: 32767   bits: 16/15
c ---[ 402]---> Adder-cost: 276   maxlim: 65534   bits: 17/16
c ---[ 400]---> Adder-cost: 295   maxlim: 65534   bits: 17/16
c ---[ 398]---> Adder-cost: 276   maxlim: 65534   bits: 17/16
c ---[ 396]---> Adder-cost: 295   maxlim: 65534   bits: 17/16
c ---[ 394]---> Adder-cost: 408   maxlim: 65535   bits: 17/16
c ---[ 392]---> Adder-cost: 405   maxlim: 65535   bits: 17/16
c ---[ 390]---> Adder-cost: 298   maxlim: 133117   bits: 18/18
c ---[ 388]---> Adder-cost: 318   maxlim: 135165   bits: 18/18
c ---[ 386]---> Adder-cost: 298   maxlim: 133117   bits: 18/18
c ---[ 384]---> Adder-cost: 318   maxlim: 135165   bits: 18/18
c ---[ 382]---> Adder-cost: 382   maxlim: 32767   bits: 16/15
c ---[ 380]---> Adder-cost: 382   maxlim: 32767   bits: 16/15
c ---[ 378]---> Adder-cost: 294   maxlim: 67581   bits: 17/17
c ---[ 376]---> Adder-cost: 338   maxlim: 69629   bits: 18/17
c ---[ 374]---> Adder-cost: 294   maxlim: 67581   bits: 17/17
c ---[ 372]---> Adder-cost: 338   maxlim: 69629   bits: 18/17
c ---[ 370]---> Adder-cost: 408   maxlim: 65535   bits: 17/16
c ---[ 368]---> Adder-cost: 405   maxlim: 65535   bits: 17/16
c ---[ 366]---> Adder-cost: 298   maxlim: 133117   bits: 18/18
c ---[ 364]---> Adder-cost: 344   maxlim: 147453   bits: 19/18
c ---[ 362]---> Adder-cost: 298   maxlim: 133117   bits: 18/18
c ---[ 360]---> Adder-cost: 344   maxlim: 147453   bits: 19/18
c ---[ 358]---> Adder-cost: 382   maxlim: 32767   bits: 16/15
c ---[ 356]---> Adder-cost: 382   maxlim: 32767   bits: 16/15
c ---[ 354]---> Adder-cost: 294   maxlim: 67581   bits: 17/17
c ---[ 352]---> Adder-cost: 360   maxlim: 81917   bits: 18/17
c ---[ 350]---> Adder-cost: 294   maxlim: 67581   bits: 17/17
c ---[ 348]---> Adder-cost: 360   maxlim: 81917   bits: 18/17
c ---[ 346]---> Adder-cost: 408   maxlim: 65535   bits: 17/16
c ---[ 344]---> Adder-cost: 405   maxlim: 65535   bits: 17/16
c ---[ 342]---> Adder-cost: 298   maxlim: 133117   bits: 18/18
c ---[ 340]---> Adder-cost: 362   maxlim: 163837   bits: 19/18
c ---[ 338]---> Adder-cost: 298   maxlim: 133117   bits: 18/18
c ---[ 336]---> Adder-cost: 362   maxlim: 163837   bits: 19/18
c ---[ 334]---> BDD-cost:   31
c ---[ 332]---> BDD-cost:   34
c ---[ 330]---> BDD-cost:   31
c ---[ 328]---> BDD-cost:   34
c ---[ 326]---> BDD-cost:   31
c ---[ 324]---> BDD-cost:   34
c ---[ 322]---> BDD-cost:   31
c ---[ 320]---> BDD-cost:   34
c ---[ 318]---> BDD-cost:   91
c ---[ 316]---> Sorter-cost:  496     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> BDD-cost:   91
c ---[ 312]---> Sorter-cost:  496     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> BDD-cost:   31
c ---[ 308]---> BDD-cost:   40
c ---[ 306]---> BDD-cost:   31
c ---[ 304]---> BDD-cost:   40
c ---[ 302]---> BDD-cost:   91
c ---[ 300]---> Sorter-cost:  494     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> BDD-cost:   91
c ---[ 296]---> Sorter-cost:  494     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 294]---> BDD-cost:   31
c ---[ 292]---> BDD-cost:   43
c ---[ 290]---> BDD-cost:   31
c ---[ 288]---> BDD-cost:   43
c ---[ 286]---> Adder-cost: 3650   maxlim: 6944215190   bits: 34/33
c ---[ 284]---> Adder-cost: 1968   maxlim: 1425264   bits: 22/21
c ---[ 283]---> Adder-cost: 758   maxlim: 8556339   bits: 25/24
c ---[ 282]---> Adder-cost: 941   maxlim: 13112437   bits: 25/24
c ---[ 281]---> Adder-cost: 847   maxlim: 12840657   bits: 25/24
c ---[ 279]---> Adder-cost: 584   maxlim: 1241022   bits: 22/21
c ---[ 277]---> Adder-cost: 72306   maxlim: 8075354693   bits: 33/33
c ---[ 276]---> BDD-cost:   87
c ---[ 275]---> BDD-cost:   96
c ---[ 274]---> BDD-cost:   87
c ---[ 273]---> BDD-cost:   96
c ---[ 272]---> BDD-cost:   87
c ---[ 271]---> BDD-cost:   96
c ---[ 270]---> BDD-cost:   87
c ---[ 269]---> BDD-cost:   96
c ---[ 268]---> BDD-cost:   87
c ---[ 267]---> BDD-cost:  114
c ---[ 266]---> BDD-cost:   87
c ---[ 265]---> BDD-cost:  114
c ---[ 264]---> BDD-cost:   87
c ---[ 263]---> BDD-cost:  114
c ---[ 262]---> BDD-cost:   87
c ---[ 261]---> BDD-cost:  114
c ---[ 260]---> BDD-cost:   87
c ---[ 259]---> BDD-cost:  123
c ---[ 258]---> BDD-cost:   87
c ---[ 257]---> BDD-cost:  123
c ---[ 256]---> BDD-cost:   87
c ---[ 255]---> BDD-cost:  123
c ---[ 254]---> BDD-cost:   87
c ---[ 253]---> BDD-cost:  123
c ---[ 251]---> Sorter-cost:  483     Base: 2 2 2 3 5 2 2 2
c ---[ 249]---> Sorter-cost:  483     Base: 2 2 2 3 5 2 2 2
c ---[ 247]---> Sorter-cost:  483     Base: 2 2 2 3 5 2 2 2
c ---[ 245]---> Sorter-cost:  483     Base: 2 2 2 3 5 2 2 2
c ---[ 243]---> Sorter-cost:  483     Base: 2 2 2 3 5 2 2 2
c ---[ 241]---> Sorter-cost:  483     Base: 2 2 2 3 5 2 2 2
c ---[ 240]---> BDD-cost:    3
c ---[ 239]---> BDD-cost:   71
c ---[ 238]---> BDD-cost:    3
c ---[ 237]---> BDD-cost:   71
c ---[ 235]---> BDD-cost:   71
c ---[ 233]---> BDD-cost:   71
c ---[ 231]---> BDD-cost:   71
c ---[ 229]---> BDD-cost:   71
c ---[ 228]---> BDD-cost:    0
c ---[ 227]---> BDD-cost:   22
c ---[ 226]---> BDD-cost:   22
c ---[ 225]---> BDD-cost:   63
c ---[ 224]---> BDD-cost:   63
c ---[ 223]---> Sorter-cost:  178     Base: 2 2 2 2 2 2 2 2 2
c ---[ 222]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> BDD-cost:   10
c ---[ 220]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 219]---> BDD-cost:   10
c ---[ 218]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 217]---> BDD-cost:   10
c ---[ 216]---> Sorter-cost:  180     Base: 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> BDD-cost:   23
c ---[ 207]---> BDD-cost:   73
c ---[ 206]---> BDD-cost:   73
c ---[ 204]---> Sorter-cost:  548     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 202]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 200]---> BDD-cost:  132
c ---[ 198]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 196]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 194]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 192]---> BDD-cost:  132
c ---[ 190]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost:  579     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 184]---> BDD-cost:  136
c ---[ 182]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 178]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  588     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost:  588     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost:  548     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 156]---> Sorter-cost:  579     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 154]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 152]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 150]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 146]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 144]---> Sorter-cost:  588     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 142]---> Sorter-cost:  588     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> Sorter-cost:  548     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 138]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 136]---> BDD-cost:  132
c ---[ 134]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 132]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 130]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 128]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> Sorter-cost:  557     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 124]---> Sorter-cost:  579     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 122]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> BDD-cost:  136
c ---[ 118]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 116]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 114]---> Sorter-cost:  603     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> Sorter-cost:  588     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 110]---> Sorter-cost:  588     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 109]---> BDD-cost:   11
c ---[ 108]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 107]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 104]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 103]---> BDD-cost:   11
c ---[ 102]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 101]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 100]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  97]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  96]---> BDD-cost:   11
c ---[  95]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  94]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  93]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  92]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  90]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  89]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  88]---> BDD-cost:   11
c ---[  87]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  86]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  85]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  84]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  83]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  82]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  81]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  80]---> BDD-cost:   11
c ---[  79]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  78]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  77]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  76]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  75]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  74]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  73]---> BDD-cost:   11
c ---[  72]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  71]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  70]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  69]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  68]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  67]---> Sorter-cost:  304     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  66]---> BDD-cost:    3
c ---[  65]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  62]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> BDD-cost:    3
c ---[  59]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  58]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> BDD-cost:    3
c ---[  52]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  50]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> BDD-cost:    3
c ---[  44]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  37]---> BDD-cost:    3
c ---[  36]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> BDD-cost:    3
c ---[  29]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  288     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Adder-cost: 700   maxlim: 144219   bits: 18/18
c ---[  22]---> Adder-cost: 816   maxlim: 294875   bits: 19/19
c ---[  21]---> Adder-cost: 700   maxlim: 144219   bits: 18/18
c ---[  20]---> Adder-cost: 816   maxlim: 294875   bits: 19/19
c ---[  19]---> Adder-cost: 840   maxlim: 144219   bits: 18/18
c ---[  18]---> Adder-cost: 1058   maxlim: 589787   bits: 20/20
c ---[  17]---> Adder-cost: 840   maxlim: 144219   bits: 18/18
c ---[  16]---> Adder-cost: 1058   maxlim: 589787   bits: 20/20
c ---[  15]---> Adder-cost: 840   maxlim: 144219   bits: 18/18
c ---[  14]---> Adder-cost: 1164   maxlim: 1179611   bits: 21/21
c ---[  13]---> Adder-cost: 840   maxlim: 144219   bits: 18/18
c ---[  12]---> Adder-cost: 1164   maxlim: 1179611   bits: 21/21
c ---[  11]---> BDD-cost:    7
c ---[  10]---> BDD-cost:    7
c ---[   9]---> BDD-cost:    7
c ---[   8]---> BDD-cost:    7
c ---[   7]---> BDD-cost:    7
c ---[   6]---> BDD-cost:    7
c ---[   5]---> BDD-cost:    7
c ---[   4]---> BDD-cost:    7
c ---[   3]---> BDD-cost:   22
c ---[   2]---> BDD-cost:   22
c ---[   1]---> BDD-cost:   22
c ---[   0]---> BDD-cost:   22
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  964494  3250947 |  321498       0        0     nan |  0.000 % |
c |       100 |  964331  3250496 |  353647      71      212     3.0 |  5.726 % |
c |       250 |  964292  3250380 |  389012     216      684     3.2 |  5.730 % |
c |       475 |  964164  3249932 |  427913     422     1338     3.2 |  5.742 % |
c |       812 |  964054  3249548 |  470705     741     2389     3.2 |  5.751 % |
c |      1318 |  963590  3248197 |  517775    1208     4611     3.8 |  5.804 % |
c |      2077 |  963438  3247780 |  569553    1930    12716     6.6 |  5.821 % |
c |      3216 |  963043  3246783 |  626508    3009    27069     9.0 |  5.873 % |
c |      4924 |  962716  3245674 |  689159    4659    40585     8.7 |  5.902 % |
c |      7486 |  962353  3244530 |  758075    7155    74764    10.4 |  5.938 % |
c |     11331 |  958289  3234249 |  833883   10771   121891    11.3 |  6.432 % |
c |     17098 |  953153  3220663 |  917271   16136   179868    11.1 |  7.050 % |
c |     25748 |  944182  3198431 | 1008998   24004   256574    10.7 |  8.232 % |
c |     38723 |  940321  3188063 | 1109898   36593   590043    16.1 |  8.670 % |

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/16597/stat): 16597 (minisat+_script) R 16596 16597 16528 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1855116382 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/16597/statm): 174 3 169 147 0 27 0
[pid=16597] 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=16598
New process pid=16599
New process pid=16600
execve syscall for /bin/sed executable
One traced child (pid=16599) 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=16600) exited with status: 0
One traced child (pid=16598) exited with status: 0
New process pid=16601
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-standata.opb

[startup+10.0034 s]
Raw data (loadavg): 0.88 0.94 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 7079 0 0 0 952 25 0 0 24 0 1 0 1855116387 25546752 5706 4294967295 134512640 135094434 3221224432 3221172512 134597418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 6237 5706 145 145 0 6092 0
[pid=16601] vsize: 24948
Current children cumulated CPU time (s) 9.77
Current children cumulated vsize (Kb) 27072

[startup+20.005 s]
Raw data (loadavg): 0.90 0.94 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 1922 41 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221219696 134677363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 19.63
Current children cumulated vsize (Kb) 28160

[startup+30.0057 s]
Raw data (loadavg): 0.91 0.94 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 2922 41 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 29.63
Current children cumulated vsize (Kb) 28160

[startup+40.0064 s]
Raw data (loadavg): 0.93 0.94 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 3922 41 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220400 134599950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 39.63
Current children cumulated vsize (Kb) 28160

[startup+50.0071 s]
Raw data (loadavg): 0.94 0.95 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 4922 41 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220288 134676341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 49.63
Current children cumulated vsize (Kb) 28160

[startup+60.0067 s]
Raw data (loadavg): 0.95 0.95 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 5922 41 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221219792 134676280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 59.63
Current children cumulated vsize (Kb) 28160

[startup+70.0074 s]
Raw data (loadavg): 0.95 0.95 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 6923 41 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221219792 134677021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 69.64
Current children cumulated vsize (Kb) 28160

[startup+80.0081 s]
Raw data (loadavg): 0.96 0.95 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 7923 41 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220224 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 79.64
Current children cumulated vsize (Kb) 28160

[startup+90.0088 s]
Raw data (loadavg): 0.97 0.95 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 8923 41 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220576 134600310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 89.64
Current children cumulated vsize (Kb) 28160

[startup+100.009 s]
Raw data (loadavg): 0.97 0.95 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 9923 41 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221219968 134676999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 99.64
Current children cumulated vsize (Kb) 28160

[startup+110.01 s]
Raw data (loadavg): 0.97 0.95 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 10923 41 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220576 134600291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 109.64
Current children cumulated vsize (Kb) 28160

[startup+120.011 s]
Raw data (loadavg): 0.98 0.95 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 11923 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 119.65
Current children cumulated vsize (Kb) 28160

[startup+130.012 s]
Raw data (loadavg): 0.98 0.95 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 12924 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220208 134600167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 129.66
Current children cumulated vsize (Kb) 28160

[startup+140.012 s]
Raw data (loadavg): 0.98 0.95 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 13924 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221219932 134676460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 139.66
Current children cumulated vsize (Kb) 28160

[startup+150.013 s]
Raw data (loadavg): 0.99 0.95 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 14924 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220448 134676465 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 149.66
Current children cumulated vsize (Kb) 28160

[startup+160.014 s]
Raw data (loadavg): 0.99 0.96 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 15924 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220192 134676993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 159.66
Current children cumulated vsize (Kb) 28160

[startup+170.014 s]
Raw data (loadavg): 0.99 0.96 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 16924 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220848 134677138 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 169.66
Current children cumulated vsize (Kb) 28160

[startup+180.015 s]
Raw data (loadavg): 0.99 0.96 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 17924 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 179.66
Current children cumulated vsize (Kb) 28160

[startup+190.017 s]
Raw data (loadavg): 0.99 0.96 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 18924 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220080 134783376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 189.66
Current children cumulated vsize (Kb) 28160

[startup+200.017 s]
Raw data (loadavg): 0.99 0.96 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 19924 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 199.66
Current children cumulated vsize (Kb) 28160

[startup+210.017 s]
Raw data (loadavg): 0.99 0.96 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 20925 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220576 134677271 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 209.67
Current children cumulated vsize (Kb) 28160

[startup+220.019 s]
Raw data (loadavg): 0.99 0.96 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 21925 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 219.67
Current children cumulated vsize (Kb) 28160

[startup+230.019 s]
Raw data (loadavg): 0.99 0.96 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 22925 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221221264 134600167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 229.67
Current children cumulated vsize (Kb) 28160

[startup+240.02 s]
Raw data (loadavg): 0.99 0.96 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 23925 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221221104 134600151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 239.67
Current children cumulated vsize (Kb) 28160

[startup+250.021 s]
Raw data (loadavg): 0.99 0.96 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 24926 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220224 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 249.68
Current children cumulated vsize (Kb) 28160

[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 25926 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220928 134677313 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 259.68
Current children cumulated vsize (Kb) 28160

[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 26926 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 269.68
Current children cumulated vsize (Kb) 28160

[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 27926 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 279.68
Current children cumulated vsize (Kb) 28160

[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 28927 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 289.69
Current children cumulated vsize (Kb) 28160

[startup+300.025 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 29927 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221221248 134518676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 299.69
Current children cumulated vsize (Kb) 28160

[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 30927 42 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220224 134600186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 309.69
Current children cumulated vsize (Kb) 28160

[startup+320.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 31927 43 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220576 134676601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 319.7
Current children cumulated vsize (Kb) 28160

[startup+330.028 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 32927 43 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220320 134676999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 329.7
Current children cumulated vsize (Kb) 28160

[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 33928 43 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220452 134676464 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 339.71
Current children cumulated vsize (Kb) 28160

[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 34928 43 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221221152 134677375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 349.71
Current children cumulated vsize (Kb) 28160

[startup+360.03 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 35928 43 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221221104 134600215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 359.71
Current children cumulated vsize (Kb) 28160

[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 36928 43 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220928 134676480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 369.71
Current children cumulated vsize (Kb) 28160

[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 37928 43 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 379.71
Current children cumulated vsize (Kb) 28160

[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 38928 43 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221219616 134676349 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 389.71
Current children cumulated vsize (Kb) 28160

[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 39929 43 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 399.72
Current children cumulated vsize (Kb) 28160

[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 40929 43 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220752 134600008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 409.72
Current children cumulated vsize (Kb) 28160

[startup+420.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 41929 43 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220472 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 419.72
Current children cumulated vsize (Kb) 28160

[startup+430.035 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 42929 43 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221221456 134600144 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 429.72
Current children cumulated vsize (Kb) 28160

[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 43929 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220208 134600167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 439.73
Current children cumulated vsize (Kb) 28160

[startup+450.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 44929 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220848 134676251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 449.73
Current children cumulated vsize (Kb) 28160

[startup+460.037 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 45930 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220928 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 459.74
Current children cumulated vsize (Kb) 28160

[startup+470.038 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 46930 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220824 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 469.74
Current children cumulated vsize (Kb) 28160

[startup+480.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 47930 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220752 134676480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 479.74
Current children cumulated vsize (Kb) 28160

[startup+490.039 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 48930 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221221280 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 489.74
Current children cumulated vsize (Kb) 28160

[startup+500.04 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 49930 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221219792 134677069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 499.74
Current children cumulated vsize (Kb) 28160

[startup+510.041 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 50931 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 509.75
Current children cumulated vsize (Kb) 28160

[startup+520.041 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 51931 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221219968 134677049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 519.75
Current children cumulated vsize (Kb) 28160

[startup+530.042 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 52931 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 529.75
Current children cumulated vsize (Kb) 28160

[startup+540.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 53931 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220740 134600159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 539.75
Current children cumulated vsize (Kb) 28160

[startup+550.044 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 54932 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220736 134600241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 549.76
Current children cumulated vsize (Kb) 28160

[startup+560.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 55932 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221221516 134677378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 559.76
Current children cumulated vsize (Kb) 28160

[startup+570.046 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 56932 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 569.76
Current children cumulated vsize (Kb) 28160

[startup+580.045 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 57932 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221220752 134676516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 579.76
Current children cumulated vsize (Kb) 28160

[startup+590.046 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12011 0 0 0 58932 44 0 0 25 0 1 0 1855116387 26660864 5992 4294967295 134512640 135094434 3221224432 3221221728 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6509 5992 145 145 0 6364 0
[pid=16601] vsize: 26036
Current children cumulated CPU time (s) 589.76
Current children cumulated vsize (Kb) 28160

[startup+600.047 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12142 0 0 0 59932 44 0 0 25 0 1 0 1855116387 26824704 5958 4294967295 134512640 135094434 3221224432 3221221984 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6549 5958 145 145 0 6404 0
[pid=16601] vsize: 26196
Current children cumulated CPU time (s) 599.76
Current children cumulated vsize (Kb) 28320

[startup+610.047 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 12142 0 0 0 60933 44 0 0 25 0 1 0 1855116387 26824704 5958 4294967295 134512640 135094434 3221224432 3221221280 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 6549 5958 145 145 0 6404 0
[pid=16601] vsize: 26196
Current children cumulated CPU time (s) 609.77
Current children cumulated vsize (Kb) 28320

[startup+620.048 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 13495 0 0 0 61930 48 0 0 25 0 1 0 1855116387 30105600 6652 4294967295 134512640 135094434 3221224432 3221220144 134676349 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 7350 6652 145 145 0 7205 0
[pid=16601] vsize: 29400
Current children cumulated CPU time (s) 619.78
Current children cumulated vsize (Kb) 31524

[startup+630.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 13495 0 0 0 62930 48 0 0 25 0 1 0 1855116387 30105600 6652 4294967295 134512640 135094434 3221224432 3221220400 134677327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 7350 6652 145 145 0 7205 0
[pid=16601] vsize: 29400
Current children cumulated CPU time (s) 629.78
Current children cumulated vsize (Kb) 31524

[startup+640.049 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 13495 0 0 0 63930 48 0 0 25 0 1 0 1855116387 30105600 6652 4294967295 134512640 135094434 3221224432 3221221552 134676321 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 7350 6652 145 145 0 7205 0
[pid=16601] vsize: 29400
Current children cumulated CPU time (s) 639.78
Current children cumulated vsize (Kb) 31524

[startup+650.05 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 13495 0 0 0 64930 48 0 0 25 0 1 0 1855116387 30105600 6652 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 7350 6652 145 145 0 7205 0
[pid=16601] vsize: 29400
Current children cumulated CPU time (s) 649.78
Current children cumulated vsize (Kb) 31524

[startup+660.051 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 13495 0 0 0 65930 48 0 0 25 0 1 0 1855116387 30105600 6652 4294967295 134512640 135094434 3221224432 3221220928 134677330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 7350 6652 145 145 0 7205 0
[pid=16601] vsize: 29400
Current children cumulated CPU time (s) 659.78
Current children cumulated vsize (Kb) 31524

[startup+670.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 13495 0 0 0 66931 48 0 0 25 0 1 0 1855116387 30105600 6652 4294967295 134512640 135094434 3221224432 3221221172 134677085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 7350 6652 145 145 0 7205 0
[pid=16601] vsize: 29400
Current children cumulated CPU time (s) 669.79
Current children cumulated vsize (Kb) 31524

[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 13495 0 0 0 67931 48 0 0 25 0 1 0 1855116387 30105600 6652 4294967295 134512640 135094434 3221224432 3221221632 134600301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 7350 6652 145 145 0 7205 0
[pid=16601] vsize: 29400
Current children cumulated CPU time (s) 679.79
Current children cumulated vsize (Kb) 31524

[startup+690.053 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 13495 0 0 0 68931 48 0 0 25 0 1 0 1855116387 30105600 6652 4294967295 134512640 135094434 3221224432 3221221704 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 7350 6652 145 145 0 7205 0
[pid=16601] vsize: 29400
Current children cumulated CPU time (s) 689.79
Current children cumulated vsize (Kb) 31524

[startup+700.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 13495 0 0 0 69931 48 0 0 25 0 1 0 1855116387 30105600 6652 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 7350 6652 145 145 0 7205 0
[pid=16601] vsize: 29400
Current children cumulated CPU time (s) 699.79
Current children cumulated vsize (Kb) 31524

[startup+710.054 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 13495 0 0 0 70931 48 0 0 25 0 1 0 1855116387 30105600 6652 4294967295 134512640 135094434 3221224432 3221222016 134783376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 7350 6652 145 145 0 7205 0
[pid=16601] vsize: 29400
Current children cumulated CPU time (s) 709.79
Current children cumulated vsize (Kb) 31524

[startup+720.055 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 13495 0 0 0 71931 48 0 0 25 0 1 0 1855116387 30105600 6652 4294967295 134512640 135094434 3221224432 3221222232 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 7350 6652 145 145 0 7205 0
[pid=16601] vsize: 29400
Current children cumulated CPU time (s) 719.79
Current children cumulated vsize (Kb) 31524

[startup+730.056 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 13495 0 0 0 72932 48 0 0 25 0 1 0 1855116387 30105600 6652 4294967295 134512640 135094434 3221224432 3221221712 134676328 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 7350 6652 145 145 0 7205 0
[pid=16601] vsize: 29400
Current children cumulated CPU time (s) 729.8
Current children cumulated vsize (Kb) 31524

[startup+740.057 s]
Raw data (loadavg): 0.99 0.97 0.97 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 18910 0 0 0 73919 61 0 0 25 0 1 0 1855116387 50343936 10749 4294967295 134512640 135094434 3221224432 3221220784 134519050 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 12291 10749 145 145 0 12146 0
[pid=16601] vsize: 49164
Current children cumulated CPU time (s) 739.8
Current children cumulated vsize (Kb) 51288

[startup+750.059 s]
Raw data (loadavg): 1.07 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35303 0 0 0 74779 128 0 0 25 0 1 0 1855116387 117649408 27050 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 28723 27050 145 145 0 28578 0
[pid=16601] vsize: 114892
Current children cumulated CPU time (s) 749.07
Current children cumulated vsize (Kb) 117016

[startup+760.059 s]
Raw data (loadavg): 1.06 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35337 0 0 0 75778 129 0 0 25 0 1 0 1855116387 117788672 27084 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 28757 27084 145 145 0 28612 0
[pid=16601] vsize: 115028
Current children cumulated CPU time (s) 759.07
Current children cumulated vsize (Kb) 117152

[startup+770.059 s]
Raw data (loadavg): 1.05 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35395 0 0 0 76778 129 0 0 25 0 1 0 1855116387 118026240 27142 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 28815 27142 145 145 0 28670 0
[pid=16601] vsize: 115260
Current children cumulated CPU time (s) 769.07
Current children cumulated vsize (Kb) 117384

[startup+780.06 s]
Raw data (loadavg): 1.04 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35487 0 0 0 77777 129 0 0 25 0 1 0 1855116387 118403072 27234 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 28907 27234 145 145 0 28762 0
[pid=16601] vsize: 115628
Current children cumulated CPU time (s) 779.06
Current children cumulated vsize (Kb) 117752

[startup+790.061 s]
Raw data (loadavg): 1.04 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35588 0 0 0 78776 130 0 0 25 0 1 0 1855116387 118820864 27335 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29009 27335 145 145 0 28864 0
[pid=16601] vsize: 116036
Current children cumulated CPU time (s) 789.06
Current children cumulated vsize (Kb) 118160

[startup+800.062 s]
Raw data (loadavg): 1.03 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35645 0 0 0 79775 131 0 0 25 0 1 0 1855116387 119054336 27392 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29066 27392 145 145 0 28921 0
[pid=16601] vsize: 116264
Current children cumulated CPU time (s) 799.06
Current children cumulated vsize (Kb) 118388

[startup+810.062 s]
Raw data (loadavg): 1.03 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35687 0 0 0 80774 131 0 0 25 0 1 0 1855116387 119222272 27434 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29107 27434 145 145 0 28962 0
[pid=16601] vsize: 116428
Current children cumulated CPU time (s) 809.05
Current children cumulated vsize (Kb) 118552

[startup+820.063 s]
Raw data (loadavg): 1.02 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35719 0 0 0 81774 131 0 0 25 0 1 0 1855116387 119382016 27466 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29146 27466 145 145 0 29001 0
[pid=16601] vsize: 116584
Current children cumulated CPU time (s) 819.05
Current children cumulated vsize (Kb) 118708

[startup+830.064 s]
Raw data (loadavg): 1.02 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35744 0 0 0 82774 131 0 0 25 0 1 0 1855116387 119484416 27491 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29171 27491 145 145 0 29026 0
[pid=16601] vsize: 116684
Current children cumulated CPU time (s) 829.05
Current children cumulated vsize (Kb) 118808

[startup+840.064 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35801 0 0 0 83773 132 0 0 25 0 1 0 1855116387 119693312 27548 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29222 27548 145 145 0 29077 0
[pid=16601] vsize: 116888
Current children cumulated CPU time (s) 839.05
Current children cumulated vsize (Kb) 119012

[startup+850.065 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35883 0 0 0 84772 132 0 0 25 0 1 0 1855116387 119992320 27630 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29295 27630 145 145 0 29150 0
[pid=16601] vsize: 117180
Current children cumulated CPU time (s) 849.04
Current children cumulated vsize (Kb) 119304

[startup+860.066 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35931 0 0 0 85771 133 0 0 25 0 1 0 1855116387 120172544 27678 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29339 27678 145 145 0 29194 0
[pid=16601] vsize: 117356
Current children cumulated CPU time (s) 859.04
Current children cumulated vsize (Kb) 119480

[startup+870.066 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 35983 0 0 0 86770 133 0 0 25 0 1 0 1855116387 120385536 27730 4294967295 134512640 135094434 3221224432 3221223116 134553526 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29391 27730 145 145 0 29246 0
[pid=16601] vsize: 117564
Current children cumulated CPU time (s) 869.03
Current children cumulated vsize (Kb) 119688

[startup+880.067 s]
Raw data (loadavg): 1.01 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36013 0 0 0 87770 133 0 0 25 0 1 0 1855116387 120496128 27760 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29418 27760 145 145 0 29273 0
[pid=16601] vsize: 117672
Current children cumulated CPU time (s) 879.03
Current children cumulated vsize (Kb) 119796

[startup+890.068 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36048 0 0 0 88770 133 0 0 25 0 1 0 1855116387 120635392 27795 4294967295 134512640 135094434 3221224432 3221223112 134553525 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29452 27795 145 145 0 29307 0
[pid=16601] vsize: 117808
Current children cumulated CPU time (s) 889.03
Current children cumulated vsize (Kb) 119932

[startup+900.068 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36075 0 0 0 89770 133 0 0 25 0 1 0 1855116387 120733696 27822 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29476 27822 145 145 0 29331 0
[pid=16601] vsize: 117904
Current children cumulated CPU time (s) 899.03
Current children cumulated vsize (Kb) 120028

[startup+910.068 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36112 0 0 0 90770 133 0 0 25 0 1 0 1855116387 120877056 27859 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29511 27859 145 145 0 29366 0
[pid=16601] vsize: 118044
Current children cumulated CPU time (s) 909.03
Current children cumulated vsize (Kb) 120168

[startup+920.07 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36136 0 0 0 91770 134 0 0 25 0 1 0 1855116387 120967168 27883 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16601/statm): 29533 27883 145 145 0 29388 0
[pid=16601] vsize: 118132
Current children cumulated CPU time (s) 919.04
Current children cumulated vsize (Kb) 120256

[startup+930.07 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36158 0 0 0 92770 134 0 0 25 0 1 0 1855116387 121057280 27905 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29555 27905 145 145 0 29410 0
[pid=16601] vsize: 118220
Current children cumulated CPU time (s) 929.04
Current children cumulated vsize (Kb) 120344

[startup+940.071 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36206 0 0 0 93769 134 0 0 25 0 1 0 1855116387 121286656 27953 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29611 27953 145 145 0 29466 0
[pid=16601] vsize: 118444
Current children cumulated CPU time (s) 939.03
Current children cumulated vsize (Kb) 120568

[startup+950.073 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36226 0 0 0 94768 136 0 0 25 0 1 0 1855116387 121368576 27973 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29631 27973 145 145 0 29486 0
[pid=16601] vsize: 118524
Current children cumulated CPU time (s) 949.04
Current children cumulated vsize (Kb) 120648

[startup+960.073 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36254 0 0 0 95767 136 0 0 25 0 1 0 1855116387 121479168 28001 4294967295 134512640 135094434 3221224432 3221223092 134553528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29658 28001 145 145 0 29513 0
[pid=16601] vsize: 118632
Current children cumulated CPU time (s) 959.03
Current children cumulated vsize (Kb) 120756

[startup+970.074 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36276 0 0 0 96766 137 0 0 25 0 1 0 1855116387 121569280 28023 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29680 28023 145 145 0 29535 0
[pid=16601] vsize: 118720
Current children cumulated CPU time (s) 969.03
Current children cumulated vsize (Kb) 120844

[startup+980.076 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36309 0 0 0 97766 137 0 0 25 0 1 0 1855116387 121683968 28056 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29708 28056 145 145 0 29563 0
[pid=16601] vsize: 118832
Current children cumulated CPU time (s) 979.03
Current children cumulated vsize (Kb) 120956

[startup+990.077 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36315 0 0 0 98766 137 0 0 25 0 1 0 1855116387 121708544 28062 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29714 28062 145 145 0 29569 0
[pid=16601] vsize: 118856
Current children cumulated CPU time (s) 989.03
Current children cumulated vsize (Kb) 120980

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36335 0 0 0 99765 138 0 0 25 0 1 0 1855116387 121790464 28082 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29734 28082 145 145 0 29589 0
[pid=16601] vsize: 118936
Current children cumulated CPU time (s) 999.03
Current children cumulated vsize (Kb) 121060

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36347 0 0 0 100764 139 0 0 25 0 1 0 1855116387 121835520 28094 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29745 28094 145 145 0 29600 0
[pid=16601] vsize: 118980
Current children cumulated CPU time (s) 1009.03
Current children cumulated vsize (Kb) 121104

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36371 0 0 0 101764 139 0 0 25 0 1 0 1855116387 121925632 28118 4294967295 134512640 135094434 3221224432 3221223112 134553433 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29767 28118 145 145 0 29622 0
[pid=16601] vsize: 119068
Current children cumulated CPU time (s) 1019.03
Current children cumulated vsize (Kb) 121192

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36382 0 0 0 102764 139 0 0 25 0 1 0 1855116387 121970688 28129 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29778 28129 145 145 0 29633 0
[pid=16601] vsize: 119112
Current children cumulated CPU time (s) 1029.03
Current children cumulated vsize (Kb) 121236

[startup+1040.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36393 0 0 0 103763 139 0 0 25 0 1 0 1855116387 122011648 28140 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29788 28140 145 145 0 29643 0
[pid=16601] vsize: 119152
Current children cumulated CPU time (s) 1039.02
Current children cumulated vsize (Kb) 121276

[startup+1050.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36409 0 0 0 104763 140 0 0 25 0 1 0 1855116387 122077184 28156 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29804 28156 145 145 0 29659 0
[pid=16601] vsize: 119216
Current children cumulated CPU time (s) 1049.03
Current children cumulated vsize (Kb) 121340

[startup+1060.08 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36422 0 0 0 105762 140 0 0 25 0 1 0 1855116387 122126336 28169 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29816 28169 145 145 0 29671 0
[pid=16601] vsize: 119264
Current children cumulated CPU time (s) 1059.02
Current children cumulated vsize (Kb) 121388

[startup+1070.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36435 0 0 0 106761 141 0 0 25 0 1 0 1855116387 122171392 28182 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29827 28182 145 145 0 29682 0
[pid=16601] vsize: 119308
Current children cumulated CPU time (s) 1069.02
Current children cumulated vsize (Kb) 121432

[startup+1080.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36454 0 0 0 107761 141 0 0 25 0 1 0 1855116387 122245120 28201 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29845 28201 145 145 0 29700 0
[pid=16601] vsize: 119380
Current children cumulated CPU time (s) 1079.02
Current children cumulated vsize (Kb) 121504

[startup+1090.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36467 0 0 0 108761 142 0 0 25 0 1 0 1855116387 122298368 28214 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29858 28214 145 145 0 29713 0
[pid=16601] vsize: 119432
Current children cumulated CPU time (s) 1089.03
Current children cumulated vsize (Kb) 121556

[startup+1100.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36479 0 0 0 109760 143 0 0 25 0 1 0 1855116387 122343424 28226 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29869 28226 145 145 0 29724 0
[pid=16601] vsize: 119476
Current children cumulated CPU time (s) 1099.03
Current children cumulated vsize (Kb) 121600

[startup+1110.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36493 0 0 0 110760 143 0 0 25 0 1 0 1855116387 122388480 28240 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29880 28240 145 145 0 29735 0
[pid=16601] vsize: 119520
Current children cumulated CPU time (s) 1109.03
Current children cumulated vsize (Kb) 121644

[startup+1120.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36519 0 0 0 111759 143 0 0 25 0 1 0 1855116387 122490880 28266 4294967295 134512640 135094434 3221224432 3221223120 134558992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29905 28266 145 145 0 29760 0
[pid=16601] vsize: 119620
Current children cumulated CPU time (s) 1119.02
Current children cumulated vsize (Kb) 121744

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36530 0 0 0 112759 143 0 0 25 0 1 0 1855116387 122531840 28277 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29915 28277 145 145 0 29770 0
[pid=16601] vsize: 119660
Current children cumulated CPU time (s) 1129.02
Current children cumulated vsize (Kb) 121784

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36540 0 0 0 113758 144 0 0 25 0 1 0 1855116387 122572800 28287 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29925 28287 145 145 0 29780 0
[pid=16601] vsize: 119700
Current children cumulated CPU time (s) 1139.02
Current children cumulated vsize (Kb) 121824

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36558 0 0 0 114758 144 0 0 25 0 1 0 1855116387 122634240 28305 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29940 28305 145 145 0 29795 0
[pid=16601] vsize: 119760
Current children cumulated CPU time (s) 1149.02
Current children cumulated vsize (Kb) 121884

[startup+1160.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36571 0 0 0 115757 145 0 0 25 0 1 0 1855116387 122683392 28318 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29952 28318 145 145 0 29807 0
[pid=16601] vsize: 119808
Current children cumulated CPU time (s) 1159.02
Current children cumulated vsize (Kb) 121932

[startup+1170.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36577 0 0 0 116757 145 0 0 25 0 1 0 1855116387 122707968 28324 4294967295 134512640 135094434 3221224432 3221223044 134563094 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29958 28324 145 145 0 29813 0
[pid=16601] vsize: 119832
Current children cumulated CPU time (s) 1169.02
Current children cumulated vsize (Kb) 121956

[startup+1180.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36586 0 0 0 117757 146 0 0 25 0 1 0 1855116387 122744832 28333 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 29967 28333 145 145 0 29822 0
[pid=16601] vsize: 119868
Current children cumulated CPU time (s) 1179.03
Current children cumulated vsize (Kb) 121992

[startup+1190.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36692 0 0 0 118755 147 0 0 25 0 1 0 1855116387 123170816 28439 4294967295 134512640 135094434 3221224432 3221223120 134558987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 30071 28439 145 145 0 29926 0
[pid=16601] vsize: 120284
Current children cumulated CPU time (s) 1189.02
Current children cumulated vsize (Kb) 122408

[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 36942 0 0 0 119750 148 0 0 25 0 1 0 1855116387 124305408 28689 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 30348 28689 145 145 0 30203 0
[pid=16601] vsize: 121392
Current children cumulated CPU time (s) 1198.98
Current children cumulated vsize (Kb) 123516

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 37464 0 0 0 120739 154 0 0 25 0 1 0 1855116387 126406656 29211 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 30861 29211 145 145 0 30716 0
[pid=16601] vsize: 123444
Current children cumulated CPU time (s) 1208.93
Current children cumulated vsize (Kb) 125568



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.1 s]
Raw data (loadavg): 1.00 0.99 0.98 2/57 16601
Raw data (/proc/16597/stat): 16597 (minisat+_script) S 16596 16597 16528 0 -1 0 289 239 0 0 0 0 0 0 21 0 1 0 1855116382 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16597/statm): 531 226 485 147 0 384 0
[pid=16597] vsize: 2124
Raw data (/proc/16601/stat): 16601 (minisat+_64-bit) R 16597 16597 16528 0 -1 0 37464 0 0 0 120739 154 0 0 25 0 1 0 1855116387 126406656 29211 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16601/statm): 30861 29211 145 145 0 30716 0
[pid=16601] vsize: 123444
Current children cumulated CPU time (s) 1208.93
Current children cumulated vsize (Kb) 125568

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

Child status: 0
Real time (s): 1210.16
CPU time (s): 1209
CPU user time (s): 1207.4
CPU system time (s): 1.59776
CPU usage (%): 99.9037
Max. virtual memory (cumulated for all children) (Kb): 125568

Verifier Data

ERROR: no interpretation found !