PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        682460 kB
Buffers:         12768 kB
Cached:         315148 kB
SwapCached:        524 kB
Active:          82104 kB
Inactive:       247800 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        682180 kB
SwapTotal:     2097892 kB
SwapFree:      2096460 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            16688 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:32:09 (client local time) WITH STATUS 0 IN 1042.08 SECONDS
stats: 18681 7 1042.08 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.96 2/54 31304
Raw data (stat): 31304 (runsolver) R 31303 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545356223 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.87 0.95 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 22973 0 0 0 937 62 0 0 25 0 1 0 545356223 64581632 7176 4294967295 134512640 134672761 3221224544 3220521264 134594252 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.0029 s]
Raw data (loadavg): 0.89 0.96 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 22973 0 0 0 1937 62 0 0 25 0 1 0 545356223 64581632 7176 4294967295 134512640 134672761 3221224544 3220958928 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+30.0037 s]
Raw data (loadavg): 0.91 0.96 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 23318 0 0 0 2935 64 0 0 25 0 1 0 545356223 65994752 7521 4294967295 134512640 134672761 3221224544 3220968816 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16112 7521 603 41 0 16071 0
vsize: 64448
[startup+40.0055 s]
Raw data (loadavg): 0.92 0.96 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 23730 0 0 0 3935 64 0 0 25 0 1 0 545356223 69140480 7933 4294967295 134512640 134672761 3221224544 3220920336 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16880 7933 603 41 0 16839 0
vsize: 67520
[startup+50.0062 s]
Raw data (loadavg): 0.93 0.96 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 23947 0 0 0 4934 65 0 0 25 0 1 0 545356223 69771264 8150 4294967295 134512640 134672761 3221224544 3220229152 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17034 8150 603 41 0 16993 0
vsize: 68136
[startup+60.0061 s]
Raw data (loadavg): 0.94 0.96 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 24694 0 0 0 5932 67 0 0 25 0 1 0 545356223 71118848 8567 4294967295 134512640 134672761 3221224544 3220932736 134594101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17363 8567 603 41 0 17322 0
vsize: 69452
[startup+70.0069 s]
Raw data (loadavg): 0.95 0.96 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 24820 0 0 0 6932 67 0 0 25 0 1 0 545356223 71118848 8693 4294967295 134512640 134672761 3221224544 3220519920 134594226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17363 8693 603 41 0 17322 0
vsize: 69452
[startup+80.0076 s]
Raw data (loadavg): 0.96 0.96 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 24968 0 0 0 7932 68 0 0 25 0 1 0 545356223 71458816 8841 4294967295 134512640 134672761 3221224544 3221102064 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17446 8841 603 41 0 17405 0
vsize: 69784
[startup+90.0084 s]
Raw data (loadavg): 0.96 0.96 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 25087 0 0 0 8931 69 0 0 25 0 1 0 545356223 74571776 8877 4294967295 134512640 134672761 3221224544 3219661312 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18206 8877 603 41 0 18165 0
vsize: 72824
[startup+100.009 s]
Raw data (loadavg): 0.97 0.96 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 25480 0 0 0 9931 69 0 0 25 0 1 0 545356223 75186176 9145 4294967295 134512640 134672761 3221224544 3220450624 134594133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18356 9145 603 41 0 18315 0
vsize: 73424
[startup+110.01 s]
Raw data (loadavg): 0.97 0.96 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 27404 0 0 0 10925 75 0 0 25 0 1 0 545356223 79548416 10285 4294967295 134512640 134672761 3221224544 3219738960 134594231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19421 10285 603 41 0 19380 0
vsize: 77684
[startup+120.011 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 27567 0 0 0 11924 76 0 0 25 0 1 0 545356223 79851520 10406 4294967295 134512640 134672761 3221224544 3220808976 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19495 10406 603 41 0 19454 0
vsize: 77980
[startup+130.012 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 27601 0 0 0 12924 76 0 0 25 0 1 0 545356223 79986688 10440 4294967295 134512640 134672761 3221224544 3220372576 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19528 10440 603 41 0 19487 0
vsize: 78112
[startup+140.012 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 27601 0 0 0 13924 76 0 0 25 0 1 0 545356223 79986688 10440 4294967295 134512640 134672761 3221224544 3219360064 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19528 10440 603 41 0 19487 0
vsize: 78112
[startup+150.026 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 27993 0 0 0 14925 77 0 0 25 0 1 0 545356223 80998400 10749 4294967295 134512640 134672761 3221224544 3220656336 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19775 10749 603 41 0 19734 0
vsize: 79100
[startup+160.026 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 28232 0 0 0 15924 78 0 0 25 0 1 0 545356223 81010688 10823 4294967295 134512640 134672761 3221224544 3220325328 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19778 10823 603 41 0 19737 0
vsize: 79112
[startup+170.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 28389 0 0 0 16923 79 0 0 25 0 1 0 545356223 81313792 10938 4294967295 134512640 134672761 3221224544 3221080864 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19852 10938 603 41 0 19811 0
vsize: 79408
[startup+180.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 28389 0 0 0 17923 79 0 0 25 0 1 0 545356223 81313792 10938 4294967295 134512640 134672761 3221224544 3219863392 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19852 10938 603 41 0 19811 0
vsize: 79408
[startup+190.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 28740 0 0 0 18923 80 0 0 25 0 1 0 545356223 82190336 11206 4294967295 134512640 134672761 3221224544 3221069712 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20066 11206 603 41 0 20025 0
vsize: 80264
[startup+200.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 28959 0 0 0 19922 80 0 0 25 0 1 0 545356223 82173952 11260 4294967295 134512640 134672761 3221224544 3221113968 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20062 11260 603 41 0 20021 0
vsize: 80248
[startup+210.028 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 29050 0 0 0 20922 81 0 0 25 0 1 0 545356223 82341888 11309 4294967295 134512640 134672761 3221224544 3219599296 134594101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20103 11309 603 41 0 20062 0
vsize: 80412
[startup+220.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 29544 0 0 0 21921 82 0 0 25 0 1 0 545356223 82927616 11555 4294967295 134512640 134672761 3221224544 3220084176 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20246 11555 603 41 0 20205 0
vsize: 80984
[startup+230.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 29707 0 0 0 22920 83 0 0 25 0 1 0 545356223 83230720 11676 4294967295 134512640 134672761 3221224544 3221063376 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20320 11676 603 41 0 20279 0
vsize: 81280
[startup+240.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 29721 0 0 0 23920 83 0 0 25 0 1 0 545356223 83365888 11690 4294967295 134512640 134672761 3221224544 3220153312 134594131 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.031 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 30023 0 0 0 24920 84 0 0 25 0 1 0 545356223 83972096 11909 4294967295 134512640 134672761 3221224544 3220373232 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20501 11909 603 41 0 20460 0
vsize: 82004
[startup+260.032 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 30255 0 0 0 25919 84 0 0 25 0 1 0 545356223 90292224 11976 4294967295 134512640 134672761 3221224544 3220087920 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22044 11976 603 41 0 22003 0
vsize: 88176
[startup+270.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 30416 0 0 0 26919 85 0 0 25 0 1 0 545356223 90595328 12095 4294967295 134512640 134672761 3221224544 3221033136 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22118 12095 603 41 0 22077 0
vsize: 88472
[startup+280.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 30431 0 0 0 27919 85 0 0 25 0 1 0 545356223 90730496 12110 4294967295 134512640 134672761 3221224544 3220179040 134594101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22151 12110 603 41 0 22110 0
vsize: 88604
[startup+290.033 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 30544 0 0 0 28918 86 0 0 25 0 1 0 545356223 91000832 12223 4294967295 134512640 134672761 3221224544 3220024272 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22217 12223 603 41 0 22176 0
vsize: 88868
[startup+300.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 30959 0 0 0 29917 87 0 0 25 0 1 0 545356223 91373568 12390 4294967295 134512640 134672761 3221224544 3219794832 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22308 12390 603 41 0 22267 0
vsize: 89232
[startup+310.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 31122 0 0 0 30917 87 0 0 25 0 1 0 545356223 91676672 12511 4294967295 134512640 134672761 3221224544 3220903824 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22382 12511 603 41 0 22341 0
vsize: 89528
[startup+320.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 31148 0 0 0 31917 87 0 0 25 0 1 0 545356223 91811840 12537 4294967295 134512640 134672761 3221224544 3220331584 134594095 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.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 31148 0 0 0 32917 87 0 0 25 0 1 0 545356223 91811840 12537 4294967295 134512640 134672761 3221224544 3218740000 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22415 12537 603 41 0 22374 0
vsize: 89660
[startup+340.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 31526 0 0 0 33916 88 0 0 25 0 1 0 545356223 92688384 12832 4294967295 134512640 134672761 3221224544 3221207472 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22629 12832 603 41 0 22588 0
vsize: 90516
[startup+350.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 31824 0 0 0 34915 89 0 0 25 0 1 0 545356223 92798976 12923 4294967295 134512640 134672761 3221224544 3220608720 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22656 12923 603 41 0 22615 0
vsize: 90624
[startup+360.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 31874 0 0 0 35915 89 0 0 25 0 1 0 545356223 92934144 12973 4294967295 134512640 134672761 3221224544 3220550464 134594086 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.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 31874 0 0 0 36915 90 0 0 25 0 1 0 545356223 92934144 12973 4294967295 134512640 134672761 3221224544 3219785152 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22689 12973 603 41 0 22648 0
vsize: 90756
[startup+380.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 34818 0 0 0 37909 96 0 0 25 0 1 0 545356223 98942976 14516 4294967295 134512640 134672761 3221224544 3220256016 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24156 14516 603 41 0 24115 0
vsize: 96624
[startup+390.039 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 35086 0 0 0 38908 97 0 0 25 0 1 0 545356223 99139584 14619 4294967295 134512640 134672761 3221224544 3219538608 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24204 14619 603 41 0 24163 0
vsize: 96816
[startup+400.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 35249 0 0 0 39907 98 0 0 25 0 1 0 545356223 99442688 14740 4294967295 134512640 134672761 3221224544 3220685520 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24278 14740 603 41 0 24237 0
vsize: 97112
[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 35294 0 0 0 40907 98 0 0 25 0 1 0 545356223 99577856 14785 4294967295 134512640 134672761 3221224544 3220426336 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14785 603 41 0 24270 0
vsize: 97244
[startup+420.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 35294 0 0 0 41907 99 0 0 25 0 1 0 545356223 99577856 14785 4294967295 134512640 134672761 3221224544 3219715072 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 14785 603 41 0 24270 0
vsize: 97244
[startup+430.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 35588 0 0 0 42906 100 0 0 25 0 1 0 545356223 100319232 14996 4294967295 134512640 134672761 3221224544 3220003920 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24492 14996 603 41 0 24451 0
vsize: 97968
[startup+440.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 35918 0 0 0 43905 101 0 0 25 0 1 0 545356223 100655104 15126 4294967295 134512640 134672761 3221224544 3218221680 134594220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24574 15126 603 41 0 24533 0
vsize: 98296
[startup+450.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 36174 0 0 0 44904 102 0 0 25 0 1 0 545356223 101265408 15340 4294967295 134512640 134672761 3221224544 3219927216 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24723 15340 603 41 0 24682 0
vsize: 98892
[startup+460.042 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 36227 0 0 0 45903 102 0 0 25 0 1 0 545356223 101400576 15393 4294967295 134512640 134672761 3221224544 3220572144 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24756 15393 603 41 0 24715 0
vsize: 99024
[startup+470.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 36265 0 0 0 46903 103 0 0 25 0 1 0 545356223 101535744 15431 4294967295 134512640 134672761 3221224544 3221038416 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15431 603 41 0 24748 0
vsize: 99156
[startup+480.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 36281 0 0 0 47903 103 0 0 25 0 1 0 545356223 101535744 15447 4294967295 134512640 134672761 3221224544 3219762784 134594089 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.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 36281 0 0 0 48903 103 0 0 25 0 1 0 545356223 101535744 15447 4294967295 134512640 134672761 3221224544 3219337408 134594101 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.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 36281 0 0 0 49903 104 0 0 25 0 1 0 545356223 101535744 15447 4294967295 134512640 134672761 3221224544 3218536768 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24789 15447 603 41 0 24748 0
vsize: 99156
[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 36582 0 0 0 50902 104 0 0 25 0 1 0 545356223 102277120 15665 4294967295 134512640 134672761 3221224544 3219473616 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24970 15665 603 41 0 24929 0
vsize: 99880
[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 36714 0 0 0 51901 105 0 0 25 0 1 0 545356223 102547456 15797 4294967295 134512640 134672761 3221224544 3220726992 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25036 15797 603 41 0 24995 0
vsize: 100144
[startup+530.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 37001 0 0 0 52900 106 0 0 25 0 1 0 545356223 102744064 15882 4294967295 134512640 134672761 3221224544 3219013936 134522987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25084 15882 603 41 0 25043 0
vsize: 100336
[startup+540.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 37164 0 0 0 53900 107 0 0 25 0 1 0 545356223 103047168 16003 4294967295 134512640 134672761 3221224544 3220022736 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25158 16003 603 41 0 25117 0
vsize: 100632
[startup+550.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 37211 0 0 0 54900 107 0 0 25 0 1 0 545356223 103182336 16050 4294967295 134512640 134672761 3221224544 3220600944 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25191 16050 603 41 0 25150 0
vsize: 100764
[startup+560.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 37246 0 0 0 55900 107 0 0 25 0 1 0 545356223 103317504 16085 4294967295 134512640 134672761 3221224544 3221026992 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25224 16085 603 41 0 25183 0
vsize: 100896
[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 37262 0 0 0 56900 107 0 0 25 0 1 0 545356223 103317504 16101 4294967295 134512640 134672761 3221224544 3219688384 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+580.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 37262 0 0 0 57900 107 0 0 25 0 1 0 545356223 103317504 16101 4294967295 134512640 134672761 3221224544 3219324064 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+590.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 37262 0 0 0 58900 107 0 0 25 0 1 0 545356223 103317504 16101 4294967295 134512640 134672761 3221224544 3218834176 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.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 37262 0 0 0 59900 107 0 0 25 0 1 0 545356223 103317504 16101 4294967295 134512640 134672761 3221224544 3217809472 134594101 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.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 37630 0 0 0 60900 108 0 0 25 0 1 0 545356223 104194048 16386 4294967295 134512640 134672761 3221224544 3220143024 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25438 16386 603 41 0 25397 0
vsize: 101752
[startup+620.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 37707 0 0 0 61900 108 0 0 25 0 1 0 545356223 104464384 16463 4294967295 134512640 134672761 3221224544 3221045424 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25504 16463 603 41 0 25463 0
vsize: 102016
[startup+630.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 37958 0 0 0 62899 109 0 0 25 0 1 0 545356223 104411136 16514 4294967295 134512640 134672761 3221224544 3219644208 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25491 16514 603 41 0 25450 0
vsize: 101964
[startup+640.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 38102 0 0 0 63899 109 0 0 25 0 1 0 545356223 104714240 16616 4294967295 134512640 134672761 3221224544 3220383216 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25565 16616 603 41 0 25524 0
vsize: 102260
[startup+650.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 38143 0 0 0 64900 109 0 0 25 0 1 0 545356223 104849408 16657 4294967295 134512640 134672761 3221224544 3220891152 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16657 603 41 0 25557 0
vsize: 102392
[startup+660.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 38171 0 0 0 65900 109 0 0 25 0 1 0 545356223 104849408 16685 4294967295 134512640 134672761 3221224544 3220279360 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25598 16685 603 41 0 25557 0
vsize: 102392
[startup+670.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 38171 0 0 0 66900 109 0 0 25 0 1 0 545356223 104849408 16685 4294967295 134512640 134672761 3221224544 3219507232 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+680.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 38171 0 0 0 67900 109 0 0 25 0 1 0 545356223 104849408 16685 4294967295 134512640 134672761 3221224544 3218983168 134594092 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.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 38171 0 0 0 68900 109 0 0 25 0 1 0 545356223 104849408 16685 4294967295 134512640 134672761 3221224544 3217866784 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.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 38544 0 0 0 69900 110 0 0 25 0 1 0 545356223 105725952 16975 4294967295 134512640 134672761 3221224544 3220329168 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25812 16975 603 41 0 25771 0
vsize: 103248
[startup+710.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 38615 0 0 0 70900 110 0 0 25 0 1 0 545356223 105861120 17046 4294967295 134512640 134672761 3221224544 3221204112 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25845 17046 603 41 0 25804 0
vsize: 103380
[startup+720.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 38947 0 0 0 71899 111 0 0 25 0 1 0 545356223 106065920 17136 4294967295 134512640 134672761 3221224544 3219862800 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25895 17136 603 41 0 25854 0
vsize: 103580
[startup+730.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39002 0 0 0 72900 111 0 0 25 0 1 0 545356223 106201088 17191 4294967295 134512640 134672761 3221224544 3220521840 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25928 17191 603 41 0 25887 0
vsize: 103712
[startup+740.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39040 0 0 0 73900 111 0 0 25 0 1 0 545356223 106336256 17229 4294967295 134512640 134672761 3221224544 3220994640 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 17229 603 41 0 25920 0
vsize: 103844
[startup+750.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39058 0 0 0 74900 111 0 0 25 0 1 0 545356223 106336256 17247 4294967295 134512640 134672761 3221224544 3219803104 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+760.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39058 0 0 0 75900 111 0 0 25 0 1 0 545356223 106336256 17247 4294967295 134512640 134672761 3221224544 3219397984 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.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39058 0 0 0 76900 111 0 0 25 0 1 0 545356223 106336256 17247 4294967295 134512640 134672761 3221224544 3218804032 134594106 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.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39329 0 0 0 77900 111 0 0 25 0 1 0 545356223 106942464 17435 4294967295 134512640 134672761 3221224544 3219086832 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26109 17435 603 41 0 26068 0
vsize: 104436
[startup+790.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39452 0 0 0 78900 111 0 0 25 0 1 0 545356223 107212800 17558 4294967295 134512640 134672761 3221224544 3220585296 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26175 17558 603 41 0 26134 0
vsize: 104700
[startup+800.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39688 0 0 0 79899 112 0 0 25 0 1 0 545356223 119758848 17594 4294967295 134512640 134672761 3221224544 3218865744 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29238 17594 603 41 0 29197 0
vsize: 116952
[startup+810.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39850 0 0 0 80899 112 0 0 25 0 1 0 545356223 120061952 17714 4294967295 134512640 134672761 3221224544 3220055760 134594223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29312 17714 603 41 0 29271 0
vsize: 117248
[startup+820.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39899 0 0 0 81899 112 0 0 25 0 1 0 545356223 120197120 17763 4294967295 134512640 134672761 3221224544 3220660944 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29345 17763 603 41 0 29304 0
vsize: 117380
[startup+830.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39936 0 0 0 82899 113 0 0 25 0 1 0 545356223 120332288 17800 4294967295 134512640 134672761 3221224544 3221102736 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29378 17800 603 41 0 29337 0
vsize: 117512
[startup+840.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39945 0 0 0 83900 113 0 0 25 0 1 0 545356223 120332288 17809 4294967295 134512640 134672761 3221224544 3219710080 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+850.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39945 0 0 0 84900 113 0 0 25 0 1 0 545356223 120332288 17809 4294967295 134512640 134672761 3221224544 3219267520 134594089 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.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 39945 0 0 0 85900 113 0 0 25 0 1 0 545356223 120332288 17809 4294967295 134512640 134672761 3221224544 3218330368 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.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 40268 0 0 0 86899 114 0 0 25 0 1 0 545356223 121073664 18049 4294967295 134512640 134672761 3221224544 3219733488 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29559 18049 603 41 0 29518 0
vsize: 118236
[startup+880.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 40361 0 0 0 87899 114 0 0 25 0 1 0 545356223 121344000 18142 4294967295 134512640 134672761 3221224544 3220871760 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29625 18142 603 41 0 29584 0
vsize: 118500
[startup+890.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 40726 0 0 0 88899 114 0 0 25 0 1 0 545356223 121733120 18300 4294967295 134512640 134672761 3221224544 3218796432 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29720 18300 603 41 0 29679 0
vsize: 118880
[startup+900.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 40879 0 0 0 89899 115 0 0 25 0 1 0 545356223 122036224 18411 4294967295 134512640 134672761 3221224544 3219644400 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29794 18411 603 41 0 29753 0
vsize: 119176
[startup+910.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 40924 0 0 0 90898 115 0 0 25 0 1 0 545356223 122171392 18456 4294967295 134512640 134672761 3221224544 3220186320 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29827 18456 603 41 0 29786 0
vsize: 119308
[startup+920.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 40957 0 0 0 91899 115 0 0 25 0 1 0 545356223 122306560 18489 4294967295 134512640 134672761 3221224544 3220590672 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29860 18489 603 41 0 29819 0
vsize: 119440
[startup+930.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 40983 0 0 0 92899 115 0 0 25 0 1 0 545356223 122306560 18515 4294967295 134512640 134672761 3221224544 3220911984 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29860 18515 603 41 0 29819 0
vsize: 119440
[startup+940.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 41006 0 0 0 93899 115 0 0 25 0 1 0 545356223 122441728 18538 4294967295 134512640 134672761 3221224544 3221189232 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29893 18538 603 41 0 29852 0
vsize: 119572
[startup+950.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 41009 0 0 0 94899 115 0 0 25 0 1 0 545356223 122441728 18541 4294967295 134512640 134672761 3221224544 3219222880 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.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 41009 0 0 0 95899 115 0 0 25 0 1 0 545356223 122441728 18541 4294967295 134512640 134672761 3221224544 3218935168 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+970.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 41009 0 0 0 96899 115 0 0 25 0 1 0 545356223 122441728 18541 4294967295 134512640 134672761 3221224544 3218614336 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+980.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 41009 0 0 0 97900 115 0 0 25 0 1 0 545356223 122441728 18541 4294967295 134512640 134672761 3221224544 3218216224 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.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 41009 0 0 0 98900 115 0 0 25 0 1 0 545356223 122441728 18541 4294967295 134512640 134672761 3221224544 3217521568 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+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 41329 0 0 0 99900 116 0 0 25 0 1 0 545356223 123183104 18778 4294967295 134512640 134672761 3221224544 3219068112 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30074 18778 603 41 0 30033 0
vsize: 120296
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 41432 0 0 0 100899 116 0 0 25 0 1 0 545356223 123453440 18881 4294967295 134512640 134672761 3221224544 3220320816 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30140 18881 603 41 0 30099 0
vsize: 120560
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 41513 0 0 0 101899 117 0 0 25 0 1 0 545356223 123723776 18962 4294967295 134512640 134672761 3221224544 3220984560 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30206 18962 603 41 0 30165 0
vsize: 120824
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 41971 0 0 0 102898 118 0 0 25 0 1 0 545356223 124088320 19171 4294967295 134512640 134672761 3221224544 3220725856 134594124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30295 19171 603 41 0 30254 0
vsize: 121180
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 63208 0 0 0 103846 171 0 0 25 0 1 0 545356223 185774080 37757 4294967295 134512640 134672761 3221224544 3220159664 134556917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45355 37762 603 41 0 45314 0
vsize: 181420
[startup+1041.97 s]
Raw data (loadavg): 0.99 0.97 0.96 1/53 31304
Raw data (stat): 31304 (minisat+) R 31303 27222 27221 0 -1 0 63208 0 0 0 103846 171 0 0 25 0 1 0 545356223 185774080 37757 4294967295 134512640 134672761 3221224544 3220159664 134556917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45355 37762 603 41 0 45314 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1041.97
CPU time (s): 1042.08
CPU user time (s): 1040.05
CPU system time (s): 2.02769
CPU usage (%): 100.01
Max. virtual memory (Kb): 181420
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####