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 18553

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 15:35:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17854 boxname=wulflinc20 idbench=1374 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  5a18ff1f45b144b201f1f80233dc9b6b  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-nw04.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-nw04.opb
IDLAUNCH: 17854
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        196000 kB
Buffers:         30308 kB
Cached:         783476 kB
SwapCached:        516 kB
Active:          78268 kB
Inactive:       737468 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        195748 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            17352 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 15:53:30 (client local time) WITH STATUS 0 IN 1102.7 SECONDS
stats: 17854 7 1102.7 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.93 0.95 0.93 2/54 8915
Raw data (stat): 8915 (runsolver) R 8914 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546200626 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99999 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 22973 0 0 0 936 62 0 0 25 0 1 0 546200626 64581632 7176 4294967295 134512640 134672761 3221224624 3220474304 134594214 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.0012 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 22973 0 0 0 1935 62 0 0 25 0 1 0 546200626 64581632 7176 4294967295 134512640 134672761 3221224624 3220807520 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15767 7176 603 41 0 15726 0
vsize: 63068
[startup+30.0006 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 23318 0 0 0 2935 63 0 0 25 0 1 0 546200626 65994752 7521 4294967295 134512640 134672761 3221224624 3220629536 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16112 7521 603 41 0 16071 0
vsize: 64448
[startup+40.0011 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 23706 0 0 0 3934 64 0 0 25 0 1 0 546200626 69140480 7909 4294967295 134512640 134672761 3221224624 3220431984 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16880 7909 603 41 0 16839 0
vsize: 67520
[startup+50.0011 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 23947 0 0 0 4934 64 0 0 25 0 1 0 546200626 69771264 8150 4294967295 134512640 134672761 3221224624 3220368240 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17034 8150 603 41 0 16993 0
vsize: 68136
[startup+60.0008 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 24688 0 0 0 5932 66 0 0 25 0 1 0 546200626 71118848 8561 4294967295 134512640 134672761 3221224624 3221035328 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8561 603 41 0 17322 0
vsize: 69452
[startup+70.0012 s]
Raw data (loadavg): 1.06 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 24788 0 0 0 6932 66 0 0 25 0 1 0 546200626 71118848 8661 4294967295 134512640 134672761 3221224624 3221014016 134594223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8661 603 41 0 17322 0
vsize: 69452
[startup+80.0012 s]
Raw data (loadavg): 1.05 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 24854 0 0 0 7932 67 0 0 25 0 1 0 546200626 71118848 8727 4294967295 134512640 134672761 3221224624 3220111616 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8727 603 41 0 17322 0
vsize: 69452
[startup+90.0073 s]
Raw data (loadavg): 1.04 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 25087 0 0 0 8932 67 0 0 25 0 1 0 546200626 74571776 8877 4294967295 134512640 134672761 3221224624 3220299408 134594124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18206 8877 603 41 0 18165 0
vsize: 72824
[startup+100.007 s]
Raw data (loadavg): 1.03 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 25474 0 0 0 9931 69 0 0 25 0 1 0 546200626 75186176 9139 4294967295 134512640 134672761 3221224624 3221136128 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18356 9139 603 41 0 18315 0
vsize: 73424
[startup+110.007 s]
Raw data (loadavg): 1.03 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 25985 0 0 0 10930 70 0 0 25 0 1 0 546200626 76541952 9525 4294967295 134512640 134672761 3221224624 3218996864 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18687 9525 603 41 0 18646 0
vsize: 74748
[startup+120.008 s]
Raw data (loadavg): 1.02 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 27553 0 0 0 11927 73 0 0 25 0 1 0 546200626 79851520 10392 4294967295 134512640 134672761 3221224624 3220640864 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19495 10392 603 41 0 19454 0
vsize: 77980
[startup+130.008 s]
Raw data (loadavg): 1.02 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 27601 0 0 0 12927 73 0 0 25 0 1 0 546200626 79986688 10440 4294967295 134512640 134672761 3221224624 3220549392 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19528 10440 603 41 0 19487 0
vsize: 78112
[startup+140.009 s]
Raw data (loadavg): 1.02 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 27601 0 0 0 13927 73 0 0 25 0 1 0 546200626 79986688 10440 4294967295 134512640 134672761 3221224624 3219836688 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19528 10440 603 41 0 19487 0
vsize: 78112
[startup+150.009 s]
Raw data (loadavg): 1.01 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 27905 0 0 0 14927 74 0 0 25 0 1 0 546200626 80728064 10661 4294967295 134512640 134672761 3221224624 3219937856 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19709 10661 603 41 0 19668 0
vsize: 78836
[startup+160.009 s]
Raw data (loadavg): 1.01 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 28141 0 0 0 15926 74 0 0 25 0 1 0 546200626 80703488 10732 4294967295 134512640 134672761 3221224624 3219476864 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19703 10732 603 41 0 19662 0
vsize: 78812
[startup+170.009 s]
Raw data (loadavg): 1.01 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 28369 0 0 0 16926 75 0 0 25 0 1 0 546200626 81313792 10918 4294967295 134512640 134672761 3221224624 3220994048 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19852 10918 603 41 0 19811 0
vsize: 79408
[startup+180.008 s]
Raw data (loadavg): 1.01 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 28389 0 0 0 17926 75 0 0 25 0 1 0 546200626 81313792 10938 4294967295 134512640 134672761 3221224624 3220245552 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19852 10938 603 41 0 19811 0
vsize: 79408
[startup+190.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 28692 0 0 0 18926 76 0 0 25 0 1 0 546200626 82055168 11158 4294967295 134512640 134672761 3221224624 3220485056 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20033 11158 603 41 0 19992 0
vsize: 80132
[startup+200.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 28924 0 0 0 19925 76 0 0 25 0 1 0 546200626 82038784 11225 4294967295 134512640 134672761 3221224624 3220704800 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20029 11225 603 41 0 19988 0
vsize: 80116
[startup+210.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 29050 0 0 0 20925 76 0 0 25 0 1 0 546200626 82341888 11309 4294967295 134512640 134672761 3221224624 3220541424 134594092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20103 11309 603 41 0 20062 0
vsize: 80412
[startup+220.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 29384 0 0 0 21924 78 0 0 25 0 1 0 546200626 83083264 11560 4294967295 134512640 134672761 3221224624 3221198528 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20284 11560 603 41 0 20243 0
vsize: 81136
[startup+230.009 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 29686 0 0 0 22924 78 0 0 25 0 1 0 546200626 83230720 11655 4294967295 134512640 134672761 3221224624 3220803296 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20320 11655 603 41 0 20279 0
vsize: 81280
[startup+240.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 29721 0 0 0 23924 78 0 0 25 0 1 0 546200626 83365888 11690 4294967295 134512640 134672761 3221224624 3220482192 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20353 11690 603 41 0 20312 0
vsize: 81412
[startup+250.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 29721 0 0 0 24924 78 0 0 25 0 1 0 546200626 83365888 11690 4294967295 134512640 134672761 3221224624 3218981424 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20353 11690 603 41 0 20312 0
vsize: 81412
[startup+260.011 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 30085 0 0 0 25923 79 0 0 25 0 1 0 546200626 90398720 11971 4294967295 134512640 134672761 3221224624 3221135360 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22070 11971 603 41 0 22029 0
vsize: 88280
[startup+270.011 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 30387 0 0 0 26923 80 0 0 25 0 1 0 546200626 90595328 12066 4294967295 134512640 134672761 3221224624 3220691648 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22118 12066 603 41 0 22077 0
vsize: 88472
[startup+280.01 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 30431 0 0 0 27923 80 0 0 25 0 1 0 546200626 90730496 12110 4294967295 134512640 134672761 3221224624 3220555248 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22151 12110 603 41 0 22110 0
vsize: 88604
[startup+290.011 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 30431 0 0 0 28923 80 0 0 25 0 1 0 546200626 90730496 12110 4294967295 134512640 134672761 3221224624 3219434736 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22151 12110 603 41 0 22110 0
vsize: 88604
[startup+300.011 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 30770 0 0 0 29922 81 0 0 25 0 1 0 546200626 91471872 12366 4294967295 134512640 134672761 3221224624 3220776128 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22332 12366 603 41 0 22291 0
vsize: 89328
[startup+310.011 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 30991 0 0 0 30922 82 0 0 25 0 1 0 546200626 91373568 12422 4294967295 134512640 134672761 3221224624 3220317056 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22308 12422 603 41 0 22267 0
vsize: 89232
[startup+320.012 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 31141 0 0 0 31922 82 0 0 25 0 1 0 546200626 91811840 12530 4294967295 134512640 134672761 3221224624 3221147168 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22415 12530 603 41 0 22374 0
vsize: 89660
[startup+330.011 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 31148 0 0 0 32922 82 0 0 25 0 1 0 546200626 91811840 12537 4294967295 134512640 134672761 3221224624 3220053936 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22415 12537 603 41 0 22374 0
vsize: 89660
[startup+340.012 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 31262 0 0 0 33922 82 0 0 25 0 1 0 546200626 92082176 12651 4294967295 134512640 134672761 3221224624 3220003232 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22481 12651 603 41 0 22440 0
vsize: 89924
[startup+350.013 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 31613 0 0 0 34921 83 0 0 25 0 1 0 546200626 92188672 12754 4294967295 134512640 134672761 3221224624 3219315584 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22507 12754 603 41 0 22466 0
vsize: 90028
[startup+360.012 s]
Raw data (loadavg): 1.00 0.98 0.93 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 31836 0 0 0 35921 83 0 0 25 0 1 0 546200626 92798976 12935 4294967295 134512640 134672761 3221224624 3220748192 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22656 12935 603 41 0 22615 0
vsize: 90624
[startup+370.013 s]
Raw data (loadavg): 1.08 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 31874 0 0 0 36922 83 0 0 25 0 1 0 546200626 92934144 12973 4294967295 134512640 134672761 3221224624 3220462896 134594092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22689 12973 603 41 0 22648 0
vsize: 90756
[startup+380.013 s]
Raw data (loadavg): 1.07 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 31874 0 0 0 37922 83 0 0 25 0 1 0 546200626 92934144 12973 4294967295 134512640 134672761 3221224624 3219626352 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22689 12973 603 41 0 22648 0
vsize: 90756
[startup+390.014 s]
Raw data (loadavg): 1.06 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 34827 0 0 0 38916 89 0 0 25 0 1 0 546200626 99078144 14525 4294967295 134512640 134672761 3221224624 3220361696 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24189 14525 603 41 0 24148 0
vsize: 96756
[startup+400.013 s]
Raw data (loadavg): 1.05 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 35087 0 0 0 39915 90 0 0 25 0 1 0 546200626 99139584 14620 4294967295 134512640 134672761 3221224624 3219541472 134594220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24204 14620 603 41 0 24163 0
vsize: 96816
[startup+410.013 s]
Raw data (loadavg): 1.04 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 35253 0 0 0 40915 90 0 0 25 0 1 0 546200626 99442688 14744 4294967295 134512640 134672761 3221224624 3220726592 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24278 14744 603 41 0 24237 0
vsize: 97112
[startup+420.014 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 35294 0 0 0 41915 90 0 0 25 0 1 0 546200626 99577856 14785 4294967295 134512640 134672761 3221224624 3220426128 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24311 14785 603 41 0 24270 0
vsize: 97244
[startup+430.013 s]
Raw data (loadavg): 1.03 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 35294 0 0 0 42916 90 0 0 25 0 1 0 546200626 99577856 14785 4294967295 134512640 134672761 3221224624 3219826320 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24311 14785 603 41 0 24270 0
vsize: 97244
[startup+440.014 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 35350 0 0 0 43916 91 0 0 25 0 1 0 546200626 99713024 14841 4294967295 134512640 134672761 3221224624 3219096800 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24344 14841 603 41 0 24303 0
vsize: 97376
[startup+450.015 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 35675 0 0 0 44915 91 0 0 25 0 1 0 546200626 100454400 15083 4294967295 134512640 134672761 3221224624 3221052320 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24525 15083 603 41 0 24484 0
vsize: 98100
[startup+460.014 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 36077 0 0 0 45915 92 0 0 25 0 1 0 546200626 101097472 15285 4294967295 134512640 134672761 3221224624 3219754784 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24682 15285 603 41 0 24641 0
vsize: 98728
[startup+470.015 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 36218 0 0 0 46914 92 0 0 25 0 1 0 546200626 101400576 15384 4294967295 134512640 134672761 3221224624 3220463168 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24756 15384 603 41 0 24715 0
vsize: 99024
[startup+480.015 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 36255 0 0 0 47914 93 0 0 25 0 1 0 546200626 101535744 15421 4294967295 134512640 134672761 3221224624 3220915616 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24789 15421 603 41 0 24748 0
vsize: 99156
[startup+490.016 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 36281 0 0 0 48914 93 0 0 25 0 1 0 546200626 101535744 15447 4294967295 134512640 134672761 3221224624 3220383120 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+500.016 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 36281 0 0 0 49915 93 0 0 25 0 1 0 546200626 101535744 15447 4294967295 134512640 134672761 3221224624 3219582672 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+510.015 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 36281 0 0 0 50915 93 0 0 25 0 1 0 546200626 101535744 15447 4294967295 134512640 134672761 3221224624 3219142992 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+520.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 36281 0 0 0 51915 93 0 0 25 0 1 0 546200626 101535744 15447 4294967295 134512640 134672761 3221224624 3218298384 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+530.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 36591 0 0 0 52914 94 0 0 25 0 1 0 546200626 102277120 15674 4294967295 134512640 134672761 3221224624 3219578720 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24970 15674 603 41 0 24929 0
vsize: 99880
[startup+540.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 36708 0 0 0 53914 94 0 0 25 0 1 0 546200626 102547456 15791 4294967295 134512640 134672761 3221224624 3220686176 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25036 15791 603 41 0 24995 0
vsize: 100144
[startup+550.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 36994 0 0 0 54914 94 0 0 25 0 1 0 546200626 102744064 15875 4294967295 134512640 134672761 3221224624 3218784032 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25084 15875 603 41 0 25043 0
vsize: 100336
[startup+560.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 37160 0 0 0 55914 95 0 0 25 0 1 0 546200626 103047168 15999 4294967295 134512640 134672761 3221224624 3219980192 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25158 15999 603 41 0 25117 0
vsize: 100632
[startup+570.017 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 37206 0 0 0 56914 95 0 0 25 0 1 0 546200626 103182336 16045 4294967295 134512640 134672761 3221224624 3220547168 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25191 16045 603 41 0 25150 0
vsize: 100764
[startup+580.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 37240 0 0 0 57914 95 0 0 25 0 1 0 546200626 103317504 16079 4294967295 134512640 134672761 3221224624 3220947872 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25224 16079 603 41 0 25183 0
vsize: 100896
[startup+590.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 37262 0 0 0 58914 95 0 0 25 0 1 0 546200626 103317504 16101 4294967295 134512640 134672761 3221224624 3220299120 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+600.017 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 37262 0 0 0 59914 95 0 0 25 0 1 0 546200626 103317504 16101 4294967295 134512640 134672761 3221224624 3219483312 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+610.016 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 37262 0 0 0 60914 95 0 0 25 0 1 0 546200626 103317504 16101 4294967295 134512640 134672761 3221224624 3219074640 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+620.017 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 37262 0 0 0 61914 96 0 0 25 0 1 0 546200626 103317504 16101 4294967295 134512640 134672761 3221224624 3218338704 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+630.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 37537 0 0 0 62914 96 0 0 25 0 1 0 546200626 103923712 16293 4294967295 134512640 134672761 3221224624 3219005504 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25372 16293 603 41 0 25331 0
vsize: 101488
[startup+640.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 37653 0 0 0 63914 96 0 0 25 0 1 0 546200626 104329216 16409 4294967295 134512640 134672761 3221224624 3220419200 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 16409 603 41 0 25430 0
vsize: 101884
[startup+650.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 37721 0 0 0 64914 96 0 0 25 0 1 0 546200626 104464384 16477 4294967295 134512640 134672761 3221224624 3221163872 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25504 16477 603 41 0 25463 0
vsize: 102016
[startup+660.018 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 38057 0 0 0 65913 97 0 0 25 0 1 0 546200626 104579072 16571 4294967295 134512640 134672761 3221224624 3219840320 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25532 16571 603 41 0 25491 0
vsize: 102128
[startup+670.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 38113 0 0 0 66913 97 0 0 25 0 1 0 546200626 104714240 16627 4294967295 134512640 134672761 3221224624 3220508960 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25565 16627 603 41 0 25524 0
vsize: 102260
[startup+680.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 38148 0 0 0 67913 97 0 0 25 0 1 0 546200626 104849408 16662 4294967295 134512640 134672761 3221224624 3220947584 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16662 603 41 0 25557 0
vsize: 102392
[startup+690.019 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 38171 0 0 0 68914 97 0 0 25 0 1 0 546200626 104849408 16685 4294967295 134512640 134672761 3221224624 3220178928 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+700.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 38171 0 0 0 69914 98 0 0 25 0 1 0 546200626 104849408 16685 4294967295 134512640 134672761 3221224624 3219547344 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+710.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 38171 0 0 0 70914 98 0 0 25 0 1 0 546200626 104849408 16685 4294967295 134512640 134672761 3221224624 3219098160 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+720.02 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 38171 0 0 0 71914 98 0 0 25 0 1 0 546200626 104849408 16685 4294967295 134512640 134672761 3221224624 3218245296 134594133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+730.021 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 38490 0 0 0 72914 98 0 0 25 0 1 0 546200626 105590784 16921 4294967295 134512640 134672761 3221224624 3219684896 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25779 16921 603 41 0 25738 0
vsize: 103116
[startup+740.022 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 38577 0 0 0 73914 98 0 0 25 0 1 0 546200626 105861120 17008 4294967295 134512640 134672761 3221224624 3220743008 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25845 17008 603 41 0 25804 0
vsize: 103380
[startup+750.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 38807 0 0 0 74915 99 0 0 25 0 1 0 546200626 105762816 17038 4294967295 134512640 134672761 3221224624 3219091520 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25821 17038 603 41 0 25780 0
vsize: 103284
[startup+760.031 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 38972 0 0 0 75915 99 0 0 25 0 1 0 546200626 106065920 17161 4294967295 134512640 134672761 3221224624 3220167584 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25895 17161 603 41 0 25854 0
vsize: 103580
[startup+770.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39017 0 0 0 76915 99 0 0 25 0 1 0 546200626 106201088 17206 4294967295 134512640 134672761 3221224624 3220712864 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25928 17206 603 41 0 25887 0
vsize: 103712
[startup+780.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39050 0 0 0 77915 99 0 0 25 0 1 0 546200626 106336256 17239 4294967295 134512640 134672761 3221224624 3221106176 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 17239 603 41 0 25920 0
vsize: 103844
[startup+790.032 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39058 0 0 0 78915 99 0 0 25 0 1 0 546200626 106336256 17247 4294967295 134512640 134672761 3221224624 3219754800 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+800.044 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39058 0 0 0 79917 99 0 0 25 0 1 0 546200626 106336256 17247 4294967295 134512640 134672761 3221224624 3219371280 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+810.044 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39058 0 0 0 80917 99 0 0 25 0 1 0 546200626 106336256 17247 4294967295 134512640 134672761 3221224624 3218846352 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+820.044 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39058 0 0 0 81917 99 0 0 25 0 1 0 546200626 106336256 17247 4294967295 134512640 134672761 3221224624 3217884912 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+830.044 s]
Raw data (loadavg): 1.07 1.01 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39424 0 0 0 82916 100 0 0 25 0 1 0 546200626 107212800 17530 4294967295 134512640 134672761 3221224624 3220239488 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26175 17530 603 41 0 26134 0
vsize: 104700
[startup+840.045 s]
Raw data (loadavg): 1.06 1.01 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39493 0 0 0 83916 100 0 0 25 0 1 0 546200626 107347968 17599 4294967295 134512640 134672761 3221224624 3221077856 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26208 17599 603 41 0 26167 0
vsize: 104832
[startup+850.045 s]
Raw data (loadavg): 1.05 1.01 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39741 0 0 0 84916 101 0 0 25 0 1 0 546200626 119894016 17647 4294967295 134512640 134672761 3221224624 3219737056 134522883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29271 17647 603 41 0 29230 0
vsize: 117084
[startup+860.052 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39883 0 0 0 85916 101 0 0 25 0 1 0 546200626 120197120 17747 4294967295 134512640 134672761 3221224624 3220457696 134594261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29345 17747 603 41 0 29304 0
vsize: 117380
[startup+870.057 s]
Raw data (loadavg): 1.04 1.01 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39920 0 0 0 86917 101 0 0 25 0 1 0 546200626 120332288 17784 4294967295 134512640 134672761 3221224624 3220914368 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29378 17784 603 41 0 29337 0
vsize: 117512
[startup+880.065 s]
Raw data (loadavg): 1.03 1.01 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39945 0 0 0 87918 101 0 0 25 0 1 0 546200626 120332288 17809 4294967295 134512640 134672761 3221224624 3220379280 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+890.065 s]
Raw data (loadavg): 1.02 1.01 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39945 0 0 0 88918 101 0 0 25 0 1 0 546200626 120332288 17809 4294967295 134512640 134672761 3221224624 3219586032 134594084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+900.067 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39945 0 0 0 89918 101 0 0 25 0 1 0 546200626 120332288 17809 4294967295 134512640 134672761 3221224624 3219139248 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+910.066 s]
Raw data (loadavg): 1.02 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 39945 0 0 0 90918 101 0 0 25 0 1 0 546200626 120332288 17809 4294967295 134512640 134672761 3221224624 3218287344 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29378 17809 603 41 0 29337 0
vsize: 117512
[startup+920.066 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 40260 0 0 0 91918 102 0 0 25 0 1 0 546200626 121073664 18041 4294967295 134512640 134672761 3221224624 3219642656 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29559 18041 603 41 0 29518 0
vsize: 118236
[startup+930.07 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 40349 0 0 0 92918 102 0 0 25 0 1 0 546200626 121344000 18130 4294967295 134512640 134672761 3221224624 3220727648 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29625 18130 603 41 0 29584 0
vsize: 118500
[startup+940.07 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 40706 0 0 0 93918 103 0 0 25 0 1 0 546200626 121733120 18280 4294967295 134512640 134672761 3221224624 3218437664 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29720 18280 603 41 0 29679 0
vsize: 118880
[startup+950.076 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 40871 0 0 0 94918 103 0 0 25 0 1 0 546200626 122036224 18403 4294967295 134512640 134672761 3221224624 3219538592 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29794 18403 603 41 0 29753 0
vsize: 119176
[startup+960.076 s]
Raw data (loadavg): 1.01 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 40916 0 0 0 95918 103 0 0 25 0 1 0 546200626 122171392 18448 4294967295 134512640 134672761 3221224624 3220087904 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29827 18448 603 41 0 29786 0
vsize: 119308
[startup+970.076 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 40948 0 0 0 96919 103 0 0 25 0 1 0 546200626 122306560 18480 4294967295 134512640 134672761 3221224624 3220482944 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29860 18480 603 41 0 29819 0
vsize: 119440
[startup+980.196 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 40975 0 0 0 97931 103 0 0 25 0 1 0 546200626 122306560 18507 4294967295 134512640 134672761 3221224624 3220806848 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29860 18507 603 41 0 29819 0
vsize: 119440
[startup+990.206 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 40997 0 0 0 98932 103 0 0 25 0 1 0 546200626 122441728 18529 4294967295 134512640 134672761 3221224624 3221080736 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18529 603 41 0 29852 0
vsize: 119572
[startup+1000.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 41009 0 0 0 99934 103 0 0 25 0 1 0 546200626 122441728 18541 4294967295 134512640 134672761 3221224624 3219723984 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1010.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 41009 0 0 0 100934 103 0 0 25 0 1 0 546200626 122441728 18541 4294967295 134512640 134672761 3221224624 3219092592 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1020.23 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 41009 0 0 0 101935 103 0 0 25 0 1 0 546200626 122441728 18541 4294967295 134512640 134672761 3221224624 3218813040 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1030.24 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 41009 0 0 0 102936 103 0 0 25 0 1 0 546200626 122441728 18541 4294967295 134512640 134672761 3221224624 3218487792 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1040.24 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 41009 0 0 0 103936 103 0 0 25 0 1 0 546200626 122441728 18541 4294967295 134512640 134672761 3221224624 3218028432 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1050.24 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 41009 0 0 0 104936 104 0 0 25 0 1 0 546200626 122441728 18541 4294967295 134512640 134672761 3221224624 3217488048 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1060.25 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 41327 0 0 0 105937 104 0 0 25 0 1 0 546200626 123183104 18776 4294967295 134512640 134672761 3221224624 3219054080 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30074 18776 603 41 0 30033 0
vsize: 120296
[startup+1070.28 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 41423 0 0 0 106940 105 0 0 25 0 1 0 546200626 123453440 18872 4294967295 134512640 134672761 3221224624 3220224800 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30140 18872 603 41 0 30099 0
vsize: 120560
[startup+1080.29 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 41504 0 0 0 107940 105 0 0 25 0 1 0 546200626 123588608 18953 4294967295 134512640 134672761 3221224624 3220902560 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30173 18953 603 41 0 30132 0
vsize: 120692
[startup+1090.31 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 41842 0 0 0 108941 106 0 0 25 0 1 0 546200626 123748352 19084 4294967295 134512640 134672761 3221224624 3221075856 134594124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30212 19084 603 41 0 30171 0
vsize: 120848
[startup+1100.31 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 55896 0 0 0 109909 139 0 0 25 0 1 0 546200626 144748544 30448 4294967295 134512640 134672761 3221224624 3215272656 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35339 30449 603 41 0 35298 0
vsize: 141356
[startup+1102.54 s]
Raw data (loadavg): 1.00 1.00 0.94 1/53 8915
Raw data (stat): 8915 (minisat+) R 8914 27565 27564 0 -1 0 55896 0 0 0 109909 139 0 0 25 0 1 0 546200626 144748544 30448 4294967295 134512640 134672761 3221224624 3215272656 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35339 30449 603 41 0 35298 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1102.54
CPU time (s): 1102.7
CPU user time (s): 1100.9
CPU system time (s): 1.79573
CPU usage (%): 100.015
Max. virtual memory (Kb): 141356
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####