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-scorpion.opb
MD5SUM407688f2ee1c26681a4ae06671027d6f
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 5640
Biggest coefficient in the objective function 10536091648
Number of bits for the biggest coefficient in the objective function 34
Sum of the numbers in the objective function 589543467975
Number of bits of the sum of numbers in the objective function 40
Biggest number in a constraint 32768000000
Number of bits of the biggest number in a constraint 35
Biggest sum of numbers in a constraint 589543467975
Number of bits of the biggest sum of numbers40
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables7160
Total number of constraints388
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 constraints388
Minimum length of a constraint20
Maximum length of a constraint400

Trace number 6049

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        786112 kB
Buffers:         38420 kB
Cached:         182420 kB
SwapCached:        228 kB
Active:          84220 kB
Inactive:       139572 kB
HighTotal:      131008 kB
HighFree:         6748 kB
LowTotal:       903652 kB
LowFree:        779364 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6272 kB
Slab:            19124 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:13:17 (client local time) WITH STATUS 0 IN 1207.31 SECONDS
stats: 3189 7 1207.31 0

Solver Data

c Parsing PB file...
c Converting 562 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #############################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssss
c ---[ 596]---> Sorter-cost: 6011     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 594]---> Sorter-cost: 6011     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 592]---> Sorter-cost: 6011     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 590]---> Sorter-cost: 6011     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 588]---> Sorter-cost: 6011     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 586]---> Sorter-cost: 6011     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 584]---> Sorter-cost: 5993     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 582]---> Sorter-cost: 5993     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 580]---> Sorter-cost: 5993     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 578]---> Sorter-cost: 5993     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 576]---> Sorter-cost: 5993     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 574]---> Sorter-cost: 5993     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 572]---> Sorter-cost: 5993     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 7
c ---[ 570]---> Sorter-cost: 5993     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 7
c ---[ 568]---> Sorter-cost: 5993     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 7
c ---[ 566]---> Sorter-cost: 5993     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 7
c ---[ 564]---> Sorter-cost: 5993     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 7
c ---[ 562]---> Sorter-cost: 5993     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 7
c ---[ 560]---> Sorter-cost: 6087     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 558]---> Sorter-cost: 6087     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 556]---> Sorter-cost: 6087     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 554]---> Sorter-cost: 6087     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 552]---> Sorter-cost: 6087     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 550]---> Sorter-cost: 6087     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 548]---> Sorter-cost: 6326     Base: 2 2 2 2 2 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 546]---> Sorter-cost: 6326     Base: 2 2 2 2 2 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 544]---> Sorter-cost: 6326     Base: 2 2 2 2 2 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 542]---> Sorter-cost: 6326     Base: 2 2 2 2 2 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 540]---> Sorter-cost: 6326     Base: 2 2 2 2 2 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 538]---> Sorter-cost: 6326     Base: 2 2 2 2 2 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 536]---> Sorter-cost: 6374     Base: 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 534]---> Sorter-cost: 6374     Base: 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 532]---> Sorter-cost: 6374     Base: 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 530]---> Sorter-cost: 6374     Base: 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 528]---> Sorter-cost: 6374     Base: 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 526]---> Sorter-cost: 6374     Base: 3 3 11 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 524]---> Sorter-cost: 3933     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2
c ---[ 522]---> Sorter-cost: 3933     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2
c ---[ 520]---> Sorter-cost: 3933     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2
c ---[ 518]---> Sorter-cost: 3933     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2
c ---[ 516]---> Sorter-cost: 3933     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2
c ---[ 514]---> Sorter-cost: 3933     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 3 5 2
c ---[ 512]---> Adder-cost: 636   maxlim: 314572500   bits: 29/29
c ---[ 510]---> Adder-cost: 636   maxlim: 314572500   bits: 29/29
c ---[ 508]---> Adder-cost: 636   maxlim: 314572500   bits: 29/29
c ---[ 506]---> Adder-cost: 636   maxlim: 314572500   bits: 29/29
c ---[ 504]---> Adder-cost: 636   maxlim: 314572500   bits: 29/29
c ---[ 502]---> Adder-cost: 636   maxlim: 314572500   bits: 29/29
c ---[ 500]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 498]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 496]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 494]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 492]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 490]---> Sorter-cost: 1658     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 488]---> Sorter-cost: 1439     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 486]---> Sorter-cost: 1439     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 484]---> Sorter-cost: 1439     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 482]---> Sorter-cost: 1439     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 480]---> Sorter-cost: 1439     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 478]---> Sorter-cost: 1439     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 476]---> BDD-cost:   58
c ---[ 474]---> BDD-cost:   58
c ---[ 472]---> BDD-cost:   58
c ---[ 470]---> BDD-cost:   58
c ---[ 468]---> BDD-cost:   58
c ---[ 466]---> BDD-cost:   58
c ---[ 464]---> BDD-cost:  172
c ---[ 462]---> BDD-cost:  172
c ---[ 460]---> BDD-cost:  172
c ---[ 458]---> BDD-cost:  172
c ---[ 456]---> BDD-cost:  172
c ---[ 454]---> BDD-cost:  172
c ---[ 452]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 450]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 448]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 446]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 444]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 442]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 440]---> BDD-cost:  172
c ---[ 438]---> BDD-cost:  172
c ---[ 436]---> BDD-cost:  172
c ---[ 434]---> BDD-cost:  172
c ---[ 432]---> BDD-cost:  172
c ---[ 430]---> BDD-cost:  172
c ---[ 428]---> BDD-cost:   58
c ---[ 426]---> BDD-cost:   58
c ---[ 424]---> BDD-cost:   58
c ---[ 422]---> BDD-cost:   58
c ---[ 420]---> BDD-cost:   58
c ---[ 418]---> BDD-cost:   58
c ---[ 416]---> BDD-cost:   58
c ---[ 414]---> BDD-cost:   58
c ---[ 412]---> BDD-cost:   58
c ---[ 410]---> BDD-cost:   58
c ---[ 408]---> BDD-cost:   58
c ---[ 406]---> BDD-cost:   58
c ---[ 404]---> BDD-cost:   58
c ---[ 402]---> BDD-cost:   58
c ---[ 400]---> BDD-cost:   58
c ---[ 398]---> BDD-cost:   58
c ---[ 396]---> BDD-cost:   58
c ---[ 394]---> BDD-cost:   58
c ---[ 392]---> BDD-cost:   58
c ---[ 390]---> BDD-cost:   58
c ---[ 388]---> BDD-cost:   58
c ---[ 386]---> BDD-cost:   58
c ---[ 384]---> BDD-cost:   58
c ---[ 382]---> BDD-cost:   58
c ---[ 381]---> Sorter-cost: 3271     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 380]---> Adder-cost: 440   maxlim: 62911338   bits: 27/26
c ---[ 379]---> Adder-cost: 440   maxlim: 62912311   bits: 27/26
c ---[ 378]---> Adder-cost: 671   maxlim: 62914499   bits: 27/26
c ---[ 377]---> Adder-cost: 440   maxlim: 62914499   bits: 27/26
c ---[ 376]---> Sorter-cost: 3271     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 375]---> Sorter-cost:  725     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost:  727     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 373]---> Sorter-cost: 1550     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost: 1554     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> Sorter-cost: 2469     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> Sorter-cost: 2475     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 369]---> Sorter-cost: 3828     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost: 3832     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 367]---> Sorter-cost: 1550     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost: 1552     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Sorter-cost: 1420     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 364]---> Sorter-cost: 1420     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2
c ---[ 363]---> Sorter-cost: 2040     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[ 362]---> Sorter-cost: 3946     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 7
c ---[ 361]---> Adder-cost: 467   maxlim: 933882   bits: 21/20
c ---[ 360]---> Adder-cost: 559   maxlim: 933882   bits: 21/20
c ---[ 359]---> Adder-cost: 649   maxlim: 933882   bits: 21/20
c ---[ 358]---> Sorter-cost: 3946     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 7
c ---[ 357]---> Adder-cost: 436   maxlim: 9469674   bits: 24/24
c ---[ 356]---> Adder-cost: 476   maxlim: 9469700   bits: 25/24
c ---[ 355]---> Adder-cost: 516   maxlim: 9469741   bits: 25/24
c ---[ 354]---> Adder-cost: 556   maxlim: 9469838   bits: 25/24
c ---[ 353]---> Adder-cost: 556   maxlim: 9469940   bits: 25/24
c ---[ 352]---> Adder-cost: 476   maxlim: 9469940   bits: 25/24
c ---[ 344]---> Sorter-cost: 1416     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 342]---> Sorter-cost: 1416     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 340]---> Sorter-cost: 1416     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost: 1416     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 336]---> Sorter-cost: 1416     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 334]---> Sorter-cost: 1416     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> Sorter-cost: 4634     Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 330]---> Sorter-cost: 4634     Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost: 4634     Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost: 4634     Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost: 4634     Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost: 4634     Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost:  722     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost:  722     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost:  722     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost:  722     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost:  722     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost:  722     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost: 4594     Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost: 4594     Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost: 4594     Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost: 4594     Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost: 4594     Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 298]---> Sorter-cost: 4594     Base: 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 296]---> Adder-cost: 504   maxlim: 64551975   bits: 27/26
c ---[ 294]---> Adder-cost: 504   maxlim: 64551975   bits: 27/26
c ---[ 292]---> Adder-cost: 504   maxlim: 64551975   bits: 27/26
c ---[ 290]---> Adder-cost: 504   maxlim: 64551975   bits: 27/26
c ---[ 288]---> Adder-cost: 504   maxlim: 64551975   bits: 27/26
c ---[ 286]---> Adder-cost: 504   maxlim: 64551975   bits: 27/26
c ---[ 284]---> Adder-cost: 384   maxlim: 13631475   bits: 25/24
c ---[ 282]---> Adder-cost: 384   maxlim: 13631475   bits: 25/24
c ---[ 280]---> Adder-cost: 384   maxlim: 13631475   bits: 25/24
c ---[ 278]---> Adder-cost: 384   maxlim: 13631475   bits: 25/24
c ---[ 276]---> Adder-cost: 384   maxlim: 13631475   bits: 25/24
c ---[ 274]---> Adder-cost: 384   maxlim: 13631475   bits: 25/24
c ---[ 272]---> Sorter-cost: 4081     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[ 270]---> Sorter-cost: 4081     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[ 268]---> Sorter-cost: 4081     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[ 266]---> Sorter-cost: 4081     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[ 264]---> Sorter-cost: 4081     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[ 262]---> Sorter-cost: 4081     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[ 260]---> Adder-cost: 507   maxlim: 28311525   bits: 26/25
c ---[ 258]---> Adder-cost: 507   maxlim: 28311525   bits: 26/25
c ---[ 256]---> Adder-cost: 507   maxlim: 28311525   bits: 26/25
c ---[ 254]---> Adder-cost: 507   maxlim: 28311525   bits: 26/25
c ---[ 252]---> Adder-cost: 507   maxlim: 28311525   bits: 26/25
c ---[ 250]---> Adder-cost: 507   maxlim: 28311525   bits: 26/25
c ---[ 248]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 246]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 244]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 242]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 240]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 238]---> Sorter-cost: 1525     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 236]---> Sorter-cost: 3931     Base: 2 2 2 2 3 3 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 234]---> Sorter-cost: 3931     Base: 2 2 2 2 3 3 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 232]---> Sorter-cost: 3931     Base: 2 2 2 2 3 3 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 230]---> Sorter-cost: 3931     Base: 2 2 2 2 3 3 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 228]---> Sorter-cost: 3931     Base: 2 2 2 2 3 3 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 226]---> Sorter-cost: 3931     Base: 2 2 2 2 3 3 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 224]---> Sorter-cost: 2881     Base: 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 222]---> Sorter-cost: 2881     Base: 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 220]---> Sorter-cost: 2881     Base: 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 218]---> Sorter-cost: 2881     Base: 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 216]---> Sorter-cost: 2881     Base: 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost: 2881     Base: 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 212]---> Sorter-cost: 3524     Base: 2 2 2 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 210]---> Sorter-cost: 3524     Base: 2 2 2 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 208]---> Sorter-cost: 3524     Base: 2 2 2 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 206]---> Sorter-cost: 3524     Base: 2 2 2 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 204]---> Sorter-cost: 3524     Base: 2 2 2 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 202]---> Sorter-cost: 3524     Base: 2 2 2 2 2 7 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 200]---> Adder-cost: 656   maxlim: 160431975   bits: 29/28
c ---[ 198]---> Adder-cost: 660   maxlim: 160431975   bits: 29/28
c ---[ 196]---> Adder-cost: 660   maxlim: 160431975   bits: 29/28
c ---[ 194]---> Adder-cost: 660   maxlim: 160431975   bits: 29/28
c ---[ 192]---> Adder-cost: 660   maxlim: 160431975   bits: 29/28
c ---[ 190]---> Adder-cost: 660   maxlim: 160431975   bits: 29/28
c ---[ 188]---> Sorter-cost: 3131     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[ 186]---> Sorter-cost: 3131     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[ 184]---> Sorter-cost: 3131     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[ 182]---> Sorter-cost: 3131     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[ 180]---> Sorter-cost: 3131     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[ 178]---> Sorter-cost: 3131     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[ 176]---> Adder-cost: 460   maxlim: 28311525   bits: 26/25
c ---[ 174]---> Adder-cost: 460   maxlim: 28311525   bits: 26/25
c ---[ 172]---> Adder-cost: 460   maxlim: 28311525   bits: 26/25
c ---[ 170]---> Adder-cost: 460   maxlim: 28311525   bits: 26/25
c ---[ 168]---> Adder-cost: 460   maxlim: 28311525   bits: 26/25
c ---[ 166]---> Adder-cost: 460   maxlim: 28311525   bits: 26/25
c ---[ 164]---> Sorter-cost: 1143     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost: 1143     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost: 1143     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> Sorter-cost: 1143     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 156]---> Sorter-cost: 1143     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 154]---> Sorter-cost: 1143     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 152]---> Sorter-cost: 1173     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2
c ---[ 150]---> Sorter-cost: 1173     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2
c ---[ 148]---> Sorter-cost: 1173     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2
c ---[ 146]---> Sorter-cost: 1173     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2
c ---[ 144]---> Sorter-cost: 1173     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2
c ---[ 142]---> Sorter-cost: 1173     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2
c ---[ 140]---> Sorter-cost:  903     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2
c ---[ 138]---> Sorter-cost:  903     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2
c ---[ 136]---> Sorter-cost:  903     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2
c ---[ 134]---> Sorter-cost:  903     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2
c ---[ 132]---> Sorter-cost:  903     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2
c ---[ 130]---> Sorter-cost:  903     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2
c ---[  79]---> BDD-cost:   58
c ---[  77]---> BDD-cost:   58
c ---[  75]---> BDD-cost:   58
c ---[  73]---> BDD-cost:   58
c ---[  71]---> BDD-cost:   58
c ---[  69]---> BDD-cost:   58
c ---[  67]---> BDD-cost:   58
c ---[  65]---> BDD-cost:   58
c ---[  63]---> BDD-cost:   58
c ---[  61]---> BDD-cost:   58
c ---[  59]---> BDD-cost:   58
c ---[  57]---> BDD-cost:   58
c ---[  55]---> BDD-cost:   58
c ---[  53]---> BDD-cost:   58
c ---[  51]---> BDD-cost:   58
c ---[  49]---> BDD-cost:   58
c ---[  47]---> BDD-cost:   58
c ---[  45]---> BDD-cost:   58
c ---[  43]---> BDD-cost:  172
c ---[  41]---> BDD-cost:   58
c ---[  39]---> BDD-cost:   58
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    4
c ---[  36]---> BDD-cost:    3
c ---[  35]---> BDD-cost:    4
c ---[  34]---> BDD-cost:    5
c ---[  33]---> BDD-cost:    6
c ---[  32]---> BDD-cost:    6
c ---[  31]---> BDD-cost:    4
c ---[  30]---> BDD-cost:    4
c ---[  29]---> BDD-cost:    5
c ---[  28]---> BDD-cost:    5
c ---[  27]---> BDD-cost:    7
c ---[  26]---> BDD-cost:    7
c ---[  25]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    5
c ---[  23]---> BDD-cost:    4
c ---[  22]---> BDD-cost:    6
c ---[  21]---> BDD-cost:    4
c ---[  20]---> BDD-cost:    4
c ---[  19]---> BDD-cost:    4
c ---[  18]---> BDD-cost:    2
c ---[  17]---> BDD-cost:    2
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    4
c ---[  13]---> BDD-cost:    3
c ---[  12]---> BDD-cost:    2
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:    4
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    5
c ---[   7]---> BDD-cost:    2
c ---[   6]---> BDD-cost:    4
c ---[   5]---> BDD-cost:    4
c ---[   4]---> BDD-cost:    4
c ---[   3]---> BDD-cost:    5
c ---[   2]---> BDD-cost:    3
c ---[   1]---> BDD-cost:    2
c ---[   0]---> BDD-cost:    2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1487022  3712364 |  495674       0        0     nan |  0.000 % |
c |       105 | 1486988  3712291 |  545241      97     1917    19.8 |  3.939 % |
c |       257 | 1486988  3712291 |  599765     249     6540    26.3 |  3.939 % |
c |       482 | 1486988  3712291 |  659742     474    11053    23.3 |  3.939 % |
c |       819 | 1486963  3712234 |  725716     810    20009    24.7 |  3.941 % |
c |      1326 | 1486742  3711734 |  798287    1304    27952    21.4 |  3.953 % |
c |      2086 | 1486706  3711655 |  878116    2061    43612    21.2 |  3.956 % |
c |      3225 | 1485882  3709781 |  965928    3159    65814    20.8 |  4.003 % |
c |      4933 | 1485788  3709572 | 1062521    4856   108654    22.4 |  4.009 % |
c |      7499 | 1485674  3709316 | 1168773    7412   193875    26.2 |  4.015 % |
c |     11343 | 1485367  3708618 | 1285650   11237   386372    34.4 |  4.032 % |
c |     17109 | 1484307  3706149 | 1414215   16930   572771    33.8 |  4.087 % |
c |     25758 | 1479304  3694129 | 1555637   25380   896632    35.3 |  4.346 % |
c |     38732 | 1457528  3642805 | 1711201   37975  1371377    36.1 |  5.682 % |
c |     58193 | 1424492  3564636 | 1882321   56635  2139712    37.8 |  7.953 % |
c |     87385 | 1396504  3492008 | 2070553   76191  3037307    39.9 |  9.542 % |
c |    131175 | 1375745  3438759 | 2277608  114021  5134768    45.0 | 10.814 % |
c |    196859 | 1370848  3427268 | 2505369  179162  8654298    48.3 | 11.084 % |

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/13906/stat): 13906 (minisat+_script) R 13905 13906 22582 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1796895075 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/13906/statm): 174 3 169 147 0 27 0
[pid=13906] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=13907
New process pid=13908
New process pid=13909
execve syscall for /bin/sed executable
One traced child (pid=13908) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=13909) exited with status: 0
One traced child (pid=13907) exited with status: 0
New process pid=13910
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-scorpion.opb

[startup+10.0052 s]
Raw data (loadavg): 0.77 0.91 0.90 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 1679 0 0 0 983 6 0 0 25 0 1 0 1796895080 6615040 1499 4294967295 134512640 135094434 3221224432 3221222336 134600310 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13910/statm): 1615 1499 145 145 0 1470 0
[pid=13910] vsize: 6460
Current children cumulated CPU time (s) 9.9
Current children cumulated vsize (Kb) 8584

[startup+20.0058 s]
Raw data (loadavg): 0.80 0.92 0.90 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 2591 0 0 0 1980 9 0 0 25 0 1 0 1796895080 11165696 2246 4294967295 134512640 135094434 3221224432 3221220928 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13910/statm): 2726 2246 145 145 0 2581 0
[pid=13910] vsize: 10904
Current children cumulated CPU time (s) 19.9
Current children cumulated vsize (Kb) 13028

[startup+30.0063 s]
Raw data (loadavg): 0.83 0.92 0.90 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 3596 0 0 0 2976 12 0 0 25 0 1 0 1796895080 13479936 2921 4294967295 134512640 135094434 3221224432 3221221632 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13910/statm): 3291 2921 145 145 0 3146 0
[pid=13910] vsize: 13164
Current children cumulated CPU time (s) 29.89
Current children cumulated vsize (Kb) 15288

[startup+40.0079 s]
Raw data (loadavg): 0.86 0.92 0.90 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 3928 0 0 0 3975 13 0 0 25 0 1 0 1796895080 14016512 3127 4294967295 134512640 135094434 3221224432 3221222192 134783048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13910/statm): 3422 3127 145 145 0 3277 0
[pid=13910] vsize: 13688
Current children cumulated CPU time (s) 39.89
Current children cumulated vsize (Kb) 15812

[startup+50.0084 s]
Raw data (loadavg): 0.88 0.92 0.90 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 4321 0 0 0 4973 14 0 0 25 0 1 0 1796895080 14622720 3394 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13910/statm): 3570 3394 145 145 0 3425 0
[pid=13910] vsize: 14280
Current children cumulated CPU time (s) 49.88
Current children cumulated vsize (Kb) 16404

[startup+60.01 s]
Raw data (loadavg): 0.90 0.92 0.90 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 6708 0 0 0 5963 21 0 0 25 0 1 0 1796895080 22757376 4927 4294967295 134512640 135094434 3221224432 3221220204 134676240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13910/statm): 5556 4927 145 145 0 5411 0
[pid=13910] vsize: 22224
Current children cumulated CPU time (s) 59.85
Current children cumulated vsize (Kb) 24348

[startup+70.0115 s]
Raw data (loadavg): 0.91 0.93 0.90 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 7359 0 0 0 6960 23 0 0 25 0 1 0 1796895080 24031232 5421 4294967295 134512640 135094434 3221224432 3221221552 134676308 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 5867 5421 145 145 0 5722 0
[pid=13910] vsize: 23468
Current children cumulated CPU time (s) 69.84
Current children cumulated vsize (Kb) 25592

[startup+80.0121 s]
Raw data (loadavg): 0.92 0.93 0.90 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 7764 0 0 0 7957 24 0 0 25 0 1 0 1796895080 24997888 5787 4294967295 134512640 135094434 3221224432 3221221376 134677049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13910/statm): 6103 5787 145 145 0 5958 0
[pid=13910] vsize: 24412
Current children cumulated CPU time (s) 79.82
Current children cumulated vsize (Kb) 26536

[startup+90.0127 s]
Raw data (loadavg): 0.94 0.93 0.90 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 8325 0 0 0 8954 26 0 0 25 0 1 0 1796895080 26361856 6312 4294967295 134512640 135094434 3221224432 3221220608 134780812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13910/statm): 6436 6312 145 145 0 6291 0
[pid=13910] vsize: 25744
Current children cumulated CPU time (s) 89.81
Current children cumulated vsize (Kb) 27868

[startup+100.013 s]
Raw data (loadavg): 0.95 0.93 0.91 1/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) T 13906 13906 22582 0 -1 0 11667 0 0 0 9933 38 0 0 24 0 1 0 1796895080 47321088 9517 4294967295 134512640 135094434 3221224432 3221169564 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/13910/statm): 11553 9517 145 145 0 11408 0
[pid=13910] vsize: 46212
Current children cumulated CPU time (s) 99.72
Current children cumulated vsize (Kb) 48336

[startup+110.015 s]
Raw data (loadavg): 0.95 0.93 0.91 1/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) T 13906 13906 22582 0 -1 0 40789 0 0 0 10679 157 0 0 22 0 1 0 1796895080 174149632 38639 4294967295 134512640 135094434 3221224432 3221184060 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/13910/statm): 42517 38639 145 145 0 42372 0
[pid=13910] vsize: 170068
Current children cumulated CPU time (s) 108.37
Current children cumulated vsize (Kb) 172192

[startup+120.015 s]
Raw data (loadavg): 0.96 0.94 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 41721 0 0 0 11670 161 0 0 25 0 1 0 1796895080 176873472 39571 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 43182 39571 145 145 0 43037 0
[pid=13910] vsize: 172728
Current children cumulated CPU time (s) 118.32
Current children cumulated vsize (Kb) 174852

[startup+130.016 s]
Raw data (loadavg): 0.97 0.94 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 41777 0 0 0 12669 162 0 0 25 0 1 0 1796895080 177102848 39627 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 43238 39627 145 145 0 43093 0
[pid=13910] vsize: 172952
Current children cumulated CPU time (s) 128.32
Current children cumulated vsize (Kb) 175076

[startup+140.016 s]
Raw data (loadavg): 0.97 0.94 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 41924 0 0 0 13667 163 0 0 25 0 1 0 1796895080 177709056 39774 4294967295 134512640 135094434 3221224432 3221223104 134553437 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13910/statm): 43386 39774 145 145 0 43241 0
[pid=13910] vsize: 173544
Current children cumulated CPU time (s) 138.31
Current children cumulated vsize (Kb) 175668

[startup+150.017 s]
Raw data (loadavg): 0.97 0.94 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42122 0 0 0 14663 165 0 0 25 0 1 0 1796895080 178536448 39972 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 43588 39972 145 145 0 43443 0
[pid=13910] vsize: 174352
Current children cumulated CPU time (s) 148.29
Current children cumulated vsize (Kb) 176476

[startup+160.019 s]
Raw data (loadavg): 0.98 0.94 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42238 0 0 0 15660 167 0 0 25 0 1 0 1796895080 179007488 40088 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 43703 40088 145 145 0 43558 0
[pid=13910] vsize: 174812
Current children cumulated CPU time (s) 158.28
Current children cumulated vsize (Kb) 176936

[startup+170.019 s]
Raw data (loadavg): 0.98 0.94 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) T 13906 13906 22582 0 -1 0 42365 0 0 0 16659 168 0 0 25 0 1 0 1796895080 179580928 40215 4294967295 134512640 135094434 3221224432 3221223128 134801757 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/13910/statm): 43843 40215 145 145 0 43698 0
[pid=13910] vsize: 175372
Current children cumulated CPU time (s) 168.28
Current children cumulated vsize (Kb) 177496

[startup+180.02 s]
Raw data (loadavg): 0.98 0.94 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42423 0 0 0 17658 168 0 0 25 0 1 0 1796895080 179810304 40273 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 43899 40273 145 145 0 43754 0
[pid=13910] vsize: 175596
Current children cumulated CPU time (s) 178.27
Current children cumulated vsize (Kb) 177720

[startup+190.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42601 0 0 0 18656 169 0 0 25 0 1 0 1796895080 180502528 40451 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 44068 40451 145 145 0 43923 0
[pid=13910] vsize: 176272
Current children cumulated CPU time (s) 188.26
Current children cumulated vsize (Kb) 178396

[startup+200.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42795 0 0 0 19652 171 0 0 25 0 1 0 1796895080 181248000 40645 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 44250 40645 145 145 0 44105 0
[pid=13910] vsize: 177000
Current children cumulated CPU time (s) 198.24
Current children cumulated vsize (Kb) 179124

[startup+210.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42952 0 0 0 20649 173 0 0 25 0 1 0 1796895080 181878784 40802 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 44404 40802 145 145 0 44259 0
[pid=13910] vsize: 177616
Current children cumulated CPU time (s) 208.23
Current children cumulated vsize (Kb) 179740

[startup+220.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 42972 0 0 0 21649 173 0 0 25 0 1 0 1796895080 181952512 40822 4294967295 134512640 135094434 3221224432 3221223024 134557227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 44422 40822 145 145 0 44277 0
[pid=13910] vsize: 177688
Current children cumulated CPU time (s) 218.23
Current children cumulated vsize (Kb) 179812

[startup+230.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43102 0 0 0 22647 174 0 0 25 0 1 0 1796895080 182575104 40952 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 44574 40952 145 145 0 44429 0
[pid=13910] vsize: 178296
Current children cumulated CPU time (s) 228.22
Current children cumulated vsize (Kb) 180420

[startup+240.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43140 0 0 0 23646 175 0 0 25 0 1 0 1796895080 182722560 40990 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 44610 40990 145 145 0 44465 0
[pid=13910] vsize: 178440
Current children cumulated CPU time (s) 238.22
Current children cumulated vsize (Kb) 180564

[startup+250.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43419 0 0 0 24641 177 0 0 25 0 1 0 1796895080 183848960 41269 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 44885 41269 145 145 0 44740 0
[pid=13910] vsize: 179540
Current children cumulated CPU time (s) 248.19
Current children cumulated vsize (Kb) 181664

[startup+260.023 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43601 0 0 0 25638 178 0 0 25 0 1 0 1796895080 184578048 41451 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 45063 41451 145 145 0 44918 0
[pid=13910] vsize: 180252
Current children cumulated CPU time (s) 258.17
Current children cumulated vsize (Kb) 182376

[startup+270.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43637 0 0 0 26638 178 0 0 25 0 1 0 1796895080 184717312 41487 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 45097 41487 145 145 0 44952 0
[pid=13910] vsize: 180388
Current children cumulated CPU time (s) 268.17
Current children cumulated vsize (Kb) 182512

[startup+280.024 s]
Raw data (loadavg): 0.99 0.95 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43854 0 0 0 27635 180 0 0 25 0 1 0 1796895080 185593856 41704 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 45311 41704 145 145 0 45166 0
[pid=13910] vsize: 181244
Current children cumulated CPU time (s) 278.16
Current children cumulated vsize (Kb) 183368

[startup+290.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 43987 0 0 0 28633 181 0 0 25 0 1 0 1796895080 186126336 41837 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 45441 41837 145 145 0 45296 0
[pid=13910] vsize: 181764
Current children cumulated CPU time (s) 288.15
Current children cumulated vsize (Kb) 183888

[startup+300.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 44179 0 0 0 29630 182 0 0 25 0 1 0 1796895080 186896384 42029 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 45629 42029 145 145 0 45484 0
[pid=13910] vsize: 182516
Current children cumulated CPU time (s) 298.13
Current children cumulated vsize (Kb) 184640

[startup+310.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 44354 0 0 0 30627 184 0 0 25 0 1 0 1796895080 187596800 42204 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 45800 42204 145 145 0 45655 0
[pid=13910] vsize: 183200
Current children cumulated CPU time (s) 308.12
Current children cumulated vsize (Kb) 185324

[startup+320.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 44632 0 0 0 31621 186 0 0 25 0 1 0 1796895080 188973056 42482 4294967295 134512640 135094434 3221224432 3221223112 134551489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 46136 42482 145 145 0 45991 0
[pid=13910] vsize: 184544
Current children cumulated CPU time (s) 318.08
Current children cumulated vsize (Kb) 186668

[startup+330.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 44787 0 0 0 32618 187 0 0 25 0 1 0 1796895080 189595648 42637 4294967295 134512640 135094434 3221224432 3221223088 134558276 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 46288 42637 145 145 0 46143 0
[pid=13910] vsize: 185152
Current children cumulated CPU time (s) 328.06
Current children cumulated vsize (Kb) 187276

[startup+340.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 44839 0 0 0 33617 188 0 0 25 0 1 0 1796895080 189800448 42689 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 46338 42689 145 145 0 46193 0
[pid=13910] vsize: 185352
Current children cumulated CPU time (s) 338.06
Current children cumulated vsize (Kb) 187476

[startup+350.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 44904 0 0 0 34617 188 0 0 25 0 1 0 1796895080 190062592 42754 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 46402 42754 145 145 0 46257 0
[pid=13910] vsize: 185608
Current children cumulated CPU time (s) 348.06
Current children cumulated vsize (Kb) 187732

[startup+360.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45035 0 0 0 35614 189 0 0 25 0 1 0 1796895080 190582784 42885 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 46529 42885 145 145 0 46384 0
[pid=13910] vsize: 186116
Current children cumulated CPU time (s) 358.04
Current children cumulated vsize (Kb) 188240

[startup+370.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45117 0 0 0 36614 189 0 0 25 0 1 0 1796895080 190914560 42967 4294967295 134512640 135094434 3221224432 3221223024 134557363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 46610 42967 145 145 0 46465 0
[pid=13910] vsize: 186440
Current children cumulated CPU time (s) 368.04
Current children cumulated vsize (Kb) 188564

[startup+380.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45209 0 0 0 37613 190 0 0 25 0 1 0 1796895080 191283200 43059 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 46700 43059 145 145 0 46555 0
[pid=13910] vsize: 186800
Current children cumulated CPU time (s) 378.04
Current children cumulated vsize (Kb) 188924

[startup+390.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45337 0 0 0 38610 191 0 0 25 0 1 0 1796895080 191795200 43187 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 46825 43187 145 145 0 46680 0
[pid=13910] vsize: 187300
Current children cumulated CPU time (s) 388.02
Current children cumulated vsize (Kb) 189424

[startup+400.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45437 0 0 0 39609 192 0 0 25 0 1 0 1796895080 192196608 43287 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 46923 43287 145 145 0 46778 0
[pid=13910] vsize: 187692
Current children cumulated CPU time (s) 398.02
Current children cumulated vsize (Kb) 189816

[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45526 0 0 0 40608 193 0 0 25 0 1 0 1796895080 192557056 43376 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 47011 43376 145 145 0 46866 0
[pid=13910] vsize: 188044
Current children cumulated CPU time (s) 408.02
Current children cumulated vsize (Kb) 190168

[startup+420.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45620 0 0 0 41606 194 0 0 25 0 1 0 1796895080 192937984 43470 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 47104 43470 145 145 0 46959 0
[pid=13910] vsize: 188416
Current children cumulated CPU time (s) 418.01
Current children cumulated vsize (Kb) 190540

[startup+430.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45730 0 0 0 42604 195 0 0 25 0 1 0 1796895080 193380352 43580 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 47212 43580 145 145 0 47067 0
[pid=13910] vsize: 188848
Current children cumulated CPU time (s) 428
Current children cumulated vsize (Kb) 190972

[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45815 0 0 0 43602 196 0 0 25 0 1 0 1796895080 193724416 43665 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 47296 43665 145 145 0 47151 0
[pid=13910] vsize: 189184
Current children cumulated CPU time (s) 437.99
Current children cumulated vsize (Kb) 191308

[startup+450.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45882 0 0 0 44601 197 0 0 25 0 1 0 1796895080 193998848 43732 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 47363 43732 145 145 0 47218 0
[pid=13910] vsize: 189452
Current children cumulated CPU time (s) 447.99
Current children cumulated vsize (Kb) 191576

[startup+460.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 45969 0 0 0 45599 198 0 0 25 0 1 0 1796895080 194367488 43819 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 47453 43819 145 145 0 47308 0
[pid=13910] vsize: 189812
Current children cumulated CPU time (s) 457.98
Current children cumulated vsize (Kb) 191936

[startup+470.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46056 0 0 0 46598 199 0 0 25 0 1 0 1796895080 194711552 43906 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 47537 43906 145 145 0 47392 0
[pid=13910] vsize: 190148
Current children cumulated CPU time (s) 467.98
Current children cumulated vsize (Kb) 192272

[startup+480.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46183 0 0 0 47596 200 0 0 25 0 1 0 1796895080 195227648 44033 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 47663 44033 145 145 0 47518 0
[pid=13910] vsize: 190652
Current children cumulated CPU time (s) 477.97
Current children cumulated vsize (Kb) 192776

[startup+490.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46230 0 0 0 48596 200 0 0 25 0 1 0 1796895080 195420160 44080 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 47710 44080 145 145 0 47565 0
[pid=13910] vsize: 190840
Current children cumulated CPU time (s) 487.97
Current children cumulated vsize (Kb) 192964

[startup+500.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46411 0 0 0 49592 202 0 0 25 0 1 0 1796895080 196149248 44261 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 47888 44261 145 145 0 47743 0
[pid=13910] vsize: 191552
Current children cumulated CPU time (s) 497.95
Current children cumulated vsize (Kb) 193676

[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46492 0 0 0 50591 202 0 0 25 0 1 0 1796895080 196476928 44342 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 47968 44342 145 145 0 47823 0
[pid=13910] vsize: 191872
Current children cumulated CPU time (s) 507.94
Current children cumulated vsize (Kb) 193996

[startup+520.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46615 0 0 0 51590 203 0 0 25 0 1 0 1796895080 196952064 44465 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 48084 44465 145 145 0 47939 0
[pid=13910] vsize: 192336
Current children cumulated CPU time (s) 517.94
Current children cumulated vsize (Kb) 194460

[startup+530.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46617 0 0 0 52590 203 0 0 25 0 1 0 1796895080 196960256 44467 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 48086 44467 145 145 0 47941 0
[pid=13910] vsize: 192344
Current children cumulated CPU time (s) 527.94
Current children cumulated vsize (Kb) 194468

[startup+540.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46696 0 0 0 53589 204 0 0 25 0 1 0 1796895080 197279744 44546 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 48164 44546 145 145 0 48019 0
[pid=13910] vsize: 192656
Current children cumulated CPU time (s) 537.94
Current children cumulated vsize (Kb) 194780

[startup+550.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46776 0 0 0 54588 204 0 0 25 0 1 0 1796895080 197603328 44626 4294967295 134512640 135094434 3221224432 3221223092 134553530 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 48243 44626 145 145 0 48098 0
[pid=13910] vsize: 192972
Current children cumulated CPU time (s) 547.93
Current children cumulated vsize (Kb) 195096

[startup+560.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 46979 0 0 0 55586 205 0 0 25 0 1 0 1796895080 198402048 44829 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 48438 44829 145 145 0 48293 0
[pid=13910] vsize: 193752
Current children cumulated CPU time (s) 557.92
Current children cumulated vsize (Kb) 195876

[startup+570.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 47436 0 0 0 56578 208 0 0 25 0 1 0 1796895080 200249344 45286 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 48889 45286 145 145 0 48744 0
[pid=13910] vsize: 195556
Current children cumulated CPU time (s) 567.87
Current children cumulated vsize (Kb) 197680

[startup+580.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 47639 0 0 0 57574 210 0 0 25 0 1 0 1796895080 201068544 45489 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 49089 45489 145 145 0 48944 0
[pid=13910] vsize: 196356
Current children cumulated CPU time (s) 577.85
Current children cumulated vsize (Kb) 198480

[startup+590.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 47844 0 0 0 58570 212 0 0 25 0 1 0 1796895080 201895936 45694 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 49291 45694 145 145 0 49146 0
[pid=13910] vsize: 197164
Current children cumulated CPU time (s) 587.83
Current children cumulated vsize (Kb) 199288

[startup+600.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 47987 0 0 0 59567 213 0 0 25 0 1 0 1796895080 202469376 45837 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 49431 45837 145 145 0 49286 0
[pid=13910] vsize: 197724
Current children cumulated CPU time (s) 597.81
Current children cumulated vsize (Kb) 199848

[startup+610.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 48191 0 0 0 60565 214 0 0 25 0 1 0 1796895080 203292672 46041 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 49632 46041 145 145 0 49487 0
[pid=13910] vsize: 198528
Current children cumulated CPU time (s) 607.8
Current children cumulated vsize (Kb) 200652

[startup+620.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 48445 0 0 0 61560 216 0 0 25 0 1 0 1796895080 204316672 46295 4294967295 134512640 135094434 3221224432 3221223136 134558968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 49882 46295 145 145 0 49737 0
[pid=13910] vsize: 199528
Current children cumulated CPU time (s) 617.77
Current children cumulated vsize (Kb) 201652

[startup+630.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 48547 0 0 0 62558 217 0 0 25 0 1 0 1796895080 204726272 46397 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 49982 46397 145 145 0 49837 0
[pid=13910] vsize: 199928
Current children cumulated CPU time (s) 627.76
Current children cumulated vsize (Kb) 202052

[startup+640.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 48627 0 0 0 63557 217 0 0 25 0 1 0 1796895080 205045760 46477 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 50060 46477 145 145 0 49915 0
[pid=13910] vsize: 200240
Current children cumulated CPU time (s) 637.75
Current children cumulated vsize (Kb) 202364

[startup+650.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 48790 0 0 0 64555 219 0 0 25 0 1 0 1796895080 206192640 46640 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 50340 46640 145 145 0 50195 0
[pid=13910] vsize: 201360
Current children cumulated CPU time (s) 647.75
Current children cumulated vsize (Kb) 203484

[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 48952 0 0 0 65551 220 0 0 25 0 1 0 1796895080 206848000 46802 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 50500 46802 145 145 0 50355 0
[pid=13910] vsize: 202000
Current children cumulated CPU time (s) 657.72
Current children cumulated vsize (Kb) 204124

[startup+670.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49106 0 0 0 66549 221 0 0 25 0 1 0 1796895080 207470592 46956 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 50652 46956 145 145 0 50507 0
[pid=13910] vsize: 202608
Current children cumulated CPU time (s) 667.71
Current children cumulated vsize (Kb) 204732

[startup+680.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49253 0 0 0 67547 222 0 0 25 0 1 0 1796895080 208064512 47103 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 50797 47103 145 145 0 50652 0
[pid=13910] vsize: 203188
Current children cumulated CPU time (s) 677.7
Current children cumulated vsize (Kb) 205312

[startup+690.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49383 0 0 0 68545 223 0 0 25 0 1 0 1796895080 208592896 47233 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 50926 47233 145 145 0 50781 0
[pid=13910] vsize: 203704
Current children cumulated CPU time (s) 687.69
Current children cumulated vsize (Kb) 205828

[startup+700.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49526 0 0 0 69543 225 0 0 25 0 1 0 1796895080 209166336 47376 4294967295 134512640 135094434 3221224432 3221223024 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 51066 47376 145 145 0 50921 0
[pid=13910] vsize: 204264
Current children cumulated CPU time (s) 697.69
Current children cumulated vsize (Kb) 206388

[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49636 0 0 0 70541 225 0 0 25 0 1 0 1796895080 209612800 47486 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 51175 47486 145 145 0 51030 0
[pid=13910] vsize: 204700
Current children cumulated CPU time (s) 707.67
Current children cumulated vsize (Kb) 206824

[startup+720.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49741 0 0 0 71540 226 0 0 25 0 1 0 1796895080 210030592 47591 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 51277 47591 145 145 0 51132 0
[pid=13910] vsize: 205108
Current children cumulated CPU time (s) 717.67
Current children cumulated vsize (Kb) 207232

[startup+730.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 49910 0 0 0 72537 228 0 0 25 0 1 0 1796895080 210706432 47760 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 51442 47760 145 145 0 51297 0
[pid=13910] vsize: 205768
Current children cumulated CPU time (s) 727.66
Current children cumulated vsize (Kb) 207892

[startup+740.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50021 0 0 0 73535 229 0 0 25 0 1 0 1796895080 211156992 47871 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 51552 47871 145 145 0 51407 0
[pid=13910] vsize: 206208
Current children cumulated CPU time (s) 737.65
Current children cumulated vsize (Kb) 208332

[startup+750.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50156 0 0 0 74533 230 0 0 25 0 1 0 1796895080 211697664 48006 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 51684 48006 145 145 0 51539 0
[pid=13910] vsize: 206736
Current children cumulated CPU time (s) 747.64
Current children cumulated vsize (Kb) 208860

[startup+760.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50281 0 0 0 75531 230 0 0 25 0 1 0 1796895080 212230144 48131 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 51814 48131 145 145 0 51669 0
[pid=13910] vsize: 207256
Current children cumulated CPU time (s) 757.62
Current children cumulated vsize (Kb) 209380

[startup+770.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50419 0 0 0 76529 231 0 0 25 0 1 0 1796895080 212791296 48269 4294967295 134512640 135094434 3221224432 3221223024 134557182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 51951 48269 145 145 0 51806 0
[pid=13910] vsize: 207804
Current children cumulated CPU time (s) 767.61
Current children cumulated vsize (Kb) 209928

[startup+780.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50612 0 0 0 77525 233 0 0 25 0 1 0 1796895080 213569536 48462 4294967295 134512640 135094434 3221224432 3221223056 134557726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 52141 48462 145 145 0 51996 0
[pid=13910] vsize: 208564
Current children cumulated CPU time (s) 777.59
Current children cumulated vsize (Kb) 210688

[startup+790.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50756 0 0 0 78523 234 0 0 25 0 1 0 1796895080 214155264 48606 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 52284 48606 145 145 0 52139 0
[pid=13910] vsize: 209136
Current children cumulated CPU time (s) 787.58
Current children cumulated vsize (Kb) 211260

[startup+800.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 50878 0 0 0 79521 234 0 0 25 0 1 0 1796895080 214646784 48728 4294967295 134512640 135094434 3221224432 3221223024 134557377 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 52404 48728 145 145 0 52259 0
[pid=13910] vsize: 209616
Current children cumulated CPU time (s) 797.56
Current children cumulated vsize (Kb) 211740

[startup+810.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51021 0 0 0 80518 235 0 0 25 0 1 0 1796895080 215224320 48871 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 52545 48871 145 145 0 52400 0
[pid=13910] vsize: 210180
Current children cumulated CPU time (s) 807.54
Current children cumulated vsize (Kb) 212304

[startup+820.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51162 0 0 0 81516 236 0 0 25 0 1 0 1796895080 215797760 49012 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 52685 49012 145 145 0 52540 0
[pid=13910] vsize: 210740
Current children cumulated CPU time (s) 817.53
Current children cumulated vsize (Kb) 212864

[startup+830.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51260 0 0 0 82514 237 0 0 25 0 1 0 1796895080 216190976 49110 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 52781 49110 145 145 0 52636 0
[pid=13910] vsize: 211124
Current children cumulated CPU time (s) 827.52
Current children cumulated vsize (Kb) 213248

[startup+840.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51385 0 0 0 83513 238 0 0 25 0 1 0 1796895080 216698880 49235 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 52905 49235 145 145 0 52760 0
[pid=13910] vsize: 211620
Current children cumulated CPU time (s) 837.52
Current children cumulated vsize (Kb) 213744

[startup+850.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51505 0 0 0 84511 238 0 0 25 0 1 0 1796895080 217186304 49355 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 53024 49355 145 145 0 52879 0
[pid=13910] vsize: 212096
Current children cumulated CPU time (s) 847.5
Current children cumulated vsize (Kb) 214220

[startup+860.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51633 0 0 0 85509 239 0 0 25 0 1 0 1796895080 217718784 49483 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 53154 49483 145 145 0 53009 0
[pid=13910] vsize: 212616
Current children cumulated CPU time (s) 857.49
Current children cumulated vsize (Kb) 214740

[startup+870.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51738 0 0 0 86507 240 0 0 25 0 1 0 1796895080 218140672 49588 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 53257 49588 145 145 0 53112 0
[pid=13910] vsize: 213028
Current children cumulated CPU time (s) 867.48
Current children cumulated vsize (Kb) 215152

[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51841 0 0 0 87505 241 0 0 25 0 1 0 1796895080 218570752 49691 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13910/statm): 53362 49691 145 145 0 53217 0
[pid=13910] vsize: 213448
Current children cumulated CPU time (s) 877.47
Current children cumulated vsize (Kb) 215572

[startup+890.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 51994 0 0 0 88502 243 0 0 25 0 1 0 1796895080 219193344 49844 4294967295 134512640 135094434 3221224432 3221223060 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 53514 49844 145 145 0 53369 0
[pid=13910] vsize: 214056
Current children cumulated CPU time (s) 887.46
Current children cumulated vsize (Kb) 216180

[startup+900.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52125 0 0 0 89501 243 0 0 25 0 1 0 1796895080 219713536 49975 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 53641 49975 145 145 0 53496 0
[pid=13910] vsize: 214564
Current children cumulated CPU time (s) 897.45
Current children cumulated vsize (Kb) 216688

[startup+910.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52235 0 0 0 90499 244 0 0 25 0 1 0 1796895080 220147712 50085 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 53747 50085 145 145 0 53602 0
[pid=13910] vsize: 214988
Current children cumulated CPU time (s) 907.44
Current children cumulated vsize (Kb) 217112

[startup+920.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52343 0 0 0 91497 245 0 0 25 0 1 0 1796895080 220585984 50193 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 53854 50193 145 145 0 53709 0
[pid=13910] vsize: 215416
Current children cumulated CPU time (s) 917.43
Current children cumulated vsize (Kb) 217540

[startup+930.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52447 0 0 0 92496 246 0 0 25 0 1 0 1796895080 220999680 50297 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 53955 50297 145 145 0 53810 0
[pid=13910] vsize: 215820
Current children cumulated CPU time (s) 927.43
Current children cumulated vsize (Kb) 217944

[startup+940.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52509 0 0 0 93494 246 0 0 25 0 1 0 1796895080 221253632 50359 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 54017 50359 145 145 0 53872 0
[pid=13910] vsize: 216068
Current children cumulated CPU time (s) 937.41
Current children cumulated vsize (Kb) 218192

[startup+950.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52575 0 0 0 94493 247 0 0 25 0 1 0 1796895080 221519872 50425 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 54082 50425 145 145 0 53937 0
[pid=13910] vsize: 216328
Current children cumulated CPU time (s) 947.41
Current children cumulated vsize (Kb) 218452

[startup+960.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52649 0 0 0 95491 248 0 0 17 0 1 0 1796895080 221822976 50499 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 54156 50499 145 145 0 54011 0
[pid=13910] vsize: 216624
Current children cumulated CPU time (s) 957.4
Current children cumulated vsize (Kb) 218748

[startup+970.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52743 0 0 0 96489 249 0 0 25 0 1 0 1796895080 222203904 50593 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13910/statm): 54249 50593 145 145 0 54104 0
[pid=13910] vsize: 216996
Current children cumulated CPU time (s) 967.39
Current children cumulated vsize (Kb) 219120

[startup+980.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52887 0 0 0 97485 250 0 0 25 0 1 0 1796895080 222777344 50737 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 54389 50737 145 145 0 54244 0
[pid=13910] vsize: 217556
Current children cumulated CPU time (s) 977.36
Current children cumulated vsize (Kb) 219680

[startup+990.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 52979 0 0 0 98484 251 0 0 25 0 1 0 1796895080 223170560 50829 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 54485 50829 145 145 0 54340 0
[pid=13910] vsize: 217940
Current children cumulated CPU time (s) 987.36
Current children cumulated vsize (Kb) 220064

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) T 13906 13906 22582 0 -1 0 53114 0 0 0 99481 252 0 0 25 0 1 0 1796895080 223707136 50964 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/13910/statm): 54616 50964 145 145 0 54471 0
[pid=13910] vsize: 218464
Current children cumulated CPU time (s) 997.34
Current children cumulated vsize (Kb) 220588

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53244 0 0 0 100479 253 0 0 25 0 1 0 1796895080 224231424 51094 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 54744 51094 145 145 0 54599 0
[pid=13910] vsize: 218976
Current children cumulated CPU time (s) 1007.33
Current children cumulated vsize (Kb) 221100

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53339 0 0 0 101477 254 0 0 25 0 1 0 1796895080 224624640 51189 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 54840 51189 145 145 0 54695 0
[pid=13910] vsize: 219360
Current children cumulated CPU time (s) 1017.32
Current children cumulated vsize (Kb) 221484

[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53412 0 0 0 102476 254 0 0 25 0 1 0 1796895080 224927744 51262 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 54914 51262 145 145 0 54769 0
[pid=13910] vsize: 219656
Current children cumulated CPU time (s) 1027.31
Current children cumulated vsize (Kb) 221780

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53492 0 0 0 103475 255 0 0 25 0 1 0 1796895080 225271808 51342 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 54998 51342 145 145 0 54853 0
[pid=13910] vsize: 219992
Current children cumulated CPU time (s) 1037.31
Current children cumulated vsize (Kb) 222116

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53552 0 0 0 104475 255 0 0 25 0 1 0 1796895080 225529856 51402 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 55061 51402 145 145 0 54916 0
[pid=13910] vsize: 220244
Current children cumulated CPU time (s) 1047.31
Current children cumulated vsize (Kb) 222368

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53639 0 0 0 105473 256 0 0 25 0 1 0 1796895080 225894400 51489 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 55150 51489 145 145 0 55005 0
[pid=13910] vsize: 220600
Current children cumulated CPU time (s) 1057.3
Current children cumulated vsize (Kb) 222724

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53737 0 0 0 106471 257 0 0 25 0 1 0 1796895080 226283520 51587 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 55245 51587 145 145 0 55100 0
[pid=13910] vsize: 220980
Current children cumulated CPU time (s) 1067.29
Current children cumulated vsize (Kb) 223104

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53830 0 0 0 107471 258 0 0 25 0 1 0 1796895080 226684928 51680 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 55343 51680 145 145 0 55198 0
[pid=13910] vsize: 221372
Current children cumulated CPU time (s) 1077.3
Current children cumulated vsize (Kb) 223496

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 53937 0 0 0 108469 259 0 0 25 0 1 0 1796895080 227110912 51787 4294967295 134512640 135094434 3221224432 3221223056 134557593 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 55447 51787 145 145 0 55302 0
[pid=13910] vsize: 221788
Current children cumulated CPU time (s) 1087.29
Current children cumulated vsize (Kb) 223912

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54021 0 0 0 109468 260 0 0 25 0 1 0 1796895080 227442688 51871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 55528 51871 145 145 0 55383 0
[pid=13910] vsize: 222112
Current children cumulated CPU time (s) 1097.29
Current children cumulated vsize (Kb) 224236

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54123 0 0 0 110466 260 0 0 25 0 1 0 1796895080 227848192 51973 4294967295 134512640 135094434 3221224432 3221223024 134557366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 55627 51973 145 145 0 55482 0
[pid=13910] vsize: 222508
Current children cumulated CPU time (s) 1107.27
Current children cumulated vsize (Kb) 224632

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54213 0 0 0 111464 262 0 0 25 0 1 0 1796895080 228216832 52063 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 55717 52063 145 145 0 55572 0
[pid=13910] vsize: 222868
Current children cumulated CPU time (s) 1117.27
Current children cumulated vsize (Kb) 224992

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54278 0 0 0 112463 262 0 0 25 0 1 0 1796895080 228470784 52128 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 55779 52128 145 145 0 55634 0
[pid=13910] vsize: 223116
Current children cumulated CPU time (s) 1127.26
Current children cumulated vsize (Kb) 225240

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54372 0 0 0 113462 263 0 0 25 0 1 0 1796895080 228851712 52222 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 55872 52222 145 145 0 55727 0
[pid=13910] vsize: 223488
Current children cumulated CPU time (s) 1137.26
Current children cumulated vsize (Kb) 225612

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54460 0 0 0 114460 263 0 0 25 0 1 0 1796895080 229199872 52310 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 55957 52310 145 145 0 55812 0
[pid=13910] vsize: 223828
Current children cumulated CPU time (s) 1147.24
Current children cumulated vsize (Kb) 225952

[startup+1160.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54531 0 0 0 115458 264 0 0 25 0 1 0 1796895080 229486592 52381 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 56027 52381 145 145 0 55882 0
[pid=13910] vsize: 224108
Current children cumulated CPU time (s) 1157.23
Current children cumulated vsize (Kb) 226232

[startup+1170.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54595 0 0 0 116458 264 0 0 25 0 1 0 1796895080 229744640 52445 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 56090 52445 145 145 0 55945 0
[pid=13910] vsize: 224360
Current children cumulated CPU time (s) 1167.23
Current children cumulated vsize (Kb) 226484

[startup+1180.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54673 0 0 0 117456 265 0 0 25 0 1 0 1796895080 230100992 52523 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 56177 52523 145 145 0 56032 0
[pid=13910] vsize: 224708
Current children cumulated CPU time (s) 1177.22
Current children cumulated vsize (Kb) 226832

[startup+1190.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54729 0 0 0 118455 265 0 0 25 0 1 0 1796895080 230326272 52579 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 56232 52579 145 145 0 56087 0
[pid=13910] vsize: 224928
Current children cumulated CPU time (s) 1187.21
Current children cumulated vsize (Kb) 227052

[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54793 0 0 0 119455 266 0 0 25 0 1 0 1796895080 230580224 52643 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 56294 52643 145 145 0 56149 0
[pid=13910] vsize: 225176
Current children cumulated CPU time (s) 1197.22
Current children cumulated vsize (Kb) 227300

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54866 0 0 0 120453 267 0 0 25 0 1 0 1796895080 230879232 52716 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 56367 52716 145 145 0 56222 0
[pid=13910] vsize: 225468
Current children cumulated CPU time (s) 1207.21
Current children cumulated vsize (Kb) 227592



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 13910
Raw data (/proc/13906/stat): 13906 (minisat+_script) S 13905 13906 22582 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1796895075 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13906/statm): 531 226 485 147 0 384 0
[pid=13906] vsize: 2124
Raw data (/proc/13910/stat): 13910 (minisat+_64-bit) R 13906 13906 22582 0 -1 0 54866 0 0 0 120453 267 0 0 25 0 1 0 1796895080 230879232 52716 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13910/statm): 56367 52716 145 145 0 56222 0
[pid=13910] vsize: 225468
Current children cumulated CPU time (s) 1207.21
Current children cumulated vsize (Kb) 227592

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

Child status: 0
Real time (s): 1210.19
CPU time (s): 1207.31
CPU user time (s): 1204.53
CPU system time (s): 2.77658
CPU usage (%): 99.762
Max. virtual memory (cumulated for all children) (Kb): 227592

Verifier Data

ERROR: no interpretation found !