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/MIPLIB/miplib3/normalized-mps-v2-13-7-nw04.opb
MD5SUM	a5c401bba5afccf02c7b40cb1c595b15
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	30407
Optimality of the best value was proved	NO
Number of terms in the objective function	87482
Biggest coefficient in the objective function	5220
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	120189580
Number of bits of the sum of numbers in the objective function	27
Biggest number in a constraint	5220
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	120189580
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1192.4
Number of variables	87482
Total number of constraints	87518
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	87518
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	42032
Trace number 15010

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 02:38:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18673 boxname=wulflinc29 idbench=1437 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  a5c401bba5afccf02c7b40cb1c595b15  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-nw04.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-nw04.opb
IDLAUNCH: 18673
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        847384 kB
Buffers:          7492 kB
Cached:         151096 kB
SwapCached:        464 kB
Active:          52296 kB
Inactive:       108464 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        847104 kB
SwapTotal:     2097892 kB
SwapFree:      2096700 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            20796 kB
Committed_AS:    63568 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 02:56:48 (client local time) WITH STATUS 0 IN 1080.21 SECONDS
stats: 18673 7 1080.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
#### 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.86 0.96 0.92 2/54 20475
Raw data (stat): 20475 (runsolver) R 20474 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541539828 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.001 s]
Raw data (loadavg): 0.88 0.96 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 22973 0 0 0 936 62 0 0 25 0 1 0 541539828 64581632 7176 4294967295 134512640 134672761 3221224624 3220512320 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15767 7176 603 41 0 15726 0
vsize: 63068
[startup+20.0013 s]
Raw data (loadavg): 0.90 0.96 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 22973 0 0 0 1936 62 0 0 25 0 1 0 541539828 64581632 7176 4294967295 134512640 134672761 3221224624 3220793120 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15767 7176 603 41 0 15726 0
vsize: 63068
[startup+30.0011 s]
Raw data (loadavg): 0.91 0.96 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 23318 0 0 0 2935 63 0 0 25 0 1 0 541539828 65994752 7521 4294967295 134512640 134672761 3221224624 3220600352 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16112 7521 603 41 0 16071 0
vsize: 64448
[startup+40.0012 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 23706 0 0 0 3935 64 0 0 25 0 1 0 541539828 69140480 7909 4294967295 134512640 134672761 3221224624 3220734768 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16880 7909 603 41 0 16839 0
vsize: 67520
[startup+50.0007 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 23947 0 0 0 4934 65 0 0 25 0 1 0 541539828 69771264 8150 4294967295 134512640 134672761 3221224624 3220437648 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17034 8150 603 41 0 16993 0
vsize: 68136
[startup+60.0006 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 24685 0 0 0 5932 67 0 0 25 0 1 0 541539828 71118848 8558 4294967295 134512640 134672761 3221224624 3220928096 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17363 8558 603 41 0 17322 0
vsize: 69452
[startup+70.0006 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 24780 0 0 0 6931 67 0 0 25 0 1 0 541539828 71118848 8653 4294967295 134512640 134672761 3221224624 3220735904 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17363 8653 603 41 0 17322 0
vsize: 69452
[startup+80.0001 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 24841 0 0 0 7931 68 0 0 25 0 1 0 541539828 71118848 8714 4294967295 134512640 134672761 3221224624 3219870576 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17363 8714 603 41 0 17322 0
vsize: 69452
[startup+90 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 25087 0 0 0 8931 68 0 0 25 0 1 0 541539828 74571776 8877 4294967295 134512640 134672761 3221224624 3220505136 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18206 8877 603 41 0 18165 0
vsize: 72824
[startup+100 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 25457 0 0 0 9930 69 0 0 25 0 1 0 541539828 75186176 9122 4294967295 134512640 134672761 3221224624 3220918304 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18356 9122 603 41 0 18315 0
vsize: 73424
[startup+110.001 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 25683 0 0 0 10930 69 0 0 25 0 1 0 541539828 75624448 9306 4294967295 134512640 134672761 3221224624 3221005184 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18463 9306 603 41 0 18422 0
vsize: 73852
[startup+120 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 27544 0 0 0 11926 74 0 0 25 0 1 0 541539828 79851520 10383 4294967295 134512640 134672761 3221224624 3220532384 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19495 10383 603 41 0 19454 0
vsize: 77980
[startup+130 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 27599 0 0 0 12926 74 0 0 25 0 1 0 541539828 79986688 10438 4294967295 134512640 134672761 3221224624 3221203808 134594220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19528 10438 603 41 0 19487 0
vsize: 78112
[startup+140 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 27601 0 0 0 13926 74 0 0 25 0 1 0 541539828 79986688 10440 4294967295 134512640 134672761 3221224624 3219998160 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19528 10440 603 41 0 19487 0
vsize: 78112
[startup+150 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 27601 0 0 0 14926 74 0 0 25 0 1 0 541539828 79986688 10440 4294967295 134512640 134672761 3221224624 3218540688 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19528 10440 603 41 0 19487 0
vsize: 78112
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 28057 0 0 0 15925 75 0 0 25 0 1 0 541539828 81133568 10813 4294967295 134512640 134672761 3221224624 3221170208 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19808 10813 603 41 0 19767 0
vsize: 79232
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 28360 0 0 0 16924 76 0 0 25 0 1 0 541539828 81313792 10909 4294967295 134512640 134672761 3221224624 3220878080 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19852 10909 603 41 0 19811 0
vsize: 79408
[startup+179.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 28389 0 0 0 17924 76 0 0 25 0 1 0 541539828 81313792 10938 4294967295 134512640 134672761 3221224624 3220429488 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19852 10938 603 41 0 19811 0
vsize: 79408
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 28471 0 0 0 18925 76 0 0 25 0 1 0 541539828 81584128 11020 4294967295 134512640 134672761 3221224624 3219816608 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19918 11020 603 41 0 19877 0
vsize: 79672
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 28909 0 0 0 19923 78 0 0 25 0 1 0 541539828 82038784 11210 4294967295 134512640 134672761 3221224624 3220466624 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20029 11210 603 41 0 19988 0
vsize: 80116
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 29050 0 0 0 20923 78 0 0 25 0 1 0 541539828 82341888 11309 4294967295 134512640 134672761 3221224624 3220706736 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20103 11309 603 41 0 20062 0
vsize: 80412
[startup+220 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 29378 0 0 0 21923 78 0 0 25 0 1 0 541539828 83083264 11554 4294967295 134512640 134672761 3221224624 3221123936 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20284 11554 603 41 0 20243 0
vsize: 81136
[startup+230 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 29683 0 0 0 22923 79 0 0 25 0 1 0 541539828 83230720 11652 4294967295 134512640 134672761 3221224624 3220773440 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20320 11652 603 41 0 20279 0
vsize: 81280
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 29721 0 0 0 23923 79 0 0 25 0 1 0 541539828 83365888 11690 4294967295 134512640 134672761 3221224624 3220501968 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20353 11690 603 41 0 20312 0
vsize: 81412
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 29721 0 0 0 24923 79 0 0 25 0 1 0 541539828 83365888 11690 4294967295 134512640 134672761 3221224624 3219101808 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20353 11690 603 41 0 20312 0
vsize: 81412
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 30090 0 0 0 25922 80 0 0 25 0 1 0 541539828 90398720 11976 4294967295 134512640 134672761 3221224624 3221195456 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22070 11976 603 41 0 22029 0
vsize: 88280
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 30392 0 0 0 26921 81 0 0 25 0 1 0 541539828 90595328 12071 4294967295 134512640 134672761 3221224624 3220746080 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22118 12071 603 41 0 22077 0
vsize: 88472
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 30431 0 0 0 27921 81 0 0 25 0 1 0 541539828 90730496 12110 4294967295 134512640 134672761 3221224624 3220511952 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22151 12110 603 41 0 22110 0
vsize: 88604
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 30431 0 0 0 28922 81 0 0 25 0 1 0 541539828 90730496 12110 4294967295 134512640 134672761 3221224624 3219372432 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22151 12110 603 41 0 22110 0
vsize: 88604
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 30785 0 0 0 29921 82 0 0 25 0 1 0 541539828 91471872 12381 4294967295 134512640 134672761 3221224624 3220947584 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22332 12381 603 41 0 22291 0
vsize: 89328
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 31007 0 0 0 30920 83 0 0 25 0 1 0 541539828 91508736 12438 4294967295 134512640 134672761 3221224624 3220523072 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22341 12438 603 41 0 22300 0
vsize: 89364
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 31148 0 0 0 31920 83 0 0 25 0 1 0 541539828 91811840 12537 4294967295 134512640 134672761 3221224624 3220637616 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22415 12537 603 41 0 22374 0
vsize: 89660
[startup+330.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 31148 0 0 0 32920 83 0 0 25 0 1 0 541539828 91811840 12537 4294967295 134512640 134672761 3221224624 3219895344 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22415 12537 603 41 0 22374 0
vsize: 89660
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 31460 0 0 0 33920 84 0 0 25 0 1 0 541539828 92553216 12766 4294967295 134512640 134672761 3221224624 3220401728 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22596 12766 603 41 0 22555 0
vsize: 90384
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 31693 0 0 0 34919 84 0 0 25 0 1 0 541539828 92495872 12834 4294967295 134512640 134672761 3221224624 3220021568 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22582 12834 603 41 0 22541 0
vsize: 90328
[startup+360.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 31855 0 0 0 35919 85 0 0 25 0 1 0 541539828 92798976 12954 4294967295 134512640 134672761 3221224624 3220991456 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22656 12954 603 41 0 22615 0
vsize: 90624
[startup+370.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 31874 0 0 0 36919 85 0 0 25 0 1 0 541539828 92934144 12973 4294967295 134512640 134672761 3221224624 3220261584 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22689 12973 603 41 0 22648 0
vsize: 90756
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 31874 0 0 0 37919 85 0 0 25 0 1 0 541539828 92934144 12973 4294967295 134512640 134672761 3221224624 3219014160 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22689 12973 603 41 0 22648 0
vsize: 90756
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 34867 0 0 0 38913 92 0 0 25 0 1 0 541539828 99078144 14565 4294967295 134512640 134672761 3221224624 3220855904 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24189 14565 603 41 0 24148 0
vsize: 96756
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 35128 0 0 0 39913 92 0 0 25 0 1 0 541539828 99274752 14661 4294967295 134512640 134672761 3221224624 3220209056 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24237 14661 603 41 0 24196 0
vsize: 96948
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 35276 0 0 0 40912 93 0 0 25 0 1 0 541539828 99577856 14767 4294967295 134512640 134672761 3221224624 3221007776 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14767 603 41 0 24270 0
vsize: 97244
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 35294 0 0 0 41912 93 0 0 25 0 1 0 541539828 99577856 14785 4294967295 134512640 134672761 3221224624 3220203120 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14785 603 41 0 24270 0
vsize: 97244
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 35294 0 0 0 42912 93 0 0 25 0 1 0 541539828 99577856 14785 4294967295 134512640 134672761 3221224624 3219470832 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14785 603 41 0 24270 0
vsize: 97244
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 35615 0 0 0 43912 93 0 0 25 0 1 0 541539828 100319232 15023 4294967295 134512640 134672761 3221224624 3220320224 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24492 15023 603 41 0 24451 0
vsize: 97968
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 36028 0 0 0 44911 95 0 0 25 0 1 0 541539828 100962304 15236 4294967295 134512640 134672761 3221224624 3219072128 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24649 15236 603 41 0 24608 0
vsize: 98596
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 36195 0 0 0 45911 95 0 0 25 0 1 0 541539828 101265408 15361 4294967295 134512640 134672761 3221224624 3220181504 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24723 15361 603 41 0 24682 0
vsize: 98892
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 36238 0 0 0 46911 95 0 0 25 0 1 0 541539828 101400576 15404 4294967295 134512640 134672761 3221224624 3220714496 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24756 15404 603 41 0 24715 0
vsize: 99024
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 36270 0 0 0 47911 95 0 0 25 0 1 0 541539828 101535744 15436 4294967295 134512640 134672761 3221224624 3221098400 134594231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15436 603 41 0 24748 0
vsize: 99156
[startup+490.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 36281 0 0 0 48911 95 0 0 25 0 1 0 541539828 101535744 15447 4294967295 134512640 134672761 3221224624 3219752016 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+500.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 36281 0 0 0 49911 95 0 0 25 0 1 0 541539828 101535744 15447 4294967295 134512640 134672761 3221224624 3219369264 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+510.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 36281 0 0 0 50911 95 0 0 25 0 1 0 541539828 101535744 15447 4294967295 134512640 134672761 3221224624 3218802288 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+520.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 36515 0 0 0 51910 96 0 0 25 0 1 0 541539828 102006784 15598 4294967295 134512640 134672761 3221224624 3218660384 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24904 15598 603 41 0 24863 0
vsize: 99616
[startup+530.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 36689 0 0 0 52910 97 0 0 25 0 1 0 541539828 102547456 15772 4294967295 134512640 134672761 3221224624 3220526336 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25036 15772 603 41 0 24995 0
vsize: 100144
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 36918 0 0 0 53910 97 0 0 25 0 1 0 541539828 102436864 15799 4294967295 134512640 134672761 3221224624 3218210336 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25009 15799 603 41 0 24968 0
vsize: 100036
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 37150 0 0 0 54910 98 0 0 25 0 1 0 541539828 103047168 15989 4294967295 134512640 134672761 3221224624 3219852608 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25158 15989 603 41 0 25117 0
vsize: 100632
[startup+560.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 37200 0 0 0 55910 98 0 0 25 0 1 0 541539828 103182336 16039 4294967295 134512640 134672761 3221224624 3220458560 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25191 16039 603 41 0 25150 0
vsize: 100764
[startup+570.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 37233 0 0 0 56910 98 0 0 25 0 1 0 541539828 103317504 16072 4294967295 134512640 134672761 3221224624 3220868672 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16072 603 41 0 25183 0
vsize: 100896
[startup+580.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 37260 0 0 0 57910 98 0 0 25 0 1 0 541539828 103317504 16099 4294967295 134512640 134672761 3221224624 3221197664 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16099 603 41 0 25183 0
vsize: 100896
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 37262 0 0 0 58910 98 0 0 25 0 1 0 541539828 103317504 16101 4294967295 134512640 134672761 3221224624 3219551856 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 37262 0 0 0 59910 98 0 0 25 0 1 0 541539828 103317504 16101 4294967295 134512640 134672761 3221224624 3219182352 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+610.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 37262 0 0 0 60911 98 0 0 25 0 1 0 541539828 103317504 16101 4294967295 134512640 134672761 3221224624 3218633904 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 37262 0 0 0 61911 98 0 0 25 0 1 0 541539828 103317504 16101 4294967295 134512640 134672761 3221224624 3217686960 134594077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+630.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 37642 0 0 0 62910 99 0 0 25 0 1 0 541539828 104194048 16398 4294967295 134512640 134672761 3221224624 3220289312 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25438 16398 603 41 0 25397 0
vsize: 101752
[startup+640.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 37712 0 0 0 63910 99 0 0 25 0 1 0 541539828 104464384 16468 4294967295 134512640 134672761 3221224624 3221080544 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25504 16468 603 41 0 25463 0
vsize: 102016
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 37962 0 0 0 64909 99 0 0 25 0 1 0 541539828 104411136 16518 4294967295 134512640 134672761 3221224624 3219690752 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25491 16518 603 41 0 25450 0
vsize: 101964
[startup+660.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 38107 0 0 0 65909 100 0 0 25 0 1 0 541539828 104714240 16621 4294967295 134512640 134672761 3221224624 3220436960 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25565 16621 603 41 0 25524 0
vsize: 102260
[startup+670.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 38143 0 0 0 66909 100 0 0 25 0 1 0 541539828 104849408 16657 4294967295 134512640 134672761 3221224624 3220884992 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16657 603 41 0 25557 0
vsize: 102392
[startup+680.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 38171 0 0 0 67909 100 0 0 25 0 1 0 541539828 104849408 16685 4294967295 134512640 134672761 3221224624 3220810128 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+690.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 38171 0 0 0 68910 100 0 0 25 0 1 0 541539828 104849408 16685 4294967295 134512640 134672761 3221224624 3219602640 134594084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+700.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 38171 0 0 0 69910 100 0 0 25 0 1 0 541539828 104849408 16685 4294967295 134512640 134672761 3221224624 3219169296 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+710.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 38171 0 0 0 70910 100 0 0 25 0 1 0 541539828 104849408 16685 4294967295 134512640 134672761 3221224624 3218269392 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+720.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 38499 0 0 0 71909 101 0 0 25 0 1 0 541539828 105590784 16930 4294967295 134512640 134672761 3221224624 3219790880 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25779 16930 603 41 0 25738 0
vsize: 103116
[startup+730.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 38587 0 0 0 72909 101 0 0 25 0 1 0 541539828 105861120 17018 4294967295 134512640 134672761 3221224624 3220858496 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25845 17018 603 41 0 25804 0
vsize: 103380
[startup+740.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 38819 0 0 0 73909 102 0 0 25 0 1 0 541539828 105762816 17050 4294967295 134512640 134672761 3221224624 3219308480 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25821 17050 603 41 0 25780 0
vsize: 103284
[startup+750.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 38980 0 0 0 74908 102 0 0 25 0 1 0 541539828 106065920 17169 4294967295 134512640 134672761 3221224624 3220269632 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25895 17169 603 41 0 25854 0
vsize: 103580
[startup+760.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39021 0 0 0 75908 102 0 0 25 0 1 0 541539828 106201088 17210 4294967295 134512640 134672761 3221224624 3220771232 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25928 17210 603 41 0 25887 0
vsize: 103712
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39053 0 0 0 76909 102 0 0 25 0 1 0 541539828 106336256 17242 4294967295 134512640 134672761 3221224624 3221142272 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17242 603 41 0 25920 0
vsize: 103844
[startup+780.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39058 0 0 0 77909 102 0 0 25 0 1 0 541539828 106336256 17247 4294967295 134512640 134672761 3221224624 3219704688 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+790.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39058 0 0 0 78909 102 0 0 25 0 1 0 541539828 106336256 17247 4294967295 134512640 134672761 3221224624 3219308400 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+800.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39058 0 0 0 79909 103 0 0 25 0 1 0 541539828 106336256 17247 4294967295 134512640 134672761 3221224624 3218593968 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+810.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39334 0 0 0 80909 103 0 0 25 0 1 0 541539828 106942464 17440 4294967295 134512640 134672761 3221224624 3219157184 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26109 17441 603 41 0 26068 0
vsize: 104436
[startup+820.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39456 0 0 0 81908 103 0 0 25 0 1 0 541539828 107212800 17562 4294967295 134512640 134672761 3221224624 3220631456 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26175 17562 603 41 0 26134 0
vsize: 104700
[startup+830.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39644 0 0 0 82908 104 0 0 25 0 1 0 541539828 119586816 17550 4294967295 134512640 134672761 3221224624 3218821432 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29196 17550 603 41 0 29155 0
vsize: 116784
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39854 0 0 0 83907 105 0 0 25 0 1 0 541539828 120061952 17718 4294967295 134512640 134672761 3221224624 3220106624 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29312 17718 603 41 0 29271 0
vsize: 117248
[startup+850.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39901 0 0 0 84907 105 0 0 25 0 1 0 541539828 120197120 17765 4294967295 134512640 134672761 3221224624 3220668896 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29345 17765 603 41 0 29304 0
vsize: 117380
[startup+860.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39933 0 0 0 85907 105 0 0 25 0 1 0 541539828 120332288 17797 4294967295 134512640 134672761 3221224624 3221063840 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17797 603 41 0 29337 0
vsize: 117512
[startup+870.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39945 0 0 0 86907 105 0 0 25 0 1 0 541539828 120332288 17809 4294967295 134512640 134672761 3221224624 3219790800 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+880.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39945 0 0 0 87908 105 0 0 25 0 1 0 541539828 120332288 17809 4294967295 134512640 134672761 3221224624 3219417840 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+890.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39945 0 0 0 88908 105 0 0 25 0 1 0 541539828 120332288 17809 4294967295 134512640 134672761 3221224624 3218882832 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+900.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 39945 0 0 0 89908 105 0 0 25 0 1 0 541539828 120332288 17809 4294967295 134512640 134672761 3221224624 3217823664 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+910.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 40327 0 0 0 90907 106 0 0 25 0 1 0 541539828 121208832 18108 4294967295 134512640 134672761 3221224624 3220453184 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29592 18108 603 41 0 29551 0
vsize: 118368
[startup+920.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 40590 0 0 0 91907 107 0 0 25 0 1 0 541539828 121290752 18164 4294967295 134512640 134672761 3221224624 3217501760 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29612 18164 603 41 0 29571 0
vsize: 118448
[startup+930.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 40854 0 0 0 92906 108 0 0 25 0 1 0 541539828 122036224 18386 4294967295 134512640 134672761 3221224624 3219332672 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29794 18386 603 41 0 29753 0
vsize: 119176
[startup+940.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 40905 0 0 0 93906 108 0 0 25 0 1 0 541539828 122171392 18437 4294967295 134512640 134672761 3221224624 3219952448 134594261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29827 18437 603 41 0 29786 0
vsize: 119308
[startup+950.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 40938 0 0 0 94906 108 0 0 25 0 1 0 541539828 122171392 18470 4294967295 134512640 134672761 3221224624 3220366976 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29827 18470 603 41 0 29786 0
vsize: 119308
[startup+960.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 40966 0 0 0 95906 108 0 0 25 0 1 0 541539828 122306560 18498 4294967295 134512640 134672761 3221224624 3220698464 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18498 603 41 0 29819 0
vsize: 119440
[startup+970.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 40989 0 0 0 96906 108 0 0 25 0 1 0 541539828 122306560 18521 4294967295 134512640 134672761 3221224624 3220983968 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18521 603 41 0 29819 0
vsize: 119440
[startup+980.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 41009 0 0 0 97906 108 0 0 25 0 1 0 541539828 122441728 18541 4294967295 134512640 134672761 3221224624 3220577520 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+990.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 41009 0 0 0 98907 108 0 0 25 0 1 0 541539828 122441728 18541 4294967295 134512640 134672761 3221224624 3219139248 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 41009 0 0 0 99907 108 0 0 25 0 1 0 541539828 122441728 18541 4294967295 134512640 134672761 3221224624 3218869584 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 41009 0 0 0 100907 108 0 0 25 0 1 0 541539828 122441728 18541 4294967295 134512640 134672761 3221224624 3218553744 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 41009 0 0 0 101907 108 0 0 25 0 1 0 541539828 122441728 18541 4294967295 134512640 134672761 3221224624 3218104944 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 41009 0 0 0 102907 108 0 0 25 0 1 0 541539828 122441728 18541 4294967295 134512640 134672761 3221224624 3217464720 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 41345 0 0 0 103907 109 0 0 25 0 1 0 541539828 123183104 18794 4294967295 134512640 134672761 3221224624 3219273920 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 18794 603 41 0 30033 0
vsize: 120296
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 41438 0 0 0 104907 109 0 0 25 0 1 0 541539828 123453440 18887 4294967295 134512640 134672761 3221224624 3220375808 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30140 18887 603 41 0 30099 0
vsize: 120560
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 41517 0 0 0 105907 110 0 0 25 0 1 0 541539828 123723776 18966 4294967295 134512640 134672761 3221224624 3221015648 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30206 18966 603 41 0 30165 0
vsize: 120824
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 0 42065 0 0 0 106906 111 0 0 25 0 1 0 541539828 124088320 19223 4294967295 134512640 134672761 3221224624 3220720256 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30295 19223 603 41 0 30254 0
vsize: 121180
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 1028 68815 0 0 0 107835 182 0 0 25 0 1 0 541539828 0 0 4294967295 0 0 0 0 0 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.92 1/53 20475
Raw data (stat): 20475 (minisat+) R 20474 27222 27221 0 -1 1028 68815 0 0 0 107835 182 0 0 25 0 1 0 541539828 0 0 4294967295 0 0 0 0 0 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1080.05
CPU time (s): 1080.21
CPU user time (s): 1078.35
CPU system time (s): 1.86472
CPU usage (%): 100.015
Max. virtual memory (Kb): 121180
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####