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 15009

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        774372 kB
Buffers:         10476 kB
Cached:         217528 kB
SwapCached:          0 kB
Active:          66276 kB
Inactive:       164548 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        774092 kB
SwapTotal:     2097892 kB
SwapFree:      2097824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            23844 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 02:56:12 (client local time) WITH STATUS 0 IN 1061.47 SECONDS
stats: 18679 7 1061.47 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.82 0.94 0.92 1/54 10340
Raw data (stat): 10340 (runsolver) D 10339 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 541538096 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0139 s]
Raw data (loadavg): 0.85 0.94 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 23768 0 0 0 929 65 0 0 25 0 1 0 541538096 69439488 8007 4294967295 134512640 134672761 3221224544 3220407600 134594229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16953 8007 603 41 0 16912 0
vsize: 67812
[startup+20.0275 s]
Raw data (loadavg): 0.87 0.94 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 23768 0 0 0 1930 65 0 0 25 0 1 0 541538096 69439488 8007 4294967295 134512640 134672761 3221224544 3220918224 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16953 8007 603 41 0 16912 0
vsize: 67812
[startup+30.0271 s]
Raw data (loadavg): 0.89 0.94 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 24113 0 0 0 2929 66 0 0 25 0 1 0 541538096 70852608 8352 4294967295 134512640 134672761 3221224544 3220937040 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17298 8352 603 41 0 17257 0
vsize: 69192
[startup+40.0279 s]
Raw data (loadavg): 0.91 0.94 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 24524 0 0 0 3929 68 0 0 25 0 1 0 541538096 73998336 8763 4294967295 134512640 134672761 3221224544 3220892496 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18066 8763 603 41 0 18025 0
vsize: 72264
[startup+50.0284 s]
Raw data (loadavg): 0.92 0.95 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 24742 0 0 0 4928 68 0 0 25 0 1 0 541538096 74629120 8981 4294967295 134512640 134672761 3221224544 3220198336 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18220 8981 603 41 0 18179 0
vsize: 72880
[startup+60.0285 s]
Raw data (loadavg): 0.93 0.95 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 25489 0 0 0 5926 70 0 0 25 0 1 0 541538096 75976704 9398 4294967295 134512640 134672761 3221224544 3220984288 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18549 9398 603 41 0 18508 0
vsize: 74196
[startup+70.0283 s]
Raw data (loadavg): 0.94 0.95 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 25613 0 0 0 6926 70 0 0 25 0 1 0 541538096 75976704 9522 4294967295 134512640 134672761 3221224544 3220465296 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18549 9522 603 41 0 18508 0
vsize: 74196
[startup+80.0278 s]
Raw data (loadavg): 0.95 0.95 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 25762 0 0 0 7926 71 0 0 25 0 1 0 541538096 76316672 9671 4294967295 134512640 134672761 3221224544 3221079792 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18632 9671 603 41 0 18591 0
vsize: 74528
[startup+90.0279 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 25882 0 0 0 8925 72 0 0 25 0 1 0 541538096 79429632 9708 4294967295 134512640 134672761 3221224544 3219672544 134594047 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19392 9708 603 41 0 19351 0
vsize: 77568
[startup+100.028 s]
Raw data (loadavg): 0.96 0.95 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 26275 0 0 0 9925 72 0 0 25 0 1 0 541538096 80044032 9976 4294967295 134512640 134672761 3221224544 3220429792 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19542 9976 603 41 0 19501 0
vsize: 78168
[startup+110.028 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 28199 0 0 0 10920 78 0 0 25 0 1 0 541538096 84406272 11116 4294967295 134512640 134672761 3221224544 3219726384 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20607 11116 603 41 0 20566 0
vsize: 82428
[startup+120.028 s]
Raw data (loadavg): 0.97 0.95 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 28368 0 0 0 11919 78 0 0 25 0 1 0 541538096 84709376 11243 4294967295 134512640 134672761 3221224544 3220875888 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20681 11243 603 41 0 20640 0
vsize: 82724
[startup+130.028 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 28396 0 0 0 12920 78 0 0 25 0 1 0 541538096 84844544 11271 4294967295 134512640 134672761 3221224544 3220318336 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20714 11271 603 41 0 20673 0
vsize: 82856
[startup+140.029 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 28396 0 0 0 13920 78 0 0 25 0 1 0 541538096 84844544 11271 4294967295 134512640 134672761 3221224544 3219482656 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20714 11271 603 41 0 20673 0
vsize: 82856
[startup+150.028 s]
Raw data (loadavg): 0.98 0.95 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 28776 0 0 0 14919 79 0 0 25 0 1 0 541538096 85721088 11568 4294967295 134512640 134672761 3221224544 3220550736 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20928 11568 603 41 0 20887 0
vsize: 83712
[startup+160.028 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 29029 0 0 0 15919 80 0 0 25 0 1 0 541538096 85868544 11656 4294967295 134512640 134672761 3221224544 3220346544 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20964 11656 603 41 0 20923 0
vsize: 83856
[startup+170.028 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 29185 0 0 0 16918 80 0 0 25 0 1 0 541538096 86171648 11770 4294967295 134512640 134672761 3221224544 3220758400 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21038 11770 603 41 0 20997 0
vsize: 84152
[startup+180.028 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 29185 0 0 0 17918 80 0 0 25 0 1 0 541538096 86171648 11770 4294967295 134512640 134672761 3221224544 3219357184 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21038 11770 603 41 0 20997 0
vsize: 84152
[startup+190.029 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 29543 0 0 0 18918 81 0 0 25 0 1 0 541538096 87048192 12045 4294967295 134512640 134672761 3221224544 3221167248 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21252 12045 603 41 0 21211 0
vsize: 85008
[startup+200.029 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 29846 0 0 0 19917 82 0 0 25 0 1 0 541538096 87199744 12141 4294967295 134512640 134672761 3221224544 3221133760 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21289 12141 603 41 0 21248 0
vsize: 85156
[startup+210.03 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 29935 0 0 0 20917 82 0 0 25 0 1 0 541538096 87470080 12230 4294967295 134512640 134672761 3221224544 3220225680 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21355 12230 603 41 0 21314 0
vsize: 85420
[startup+220.03 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 30363 0 0 0 21916 83 0 0 25 0 1 0 541538096 87785472 12410 4294967295 134512640 134672761 3221224544 3220374288 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21432 12410 603 41 0 21391 0
vsize: 85728
[startup+230.03 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 30516 0 0 0 22916 83 0 0 25 0 1 0 541538096 88223744 12521 4294967295 134512640 134672761 3221224544 3220713952 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21539 12521 603 41 0 21498 0
vsize: 86156
[startup+240.031 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 30516 0 0 0 23917 83 0 0 25 0 1 0 541538096 88223744 12521 4294967295 134512640 134672761 3221224544 3219867040 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21539 12521 603 41 0 21498 0
vsize: 86156
[startup+250.032 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 30845 0 0 0 24916 84 0 0 25 0 1 0 541538096 88965120 12767 4294967295 134512640 134672761 3221224544 3220696176 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21720 12767 603 41 0 21679 0
vsize: 86880
[startup+260.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 31075 0 0 0 25916 85 0 0 25 0 1 0 541538096 95150080 12832 4294967295 134512640 134672761 3221224544 3220393200 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23230 12832 603 41 0 23189 0
vsize: 92920
[startup+270.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 31226 0 0 0 26915 85 0 0 25 0 1 0 541538096 95588352 12941 4294967295 134512640 134672761 3221224544 3220922656 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23337 12941 603 41 0 23296 0
vsize: 93348
[startup+280.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 31226 0 0 0 27915 85 0 0 25 0 1 0 541538096 95588352 12941 4294967295 134512640 134672761 3221224544 3219907840 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23337 12941 603 41 0 23296 0
vsize: 93348
[startup+290.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 31538 0 0 0 28915 86 0 0 25 0 1 0 541538096 96194560 13170 4294967295 134512640 134672761 3221224544 3220438896 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23485 13170 603 41 0 23444 0
vsize: 93940
[startup+300.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 31771 0 0 0 29915 86 0 0 25 0 1 0 541538096 96231424 13238 4294967295 134512640 134672761 3221224544 3220136880 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23494 13238 603 41 0 23453 0
vsize: 93976
[startup+310.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 31934 0 0 0 30914 87 0 0 25 0 1 0 541538096 96669696 13359 4294967295 134512640 134672761 3221224544 3221106000 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23601 13359 603 41 0 23560 0
vsize: 94404
[startup+320.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 31944 0 0 0 31914 87 0 0 25 0 1 0 541538096 96669696 13369 4294967295 134512640 134672761 3221224544 3220114048 134594084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23601 13369 603 41 0 23560 0
vsize: 94404
[startup+330.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 32035 0 0 0 32915 87 0 0 25 0 1 0 541538096 96804864 13460 4294967295 134512640 134672761 3221224544 3219734640 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23634 13460 603 41 0 23593 0
vsize: 94536
[startup+340.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 32469 0 0 0 33914 88 0 0 25 0 1 0 541538096 97353728 13646 4294967295 134512640 134672761 3221224544 3219559056 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23768 13646 603 41 0 23727 0
vsize: 95072
[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 32639 0 0 0 34913 89 0 0 25 0 1 0 541538096 97656832 13774 4294967295 134512640 134672761 3221224544 3220844208 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23842 13774 603 41 0 23801 0
vsize: 95368
[startup+360.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 32669 0 0 0 35913 89 0 0 25 0 1 0 541538096 97792000 13804 4294967295 134512640 134672761 3221224544 3220356544 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23875 13804 603 41 0 23834 0
vsize: 95500
[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 32669 0 0 0 36914 89 0 0 25 0 1 0 541538096 97792000 13804 4294967295 134512640 134672761 3221224544 3219398080 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23875 13804 603 41 0 23834 0
vsize: 95500
[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 35644 0 0 0 37906 96 0 0 25 0 1 0 541538096 103936000 15378 4294967295 134512640 134672761 3221224544 3220637520 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25375 15378 603 41 0 25334 0
vsize: 101500
[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 35909 0 0 0 38906 97 0 0 25 0 1 0 541538096 103997440 15478 4294967295 134512640 134672761 3221224544 3220043376 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25390 15478 603 41 0 25349 0
vsize: 101560
[startup+400.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 36067 0 0 0 39906 97 0 0 25 0 1 0 541538096 104435712 15594 4294967295 134512640 134672761 3221224544 3220950576 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25497 15594 603 41 0 25456 0
vsize: 101988
[startup+410.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 36089 0 0 0 40906 97 0 0 25 0 1 0 541538096 104435712 15616 4294967295 134512640 134672761 3221224544 3220216576 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25497 15616 603 41 0 25456 0
vsize: 101988
[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 36089 0 0 0 41906 97 0 0 25 0 1 0 541538096 104435712 15616 4294967295 134512640 134672761 3221224544 3219460096 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25497 15616 603 41 0 25456 0
vsize: 101988
[startup+430.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 36416 0 0 0 42905 98 0 0 25 0 1 0 541538096 105177088 15860 4294967295 134512640 134672761 3221224544 3220399152 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 15860 603 41 0 25637 0
vsize: 102712
[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 36825 0 0 0 43905 99 0 0 25 0 1 0 541538096 105820160 16069 4294967295 134512640 134672761 3221224544 3219133392 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25835 16069 603 41 0 25794 0
vsize: 103340
[startup+450.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 36994 0 0 0 44906 99 0 0 25 0 1 0 541538096 106123264 16196 4294967295 134512640 134672761 3221224544 3220223376 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25909 16196 603 41 0 25868 0
vsize: 103636
[startup+460.059 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 37038 0 0 0 45907 99 0 0 25 0 1 0 541538096 106258432 16240 4294967295 134512640 134672761 3221224544 3220773168 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25942 16240 603 41 0 25901 0
vsize: 103768
[startup+470.059 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 37071 0 0 0 46907 99 0 0 25 0 1 0 541538096 106393600 16273 4294967295 134512640 134672761 3221224544 3221172624 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25975 16273 603 41 0 25934 0
vsize: 103900
[startup+480.058 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 37076 0 0 0 47907 99 0 0 25 0 1 0 541538096 106393600 16278 4294967295 134512640 134672761 3221224544 3219652480 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25975 16278 603 41 0 25934 0
vsize: 103900
[startup+490.059 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 37076 0 0 0 48907 99 0 0 25 0 1 0 541538096 106393600 16278 4294967295 134512640 134672761 3221224544 3219220096 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25975 16278 603 41 0 25934 0
vsize: 103900
[startup+500.059 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 37076 0 0 0 49908 99 0 0 25 0 1 0 541538096 106393600 16278 4294967295 134512640 134672761 3221224544 3218400832 134594084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25975 16278 603 41 0 25934 0
vsize: 103900
[startup+510.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 37376 0 0 0 50907 100 0 0 25 0 1 0 541538096 107134976 16495 4294967295 134512640 134672761 3221224544 3219452496 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26156 16495 603 41 0 26115 0
vsize: 104624
[startup+520.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 37506 0 0 0 51907 101 0 0 25 0 1 0 541538096 107405312 16625 4294967295 134512640 134672761 3221224544 3220704432 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26222 16625 603 41 0 26181 0
vsize: 104888
[startup+530.061 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 37793 0 0 0 52906 101 0 0 25 0 1 0 541538096 107606016 16710 4294967295 134512640 134672761 3221224544 3218905680 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26271 16710 603 41 0 26230 0
vsize: 105084
[startup+540.061 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 37961 0 0 0 53906 102 0 0 25 0 1 0 541538096 107909120 16836 4294967295 134512640 134672761 3221224544 3220053552 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26345 16836 603 41 0 26304 0
vsize: 105380
[startup+550.061 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38008 0 0 0 54906 102 0 0 25 0 1 0 541538096 108044288 16883 4294967295 134512640 134672761 3221224544 3220615824 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26378 16883 603 41 0 26337 0
vsize: 105512
[startup+560.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38041 0 0 0 55906 102 0 0 25 0 1 0 541538096 108179456 16916 4294967295 134512640 134672761 3221224544 3221019984 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26411 16916 603 41 0 26370 0
vsize: 105644
[startup+570.063 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38057 0 0 0 56906 102 0 0 25 0 1 0 541538096 108179456 16932 4294967295 134512640 134672761 3221224544 3219764416 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+580.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38057 0 0 0 57906 102 0 0 25 0 1 0 541538096 108179456 16932 4294967295 134512640 134672761 3221224544 3219356224 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+590.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38057 0 0 0 58907 102 0 0 25 0 1 0 541538096 108179456 16932 4294967295 134512640 134672761 3221224544 3218911648 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+600.063 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38057 0 0 0 59907 102 0 0 25 0 1 0 541538096 108179456 16932 4294967295 134512640 134672761 3221224544 3218075872 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+610.064 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38382 0 0 0 60906 103 0 0 25 0 1 0 541538096 108920832 17174 4294967295 134512640 134672761 3221224544 3219623472 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26592 17174 603 41 0 26551 0
vsize: 106368
[startup+620.064 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38473 0 0 0 61906 104 0 0 25 0 1 0 541538096 109191168 17265 4294967295 134512640 134672761 3221224544 3220725360 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26658 17265 603 41 0 26617 0
vsize: 106632
[startup+630.064 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38710 0 0 0 62905 104 0 0 25 0 1 0 541538096 109133824 17302 4294967295 134512640 134672761 3221224544 3218975856 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26644 17302 603 41 0 26603 0
vsize: 106576
[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38879 0 0 0 63905 105 0 0 25 0 1 0 541538096 109572096 17429 4294967295 134512640 134672761 3221224544 3220161168 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26751 17429 603 41 0 26710 0
vsize: 107004
[startup+650.064 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38926 0 0 0 64905 105 0 0 25 0 1 0 541538096 109572096 17476 4294967295 134512640 134672761 3221224544 3220730832 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26751 17476 603 41 0 26710 0
vsize: 107004
[startup+660.065 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38959 0 0 0 65905 105 0 0 25 0 1 0 541538096 109707264 17509 4294967295 134512640 134672761 3221224544 3221137584 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26784 17509 603 41 0 26743 0
vsize: 107136
[startup+670.066 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38967 0 0 0 66905 105 0 0 25 0 1 0 541538096 109707264 17517 4294967295 134512640 134672761 3221224544 3219685024 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26784 17517 603 41 0 26743 0
vsize: 107136
[startup+680.066 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38967 0 0 0 67906 105 0 0 25 0 1 0 541538096 109707264 17517 4294967295 134512640 134672761 3221224544 3219265696 134594133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26784 17517 603 41 0 26743 0
vsize: 107136
[startup+690.067 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 38967 0 0 0 68906 105 0 0 25 0 1 0 541538096 109707264 17517 4294967295 134512640 134672761 3221224544 3218533024 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26784 17517 603 41 0 26743 0
vsize: 107136
[startup+700.067 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 39240 0 0 0 69906 106 0 0 25 0 1 0 541538096 110313472 17707 4294967295 134512640 134672761 3221224544 3219134832 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26932 17707 603 41 0 26891 0
vsize: 107728
[startup+710.068 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 39363 0 0 0 70906 106 0 0 25 0 1 0 541538096 110718976 17830 4294967295 134512640 134672761 3221224544 3220622352 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27031 17830 603 41 0 26990 0
vsize: 108124
[startup+720.068 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 39594 0 0 0 71905 106 0 0 25 0 1 0 541538096 110620672 17861 4294967295 134512640 134672761 3221224544 3218837136 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27007 17861 603 41 0 26966 0
vsize: 108028
[startup+730.067 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 39764 0 0 0 72905 107 0 0 25 0 1 0 541538096 110923776 17989 4294967295 134512640 134672761 3221224544 3220118448 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27081 17989 603 41 0 27040 0
vsize: 108324
[startup+740.069 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 39811 0 0 0 73905 107 0 0 25 0 1 0 541538096 111058944 18036 4294967295 134512640 134672761 3221224544 3220704240 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27114 18036 603 41 0 27073 0
vsize: 108456
[startup+750.069 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 39845 0 0 0 74905 107 0 0 25 0 1 0 541538096 111194112 18070 4294967295 134512640 134672761 3221224544 3221116944 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27147 18070 603 41 0 27106 0
vsize: 108588
[startup+760.069 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 39854 0 0 0 75905 107 0 0 25 0 1 0 541538096 111194112 18079 4294967295 134512640 134672761 3221224544 3219707488 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27147 18079 603 41 0 27106 0
vsize: 108588
[startup+770.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 39854 0 0 0 76905 107 0 0 25 0 1 0 541538096 111194112 18079 4294967295 134512640 134672761 3221224544 3219293056 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27147 18079 603 41 0 27106 0
vsize: 108588
[startup+780.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 39854 0 0 0 77905 107 0 0 25 0 1 0 541538096 111194112 18079 4294967295 134512640 134672761 3221224544 3218604256 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27147 18079 603 41 0 27106 0
vsize: 108588
[startup+790.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 40113 0 0 0 78905 108 0 0 25 0 1 0 541538096 111800320 18255 4294967295 134512640 134672761 3221224544 3218958960 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27295 18255 603 41 0 27254 0
vsize: 109180
[startup+800.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 40247 0 0 0 79905 108 0 0 25 0 1 0 541538096 112070656 18389 4294967295 134512640 134672761 3221224544 3220576944 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27361 18389 603 41 0 27320 0
vsize: 109444
[startup+810.072 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 40430 0 0 0 80904 109 0 0 25 0 1 0 541538096 124448768 18372 4294967295 134512640 134672761 3221224544 3218714832 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30383 18372 603 41 0 30342 0
vsize: 121532
[startup+820.072 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 40648 0 0 0 81904 109 0 0 25 0 1 0 541538096 124923904 18548 4294967295 134512640 134672761 3221224544 3220094448 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30499 18548 603 41 0 30458 0
vsize: 121996
[startup+830.072 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 40697 0 0 0 82904 109 0 0 25 0 1 0 541538096 125059072 18597 4294967295 134512640 134672761 3221224544 3220693296 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30532 18597 603 41 0 30491 0
vsize: 122128
[startup+840.073 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 40731 0 0 0 83905 109 0 0 25 0 1 0 541538096 125194240 18631 4294967295 134512640 134672761 3221224544 3221111088 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30565 18631 603 41 0 30524 0
vsize: 122260
[startup+850.072 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 40740 0 0 0 84905 109 0 0 25 0 1 0 541538096 125194240 18640 4294967295 134512640 134672761 3221224544 3219721024 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30565 18640 603 41 0 30524 0
vsize: 122260
[startup+860.073 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 40740 0 0 0 85905 109 0 0 25 0 1 0 541538096 125194240 18640 4294967295 134512640 134672761 3221224544 3219304192 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30565 18640 603 41 0 30524 0
vsize: 122260
[startup+870.074 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 40740 0 0 0 86905 109 0 0 25 0 1 0 541538096 125194240 18640 4294967295 134512640 134672761 3221224544 3218605696 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30565 18640 603 41 0 30524 0
vsize: 122260
[startup+880.074 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41004 0 0 0 87905 110 0 0 25 0 1 0 541538096 125800448 18821 4294967295 134512640 134672761 3221224544 3219001104 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30713 18821 603 41 0 30672 0
vsize: 122852
[startup+890.074 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41133 0 0 0 88904 110 0 0 25 0 1 0 541538096 126070784 18950 4294967295 134512640 134672761 3221224544 3220591440 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30779 18950 603 41 0 30738 0
vsize: 123116
[startup+900.074 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41447 0 0 0 89904 111 0 0 25 0 1 0 541538096 126423040 19057 4294967295 134512640 134672761 3221224544 3218145360 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30865 19057 603 41 0 30824 0
vsize: 123460
[startup+910.074 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41661 0 0 0 90904 111 0 0 25 0 1 0 541538096 126898176 19229 4294967295 134512640 134672761 3221224544 3219479472 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30981 19229 603 41 0 30940 0
vsize: 123924
[startup+920.074 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41709 0 0 0 91904 111 0 0 25 0 1 0 541538096 127033344 19277 4294967295 134512640 134672761 3221224544 3220072848 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31014 19277 603 41 0 30973 0
vsize: 124056
[startup+930.074 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41744 0 0 0 92904 111 0 0 25 0 1 0 541538096 127168512 19312 4294967295 134512640 134672761 3221224544 3220488432 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31047 19312 603 41 0 31006 0
vsize: 124188
[startup+940.075 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41771 0 0 0 93905 111 0 0 25 0 1 0 541538096 127168512 19339 4294967295 134512640 134672761 3221224544 3220826352 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31047 19339 603 41 0 31006 0
vsize: 124188
[startup+950.075 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41795 0 0 0 94905 111 0 0 25 0 1 0 541538096 127303680 19363 4294967295 134512640 134672761 3221224544 3221111952 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31080 19363 603 41 0 31039 0
vsize: 124320
[startup+960.076 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41805 0 0 0 95905 111 0 0 25 0 1 0 541538096 127303680 19373 4294967295 134512640 134672761 3221224544 3219530560 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+970.075 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41805 0 0 0 96905 111 0 0 25 0 1 0 541538096 127303680 19373 4294967295 134512640 134672761 3221224544 3219025312 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+980.075 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41805 0 0 0 97905 111 0 0 25 0 1 0 541538096 127303680 19373 4294967295 134512640 134672761 3221224544 3218730400 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+990.075 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41805 0 0 0 98905 111 0 0 25 0 1 0 541538096 127303680 19373 4294967295 134512640 134672761 3221224544 3218382880 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41805 0 0 0 99906 111 0 0 25 0 1 0 541538096 127303680 19373 4294967295 134512640 134672761 3221224544 3217804768 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 41805 0 0 0 100906 111 0 0 25 0 1 0 541538096 127303680 19373 4294967295 134512640 134672761 3221224544 3217308640 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 42164 0 0 0 101906 112 0 0 25 0 1 0 541538096 128180224 19649 4294967295 134512640 134672761 3221224544 3219557232 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31294 19649 603 41 0 31253 0
vsize: 125176
[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 42246 0 0 0 102906 112 0 0 25 0 1 0 541538096 128315392 19731 4294967295 134512640 134672761 3221224544 3220471920 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31327 19731 603 41 0 31286 0
vsize: 125308
[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 42319 0 0 0 103906 112 0 0 25 0 1 0 541538096 128585728 19804 4294967295 134512640 134672761 3221224544 3221064240 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31393 19804 603 41 0 31352 0
vsize: 125572
[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 42907 0 0 0 104904 113 0 0 25 0 1 0 541538096 129081344 20101 4294967295 134512640 134672761 3221224544 3221185680 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31514 20101 603 41 0 31473 0
vsize: 126056
[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 83059 0 0 0 105807 211 0 0 25 0 1 0 541538096 273059840 57647 4294967295 134512640 134672761 3221224544 3216295152 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66665 57648 603 41 0 66624 0
vsize: 266660
[startup+1061.36 s]
Raw data (loadavg): 0.99 0.97 0.92 1/53 10340
Raw data (stat): 10340 (minisat+) R 10339 11931 11930 0 -1 0 83059 0 0 0 105807 211 0 0 25 0 1 0 541538096 273059840 57647 4294967295 134512640 134672761 3221224544 3216295152 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66665 57648 603 41 0 66624 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1061.36
CPU time (s): 1061.47
CPU user time (s): 1059.04
CPU system time (s): 2.43563
CPU usage (%): 100.011
Max. virtual memory (Kb): 266660
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####