PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-scorpion.opb
MD5SUM	407688f2ee1c26681a4ae06671027d6f
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(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 numbers	40
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.065989
Number of variables	7160
Total number of constraints	388
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	388
Minimum length of a constraint	20
Maximum length of a constraint	400
Trace number 31052

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-05-25 21:37:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22434 boxname=wulflinc28 idbench=1250 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  407688f2ee1c26681a4ae06671027d6f  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-scorpion.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-scorpion.opb
IDLAUNCH: 22434
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        815940 kB
Buffers:         29844 kB
Cached:         167288 kB
SwapCached:        748 kB
Active:          17288 kB
Inactive:       182156 kB
HighTotal:      131008 kB
HighFree:         5068 kB
LowTotal:       903652 kB
LowFree:        810872 kB
SwapTotal:     2097640 kB
SwapFree:      2096192 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5444 kB
Slab:            13576 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 21:58:17 (client local time) WITH STATUS 152 IN 1229.93 SECONDS
stats: 22434 7 1229.93 152
#### END LAUNCHER DATA ####
#### BEGIN 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 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 10660 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.60 0.83 0.86 2/54 10656
Raw data (stat): 10656 (runsolver) R 10655 24821 24820 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842183339 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.66 0.83 0.86 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0012 s]
Raw data (loadavg): 0.71 0.84 0.87 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0012 s]
Raw data (loadavg): 0.76 0.84 0.87 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0023 s]
Raw data (loadavg): 0.79 0.85 0.87 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0029 s]
Raw data (loadavg): 0.83 0.85 0.87 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0022 s]
Raw data (loadavg): 0.85 0.86 0.87 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0034 s]
Raw data (loadavg): 0.87 0.86 0.87 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0044 s]
Raw data (loadavg): 0.89 0.86 0.87 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0053 s]
Raw data (loadavg): 0.91 0.87 0.87 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.005 s]
Raw data (loadavg): 0.92 0.87 0.87 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.006 s]
Raw data (loadavg): 0.93 0.87 0.87 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.007 s]
Raw data (loadavg): 0.94 0.88 0.88 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.007 s]
Raw data (loadavg): 0.95 0.88 0.88 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.008 s]
Raw data (loadavg): 0.96 0.89 0.88 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.008 s]
Raw data (loadavg): 0.96 0.89 0.88 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.008 s]
Raw data (loadavg): 0.97 0.89 0.88 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.009 s]
Raw data (loadavg): 0.97 0.89 0.88 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.009 s]
Raw data (loadavg): 0.98 0.90 0.88 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.01 s]
Raw data (loadavg): 0.98 0.90 0.88 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.022 s]
Raw data (loadavg): 0.98 0.90 0.88 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.029 s]
Raw data (loadavg): 0.98 0.91 0.88 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.029 s]
Raw data (loadavg): 0.99 0.91 0.89 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.029 s]
Raw data (loadavg): 0.99 0.91 0.89 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.029 s]
Raw data (loadavg): 0.99 0.91 0.89 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.03 s]
Raw data (loadavg): 0.99 0.92 0.89 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.03 s]
Raw data (loadavg): 0.99 0.92 0.89 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.03 s]
Raw data (loadavg): 0.99 0.92 0.89 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.03 s]
Raw data (loadavg): 0.99 0.92 0.89 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.031 s]
Raw data (loadavg): 0.99 0.92 0.89 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.03 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.03 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.031 s]
Raw data (loadavg): 0.99 0.93 0.89 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.03 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.031 s]
Raw data (loadavg): 0.99 0.93 0.90 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.031 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.03 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.031 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.031 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.032 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.033 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.032 s]
Raw data (loadavg): 0.99 0.94 0.90 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.032 s]
Raw data (loadavg): 0.99 0.95 0.90 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.032 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.033 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.031 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.032 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.033 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.034 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.75 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 10660
Raw data (stat): 10656 (minisat+_script) S 10655 24821 24820 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842183339 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.75
CPU time (s): 1229.93
CPU user time (s): 1228.34
CPU system time (s): 1.59176
CPU usage (%): 100.015
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####