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-standgub.opb
MD5SUM4278f4b256e2a8fa799a6ca1554251b3
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 variables22302
Total number of constraints463
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 constraints463
Minimum length of a constraint8
Maximum length of a constraint14900

Trace number 6069

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        901444 kB
Buffers:          3572 kB
Cached:         100120 kB
SwapCached:       1164 kB
Active:          32944 kB
Inactive:        73276 kB
HighTotal:      131008 kB
HighFree:        27076 kB
LowTotal:       903652 kB
LowFree:        874368 kB
SwapTotal:     2097136 kB
SwapFree:      2095232 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            21080 kB
Committed_AS:    92628 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:23:07 (client local time) WITH STATUS 0 IN 1208.79 SECONDS
stats: 3222 7 1208.79 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 |  964478  3250895 |  353647      98      304     3.1 |  6.740 % |
c |       250 |  964106  3249786 |  389012     228      797     3.5 |  6.781 % |
c |       475 |  964002  3249529 |  427913     433     1737     4.0 |  6.796 % |
c |       812 |  963795  3248800 |  470705     742     2871     3.9 |  6.814 % |
c |      1318 |  963702  3248475 |  517775    1231     4855     3.9 |  6.821 % |
c |      2077 |  963366  3247410 |  569553    1936     7861     4.1 |  6.854 % |
c |      3216 |  963175  3246814 |  626508    3033    17391     5.7 |  6.874 % |
c |      4925 |  962759  3245603 |  689159    4650    34938     7.5 |  6.918 % |
c |      7487 |  962250  3243978 |  758075    7143    61280     8.6 |  6.959 % |
c |     11332 |  958155  3233897 |  833883   10842   111683    10.3 |  7.464 % |
c |     17098 |  951800  3218279 |  917271   16238   163430    10.1 |  8.278 % |
c |     25747 |  942821  3195619 | 1008998   23980   230144     9.6 |  9.447 % |
c |     38722 |  941216  3191324 | 1109898   36800  1169188    31.8 |  9.616 % |
c |     58186 |  940987  3190590 | 1220888   56246  2436269    43.3 |  9.632 % |

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/20349/stat): 20349 (minisat+_script) R 20348 20349 10120 0 -1 0 18 0 0 0 0 0 0 0 21 0 1 0 1740061742 712704 3 4294967295 134512640 135087896 3221221664 3221221664 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/20349/statm): 174 3 169 147 0 27 0
[pid=20349] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/intel-8.0-20031016/lib/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/tls/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/i686/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/mmx/libtermcap.so.2
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libdl.so.2
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libdl.so.2
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/local/intel-8.0-20031016/lib/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/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 /usr/lib/locale/locale-archive
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
open syscall for file /usr/lib/gconv/gconv-modules.cache
New process pid=20350
New process pid=20351
New process pid=20352
execve syscall for /bin/sed executable
One traced child (pid=20351) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/i686/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/tls/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/i686/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/mmx/libc.so.6
open syscall for file /usr/local/intel-8.0-20031016/lib/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/i686/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/tls/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/i686/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/mmx/libc.so.6
open syscall for file /usr/local/pgi-5.1.3/linux86/5.1/lib/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/i686/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/tls/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/i686/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/i686/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/mmx/libc.so.6
open syscall for file /usr/local/globus-2.4.3/lib/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
open syscall for file /usr/lib/locale/locale-archive
open syscall for file /usr/lib/gconv/gconv-modules.cache
One traced child (pid=20352) exited with status: 0
One traced child (pid=20350) exited with status: 0
New process pid=20353
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-standgub.opb

[startup+10.0033 s]
Raw data (loadavg): 0.76 0.92 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 4324 0 0 0 961 16 0 0 25 0 1 0 1740061749 15196160 3209 4294967295 134512640 135094434 3221221600 3221169040 134597176 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20353/statm): 3710 3209 145 145 0 3565 0
[pid=20353] vsize: 14840
Current children cumulated CPU time (s) 9.77
Current children cumulated vsize (Kb) 19036

[startup+20.0041 s]
Raw data (loadavg): 0.79 0.93 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 1914 43 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221216744 134677377 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 19.57
Current children cumulated vsize (Kb) 30488

[startup+30.0049 s]
Raw data (loadavg): 0.82 0.93 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 2914 43 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217040 134599970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 29.57
Current children cumulated vsize (Kb) 30488

[startup+40.0047 s]
Raw data (loadavg): 0.85 0.93 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 3915 43 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221216928 134677086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 39.58
Current children cumulated vsize (Kb) 30488

[startup+50.0055 s]
Raw data (loadavg): 0.87 0.93 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 4914 44 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221216864 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 49.58
Current children cumulated vsize (Kb) 30488

[startup+60.0062 s]
Raw data (loadavg): 0.89 0.93 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 5914 44 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217216 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 59.58
Current children cumulated vsize (Kb) 30488

[startup+70.007 s]
Raw data (loadavg): 0.91 0.94 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 6914 44 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134677278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 69.58
Current children cumulated vsize (Kb) 30488

[startup+80.0078 s]
Raw data (loadavg): 0.92 0.94 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 7914 44 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217664 134677099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 79.58
Current children cumulated vsize (Kb) 30488

[startup+90.0086 s]
Raw data (loadavg): 0.93 0.94 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 8914 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217312 134677065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 89.59
Current children cumulated vsize (Kb) 30488

[startup+100.009 s]
Raw data (loadavg): 0.94 0.94 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 9914 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134601029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 99.59
Current children cumulated vsize (Kb) 30488

[startup+110.01 s]
Raw data (loadavg): 0.95 0.94 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 10914 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217920 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 109.59
Current children cumulated vsize (Kb) 30488

[startup+120.01 s]
Raw data (loadavg): 0.96 0.94 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 11914 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217468 134677081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 119.59
Current children cumulated vsize (Kb) 30488

[startup+130.011 s]
Raw data (loadavg): 0.96 0.94 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 12914 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217568 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 129.59
Current children cumulated vsize (Kb) 30488

[startup+140.012 s]
Raw data (loadavg): 0.97 0.95 0.92 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 13915 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217216 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 139.6
Current children cumulated vsize (Kb) 30488

[startup+150.013 s]
Raw data (loadavg): 1.05 0.96 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 14915 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217312 134677021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 149.6
Current children cumulated vsize (Kb) 30488

[startup+160.014 s]
Raw data (loadavg): 1.04 0.96 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 15915 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134677346 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 159.6
Current children cumulated vsize (Kb) 30488

[startup+170.014 s]
Raw data (loadavg): 1.04 0.96 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 16915 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218096 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 169.6
Current children cumulated vsize (Kb) 30488

[startup+180.015 s]
Raw data (loadavg): 1.03 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 17915 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217360 134519504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 179.6
Current children cumulated vsize (Kb) 30488

[startup+190.014 s]
Raw data (loadavg): 1.03 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 18915 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 189.6
Current children cumulated vsize (Kb) 30488

[startup+200.015 s]
Raw data (loadavg): 1.02 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 19916 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217452 134676460 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 199.61
Current children cumulated vsize (Kb) 30488

[startup+210.016 s]
Raw data (loadavg): 1.02 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 20916 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134600228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 209.61
Current children cumulated vsize (Kb) 30488

[startup+220.016 s]
Raw data (loadavg): 1.01 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 21916 45 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218096 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 219.61
Current children cumulated vsize (Kb) 30488

[startup+230.017 s]
Raw data (loadavg): 1.01 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 22916 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218448 134677310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 229.62
Current children cumulated vsize (Kb) 30488

[startup+240.016 s]
Raw data (loadavg): 1.01 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 23916 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217112 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 239.62
Current children cumulated vsize (Kb) 30488

[startup+250.017 s]
Raw data (loadavg): 1.01 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 24916 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217216 134677239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 249.62
Current children cumulated vsize (Kb) 30488

[startup+260.018 s]
Raw data (loadavg): 1.01 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 25917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217664 134677035 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 259.63
Current children cumulated vsize (Kb) 30488

[startup+270.018 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 26917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217744 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 269.63
Current children cumulated vsize (Kb) 30488

[startup+280.019 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 27917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218368 134676294 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 279.63
Current children cumulated vsize (Kb) 30488

[startup+290.018 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 28917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217744 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 289.63
Current children cumulated vsize (Kb) 30488

[startup+300.019 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 29917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217920 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 299.63
Current children cumulated vsize (Kb) 30488

[startup+310.02 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 30917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217728 134600246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 309.63
Current children cumulated vsize (Kb) 30488

[startup+320.02 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 31918 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217744 134600151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 319.64
Current children cumulated vsize (Kb) 30488

[startup+330.021 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 32917 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218272 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 329.63
Current children cumulated vsize (Kb) 30488

[startup+340.02 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 33918 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218096 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 339.64
Current children cumulated vsize (Kb) 30488

[startup+350.021 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 34918 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218168 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 349.64
Current children cumulated vsize (Kb) 30488

[startup+360.022 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 35918 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217920 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 359.64
Current children cumulated vsize (Kb) 30488

[startup+370.022 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 36918 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218272 134600228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 369.64
Current children cumulated vsize (Kb) 30488

[startup+380.022 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 37919 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218172 134677081 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 379.65
Current children cumulated vsize (Kb) 30488

[startup+390.023 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 38919 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221216336 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 389.65
Current children cumulated vsize (Kb) 30488

[startup+400.024 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 39919 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221216688 134677333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 399.65
Current children cumulated vsize (Kb) 30488

[startup+410.025 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 40919 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217136 134677099 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 409.65
Current children cumulated vsize (Kb) 30488

[startup+420.026 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 41919 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217920 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 419.65
Current children cumulated vsize (Kb) 30488

[startup+430.026 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 42920 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218368 134676251 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 429.66
Current children cumulated vsize (Kb) 30488

[startup+440.026 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 43920 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217568 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 439.66
Current children cumulated vsize (Kb) 30488

[startup+450.028 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 44920 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218096 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 449.66
Current children cumulated vsize (Kb) 30488

[startup+460.029 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 45920 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218156 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 459.66
Current children cumulated vsize (Kb) 30488

[startup+470.029 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 46920 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218544 134677069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 469.66
Current children cumulated vsize (Kb) 30488

[startup+480.029 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 47921 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218272 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 479.67
Current children cumulated vsize (Kb) 30488

[startup+490.03 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 48921 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218624 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 489.67
Current children cumulated vsize (Kb) 30488

[startup+500.031 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 49921 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134676480 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 499.67
Current children cumulated vsize (Kb) 30488

[startup+510.032 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 50921 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217816 134676334 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 509.67
Current children cumulated vsize (Kb) 30488

[startup+520.033 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 51922 46 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217392 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 519.68
Current children cumulated vsize (Kb) 30488

[startup+530.033 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 52922 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217312 134677007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 529.69
Current children cumulated vsize (Kb) 30488

[startup+540.033 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 53922 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217804 134677228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 539.69
Current children cumulated vsize (Kb) 30488

[startup+550.034 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 54922 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221217744 134677310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 549.69
Current children cumulated vsize (Kb) 30488

[startup+560.035 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 55922 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218272 134600291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 559.69
Current children cumulated vsize (Kb) 30488

[startup+570.035 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 56922 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218440 134600155 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 569.69
Current children cumulated vsize (Kb) 30488

[startup+580.036 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 57923 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218252 134676382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 579.7
Current children cumulated vsize (Kb) 30488

[startup+590.037 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12178 0 0 0 58923 47 0 0 25 0 1 0 1740061749 26923008 6087 4294967295 134512640 135094434 3221221600 3221218976 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6573 6087 145 145 0 6428 0
[pid=20353] vsize: 26292
Current children cumulated CPU time (s) 589.7
Current children cumulated vsize (Kb) 30488

[startup+600.038 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12310 0 0 0 59923 47 0 0 25 0 1 0 1740061749 27090944 6054 4294967295 134512640 135094434 3221221600 3221219024 134676465 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6614 6054 145 145 0 6469 0
[pid=20353] vsize: 26456
Current children cumulated CPU time (s) 599.7
Current children cumulated vsize (Kb) 30652

[startup+610.039 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 12310 0 0 0 60923 47 0 0 25 0 1 0 1740061749 27090944 6054 4294967295 134512640 135094434 3221221600 3221218444 134600233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 6614 6054 145 145 0 6469 0
[pid=20353] vsize: 26456
Current children cumulated CPU time (s) 609.7
Current children cumulated vsize (Kb) 30652

[startup+620.038 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 61919 51 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221217920 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0
[pid=20353] vsize: 29656
Current children cumulated CPU time (s) 619.7
Current children cumulated vsize (Kb) 33852

[startup+630.039 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 62920 51 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221217972 134677232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0
[pid=20353] vsize: 29656
Current children cumulated CPU time (s) 629.71
Current children cumulated vsize (Kb) 33852

[startup+640.039 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 63920 51 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221218096 134600314 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0
[pid=20353] vsize: 29656
Current children cumulated CPU time (s) 639.71
Current children cumulated vsize (Kb) 33852

[startup+650.04 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 64919 52 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221218272 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0
[pid=20353] vsize: 29656
Current children cumulated CPU time (s) 649.71
Current children cumulated vsize (Kb) 33852

[startup+660.04 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 65919 52 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221218368 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0
[pid=20353] vsize: 29656
Current children cumulated CPU time (s) 659.71
Current children cumulated vsize (Kb) 33852

[startup+670.04 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 66919 52 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221218272 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0
[pid=20353] vsize: 29656
Current children cumulated CPU time (s) 669.71
Current children cumulated vsize (Kb) 33852

[startup+680.041 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 67919 52 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221219072 134677059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0
[pid=20353] vsize: 29656
Current children cumulated CPU time (s) 679.71
Current children cumulated vsize (Kb) 33852

[startup+690.042 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 68919 53 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221218800 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0
[pid=20353] vsize: 29656
Current children cumulated CPU time (s) 689.72
Current children cumulated vsize (Kb) 33852

[startup+700.043 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 69919 53 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221219504 134600215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0
[pid=20353] vsize: 29656
Current children cumulated CPU time (s) 699.72
Current children cumulated vsize (Kb) 33852

[startup+710.043 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 70919 53 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221219152 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0
[pid=20353] vsize: 29656
Current children cumulated CPU time (s) 709.72
Current children cumulated vsize (Kb) 33852

[startup+720.043 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 71920 53 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221219220 134676335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0
[pid=20353] vsize: 29656
Current children cumulated CPU time (s) 719.73
Current children cumulated vsize (Kb) 33852

[startup+730.044 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 13662 0 0 0 72920 53 0 0 25 0 1 0 1740061749 30367744 6747 4294967295 134512640 135094434 3221221600 3221219600 134677042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 7414 6747 145 145 0 7269 0
[pid=20353] vsize: 29656
Current children cumulated CPU time (s) 729.73
Current children cumulated vsize (Kb) 33852

[startup+740.044 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 15790 0 0 0 73915 57 0 0 25 0 1 0 1740061749 38912000 8875 4294967295 134512640 135094434 3221221600 3221219088 134519056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 9500 8875 145 145 0 9355 0
[pid=20353] vsize: 38000
Current children cumulated CPU time (s) 739.72
Current children cumulated vsize (Kb) 42196

[startup+750.045 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35509 0 0 0 74775 128 0 0 25 0 1 0 1740061749 117919744 27184 4294967295 134512640 135094434 3221221600 3221220260 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20353/statm): 28789 27184 145 145 0 28644 0
[pid=20353] vsize: 115156
Current children cumulated CPU time (s) 749.03
Current children cumulated vsize (Kb) 119352

[startup+760.045 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35511 0 0 0 75774 129 0 0 25 0 1 0 1740061749 117927936 27186 4294967295 134512640 135094434 3221221600 3221220288 134558987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20353/statm): 28791 27186 145 145 0 28646 0
[pid=20353] vsize: 115164
Current children cumulated CPU time (s) 759.03
Current children cumulated vsize (Kb) 119360

[startup+770.046 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35604 0 0 0 76772 130 0 0 25 0 1 0 1740061749 118308864 27279 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 28884 27279 145 145 0 28739 0
[pid=20353] vsize: 115536
Current children cumulated CPU time (s) 769.02
Current children cumulated vsize (Kb) 119732

[startup+780.047 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35660 0 0 0 77771 130 0 0 25 0 1 0 1740061749 118538240 27335 4294967295 134512640 135094434 3221221600 3221220260 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 28940 27335 145 145 0 28795 0
[pid=20353] vsize: 115760
Current children cumulated CPU time (s) 779.01
Current children cumulated vsize (Kb) 119956

[startup+790.048 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35722 0 0 0 78770 131 0 0 25 0 1 0 1740061749 118792192 27397 4294967295 134512640 135094434 3221221600 3221220276 134553436 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29002 27397 145 145 0 28857 0
[pid=20353] vsize: 116008
Current children cumulated CPU time (s) 789.01
Current children cumulated vsize (Kb) 120204

[startup+800.049 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35825 0 0 0 79769 131 0 0 25 0 1 0 1740061749 119218176 27500 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29106 27500 145 145 0 28961 0
[pid=20353] vsize: 116424
Current children cumulated CPU time (s) 799
Current children cumulated vsize (Kb) 120620

[startup+810.049 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35867 0 0 0 80768 131 0 0 25 0 1 0 1740061749 119386112 27542 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20353/statm): 29147 27542 145 145 0 29002 0
[pid=20353] vsize: 116588
Current children cumulated CPU time (s) 808.99
Current children cumulated vsize (Kb) 120784

[startup+820.049 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35929 0 0 0 81767 132 0 0 25 0 1 0 1740061749 119672832 27604 4294967295 134512640 135094434 3221221600 3221220260 134553475 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20353/statm): 29217 27604 145 145 0 29072 0
[pid=20353] vsize: 116868
Current children cumulated CPU time (s) 818.99
Current children cumulated vsize (Kb) 121064

[startup+830.05 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 35975 0 0 0 82765 133 0 0 25 0 1 0 1740061749 119853056 27650 4294967295 134512640 135094434 3221221600 3221220260 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29261 27650 145 145 0 29116 0
[pid=20353] vsize: 117044
Current children cumulated CPU time (s) 828.98
Current children cumulated vsize (Kb) 121240

[startup+840.051 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36029 0 0 0 83765 133 0 0 25 0 1 0 1740061749 120070144 27704 4294967295 134512640 135094434 3221221600 3221220260 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29314 27704 145 145 0 29169 0
[pid=20353] vsize: 117256
Current children cumulated CPU time (s) 838.98
Current children cumulated vsize (Kb) 121452

[startup+850.052 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36057 0 0 0 84764 134 0 0 25 0 1 0 1740061749 120184832 27732 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29342 27732 145 145 0 29197 0
[pid=20353] vsize: 117368
Current children cumulated CPU time (s) 848.98
Current children cumulated vsize (Kb) 121564

[startup+860.052 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36111 0 0 0 85763 134 0 0 25 0 1 0 1740061749 120397824 27786 4294967295 134512640 135094434 3221221600 3221220304 134559019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29394 27786 145 145 0 29249 0
[pid=20353] vsize: 117576
Current children cumulated CPU time (s) 858.97
Current children cumulated vsize (Kb) 121772

[startup+870.053 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36156 0 0 0 86763 135 0 0 25 0 1 0 1740061749 120590336 27831 4294967295 134512640 135094434 3221221600 3221220212 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29441 27831 145 145 0 29296 0
[pid=20353] vsize: 117764
Current children cumulated CPU time (s) 868.98
Current children cumulated vsize (Kb) 121960

[startup+880.054 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36207 0 0 0 87762 135 0 0 25 0 1 0 1740061749 120795136 27882 4294967295 134512640 135094434 3221221600 3221220256 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29491 27882 145 145 0 29346 0
[pid=20353] vsize: 117964
Current children cumulated CPU time (s) 878.97
Current children cumulated vsize (Kb) 122160

[startup+890.055 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36260 0 0 0 88760 136 0 0 25 0 1 0 1740061749 121012224 27935 4294967295 134512640 135094434 3221221600 3221220260 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29544 27935 145 145 0 29399 0
[pid=20353] vsize: 118176
Current children cumulated CPU time (s) 888.96
Current children cumulated vsize (Kb) 122372

[startup+900.055 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36286 0 0 0 89760 137 0 0 25 0 1 0 1740061749 121114624 27961 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29569 27961 145 145 0 29424 0
[pid=20353] vsize: 118276
Current children cumulated CPU time (s) 898.97
Current children cumulated vsize (Kb) 122472

[startup+910.056 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36311 0 0 0 90760 137 0 0 25 0 1 0 1740061749 121217024 27986 4294967295 134512640 135094434 3221221600 3221220260 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29594 27986 145 145 0 29449 0
[pid=20353] vsize: 118376
Current children cumulated CPU time (s) 908.97
Current children cumulated vsize (Kb) 122572

[startup+920.056 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36328 0 0 0 91759 137 0 0 25 0 1 0 1740061749 121286656 28003 4294967295 134512640 135094434 3221221600 3221220224 134557655 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29611 28003 145 145 0 29466 0
[pid=20353] vsize: 118444
Current children cumulated CPU time (s) 918.96
Current children cumulated vsize (Kb) 122640

[startup+930.057 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36346 0 0 0 92759 138 0 0 25 0 1 0 1740061749 121421824 28021 4294967295 134512640 135094434 3221221600 3221220304 134559013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29644 28021 145 145 0 29499 0
[pid=20353] vsize: 118576
Current children cumulated CPU time (s) 928.97
Current children cumulated vsize (Kb) 122772

[startup+940.058 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36351 0 0 0 93759 138 0 0 25 0 1 0 1740061749 121442304 28026 4294967295 134512640 135094434 3221221600 3221220304 134558968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29649 28026 145 145 0 29504 0
[pid=20353] vsize: 118596
Current children cumulated CPU time (s) 938.97
Current children cumulated vsize (Kb) 122792

[startup+950.058 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36355 0 0 0 94760 138 0 0 25 0 1 0 1740061749 121454592 28030 4294967295 134512640 135094434 3221221600 3221220260 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29652 28030 145 145 0 29507 0
[pid=20353] vsize: 118608
Current children cumulated CPU time (s) 948.98
Current children cumulated vsize (Kb) 122804

[startup+960.059 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36373 0 0 0 95760 138 0 0 25 0 1 0 1740061749 121528320 28048 4294967295 134512640 135094434 3221221600 3221220260 134553497 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29670 28048 145 145 0 29525 0
[pid=20353] vsize: 118680
Current children cumulated CPU time (s) 958.98
Current children cumulated vsize (Kb) 122876

[startup+970.059 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36384 0 0 0 96760 138 0 0 25 0 1 0 1740061749 121569280 28059 4294967295 134512640 135094434 3221221600 3221220260 134553450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29680 28059 145 145 0 29535 0
[pid=20353] vsize: 118720
Current children cumulated CPU time (s) 968.98
Current children cumulated vsize (Kb) 122916

[startup+980.06 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36403 0 0 0 97759 138 0 0 25 0 1 0 1740061749 121638912 28078 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29697 28078 145 145 0 29552 0
[pid=20353] vsize: 118788
Current children cumulated CPU time (s) 978.97
Current children cumulated vsize (Kb) 122984

[startup+990.061 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36415 0 0 0 98759 139 0 0 25 0 1 0 1740061749 121688064 28090 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29709 28090 145 145 0 29564 0
[pid=20353] vsize: 118836
Current children cumulated CPU time (s) 988.98
Current children cumulated vsize (Kb) 123032

[startup+1000.06 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36430 0 0 0 99759 139 0 0 25 0 1 0 1740061749 121745408 28105 4294967295 134512640 135094434 3221221600 3221220260 134553489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29723 28105 145 145 0 29578 0
[pid=20353] vsize: 118892
Current children cumulated CPU time (s) 998.98
Current children cumulated vsize (Kb) 123088

[startup+1010.06 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36469 0 0 0 100758 139 0 0 25 0 1 0 1740061749 121876480 28144 4294967295 134512640 135094434 3221221600 3221220292 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29755 28144 145 145 0 29610 0
[pid=20353] vsize: 119020
Current children cumulated CPU time (s) 1008.97
Current children cumulated vsize (Kb) 123216

[startup+1020.06 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36475 0 0 0 101758 139 0 0 25 0 1 0 1740061749 121901056 28150 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29761 28150 145 145 0 29616 0
[pid=20353] vsize: 119044
Current children cumulated CPU time (s) 1018.97
Current children cumulated vsize (Kb) 123240

[startup+1030.06 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36488 0 0 0 102758 139 0 0 25 0 1 0 1740061749 121950208 28163 4294967295 134512640 135094434 3221221600 3221220260 134553501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29773 28163 145 145 0 29628 0
[pid=20353] vsize: 119092
Current children cumulated CPU time (s) 1028.97
Current children cumulated vsize (Kb) 123288

[startup+1040.06 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36511 0 0 0 103759 139 0 0 25 0 1 0 1740061749 122044416 28186 4294967295 134512640 135094434 3221221600 3221220260 134553444 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29796 28186 145 145 0 29651 0
[pid=20353] vsize: 119184
Current children cumulated CPU time (s) 1038.98
Current children cumulated vsize (Kb) 123380

[startup+1050.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36539 0 0 0 104758 140 0 0 25 0 1 0 1740061749 122155008 28214 4294967295 134512640 135094434 3221221600 3221220260 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29823 28214 145 145 0 29678 0
[pid=20353] vsize: 119292
Current children cumulated CPU time (s) 1048.98
Current children cumulated vsize (Kb) 123488

[startup+1060.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36554 0 0 0 105758 140 0 0 25 0 1 0 1740061749 122212352 28229 4294967295 134512640 135094434 3221221600 3221220260 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29837 28229 145 145 0 29692 0
[pid=20353] vsize: 119348
Current children cumulated CPU time (s) 1058.98
Current children cumulated vsize (Kb) 123544

[startup+1070.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36569 0 0 0 106758 140 0 0 25 0 1 0 1740061749 122269696 28244 4294967295 134512640 135094434 3221221600 3221220260 134553494 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29851 28244 145 145 0 29706 0
[pid=20353] vsize: 119404
Current children cumulated CPU time (s) 1068.98
Current children cumulated vsize (Kb) 123600

[startup+1080.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36579 0 0 0 107758 140 0 0 25 0 1 0 1740061749 122310656 28254 4294967295 134512640 135094434 3221221600 3221220212 134563049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29861 28254 145 145 0 29716 0
[pid=20353] vsize: 119444
Current children cumulated CPU time (s) 1078.98
Current children cumulated vsize (Kb) 123640

[startup+1090.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36592 0 0 0 108758 140 0 0 25 0 1 0 1740061749 122355712 28267 4294967295 134512640 135094434 3221221600 3221220272 134553523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29872 28267 145 145 0 29727 0
[pid=20353] vsize: 119488
Current children cumulated CPU time (s) 1088.98
Current children cumulated vsize (Kb) 123684

[startup+1100.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36595 0 0 0 109758 140 0 0 25 0 1 0 1740061749 122368000 28270 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29875 28270 145 145 0 29730 0
[pid=20353] vsize: 119500
Current children cumulated CPU time (s) 1098.98
Current children cumulated vsize (Kb) 123696

[startup+1110.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36600 0 0 0 110758 140 0 0 25 0 1 0 1740061749 122388480 28275 4294967295 134512640 135094434 3221221600 3221220212 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29880 28275 145 145 0 29735 0
[pid=20353] vsize: 119520
Current children cumulated CPU time (s) 1108.98
Current children cumulated vsize (Kb) 123716

[startup+1120.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36621 0 0 0 111758 140 0 0 25 0 1 0 1740061749 122470400 28296 4294967295 134512640 135094434 3221221600 3221220212 134563064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29900 28296 145 145 0 29755 0
[pid=20353] vsize: 119600
Current children cumulated CPU time (s) 1118.98
Current children cumulated vsize (Kb) 123796

[startup+1130.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36649 0 0 0 112757 141 0 0 25 0 1 0 1740061749 122568704 28324 4294967295 134512640 135094434 3221221600 3221220260 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29924 28324 145 145 0 29779 0
[pid=20353] vsize: 119696
Current children cumulated CPU time (s) 1128.98
Current children cumulated vsize (Kb) 123892

[startup+1140.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36667 0 0 0 113757 141 0 0 25 0 1 0 1740061749 122626048 28342 4294967295 134512640 135094434 3221221600 3221220212 134563083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/20353/statm): 29938 28342 145 145 0 29793 0
[pid=20353] vsize: 119752
Current children cumulated CPU time (s) 1138.98
Current children cumulated vsize (Kb) 123948

[startup+1150.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36679 0 0 0 114756 141 0 0 25 0 1 0 1740061749 122671104 28354 4294967295 134512640 135094434 3221221600 3221220260 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29949 28354 145 145 0 29804 0
[pid=20353] vsize: 119796
Current children cumulated CPU time (s) 1148.97
Current children cumulated vsize (Kb) 123992

[startup+1160.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36689 0 0 0 115757 141 0 0 25 0 1 0 1740061749 122712064 28364 4294967295 134512640 135094434 3221221600 3221220268 134553438 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 29959 28364 145 145 0 29814 0
[pid=20353] vsize: 119836
Current children cumulated CPU time (s) 1158.98
Current children cumulated vsize (Kb) 124032

[startup+1170.07 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 36874 0 0 0 116754 143 0 0 25 0 1 0 1740061749 123457536 28549 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 30141 28549 145 145 0 29996 0
[pid=20353] vsize: 120564
Current children cumulated CPU time (s) 1168.97
Current children cumulated vsize (Kb) 124760

[startup+1180.08 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 37551 0 0 0 117745 146 0 0 25 0 1 0 1740061749 126328832 29226 4294967295 134512640 135094434 3221221600 3221220256 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 30842 29226 145 145 0 30697 0
[pid=20353] vsize: 123368
Current children cumulated CPU time (s) 1178.91
Current children cumulated vsize (Kb) 127564

[startup+1190.08 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 38316 0 0 0 118733 151 0 0 25 0 1 0 1740061749 129433600 29991 4294967295 134512640 135094434 3221221600 3221220256 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 31600 29991 145 145 0 31455 0
[pid=20353] vsize: 126400
Current children cumulated CPU time (s) 1188.84
Current children cumulated vsize (Kb) 130596

[startup+1200.08 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 38942 0 0 0 119722 156 0 0 25 0 1 0 1740061749 131960832 30617 4294967295 134512640 135094434 3221221600 3221220256 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 32217 30617 145 145 0 32072 0
[pid=20353] vsize: 128868
Current children cumulated CPU time (s) 1198.78
Current children cumulated vsize (Kb) 133064

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 39508 0 0 0 120713 160 0 0 25 0 1 0 1740061749 134250496 31183 4294967295 134512640 135094434 3221221600 3221220272 134556242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 32776 31183 145 145 0 32631 0
[pid=20353] vsize: 131104
Current children cumulated CPU time (s) 1208.73
Current children cumulated vsize (Kb) 135300



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.97 0.93 2/56 20353
Raw data (/proc/20349/stat): 20349 (minisat+_script) S 20348 20349 10120 0 -1 0 322 277 0 0 0 0 0 0 20 0 1 0 1740061742 4296704 256 4294967295 134512640 135087896 3221221664 3221220936 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/20349/statm): 1049 256 1003 147 0 902 0
[pid=20349] vsize: 4196
Raw data (/proc/20353/stat): 20353 (minisat+_64-bit) R 20349 20349 10120 0 -1 0 39508 0 0 0 120713 160 0 0 25 0 1 0 1740061749 134250496 31183 4294967295 134512640 135094434 3221221600 3221220256 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/20353/statm): 32776 31183 145 145 0 32631 0
[pid=20353] vsize: 131104
Current children cumulated CPU time (s) 1208.73
Current children cumulated vsize (Kb) 135300

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

Child status: 0
Real time (s): 1210.14
CPU time (s): 1208.79
CPU user time (s): 1207.13
CPU system time (s): 1.66175
CPU usage (%): 99.8887
Max. virtual memory (cumulated for all children) (Kb): 135300

Verifier Data

ERROR: no interpretation found !