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/miplib3/normalized-mps-v2-20-10-nw04.opb
MD5SUM	a5c401bba5afccf02c7b40cb1c595b15
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	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	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.13683
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 21177

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 23:02:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13681 boxname=wulflinc12 idbench=1053 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  a5c401bba5afccf02c7b40cb1c595b15  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-nw04.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-nw04.opb
IDLAUNCH: 13681
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        207192 kB
Buffers:         33488 kB
Cached:         771600 kB
SwapCached:        508 kB
Active:         173344 kB
Inactive:       633932 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        206940 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            14548 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:19:53 (client local time) WITH STATUS 0 IN 1048.01 SECONDS
stats: 13681 7 1048.01 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.87 0.97 0.92 2/54 7902
Raw data (stat): 7902 (runsolver) R 7901 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490660446 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.99992 s]
Raw data (loadavg): 0.89 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 22973 0 0 0 936 63 0 0 25 0 1 0 490660446 64581632 7176 4294967295 134512640 134672761 3221224624 3220462112 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.0012 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 22973 0 0 0 1936 63 0 0 25 0 1 0 490660446 64581632 7176 4294967295 134512640 134672761 3221224624 3220774592 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+30.0031 s]
Raw data (loadavg): 0.92 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 23318 0 0 0 2935 64 0 0 25 0 1 0 490660446 65994752 7521 4294967295 134512640 134672761 3221224624 3220608224 134594259 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.0044 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 23706 0 0 0 3934 65 0 0 25 0 1 0 490660446 69140480 7909 4294967295 134512640 134672761 3221224624 3220490064 134594106 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.0112 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 23947 0 0 0 4934 66 0 0 25 0 1 0 490660446 69771264 8150 4294967295 134512640 134672761 3221224624 3220417392 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.0115 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 24684 0 0 0 5933 67 0 0 25 0 1 0 490660446 71118848 8557 4294967295 134512640 134672761 3221224624 3220907072 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8557 603 41 0 17322 0
vsize: 69452
[startup+70.0109 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 24781 0 0 0 6932 68 0 0 25 0 1 0 490660446 71118848 8654 4294967295 134512640 134672761 3221224624 3220776128 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8654 603 41 0 17322 0
vsize: 69452
[startup+80.0117 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 24841 0 0 0 7931 69 0 0 25 0 1 0 490660446 71118848 8714 4294967295 134512640 134672761 3221224624 3219896880 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17363 8714 603 41 0 17322 0
vsize: 69452
[startup+90.012 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 25087 0 0 0 8931 70 0 0 25 0 1 0 490660446 74571776 8877 4294967295 134512640 134672761 3221224624 3220522992 134594103 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.012 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 25457 0 0 0 9930 70 0 0 25 0 1 0 490660446 75186176 9122 4294967295 134512640 134672761 3221224624 3220908992 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18356 9122 603 41 0 18315 0
vsize: 73424
[startup+110.014 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 25672 0 0 0 10929 71 0 0 25 0 1 0 490660446 75624448 9295 4294967295 134512640 134672761 3221224624 3220872800 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18463 9295 603 41 0 18422 0
vsize: 73852
[startup+120.014 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 27455 0 0 0 11925 76 0 0 25 0 1 0 490660446 79683584 10336 4294967295 134512640 134672761 3221224624 3220467200 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19454 10336 603 41 0 19413 0
vsize: 77816
[startup+130.015 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 27597 0 0 0 12924 77 0 0 25 0 1 0 490660446 79986688 10436 4294967295 134512640 134672761 3221224624 3221182496 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19528 10436 603 41 0 19487 0
vsize: 78112
[startup+140.015 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 27601 0 0 0 13924 77 0 0 25 0 1 0 490660446 79986688 10440 4294967295 134512640 134672761 3221224624 3219958416 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.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 27678 0 0 0 14924 77 0 0 25 0 1 0 490660446 80121856 10517 4294967295 134512640 134672761 3221224624 3219438080 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19561 10517 603 41 0 19520 0
vsize: 78244
[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 28089 0 0 0 15923 78 0 0 25 0 1 0 490660446 80568320 10680 4294967295 134512640 134672761 3221224624 3219914580 134594036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19670 10680 603 41 0 19629 0
vsize: 78680
[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 28361 0 0 0 16922 79 0 0 25 0 1 0 490660446 81313792 10910 4294967295 134512640 134672761 3221224624 3220895072 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19852 10910 603 41 0 19811 0
vsize: 79408
[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 28389 0 0 0 17922 80 0 0 25 0 1 0 490660446 81313792 10938 4294967295 134512640 134672761 3221224624 3220387248 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.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7902
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 28503 0 0 0 18921 81 0 0 25 0 1 0 490660446 81719296 11052 4294967295 134512640 134672761 3221224624 3220196960 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19951 11052 603 41 0 19910 0
vsize: 79804
[startup+200.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 28919 0 0 0 19919 83 0 0 25 0 1 0 490660446 82038784 11220 4294967295 134512640 134672761 3221224624 3220631552 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20029 11220 603 41 0 19988 0
vsize: 80116
[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 29050 0 0 0 20919 83 0 0 25 0 1 0 490660446 82341888 11309 4294967295 134512640 134672761 3221224624 3220696176 134594084 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.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 29377 0 0 0 21918 84 0 0 25 0 1 0 490660446 83083264 11553 4294967295 134512640 134672761 3221224624 3221109344 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20284 11553 603 41 0 20243 0
vsize: 81136
[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 29680 0 0 0 22917 85 0 0 25 0 1 0 490660446 83230720 11649 4294967295 134512640 134672761 3221224624 3220733312 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20320 11649 603 41 0 20279 0
vsize: 81280
[startup+240.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 29721 0 0 0 23917 85 0 0 25 0 1 0 490660446 83365888 11690 4294967295 134512640 134672761 3221224624 3220519632 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.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 29721 0 0 0 24917 85 0 0 25 0 1 0 490660446 83365888 11690 4294967295 134512640 134672761 3221224624 3219045456 134594089 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.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 30091 0 0 0 25916 87 0 0 25 0 1 0 490660446 90398720 11977 4294967295 134512640 134672761 3221224624 3221200352 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22070 11977 603 41 0 22029 0
vsize: 88280
[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 30389 0 0 0 26915 87 0 0 25 0 1 0 490660446 90595328 12068 4294967295 134512640 134672761 3221224624 3220717568 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22118 12068 603 41 0 22077 0
vsize: 88472
[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 30431 0 0 0 27915 88 0 0 25 0 1 0 490660446 90730496 12110 4294967295 134512640 134672761 3221224624 3220511664 134594131 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.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 30431 0 0 0 28914 89 0 0 25 0 1 0 490660446 90730496 12110 4294967295 134512640 134672761 3221224624 3219250512 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.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 30788 0 0 0 29913 90 0 0 25 0 1 0 490660446 91471872 12384 4294967295 134512640 134672761 3221224624 3220974848 134594261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22332 12384 603 41 0 22291 0
vsize: 89328
[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31007 0 0 0 30912 91 0 0 25 0 1 0 490660446 91508736 12438 4294967295 134512640 134672761 3221224624 3220512896 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22341 12438 603 41 0 22300 0
vsize: 89364
[startup+320.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31148 0 0 0 31912 92 0 0 25 0 1 0 490660446 91811840 12537 4294967295 134512640 134672761 3221224624 3220661328 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22415 12537 603 41 0 22374 0
vsize: 89660
[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31148 0 0 0 32912 92 0 0 25 0 1 0 490660446 91811840 12537 4294967295 134512640 134672761 3221224624 3219843312 134594086 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.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31468 0 0 0 33910 93 0 0 25 0 1 0 490660446 92553216 12774 4294967295 134512640 134672761 3221224624 3220504832 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22596 12774 603 41 0 22555 0
vsize: 90384
[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31694 0 0 0 34909 95 0 0 25 0 1 0 490660446 92495872 12835 4294967295 134512640 134672761 3221224624 3220047200 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22582 12835 603 41 0 22541 0
vsize: 90328
[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31854 0 0 0 35909 95 0 0 25 0 1 0 490660446 92798976 12953 4294967295 134512640 134672761 3221224624 3220975424 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22656 12953 603 41 0 22615 0
vsize: 90624
[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31874 0 0 0 36909 95 0 0 25 0 1 0 490660446 92934144 12973 4294967295 134512640 134672761 3221224624 3220228848 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+380.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 31874 0 0 0 37909 95 0 0 25 0 1 0 490660446 92934144 12973 4294967295 134512640 134672761 3221224624 3218890320 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+390.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 34870 0 0 0 38902 102 0 0 25 0 1 0 490660446 99078144 14568 4294967295 134512640 134672761 3221224624 3220896032 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24189 14568 603 41 0 24148 0
vsize: 96756
[startup+400.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 35128 0 0 0 39902 103 0 0 25 0 1 0 490660446 99274752 14661 4294967295 134512640 134672761 3221224624 3220222976 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24237 14661 603 41 0 24196 0
vsize: 96948
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 35276 0 0 0 40902 103 0 0 25 0 1 0 490660446 99577856 14767 4294967295 134512640 134672761 3221224624 3221010272 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24311 14767 603 41 0 24270 0
vsize: 97244
[startup+420.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 35294 0 0 0 41901 103 0 0 25 0 1 0 490660446 99577856 14785 4294967295 134512640 134672761 3221224624 3220150800 134594106 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.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 35294 0 0 0 42901 104 0 0 25 0 1 0 490660446 99577856 14785 4294967295 134512640 134672761 3221224624 3218977488 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+440.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 35640 0 0 0 43900 105 0 0 25 0 1 0 490660446 100454400 15048 4294967295 134512640 134672761 3221224624 3220628768 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24525 15048 603 41 0 24484 0
vsize: 98100
[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36040 0 0 0 44899 106 0 0 25 0 1 0 490660446 100962304 15248 4294967295 134512640 134672761 3221224624 3219305216 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24649 15248 603 41 0 24608 0
vsize: 98596
[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36200 0 0 0 45899 107 0 0 25 0 1 0 490660446 101265408 15366 4294967295 134512640 134672761 3221224624 3220243232 134594261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24723 15366 603 41 0 24682 0
vsize: 98892
[startup+470.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36246 0 0 0 46899 107 0 0 25 0 1 0 490660446 101400576 15412 4294967295 134512640 134672761 3221224624 3220800320 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24756 15412 603 41 0 24715 0
vsize: 99024
[startup+480.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36279 0 0 0 47899 107 0 0 25 0 1 0 490660446 101535744 15445 4294967295 134512640 134672761 3221224624 3221205344 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24789 15445 603 41 0 24748 0
vsize: 99156
[startup+490.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36281 0 0 0 48899 107 0 0 25 0 1 0 490660446 101535744 15447 4294967295 134512640 134672761 3221224624 3219622800 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.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36281 0 0 0 49899 108 0 0 25 0 1 0 490660446 101535744 15447 4294967295 134512640 134672761 3221224624 3219156912 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.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36281 0 0 0 50899 108 0 0 25 0 1 0 490660446 101535744 15447 4294967295 134512640 134672761 3221224624 3218187120 134594106 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.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36630 0 0 0 51898 109 0 0 25 0 1 0 490660446 102412288 15713 4294967295 134512640 134672761 3221224624 3220043552 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25003 15713 603 41 0 24962 0
vsize: 100012
[startup+530.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 36751 0 0 0 52897 110 0 0 25 0 1 0 490660446 102682624 15834 4294967295 134512640 134672761 3221224624 3221029280 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25069 15834 603 41 0 25028 0
vsize: 100276
[startup+540.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37037 0 0 0 53896 111 0 0 25 0 1 0 490660446 102879232 15918 4294967295 134512640 134672761 3221224624 3219486752 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25117 15918 603 41 0 25076 0
vsize: 100468
[startup+550.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37184 0 0 0 54896 111 0 0 25 0 1 0 490660446 103182336 16023 4294967295 134512640 134672761 3221224624 3220270784 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25191 16023 603 41 0 25150 0
vsize: 100764
[startup+560.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37225 0 0 0 55895 111 0 0 25 0 1 0 490660446 103317504 16064 4294967295 134512640 134672761 3221224624 3220776992 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25224 16064 603 41 0 25183 0
vsize: 100896
[startup+570.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37257 0 0 0 56895 112 0 0 25 0 1 0 490660446 103317504 16096 4294967295 134512640 134672761 3221224624 3221155712 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25224 16096 603 41 0 25183 0
vsize: 100896
[startup+580.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37262 0 0 0 57895 112 0 0 25 0 1 0 490660446 103317504 16101 4294967295 134512640 134672761 3221224624 3219584496 134594106 0 0 5 16386 0 0 0 17 1 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.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37262 0 0 0 58895 112 0 0 25 0 1 0 490660446 103317504 16101 4294967295 134512640 134672761 3221224624 3219195312 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.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37262 0 0 0 59895 112 0 0 25 0 1 0 490660446 103317504 16101 4294967295 134512640 134672761 3221224624 3218649840 134594106 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.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37468 0 0 0 60895 113 0 0 25 0 1 0 490660446 103788544 16224 4294967295 134512640 134672761 3221224624 3218181632 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25339 16224 603 41 0 25298 0
vsize: 101356
[startup+620.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37654 0 0 0 61894 113 0 0 25 0 1 0 490660446 104329216 16410 4294967295 134512640 134672761 3221224624 3220443104 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25471 16410 603 41 0 25430 0
vsize: 101884
[startup+630.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 37727 0 0 0 62894 114 0 0 25 0 1 0 490660446 104464384 16483 4294967295 134512640 134672761 3221224624 3221208704 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25504 16483 603 41 0 25463 0
vsize: 102016
[startup+640.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38060 0 0 0 63893 115 0 0 25 0 1 0 490660446 104579072 16574 4294967295 134512640 134672761 3221224624 3219873056 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25532 16574 603 41 0 25491 0
vsize: 102128
[startup+650.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38116 0 0 0 64893 115 0 0 25 0 1 0 490660446 104714240 16630 4294967295 134512640 134672761 3221224624 3220548896 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25565 16630 603 41 0 25524 0
vsize: 102260
[startup+660.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38154 0 0 0 65893 115 0 0 25 0 1 0 490660446 104849408 16668 4294967295 134512640 134672761 3221224624 3221014304 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16668 603 41 0 25557 0
vsize: 102392
[startup+670.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38171 0 0 0 66893 115 0 0 25 0 1 0 490660446 104849408 16685 4294967295 134512640 134672761 3221224624 3219805104 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+680.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38171 0 0 0 67893 116 0 0 25 0 1 0 490660446 104849408 16685 4294967295 134512640 134672761 3221224624 3219409392 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+690.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38171 0 0 0 68892 116 0 0 25 0 1 0 490660446 104849408 16685 4294967295 134512640 134672761 3221224624 3218844432 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.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38413 0 0 0 69891 117 0 0 25 0 1 0 490660446 105455616 16844 4294967295 134512640 134672761 3221224624 3218745344 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25746 16844 603 41 0 25705 0
vsize: 102984
[startup+710.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38569 0 0 0 70891 118 0 0 25 0 1 0 490660446 105861120 17000 4294967295 134512640 134672761 3221224624 3220633760 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25845 17000 603 41 0 25804 0
vsize: 103380
[startup+720.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38801 0 0 0 71891 118 0 0 25 0 1 0 490660446 105762816 17032 4294967295 134512640 134672761 3221224624 3218895392 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25821 17032 603 41 0 25780 0
vsize: 103284
[startup+730.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 38965 0 0 0 72890 119 0 0 25 0 1 0 490660446 106065920 17154 4294967295 134512640 134672761 3221224624 3220079456 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25895 17154 603 41 0 25854 0
vsize: 103580
[startup+740.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39015 0 0 0 73890 119 0 0 25 0 1 0 490660446 106201088 17204 4294967295 134512640 134672761 3221224624 3220688000 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25928 17204 603 41 0 25887 0
vsize: 103712
[startup+750.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39050 0 0 0 74890 119 0 0 25 0 1 0 490660446 106336256 17239 4294967295 134512640 134672761 3221224624 3221119520 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+760.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39058 0 0 0 75890 120 0 0 25 0 1 0 490660446 106336256 17247 4294967295 134512640 134672761 3221224624 3219709392 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+770.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39058 0 0 0 76890 120 0 0 25 0 1 0 490660446 106336256 17247 4294967295 134512640 134672761 3221224624 3219279120 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+780.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39058 0 0 0 77890 120 0 0 25 0 1 0 490660446 106336256 17247 4294967295 134512640 134672761 3221224624 3218436912 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 17247 603 41 0 25920 0
vsize: 103844
[startup+790.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39372 0 0 0 78889 121 0 0 25 0 1 0 490660446 107077632 17478 4294967295 134512640 134672761 3221224624 3219611552 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26142 17478 603 41 0 26101 0
vsize: 104568
[startup+800.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39477 0 0 0 79889 121 0 0 25 0 1 0 490660446 107347968 17583 4294967295 134512640 134672761 3221224624 3220887296 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26208 17583 603 41 0 26167 0
vsize: 104832
[startup+810.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39713 0 0 0 80889 122 0 0 25 0 1 0 490660446 119758848 17619 4294967295 134512640 134672761 3221224624 3219409760 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29238 17619 603 41 0 29197 0
vsize: 116952
[startup+820.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39870 0 0 0 81888 122 0 0 25 0 1 0 490660446 120197120 17734 4294967295 134512640 134672761 3221224624 3220299200 134594223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29345 17734 603 41 0 29304 0
vsize: 117380
[startup+830.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39914 0 0 0 82888 123 0 0 25 0 1 0 490660446 120332288 17778 4294967295 134512640 134672761 3221224624 3220839968 134594223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29378 17778 603 41 0 29337 0
vsize: 117512
[startup+840.048 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39945 0 0 0 83887 123 0 0 25 0 1 0 490660446 120332288 17809 4294967295 134512640 134672761 3221224624 3220775568 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+850.049 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39945 0 0 0 84887 124 0 0 25 0 1 0 490660446 120332288 17809 4294967295 134512640 134672761 3221224624 3219590352 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+860.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39945 0 0 0 85887 124 0 0 25 0 1 0 490660446 120332288 17809 4294967295 134512640 134672761 3221224624 3219103440 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+870.049 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 39945 0 0 0 86886 125 0 0 25 0 1 0 490660446 120332288 17809 4294967295 134512640 134672761 3221224624 3218090448 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+880.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40311 0 0 0 87886 125 0 0 25 0 1 0 490660446 121208832 18092 4294967295 134512640 134672761 3221224624 3220248608 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29592 18092 603 41 0 29551 0
vsize: 118368
[startup+890.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40386 0 0 0 88886 125 0 0 25 0 1 0 490660446 121344000 18167 4294967295 134512640 134672761 3221224624 3221163296 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29625 18167 603 41 0 29584 0
vsize: 118500
[startup+900.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40760 0 0 0 89885 127 0 0 25 0 1 0 490660446 121868288 18334 4294967295 134512640 134672761 3221224624 3219200288 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29753 18334 603 41 0 29712 0
vsize: 119012
[startup+910.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40900 0 0 0 90884 127 0 0 25 0 1 0 490660446 122171392 18432 4294967295 134512640 134672761 3221224624 3219896864 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29827 18432 603 41 0 29786 0
vsize: 119308
[startup+920.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40939 0 0 0 91884 128 0 0 25 0 1 0 490660446 122171392 18471 4294967295 134512640 134672761 3221224624 3220372256 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29827 18471 603 41 0 29786 0
vsize: 119308
[startup+930.053 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40969 0 0 0 92884 128 0 0 25 0 1 0 490660446 122306560 18501 4294967295 134512640 134672761 3221224624 3220731776 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29860 18501 603 41 0 29819 0
vsize: 119440
[startup+940.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 40992 0 0 0 93883 129 0 0 25 0 1 0 490660446 122441728 18524 4294967295 134512640 134672761 3221224624 3221021792 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18524 603 41 0 29852 0
vsize: 119572
[startup+950.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41009 0 0 0 94883 129 0 0 25 0 1 0 490660446 122441728 18541 4294967295 134512640 134672761 3221224624 3220111824 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+960.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41009 0 0 0 95883 129 0 0 25 0 1 0 490660446 122441728 18541 4294967295 134512640 134672761 3221224624 3219113136 134594095 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+970.053 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41009 0 0 0 96883 129 0 0 25 0 1 0 490660446 122441728 18541 4294967295 134512640 134672761 3221224624 3218831376 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+980.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41009 0 0 0 97883 130 0 0 25 0 1 0 490660446 122441728 18541 4294967295 134512640 134672761 3221224624 3218502288 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+990.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41009 0 0 0 98883 130 0 0 25 0 1 0 490660446 122441728 18541 4294967295 134512640 134672761 3221224624 3217991568 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18541 603 41 0 29852 0
vsize: 119572
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41009 0 0 0 99883 130 0 0 25 0 1 0 490660446 122441728 18541 4294967295 134512640 134672761 3221224624 3217402896 134594089 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.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41369 0 0 0 100882 131 0 0 25 0 1 0 490660446 123318272 18818 4294967295 134512640 134672761 3221224624 3219559040 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30107 18818 603 41 0 30066 0
vsize: 120428
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41460 0 0 0 101882 132 0 0 25 0 1 0 490660446 123453440 18909 4294967295 134512640 134672761 3221224624 3220550624 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30140 18909 603 41 0 30099 0
vsize: 120560
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 41533 0 0 0 102882 132 0 0 25 0 1 0 490660446 123723776 18982 4294967295 134512640 134672761 3221224624 3221138432 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30206 18982 603 41 0 30165 0
vsize: 120824
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 42114 0 0 0 103880 133 0 0 25 0 1 0 490660446 124223488 19272 4294967295 134512640 134672761 3221224624 3220483056 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30328 19272 603 41 0 30287 0
vsize: 121312
[startup+1047.93 s]
Raw data (loadavg): 0.99 0.97 0.92 1/53 7904
Raw data (stat): 7902 (minisat+) R 7901 25285 25284 0 -1 0 42114 0 0 0 103880 133 0 0 25 0 1 0 490660446 124223488 19272 4294967295 134512640 134672761 3221224624 3220483056 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30328 19272 603 41 0 30287 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1047.92
CPU time (s): 1048.01
CPU user time (s): 1045.93
CPU system time (s): 2.08168
CPU usage (%): 100.008
Max. virtual memory (Kb): 121312
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####