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/miplib2003/normalized-mps-v2-13-7-nw04.opb
MD5SUM	5a18ff1f45b144b201f1f80233dc9b6b
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	1195.04
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 18550

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 15:34:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17862 boxname=wulflinc7 idbench=1374 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5a18ff1f45b144b201f1f80233dc9b6b  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-nw04.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-nw04.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-nw04.opb
IDLAUNCH: 17862
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        436304 kB
Buffers:         26816 kB
Cached:         548664 kB
SwapCached:          4 kB
Active:         208984 kB
Inactive:       369372 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        436052 kB
SwapTotal:     2097136 kB
SwapFree:      2097128 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            14344 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 15:51:43 (client local time) WITH STATUS 0 IN 1028.22 SECONDS
stats: 17862 7 1028.22 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.85 0.94 0.90 2/54 10406
Raw data (stat): 10406 (runsolver) R 10405 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487981660 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0008 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 22973 0 0 0 935 63 0 0 25 0 1 0 487981660 64581632 7176 4294967295 134512640 134672761 3221224560 3220436224 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+20.0059 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 22973 0 0 0 1936 63 0 0 25 0 1 0 487981660 64581632 7176 4294967295 134512640 134672761 3221224560 3220866592 134594234 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.005 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 23318 0 0 0 2935 65 0 0 25 0 1 0 487981660 65994752 7521 4294967295 134512640 134672761 3221224560 3220827616 134594229 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.0105 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 23715 0 0 0 3934 66 0 0 25 0 1 0 487981660 69140480 7918 4294967295 134512640 134672761 3221224560 3220434400 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16880 7918 603 41 0 16839 0
vsize: 67520
[startup+50.0112 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 23947 0 0 0 4933 67 0 0 25 0 1 0 487981660 69771264 8150 4294967295 134512640 134672761 3221224560 3220320272 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.0119 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 24693 0 0 0 5932 69 0 0 25 0 1 0 487981660 71118848 8566 4294967295 134512640 134672761 3221224560 3221212672 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17363 8566 603 41 0 17322 0
vsize: 69452
[startup+70.0122 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 24807 0 0 0 6931 69 0 0 25 0 1 0 487981660 71118848 8680 4294967295 134512640 134672761 3221224560 3220092352 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17363 8680 603 41 0 17322 0
vsize: 69452
[startup+80.0122 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 24954 0 0 0 7931 70 0 0 25 0 1 0 487981660 71458816 8827 4294967295 134512640 134672761 3221224560 3220642240 134594261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17446 8827 603 41 0 17405 0
vsize: 69784
[startup+90.0118 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 25087 0 0 0 8930 71 0 0 25 0 1 0 487981660 74571776 8877 4294967295 134512640 134672761 3221224560 3220069328 134594084 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.012 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 25480 0 0 0 9930 71 0 0 25 0 1 0 487981660 75186176 9145 4294967295 134512640 134672761 3221224560 3220811216 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18356 9145 603 41 0 18315 0
vsize: 73424
[startup+110.013 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 26031 0 0 0 10928 73 0 0 25 0 1 0 487981660 76677120 9571 4294967295 134512640 134672761 3221224560 3219434848 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18720 9571 603 41 0 18679 0
vsize: 74880
[startup+120.014 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 27559 0 0 0 11924 77 0 0 25 0 1 0 487981660 79851520 10398 4294967295 134512640 134672761 3221224560 3220720288 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19495 10398 603 41 0 19454 0
vsize: 77980
[startup+130.016 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 27601 0 0 0 12924 78 0 0 25 0 1 0 487981660 79986688 10440 4294967295 134512640 134672761 3221224560 3220452272 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19528 10440 603 41 0 19487 0
vsize: 78112
[startup+140.017 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 27601 0 0 0 13924 78 0 0 25 0 1 0 487981660 79986688 10440 4294967295 134512640 134672761 3221224560 3219630032 134594131 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.018 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 27968 0 0 0 14924 79 0 0 25 0 1 0 487981660 80863232 10724 4294967295 134512640 134672761 3221224560 3220440160 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19742 10724 603 41 0 19701 0
vsize: 78968
[startup+160.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 28221 0 0 0 15922 80 0 0 25 0 1 0 487981660 81010688 10812 4294967295 134512640 134672761 3221224560 3220149184 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19778 10812 603 41 0 19737 0
vsize: 79112
[startup+170.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 28385 0 0 0 16922 81 0 0 25 0 1 0 487981660 81313792 10934 4294967295 134512640 134672761 3221224560 3221180128 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19852 10934 603 41 0 19811 0
vsize: 79408
[startup+180.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 28389 0 0 0 17922 81 0 0 25 0 1 0 487981660 81313792 10938 4294967295 134512640 134672761 3221224560 3219929936 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.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 28737 0 0 0 18921 82 0 0 25 0 1 0 487981660 82190336 11203 4294967295 134512640 134672761 3221224560 3221033632 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20066 11203 603 41 0 20025 0
vsize: 80264
[startup+200.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 28959 0 0 0 19920 83 0 0 25 0 1 0 487981660 82173952 11260 4294967295 134512640 134672761 3221224560 3221115232 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20062 11260 603 41 0 20021 0
vsize: 80248
[startup+210.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 29050 0 0 0 20920 83 0 0 25 0 1 0 487981660 82341888 11309 4294967295 134512640 134672761 3221224560 3219403280 134594131 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.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 29545 0 0 0 21919 84 0 0 25 0 1 0 487981660 82927616 11556 4294967295 134512640 134672761 3221224560 3220103872 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20246 11556 603 41 0 20205 0
vsize: 80984
[startup+230.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 29710 0 0 0 22919 85 0 0 25 0 1 0 487981660 83230720 11679 4294967295 134512640 134672761 3221224560 3221099392 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20320 11679 603 41 0 20279 0
vsize: 81280
[startup+240.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 29721 0 0 0 23919 85 0 0 25 0 1 0 487981660 83365888 11690 4294967295 134512640 134672761 3221224560 3220098416 134594086 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.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 30031 0 0 0 24918 86 0 0 25 0 1 0 487981660 83972096 11917 4294967295 134512640 134672761 3221224560 3220481344 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20501 11917 603 41 0 20460 0
vsize: 82004
[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 30266 0 0 0 25917 87 0 0 25 0 1 0 487981660 90292224 11987 4294967295 134512640 134672761 3221224560 3220221568 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22044 11987 603 41 0 22003 0
vsize: 88176
[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 30422 0 0 0 26917 87 0 0 25 0 1 0 487981660 90595328 12101 4294967295 134512640 134672761 3221224560 3221120320 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22118 12101 603 41 0 22077 0
vsize: 88472
[startup+280.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 30431 0 0 0 27917 88 0 0 25 0 1 0 487981660 90730496 12110 4294967295 134512640 134672761 3221224560 3220077584 134594101 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.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 30727 0 0 0 28916 89 0 0 25 0 1 0 487981660 91336704 12323 4294967295 134512640 134672761 3221224560 3220241728 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22299 12323 603 41 0 22258 0
vsize: 89196
[startup+300.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 30964 0 0 0 29915 90 0 0 25 0 1 0 487981660 91373568 12395 4294967295 134512640 134672761 3221224560 3219972160 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22308 12395 603 41 0 22267 0
vsize: 89232
[startup+310.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 31130 0 0 0 30915 90 0 0 25 0 1 0 487981660 91676672 12519 4294967295 134512640 134672761 3221224560 3220998592 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22382 12519 603 41 0 22341 0
vsize: 89528
[startup+320.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 31148 0 0 0 31914 91 0 0 25 0 1 0 487981660 91811840 12537 4294967295 134512640 134672761 3221224560 3220250192 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.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 31197 0 0 0 32914 91 0 0 25 0 1 0 487981660 91947008 12586 4294967295 134512640 134672761 3221224560 3219210496 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22448 12586 603 41 0 22407 0
vsize: 89792
[startup+340.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 31605 0 0 0 33914 92 0 0 25 0 1 0 487981660 92188672 12746 4294967295 134512640 134672761 3221224560 3219211936 134594220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22507 12746 603 41 0 22466 0
vsize: 90028
[startup+350.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 31833 0 0 0 34913 92 0 0 25 0 1 0 487981660 92798976 12932 4294967295 134512640 134672761 3221224560 3220713184 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22656 12932 603 41 0 22615 0
vsize: 90624
[startup+360.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 31874 0 0 0 35913 93 0 0 25 0 1 0 487981660 92934144 12973 4294967295 134512640 134672761 3221224560 3220474544 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22689 12973 603 41 0 22648 0
vsize: 90756
[startup+370.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 31874 0 0 0 36913 93 0 0 25 0 1 0 487981660 92934144 12973 4294967295 134512640 134672761 3221224560 3219621968 134594103 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.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 34836 0 0 0 37906 100 0 0 25 0 1 0 487981660 99078144 14534 4294967295 134512640 134672761 3221224560 3220476256 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24189 14534 603 41 0 24148 0
vsize: 96756
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 35098 0 0 0 38905 101 0 0 25 0 1 0 487981660 99139584 14631 4294967295 134512640 134672761 3221224560 3219862720 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24204 14631 603 41 0 24163 0
vsize: 96816
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 35262 0 0 0 39904 102 0 0 25 0 1 0 487981660 99577856 14753 4294967295 134512640 134672761 3221224560 3220836352 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14753 603 41 0 24270 0
vsize: 97244
[startup+410.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 35294 0 0 0 40904 102 0 0 25 0 1 0 487981660 99577856 14785 4294967295 134512640 134672761 3221224560 3220317200 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14785 603 41 0 24270 0
vsize: 97244
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 35294 0 0 0 41904 103 0 0 25 0 1 0 487981660 99577856 14785 4294967295 134512640 134672761 3221224560 3219461072 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+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 35623 0 0 0 42903 103 0 0 25 0 1 0 487981660 100319232 15031 4294967295 134512640 134672761 3221224560 3220417312 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24492 15031 603 41 0 24451 0
vsize: 97968
[startup+440.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 36029 0 0 0 43902 105 0 0 25 0 1 0 487981660 100962304 15237 4294967295 134512640 134672761 3221224560 3219098464 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24649 15237 603 41 0 24608 0
vsize: 98596
[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 36193 0 0 0 44902 105 0 0 25 0 1 0 487981660 101265408 15359 4294967295 134512640 134672761 3221224560 3220165696 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24723 15359 603 41 0 24682 0
vsize: 98892
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 36240 0 0 0 45902 105 0 0 25 0 1 0 487981660 101400576 15406 4294967295 134512640 134672761 3221224560 3220733344 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24756 15406 603 41 0 24715 0
vsize: 99024
[startup+470.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 36275 0 0 0 46902 106 0 0 25 0 1 0 487981660 101535744 15441 4294967295 134512640 134672761 3221224560 3221157088 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15441 603 41 0 24748 0
vsize: 99156
[startup+480.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 36281 0 0 0 47901 106 0 0 25 0 1 0 487981660 101535744 15447 4294967295 134512640 134672761 3221224560 3219647984 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 36281 0 0 0 48901 106 0 0 25 0 1 0 487981660 101535744 15447 4294967295 134512640 134672761 3221224560 3219175472 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.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 36281 0 0 0 49901 106 0 0 25 0 1 0 487981660 101535744 15447 4294967295 134512640 134672761 3221224560 3218196656 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.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 36633 0 0 0 50901 107 0 0 25 0 1 0 487981660 102412288 15716 4294967295 134512640 134672761 3221224560 3220075552 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25003 15716 603 41 0 24962 0
vsize: 100012
[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 36759 0 0 0 51900 107 0 0 25 0 1 0 487981660 102682624 15842 4294967295 134512640 134672761 3221224560 3221095648 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25069 15842 603 41 0 25028 0
vsize: 100276
[startup+530.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 37047 0 0 0 52899 108 0 0 25 0 1 0 487981660 102879232 15928 4294967295 134512640 134672761 3221224560 3219617632 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25117 15928 603 41 0 25076 0
vsize: 100468
[startup+540.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 37190 0 0 0 53899 109 0 0 25 0 1 0 487981660 103182336 16029 4294967295 134512640 134672761 3221224560 3220336576 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25191 16029 603 41 0 25150 0
vsize: 100764
[startup+550.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 37230 0 0 0 54899 109 0 0 25 0 1 0 487981660 103317504 16069 4294967295 134512640 134672761 3221224560 3220826272 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16069 603 41 0 25183 0
vsize: 100896
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 37260 0 0 0 55899 110 0 0 25 0 1 0 487981660 103317504 16099 4294967295 134512640 134672761 3221224560 3221194528 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16099 603 41 0 25183 0
vsize: 100896
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 37262 0 0 0 56899 110 0 0 25 0 1 0 487981660 103317504 16101 4294967295 134512640 134672761 3221224560 3219523280 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+580.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 37262 0 0 0 57899 110 0 0 25 0 1 0 487981660 103317504 16101 4294967295 134512640 134672761 3221224560 3219102704 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+590.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 37262 0 0 0 58899 110 0 0 25 0 1 0 487981660 103317504 16101 4294967295 134512640 134672761 3221224560 3218241776 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.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 37577 0 0 0 59898 111 0 0 25 0 1 0 487981660 104058880 16333 4294967295 134512640 134672761 3221224560 3219497632 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25405 16333 603 41 0 25364 0
vsize: 101620
[startup+610.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 37683 0 0 0 60898 112 0 0 25 0 1 0 487981660 104329216 16439 4294967295 134512640 134672761 3221224560 3220789696 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25471 16439 603 41 0 25430 0
vsize: 101884
[startup+620.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 37923 0 0 0 61897 113 0 0 25 0 1 0 487981660 104275968 16479 4294967295 134512640 134672761 3221224560 3219218848 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25458 16479 603 41 0 25417 0
vsize: 101832
[startup+630.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 38088 0 0 0 62896 113 0 0 25 0 1 0 487981660 104714240 16602 4294967295 134512640 134672761 3221224560 3220209568 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25565 16602 603 41 0 25524 0
vsize: 102260
[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 38134 0 0 0 63896 114 0 0 25 0 1 0 487981660 104714240 16648 4294967295 134512640 134672761 3221224560 3220762240 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25565 16648 603 41 0 25524 0
vsize: 102260
[startup+650.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 38167 0 0 0 64896 114 0 0 25 0 1 0 487981660 104849408 16681 4294967295 134512640 134672761 3221224560 3221176480 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16681 603 41 0 25557 0
vsize: 102392
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 38171 0 0 0 65896 114 0 0 25 0 1 0 487981660 104849408 16685 4294967295 134512640 134672761 3221224560 3219622448 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 38171 0 0 0 66896 114 0 0 25 0 1 0 487981660 104849408 16685 4294967295 134512640 134672761 3221224560 3219143792 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+680.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 38171 0 0 0 67895 115 0 0 25 0 1 0 487981660 104849408 16685 4294967295 134512640 134672761 3221224560 3218150864 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.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 38530 0 0 0 68895 116 0 0 25 0 1 0 487981660 105725952 16961 4294967295 134512640 134672761 3221224560 3220160800 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25812 16961 603 41 0 25771 0
vsize: 103248
[startup+700.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 38611 0 0 0 69894 117 0 0 25 0 1 0 487981660 105861120 17042 4294967295 134512640 134672761 3221224560 3221149984 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25845 17042 603 41 0 25804 0
vsize: 103380
[startup+710.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 38860 0 0 0 70893 118 0 0 25 0 1 0 487981660 105897984 17091 4294967295 134512640 134672761 3221224560 3219817120 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25854 17091 603 41 0 25813 0
vsize: 103416
[startup+720.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39000 0 0 0 71893 118 0 0 25 0 1 0 487981660 106201088 17189 4294967295 134512640 134672761 3221224560 3220505536 134594220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25928 17189 603 41 0 25887 0
vsize: 103712
[startup+730.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39039 0 0 0 72893 118 0 0 25 0 1 0 487981660 106336256 17228 4294967295 134512640 134672761 3221224560 3220985824 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17228 603 41 0 25920 0
vsize: 103844
[startup+740.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39058 0 0 0 73892 119 0 0 25 0 1 0 487981660 106336256 17247 4294967295 134512640 134672761 3221224560 3219812048 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+750.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39058 0 0 0 74893 119 0 0 25 0 1 0 487981660 106336256 17247 4294967295 134512640 134672761 3221224560 3219402416 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+760.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39058 0 0 0 75892 119 0 0 25 0 1 0 487981660 106336256 17247 4294967295 134512640 134672761 3221224560 3218817008 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+770.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39331 0 0 0 76891 120 0 0 25 0 1 0 487981660 106942464 17437 4294967295 134512640 134672761 3221224560 3219107872 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26109 17437 603 41 0 26068 0
vsize: 104436
[startup+780.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39465 0 0 0 77891 121 0 0 25 0 1 0 487981660 107212800 17571 4294967295 134512640 134672761 3221224560 3220752064 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26175 17571 603 41 0 26134 0
vsize: 104700
[startup+790.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39701 0 0 0 78891 122 0 0 25 0 1 0 487981660 119758848 17607 4294967295 134512640 134672761 3221224560 3219252064 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29238 17607 603 41 0 29197 0
vsize: 116952
[startup+800.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39864 0 0 0 79890 122 0 0 25 0 1 0 487981660 120197120 17728 4294967295 134512640 134672761 3221224560 3220231552 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29345 17728 603 41 0 29304 0
vsize: 117380
[startup+810.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39910 0 0 0 80890 122 0 0 25 0 1 0 487981660 120197120 17774 4294967295 134512640 134672761 3221224560 3220782112 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29345 17774 603 41 0 29304 0
vsize: 117380
[startup+820.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39944 0 0 0 81890 122 0 0 25 0 1 0 487981660 120332288 17808 4294967295 134512640 134672761 3221224560 3221195104 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17808 603 41 0 29337 0
vsize: 117512
[startup+830.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39945 0 0 0 82891 122 0 0 25 0 1 0 487981660 120332288 17809 4294967295 134512640 134672761 3221224560 3219609296 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+840.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39945 0 0 0 83891 123 0 0 25 0 1 0 487981660 120332288 17809 4294967295 134512640 134672761 3221224560 3219115088 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+850.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 39945 0 0 0 84891 123 0 0 25 0 1 0 487981660 120332288 17809 4294967295 134512640 134672761 3221224560 3218087312 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+860.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 40314 0 0 0 85890 124 0 0 25 0 1 0 487981660 121208832 18095 4294967295 134512640 134672761 3221224560 3220288288 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29592 18095 603 41 0 29551 0
vsize: 118368
[startup+870.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 40432 0 0 0 86890 125 0 0 25 0 1 0 487981660 120668160 18006 4294967295 134512640 134672761 3221224560 3220170992 134594069 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29460 18006 603 41 0 29419 0
vsize: 117840
[startup+880.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 40851 0 0 0 87889 126 0 0 25 0 1 0 487981660 122036224 18383 4294967295 134512640 134672761 3221224560 3219292768 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29794 18383 603 41 0 29753 0
vsize: 119176
[startup+890.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 40905 0 0 0 88890 126 0 0 25 0 1 0 487981660 122171392 18437 4294967295 134512640 134672761 3221224560 3219945568 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29827 18437 603 41 0 29786 0
vsize: 119308
[startup+900.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 40943 0 0 0 89890 127 0 0 25 0 1 0 487981660 122306560 18475 4294967295 134512640 134672761 3221224560 3220411744 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18475 603 41 0 29819 0
vsize: 119440
[startup+910.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 40972 0 0 0 90890 127 0 0 25 0 1 0 487981660 122306560 18504 4294967295 134512640 134672761 3221224560 3220764832 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18504 603 41 0 29819 0
vsize: 119440
[startup+920.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 40996 0 0 0 91891 127 0 0 25 0 1 0 487981660 122441728 18528 4294967295 134512640 134672761 3221224560 3221060224 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18528 603 41 0 29852 0
vsize: 119572
[startup+930.088 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 41009 0 0 0 92891 127 0 0 25 0 1 0 487981660 122441728 18541 4294967295 134512640 134672761 3221224560 3219839408 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+940.105 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 41009 0 0 0 93893 127 0 0 25 0 1 0 487981660 122441728 18541 4294967295 134512640 134672761 3221224560 3219084368 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+950.113 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 41009 0 0 0 94893 128 0 0 25 0 1 0 487981660 122441728 18541 4294967295 134512640 134672761 3221224560 3218789264 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+960.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 41009 0 0 0 95893 128 0 0 25 0 1 0 487981660 122441728 18541 4294967295 134512640 134672761 3221224560 3218443568 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+970.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 41009 0 0 0 96893 128 0 0 25 0 1 0 487981660 122441728 18541 4294967295 134512640 134672761 3221224560 3217897424 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+980.118 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 41009 0 0 0 97893 129 0 0 25 0 1 0 487981660 122441728 18541 4294967295 134512640 134672761 3221224560 3217329296 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.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 41380 0 0 0 98893 130 0 0 25 0 1 0 487981660 123318272 18829 4294967295 134512640 134672761 3221224560 3219703744 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30107 18829 603 41 0 30066 0
vsize: 120428
[startup+1000.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 41468 0 0 0 99893 130 0 0 25 0 1 0 487981660 123588608 18917 4294967295 134512640 134672761 3221224560 3220622080 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30173 18917 603 41 0 30132 0
vsize: 120692
[startup+1010.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 41540 0 0 0 100893 131 0 0 25 0 1 0 487981660 123723776 18989 4294967295 134512640 134672761 3221224560 3221194624 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30206 18989 603 41 0 30165 0
vsize: 120824
[startup+1020.23 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 42277 0 0 0 101901 133 0 0 25 0 1 0 487981660 124661760 19393 4294967295 134512640 134672761 3221224560 3221114368 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30435 19393 603 41 0 30394 0
vsize: 121740
[startup+1028.18 s]
Raw data (loadavg): 1.07 0.99 0.91 1/53 10406
Raw data (stat): 10406 (minisat+) R 10405 22932 22931 0 -1 0 42277 0 0 0 101901 133 0 0 25 0 1 0 487981660 124661760 19393 4294967295 134512640 134672761 3221224560 3221114368 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30435 19393 603 41 0 30394 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1028.16
CPU time (s): 1028.22
CPU user time (s): 1026.01
CPU system time (s): 2.20666
CPU usage (%): 100.006
Max. virtual memory (Kb): 121740
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####