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-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-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	1197.16
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 21812

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-22 01:04:18 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12862 boxname=wulflinc5 idbench=990 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  5a18ff1f45b144b201f1f80233dc9b6b  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-nw04.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-nw04.opb
IDLAUNCH: 12862
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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	: 2
cpu MHz		: 451.007
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:        397000 kB
Buffers:         32324 kB
Cached:         583108 kB
SwapCached:        444 kB
Active:         121792 kB
Inactive:       495828 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        396748 kB
SwapTotal:     2097136 kB
SwapFree:      2095948 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           5200 kB
Slab:            14300 kB
Committed_AS:    63560 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 01:21:22 (client local time) WITH STATUS 0 IN 1023.39 SECONDS
stats: 12862 7 1023.39 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.92 0.90 2/54 6992
Raw data (stat): 6992 (runsolver) R 6991 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491395809 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+10.001 s]
Raw data (loadavg): 0.88 0.92 0.90 2/54 6992
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 22973 0 0 0 941 57 0 0 25 0 1 0 491395809 64581632 7176 4294967295 134512640 134672761 3221224624 3220549664 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15767 7176 603 41 0 15726 0
vsize: 63068
[startup+20.0017 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 6992
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 22973 0 0 0 1941 57 0 0 25 0 1 0 491395809 64581632 7176 4294967295 134512640 134672761 3221224624 3220853792 134594223 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.001 s]
Raw data (loadavg): 0.91 0.92 0.91 2/54 6992
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 23318 0 0 0 2940 59 0 0 25 0 1 0 491395809 65994752 7521 4294967295 134512640 134672761 3221224624 3220717376 134594212 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.0022 s]
Raw data (loadavg): 0.93 0.93 0.91 2/54 6992
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 23706 0 0 0 3940 59 0 0 25 0 1 0 491395809 69140480 7909 4294967295 134512640 134672761 3221224624 3220320816 134594095 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.0028 s]
Raw data (loadavg): 0.94 0.93 0.91 2/54 6992
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 23947 0 0 0 4939 60 0 0 25 0 1 0 491395809 69771264 8150 4294967295 134512640 134672761 3221224624 3220323984 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.0032 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 6992
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 24693 0 0 0 5937 63 0 0 25 0 1 0 491395809 71118848 8566 4294967295 134512640 134672761 3221224624 3221206784 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8566 603 41 0 17322 0
vsize: 69452
[startup+70.0035 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 24805 0 0 0 6936 63 0 0 25 0 1 0 491395809 71118848 8678 4294967295 134512640 134672761 3221224624 3220044128 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8678 603 41 0 17322 0
vsize: 69452
[startup+80.0041 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 24953 0 0 0 7936 64 0 0 25 0 1 0 491395809 71458816 8826 4294967295 134512640 134672761 3221224624 3220625408 134594261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17446 8826 603 41 0 17405 0
vsize: 69784
[startup+90.0044 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 25087 0 0 0 8935 64 0 0 25 0 1 0 491395809 74571776 8877 4294967295 134512640 134672761 3221224624 3220077552 134594086 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.005 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 25480 0 0 0 9934 66 0 0 25 0 1 0 491395809 75186176 9145 4294967295 134512640 134672761 3221224624 3220798608 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18356 9145 603 41 0 18315 0
vsize: 73424
[startup+110.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 26031 0 0 0 10933 67 0 0 25 0 1 0 491395809 76677120 9571 4294967295 134512640 134672761 3221224624 3219439616 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18720 9571 603 41 0 18679 0
vsize: 74880
[startup+120.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 27564 0 0 0 11929 71 0 0 25 0 1 0 491395809 79851520 10403 4294967295 134512640 134672761 3221224624 3220779008 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19495 10403 603 41 0 19454 0
vsize: 77980
[startup+130.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 27601 0 0 0 12928 72 0 0 25 0 1 0 491395809 79986688 10440 4294967295 134512640 134672761 3221224624 3220370160 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.008 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 27601 0 0 0 13928 72 0 0 25 0 1 0 491395809 79986688 10440 4294967295 134512640 134672761 3221224624 3219335376 134594086 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.008 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 27996 0 0 0 14927 73 0 0 25 0 1 0 491395809 80998400 10752 4294967295 134512640 134672761 3221224624 3220673312 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19775 10752 603 41 0 19734 0
vsize: 79100
[startup+160.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 28245 0 0 0 15926 74 0 0 25 0 1 0 491395809 81010688 10836 4294967295 134512640 134672761 3221224624 3220474688 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19778 10836 603 41 0 19737 0
vsize: 79112
[startup+170.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 28389 0 0 0 16926 75 0 0 25 0 1 0 491395809 81313792 10938 4294967295 134512640 134672761 3221224624 3220671984 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19852 10938 603 41 0 19811 0
vsize: 79408
[startup+180.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 28389 0 0 0 17926 75 0 0 25 0 1 0 491395809 81313792 10938 4294967295 134512640 134672761 3221224624 3219003984 134594131 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.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 28899 0 0 0 18925 76 0 0 25 0 1 0 491395809 82038784 11200 4294967295 134512640 134672761 3221224624 3220155584 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20029 11200 603 41 0 19988 0
vsize: 80116
[startup+200.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 29050 0 0 0 19924 77 0 0 25 0 1 0 491395809 82341888 11309 4294967295 134512640 134672761 3221224624 3220879056 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+210.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 29191 0 0 0 20924 77 0 0 25 0 1 0 491395809 82747392 11450 4294967295 134512640 134672761 3221224624 3220858592 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20202 11450 603 41 0 20161 0
vsize: 80808
[startup+220.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 29592 0 0 0 21924 78 0 0 25 0 1 0 491395809 83062784 11603 4294967295 134512640 134672761 3221224624 3220673408 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20279 11603 603 41 0 20238 0
vsize: 81116
[startup+230.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 29721 0 0 0 22923 78 0 0 25 0 1 0 491395809 83365888 11690 4294967295 134512640 134672761 3221224624 3220522704 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+240.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 29721 0 0 0 23924 78 0 0 25 0 1 0 491395809 83365888 11690 4294967295 134512640 134672761 3221224624 3218982480 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.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 30168 0 0 0 24923 79 0 0 25 0 1 0 491395809 89985024 11889 4294967295 134512640 134672761 3221224624 3219260864 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21969 11889 603 41 0 21928 0
vsize: 87876
[startup+260.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 30401 0 0 0 25922 80 0 0 25 0 1 0 491395809 90595328 12080 4294967295 134512640 134672761 3221224624 3220852832 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22118 12080 603 41 0 22077 0
vsize: 88472
[startup+270.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 30431 0 0 0 26922 80 0 0 25 0 1 0 491395809 90730496 12110 4294967295 134512640 134672761 3221224624 3220347024 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+280.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 30431 0 0 0 27923 80 0 0 25 0 1 0 491395809 90730496 12110 4294967295 134512640 134672761 3221224624 3218728560 134594131 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.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 30890 0 0 0 28922 81 0 0 25 0 1 0 491395809 91066368 12321 4294967295 134512640 134672761 3221224624 3219355232 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22233 12321 603 41 0 22192 0
vsize: 88932
[startup+300.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 31117 0 0 0 29921 82 0 0 25 0 1 0 491395809 91676672 12506 4294967295 134512640 134672761 3221224624 3220853696 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22382 12506 603 41 0 22341 0
vsize: 89528
[startup+310.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 31148 0 0 0 30921 82 0 0 25 0 1 0 491395809 91811840 12537 4294967295 134512640 134672761 3221224624 3220348560 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22415 12537 603 41 0 22374 0
vsize: 89660
[startup+320.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 31148 0 0 0 31922 82 0 0 25 0 1 0 491395809 91811840 12537 4294967295 134512640 134672761 3221224624 3218855856 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.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 31560 0 0 0 32921 83 0 0 25 0 1 0 491395809 92053504 12701 4294967295 134512640 134672761 3221224624 3218735648 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22474 12701 603 41 0 22433 0
vsize: 89896
[startup+340.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 31831 0 0 0 33920 83 0 0 25 0 1 0 491395809 92798976 12930 4294967295 134512640 134672761 3221224624 3220685216 134594261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22656 12930 603 41 0 22615 0
vsize: 90624
[startup+350.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 31874 0 0 0 34920 83 0 0 25 0 1 0 491395809 92934144 12973 4294967295 134512640 134672761 3221224624 3220461648 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22689 12973 603 41 0 22648 0
vsize: 90756
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 31874 0 0 0 35921 83 0 0 25 0 1 0 491395809 92934144 12973 4294967295 134512640 134672761 3221224624 3219564528 134594106 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 34839 0 0 0 36914 91 0 0 25 0 1 0 491395809 99078144 14537 4294967295 134512640 134672761 3221224624 3220511072 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24189 14537 603 41 0 24148 0
vsize: 96756
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 35108 0 0 0 37913 91 0 0 25 0 1 0 491395809 99139584 14641 4294967295 134512640 134672761 3221224624 3219966560 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24204 14641 603 41 0 24163 0
vsize: 96816
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 35270 0 0 0 38913 91 0 0 25 0 1 0 491395809 99577856 14761 4294967295 134512640 134672761 3221224624 3220932224 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14761 603 41 0 24270 0
vsize: 97244
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 35294 0 0 0 39913 91 0 0 25 0 1 0 491395809 99577856 14785 4294967295 134512640 134672761 3221224624 3220214448 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14785 603 41 0 24270 0
vsize: 97244
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 35294 0 0 0 40914 91 0 0 25 0 1 0 491395809 99577856 14785 4294967295 134512640 134672761 3221224624 3219137040 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+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 35639 0 0 0 41913 92 0 0 25 0 1 0 491395809 100454400 15047 4294967295 134512640 134672761 3221224624 3220605248 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24525 15047 603 41 0 24484 0
vsize: 98100
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 36046 0 0 0 42912 93 0 0 25 0 1 0 491395809 100962304 15254 4294967295 134512640 134672761 3221224624 3219380480 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24649 15254 603 41 0 24608 0
vsize: 98596
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 36207 0 0 0 43912 94 0 0 25 0 1 0 491395809 101400576 15373 4294967295 134512640 134672761 3221224624 3220333376 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24756 15373 603 41 0 24715 0
vsize: 99024
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 36252 0 0 0 44912 94 0 0 25 0 1 0 491395809 101400576 15418 4294967295 134512640 134672761 3221224624 3220870688 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24756 15418 603 41 0 24715 0
vsize: 99024
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 36281 0 0 0 45912 94 0 0 25 0 1 0 491395809 101535744 15447 4294967295 134512640 134672761 3221224624 3220568400 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+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 36281 0 0 0 46912 94 0 0 25 0 1 0 491395809 101535744 15447 4294967295 134512640 134672761 3221224624 3219573360 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 36281 0 0 0 47912 94 0 0 25 0 1 0 491395809 101535744 15447 4294967295 134512640 134672761 3221224624 3219094992 134594131 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.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 36281 0 0 0 48913 94 0 0 25 0 1 0 491395809 101535744 15447 4294967295 134512640 134672761 3221224624 3218094000 134594106 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 36653 0 0 0 49912 95 0 0 25 0 1 0 491395809 102412288 15736 4294967295 134512640 134672761 3221224624 3220232192 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25003 15736 603 41 0 24962 0
vsize: 100012
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 36764 0 0 0 50911 95 0 0 25 0 1 0 491395809 102817792 15847 4294967295 134512640 134672761 3221224624 3221137760 134594261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25102 15847 603 41 0 25061 0
vsize: 100408
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 37138 0 0 0 51911 96 0 0 25 0 1 0 491395809 103047168 15977 4294967295 134512640 134672761 3221224624 3219700160 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25158 15977 603 41 0 25117 0
vsize: 100632
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 37197 0 0 0 52911 96 0 0 25 0 1 0 491395809 103182336 16036 4294967295 134512640 134672761 3221224624 3220422272 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25191 16036 603 41 0 25150 0
vsize: 100764
[startup+540.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 37235 0 0 0 53911 96 0 0 25 0 1 0 491395809 103317504 16074 4294967295 134512640 134672761 3221224624 3220890656 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16074 603 41 0 25183 0
vsize: 100896
[startup+550.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 37262 0 0 0 54911 96 0 0 25 0 1 0 491395809 103317504 16101 4294967295 134512640 134672761 3221224624 3220734000 134594084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16101 603 41 0 25183 0
vsize: 100896
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 37262 0 0 0 55911 96 0 0 25 0 1 0 491395809 103317504 16101 4294967295 134512640 134672761 3221224624 3219501456 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+570.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 37262 0 0 0 56912 96 0 0 25 0 1 0 491395809 103317504 16101 4294967295 134512640 134672761 3221224624 3219107280 134594089 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 37262 0 0 0 57912 96 0 0 25 0 1 0 491395809 103317504 16101 4294967295 134512640 134672761 3221224624 3218375376 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 37540 0 0 0 58911 97 0 0 25 0 1 0 491395809 103923712 16296 4294967295 134512640 134672761 3221224624 3219050624 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25372 16296 603 41 0 25331 0
vsize: 101488
[startup+600.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 37669 0 0 0 59911 97 0 0 25 0 1 0 491395809 104329216 16425 4294967295 134512640 134672761 3221224624 3220609856 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25471 16425 603 41 0 25430 0
vsize: 101884
[startup+610.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 37860 0 0 0 60911 98 0 0 25 0 1 0 491395809 104103936 16416 4294967295 134512640 134672761 3221224624 3218705888 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25416 16416 603 41 0 25375 0
vsize: 101664
[startup+620.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 38078 0 0 0 61911 98 0 0 25 0 1 0 491395809 104579072 16592 4294967295 134512640 134672761 3221224624 3220083584 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25532 16592 603 41 0 25491 0
vsize: 102128
[startup+630.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 38129 0 0 0 62911 98 0 0 25 0 1 0 491395809 104714240 16643 4294967295 134512640 134672761 3221224624 3220705952 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25565 16643 603 41 0 25524 0
vsize: 102260
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 38164 0 0 0 63911 98 0 0 25 0 1 0 491395809 104849408 16678 4294967295 134512640 134672761 3221224624 3221130752 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25598 16678 603 41 0 25557 0
vsize: 102392
[startup+650.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 38171 0 0 0 64911 98 0 0 25 0 1 0 491395809 104849408 16685 4294967295 134512640 134672761 3221224624 3219701040 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+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 38171 0 0 0 65911 98 0 0 25 0 1 0 491395809 104849408 16685 4294967295 134512640 134672761 3221224624 3219282096 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+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 38171 0 0 0 66911 98 0 0 25 0 1 0 491395809 104849408 16685 4294967295 134512640 134672761 3221224624 3218449776 134594095 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 38485 0 0 0 67911 99 0 0 25 0 1 0 491395809 105590784 16916 4294967295 134512640 134672761 3221224624 3219611744 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25779 16916 603 41 0 25738 0
vsize: 103116
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 38588 0 0 0 68910 100 0 0 25 0 1 0 491395809 105861120 17019 4294967295 134512640 134672761 3221224624 3220873760 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25845 17019 603 41 0 25804 0
vsize: 103380
[startup+700.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 38827 0 0 0 69910 100 0 0 25 0 1 0 491395809 105762816 17058 4294967295 134512640 134672761 3221224624 3219412160 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25821 17058 603 41 0 25780 0
vsize: 103284
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 38986 0 0 0 70910 101 0 0 25 0 1 0 491395809 106201088 17175 4294967295 134512640 134672761 3221224624 3220344992 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25928 17175 603 41 0 25887 0
vsize: 103712
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39031 0 0 0 71909 101 0 0 25 0 1 0 491395809 106201088 17220 4294967295 134512640 134672761 3221224624 3220876832 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25928 17220 603 41 0 25887 0
vsize: 103712
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39058 0 0 0 72910 101 0 0 25 0 1 0 491395809 106336256 17247 4294967295 134512640 134672761 3221224624 3220526160 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+740.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39058 0 0 0 73910 101 0 0 25 0 1 0 491395809 106336256 17247 4294967295 134512640 134672761 3221224624 3219566064 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39058 0 0 0 74910 101 0 0 25 0 1 0 491395809 106336256 17247 4294967295 134512640 134672761 3221224624 3219088944 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+760.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39058 0 0 0 75910 101 0 0 25 0 1 0 491395809 106336256 17247 4294967295 134512640 134672761 3221224624 3218091984 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39424 0 0 0 76909 102 0 0 25 0 1 0 491395809 107212800 17530 4294967295 134512640 134672761 3221224624 3220247456 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26175 17530 603 41 0 26134 0
vsize: 104700
[startup+780.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39500 0 0 0 77909 103 0 0 25 0 1 0 491395809 107347968 17606 4294967295 134512640 134672761 3221224624 3221162816 134594220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26208 17606 603 41 0 26167 0
vsize: 104832
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39835 0 0 0 78908 104 0 0 25 0 1 0 491395809 120061952 17699 4294967295 134512640 134672761 3221224624 3219877664 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29312 17699 603 41 0 29271 0
vsize: 117248
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39893 0 0 0 79908 104 0 0 25 0 1 0 491395809 120197120 17757 4294967295 134512640 134672761 3221224624 3220585376 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29345 17757 603 41 0 29304 0
vsize: 117380
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39931 0 0 0 80909 104 0 0 25 0 1 0 491395809 120332288 17795 4294967295 134512640 134672761 3221224624 3221047712 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29378 17795 603 41 0 29337 0
vsize: 117512
[startup+820.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39945 0 0 0 81910 104 0 0 25 0 1 0 491395809 120332288 17809 4294967295 134512640 134672761 3221224624 3219789264 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+830.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39945 0 0 0 82911 104 0 0 25 0 1 0 491395809 120332288 17809 4294967295 134512640 134672761 3221224624 3219388656 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+840.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 39945 0 0 0 83911 104 0 0 25 0 1 0 491395809 120332288 17809 4294967295 134512640 134672761 3221224624 3218750352 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.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 40223 0 0 0 84911 104 0 0 25 0 1 0 491395809 120938496 18004 4294967295 134512640 134672761 3221224624 3219182720 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29526 18004 603 41 0 29485 0
vsize: 118104
[startup+860.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 40351 0 0 0 85911 105 0 0 25 0 1 0 491395809 121344000 18132 4294967295 134512640 134672761 3221224624 3220741472 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29625 18132 603 41 0 29584 0
vsize: 118500
[startup+870.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 40709 0 0 0 86910 106 0 0 25 0 1 0 491395809 121733120 18283 4294967295 134512640 134672761 3221224624 3218556416 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29720 18283 603 41 0 29679 0
vsize: 118880
[startup+880.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 40878 0 0 0 87910 106 0 0 25 0 1 0 491395809 122036224 18410 4294967295 134512640 134672761 3221224624 3219626336 134594261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29794 18410 603 41 0 29753 0
vsize: 119176
[startup+890.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 40925 0 0 0 88910 106 0 0 25 0 1 0 491395809 122171392 18457 4294967295 134512640 134672761 3221224624 3220193408 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29827 18457 603 41 0 29786 0
vsize: 119308
[startup+900.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 40957 0 0 0 89911 106 0 0 25 0 1 0 491395809 122306560 18489 4294967295 134512640 134672761 3221224624 3220589024 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18489 603 41 0 29819 0
vsize: 119440
[startup+910.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 40983 0 0 0 90911 106 0 0 25 0 1 0 491395809 122306560 18515 4294967295 134512640 134672761 3221224624 3220899872 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29860 18515 603 41 0 29819 0
vsize: 119440
[startup+920.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 41005 0 0 0 91911 106 0 0 25 0 1 0 491395809 122441728 18537 4294967295 134512640 134672761 3221224624 3221170208 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29893 18537 603 41 0 29852 0
vsize: 119572
[startup+930.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 41009 0 0 0 92911 106 0 0 25 0 1 0 491395809 122441728 18541 4294967295 134512640 134672761 3221224624 3219235728 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.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 41009 0 0 0 93911 106 0 0 25 0 1 0 491395809 122441728 18541 4294967295 134512640 134672761 3221224624 3218955120 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.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 41009 0 0 0 94912 106 0 0 25 0 1 0 491395809 122441728 18541 4294967295 134512640 134672761 3221224624 3218657712 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.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 41009 0 0 0 95912 106 0 0 25 0 1 0 491395809 122441728 18541 4294967295 134512640 134672761 3221224624 3218301072 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.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 41009 0 0 0 96912 106 0 0 25 0 1 0 491395809 122441728 18541 4294967295 134512640 134672761 3221224624 3217619088 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+980.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 41296 0 0 0 97912 107 0 0 25 0 1 0 491395809 123047936 18745 4294967295 134512640 134672761 3221224624 3218681408 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30041 18745 603 41 0 30000 0
vsize: 120164
[startup+990.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 41417 0 0 0 98912 107 0 0 25 0 1 0 491395809 123318272 18866 4294967295 134512640 134672761 3221224624 3220152512 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30107 18866 603 41 0 30066 0
vsize: 120428
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 41496 0 0 0 99912 107 0 0 25 0 1 0 491395809 123588608 18945 4294967295 134512640 134672761 3221224624 3220845632 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30173 18945 603 41 0 30132 0
vsize: 120692
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 41770 0 0 0 100911 108 0 0 25 0 1 0 491395809 123756544 19054 4294967295 134512640 134672761 3221224624 3221081984 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30214 19054 603 41 0 30173 0
vsize: 120856
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 49163 0 0 0 101894 125 0 0 25 0 1 0 491395809 120692736 23715 4294967295 134512640 134672761 3221224624 3220257360 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29466 23717 603 41 0 29425 0
vsize: 117864
[startup+1023.23 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 6994
Raw data (stat): 6992 (minisat+) R 6991 24215 24214 0 -1 0 49163 0 0 0 101894 125 0 0 25 0 1 0 491395809 120692736 23715 4294967295 134512640 134672761 3221224624 3220257360 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29466 23717 603 41 0 29425 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1023.23
CPU time (s): 1023.39
CPU user time (s): 1021.58
CPU system time (s): 1.80073
CPU usage (%): 100.015
Max. virtual memory (Kb): 120856
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####