PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.031
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:        293156 kB
Buffers:         35472 kB
Cached:         674968 kB
SwapCached:         24 kB
Active:         258312 kB
Inactive:       454856 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        292904 kB
SwapTotal:     2097892 kB
SwapFree:      2097660 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6640 kB
Slab:            22564 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 15:53:04 (client local time) WITH STATUS 0 IN 1091.18 SECONDS
stats: 17860 7 1091.18 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.77 0.90 0.90 2/54 4131
Raw data (stat): 4131 (runsolver) R 4130 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546198114 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.80 0.90 0.90 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 23768 0 0 0 934 64 0 0 25 0 1 0 546198114 69439488 8007 4294967295 134512640 134672761 3221224544 3220430832 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+20.001 s]
Raw data (loadavg): 0.83 0.91 0.90 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 23768 0 0 0 1934 64 0 0 25 0 1 0 546198114 69439488 8007 4294967295 134512640 134672761 3221224544 3220889232 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.0007 s]
Raw data (loadavg): 0.86 0.91 0.90 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 24113 0 0 0 2934 65 0 0 25 0 1 0 546198114 70852608 8352 4294967295 134512640 134672761 3221224544 3220871376 134594223 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.0014 s]
Raw data (loadavg): 0.88 0.91 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 24516 0 0 0 3933 66 0 0 25 0 1 0 546198114 73998336 8755 4294967295 134512640 134672761 3221224544 3220632720 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18066 8755 603 41 0 18025 0
vsize: 72264
[startup+50.0022 s]
Raw data (loadavg): 0.90 0.91 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 24742 0 0 0 4933 67 0 0 25 0 1 0 546198114 74629120 8981 4294967295 134512640 134672761 3221224544 3220301728 134594084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18220 8981 603 41 0 18179 0
vsize: 72880
[startup+60.009 s]
Raw data (loadavg): 0.91 0.92 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 25488 0 0 0 5932 69 0 0 25 0 1 0 546198114 75976704 9397 4294967295 134512640 134672761 3221224544 3221219184 134594220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18549 9397 603 41 0 18508 0
vsize: 74196
[startup+70.0094 s]
Raw data (loadavg): 0.93 0.92 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 25602 0 0 0 6931 69 0 0 25 0 1 0 546198114 75976704 9511 4294967295 134512640 134672761 3221224544 3220093872 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18549 9511 603 41 0 18508 0
vsize: 74196
[startup+80.0091 s]
Raw data (loadavg): 0.94 0.92 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 25745 0 0 0 7931 69 0 0 25 0 1 0 546198114 76316672 9654 4294967295 134512640 134672761 3221224544 3220537584 134594212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18632 9654 603 41 0 18591 0
vsize: 74528
[startup+90.0098 s]
Raw data (loadavg): 0.95 0.92 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 25882 0 0 0 8931 69 0 0 25 0 1 0 546198114 79429632 9708 4294967295 134512640 134672761 3221224544 3220224064 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19392 9708 603 41 0 19351 0
vsize: 77568
[startup+100.01 s]
Raw data (loadavg): 0.95 0.92 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 26271 0 0 0 9931 70 0 0 25 0 1 0 546198114 80044032 9972 4294967295 134512640 134672761 3221224544 3221169552 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19542 9972 603 41 0 19501 0
vsize: 78168
[startup+110.009 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 26810 0 0 0 10929 72 0 0 25 0 1 0 546198114 81399808 10386 4294967295 134512640 134672761 3221224544 3219235056 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19873 10386 603 41 0 19832 0
vsize: 79492
[startup+120.01 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 28346 0 0 0 11926 75 0 0 25 0 1 0 546198114 84709376 11221 4294967295 134512640 134672761 3221224544 3220621680 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20681 11221 603 41 0 20640 0
vsize: 82724
[startup+130.01 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 28396 0 0 0 12926 75 0 0 25 0 1 0 546198114 84844544 11271 4294967295 134512640 134672761 3221224544 3221067616 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20714 11271 603 41 0 20673 0
vsize: 82856
[startup+140.011 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 28396 0 0 0 13926 75 0 0 25 0 1 0 546198114 84844544 11271 4294967295 134512640 134672761 3221224544 3219893824 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20714 11271 603 41 0 20673 0
vsize: 82856
[startup+150.011 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 28693 0 0 0 14926 76 0 0 25 0 1 0 546198114 85585920 11485 4294967295 134512640 134672761 3221224544 3219878832 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20895 11485 603 41 0 20854 0
vsize: 83580
[startup+160.011 s]
Raw data (loadavg): 0.98 0.93 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 28951 0 0 0 15926 76 0 0 25 0 1 0 546198114 85696512 11578 4294967295 134512640 134672761 3221224544 3219666192 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20922 11578 603 41 0 20881 0
vsize: 83688
[startup+170.012 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 29163 0 0 0 16925 77 0 0 25 0 1 0 546198114 86171648 11748 4294967295 134512640 134672761 3221224544 3220970160 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21038 11748 603 41 0 20997 0
vsize: 84152
[startup+180.012 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 29185 0 0 0 17926 77 0 0 25 0 1 0 546198114 86171648 11770 4294967295 134512640 134672761 3221224544 3220376704 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21038 11770 603 41 0 20997 0
vsize: 84152
[startup+190.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 29301 0 0 0 18926 77 0 0 25 0 1 0 546198114 86577152 11886 4294967295 134512640 134672761 3221224544 3220220880 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21137 11886 603 41 0 21096 0
vsize: 84548
[startup+200.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 29711 0 0 0 19925 78 0 0 25 0 1 0 546198114 86896640 12048 4294967295 134512640 134672761 3221224544 3220590096 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21215 12048 603 41 0 21174 0
vsize: 84860
[startup+210.013 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 29846 0 0 0 20925 78 0 0 25 0 1 0 546198114 87199744 12141 4294967295 134512640 134672761 3221224544 3220787008 134594133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21289 12141 603 41 0 21248 0
vsize: 85156
[startup+220.014 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 29991 0 0 0 21925 79 0 0 25 0 1 0 546198114 87605248 12286 4294967295 134512640 134672761 3221224544 3220911600 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21388 12286 603 41 0 21347 0
vsize: 85552
[startup+230.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 30380 0 0 0 22924 80 0 0 25 0 1 0 546198114 87920640 12427 4294967295 134512640 134672761 3221224544 3220589040 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21465 12427 603 41 0 21424 0
vsize: 85860
[startup+240.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 30516 0 0 0 23924 80 0 0 25 0 1 0 546198114 88223744 12521 4294967295 134512640 134672761 3221224544 3220696576 134594124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21539 12521 603 41 0 21498 0
vsize: 86156
[startup+250.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 30516 0 0 0 24924 80 0 0 25 0 1 0 546198114 88223744 12521 4294967295 134512640 134672761 3221224544 3219859072 134594084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21539 12521 603 41 0 21498 0
vsize: 86156
[startup+260.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 30847 0 0 0 25924 81 0 0 25 0 1 0 546198114 88965120 12769 4294967295 134512640 134672761 3221224544 3220726704 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21720 12769 603 41 0 21679 0
vsize: 86880
[startup+270.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 31073 0 0 0 26923 81 0 0 25 0 1 0 546198114 95150080 12830 4294967295 134512640 134672761 3221224544 3220372464 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23230 12830 603 41 0 23189 0
vsize: 92920
[startup+280.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 31217 0 0 0 27923 81 0 0 25 0 1 0 546198114 95453184 12932 4294967295 134512640 134672761 3221224544 3221127696 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23304 12932 603 41 0 23263 0
vsize: 93216
[startup+290.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 31226 0 0 0 28924 81 0 0 25 0 1 0 546198114 95588352 12941 4294967295 134512640 134672761 3221224544 3220105504 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23337 12941 603 41 0 23296 0
vsize: 93348
[startup+300.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 31341 0 0 0 29924 82 0 0 25 0 1 0 546198114 95858688 13056 4294967295 134512640 134672761 3221224544 3220051440 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23403 13056 603 41 0 23362 0
vsize: 93612
[startup+310.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 31755 0 0 0 30923 83 0 0 25 0 1 0 546198114 96231424 13222 4294967295 134512640 134672761 3221224544 3219833328 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23494 13222 603 41 0 23453 0
vsize: 93976
[startup+320.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 31915 0 0 0 31923 83 0 0 25 0 1 0 546198114 96534528 13340 4294967295 134512640 134672761 3221224544 3220885296 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23568 13340 603 41 0 23527 0
vsize: 94272
[startup+330.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 31944 0 0 0 32923 83 0 0 25 0 1 0 546198114 96669696 13369 4294967295 134512640 134672761 3221224544 3220404160 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23601 13369 603 41 0 23560 0
vsize: 94404
[startup+340.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 31944 0 0 0 33923 83 0 0 25 0 1 0 546198114 96669696 13369 4294967295 134512640 134672761 3221224544 3219037792 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23601 13369 603 41 0 23560 0
vsize: 94404
[startup+350.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 32308 0 0 0 34922 84 0 0 25 0 1 0 546198114 97546240 13650 4294967295 134512640 134672761 3221224544 3221043888 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23815 13650 603 41 0 23774 0
vsize: 95260
[startup+360.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 32525 0 0 0 35922 84 0 0 25 0 1 0 546198114 97488896 13702 4294967295 134512640 134672761 3221224544 3220471248 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23801 13702 603 41 0 23760 0
vsize: 95204
[startup+370.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 32662 0 0 0 36922 84 0 0 25 0 1 0 546198114 97792000 13797 4294967295 134512640 134672761 3221224544 3221132688 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23875 13797 603 41 0 23834 0
vsize: 95500
[startup+380.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 32669 0 0 0 37922 84 0 0 25 0 1 0 546198114 97792000 13804 4294967295 134512640 134672761 3221224544 3220055968 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23875 13804 603 41 0 23834 0
vsize: 95500
[startup+390.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 32742 0 0 0 38922 85 0 0 25 0 1 0 546198114 97927168 13877 4294967295 134512640 134672761 3221224544 3219413136 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23908 13877 603 41 0 23867 0
vsize: 95632
[startup+400.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 35691 0 0 0 39916 92 0 0 25 0 1 0 546198114 104071168 15425 4294967295 134512640 134672761 3221224544 3221214000 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25408 15425 603 41 0 25367 0
vsize: 101632
[startup+410.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 36027 0 0 0 40914 93 0 0 25 0 1 0 546198114 104300544 15554 4294967295 134512640 134672761 3221224544 3220466928 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25464 15554 603 41 0 25423 0
vsize: 101856
[startup+420.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 36078 0 0 0 41914 93 0 0 25 0 1 0 546198114 104435712 15605 4294967295 134512640 134672761 3221224544 3221092464 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25497 15605 603 41 0 25456 0
vsize: 101988
[startup+430.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 36089 0 0 0 42914 93 0 0 25 0 1 0 546198114 104435712 15616 4294967295 134512640 134672761 3221224544 3220073632 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25497 15616 603 41 0 25456 0
vsize: 101988
[startup+440.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 36089 0 0 0 43915 93 0 0 25 0 1 0 546198114 104435712 15616 4294967295 134512640 134672761 3221224544 3218796640 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25497 15616 603 41 0 25456 0
vsize: 101988
[startup+450.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 36453 0 0 0 44914 94 0 0 25 0 1 0 546198114 105312256 15897 4294967295 134512640 134672761 3221224544 3220840080 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25711 15897 603 41 0 25670 0
vsize: 102844
[startup+460.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 36856 0 0 0 45913 95 0 0 25 0 1 0 546198114 105820160 16100 4294967295 134512640 134672761 3221224544 3219556464 134594231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25835 16100 603 41 0 25794 0
vsize: 103340
[startup+470.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 37000 0 0 0 46913 95 0 0 25 0 1 0 546198114 106258432 16202 4294967295 134512640 134672761 3221224544 3220301712 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25942 16202 603 41 0 25901 0
vsize: 103768
[startup+480.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 37041 0 0 0 47914 95 0 0 25 0 1 0 546198114 106258432 16243 4294967295 134512640 134672761 3221224544 3220803984 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25942 16243 603 41 0 25901 0
vsize: 103768
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 37073 0 0 0 48914 95 0 0 25 0 1 0 546198114 106393600 16275 4294967295 134512640 134672761 3221224544 3221191536 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25975 16275 603 41 0 25934 0
vsize: 103900
[startup+500.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 37076 0 0 0 49915 95 0 0 25 0 1 0 546198114 106393600 16278 4294967295 134512640 134672761 3221224544 3219626656 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25975 16278 603 41 0 25934 0
vsize: 103900
[startup+510.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 37076 0 0 0 50916 95 0 0 25 0 1 0 546198114 106393600 16278 4294967295 134512640 134672761 3221224544 3219184192 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25975 16278 603 41 0 25934 0
vsize: 103900
[startup+520.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 37076 0 0 0 51916 95 0 0 25 0 1 0 546198114 106393600 16278 4294967295 134512640 134672761 3221224544 3218321344 134594089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25975 16278 603 41 0 25934 0
vsize: 103900
[startup+530.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 37391 0 0 0 52915 96 0 0 25 0 1 0 546198114 107134976 16510 4294967295 134512640 134672761 3221224544 3219641232 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26156 16510 603 41 0 26115 0
vsize: 104624
[startup+540.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 37526 0 0 0 53915 96 0 0 25 0 1 0 546198114 107540480 16645 4294967295 134512640 134672761 3221224544 3220861968 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26255 16645 603 41 0 26214 0
vsize: 105020
[startup+550.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 37811 0 0 0 54915 97 0 0 25 0 1 0 546198114 107606016 16728 4294967295 134512640 134672761 3221224544 3219223728 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26271 16728 603 41 0 26230 0
vsize: 105084
[startup+560.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 37963 0 0 0 55915 97 0 0 25 0 1 0 546198114 107909120 16838 4294967295 134512640 134672761 3221224544 3220076880 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26345 16838 603 41 0 26304 0
vsize: 105380
[startup+570.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38007 0 0 0 56915 97 0 0 25 0 1 0 546198114 108044288 16882 4294967295 134512640 134672761 3221224544 3220603824 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26378 16882 603 41 0 26337 0
vsize: 105512
[startup+580.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38039 0 0 0 57915 97 0 0 25 0 1 0 546198114 108179456 16914 4294967295 134512640 134672761 3221224544 3221005200 134594223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26411 16914 603 41 0 26370 0
vsize: 105644
[startup+590.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38057 0 0 0 58915 97 0 0 25 0 1 0 546198114 108179456 16932 4294967295 134512640 134672761 3221224544 3219866080 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+600.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38057 0 0 0 59915 97 0 0 25 0 1 0 546198114 108179456 16932 4294967295 134512640 134672761 3221224544 3219396640 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+610.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38057 0 0 0 60916 97 0 0 25 0 1 0 546198114 108179456 16932 4294967295 134512640 134672761 3221224544 3218979232 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+620.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38057 0 0 0 61916 97 0 0 25 0 1 0 546198114 108179456 16932 4294967295 134512640 134672761 3221224544 3218241664 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26411 16932 603 41 0 26370 0
vsize: 105644
[startup+630.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38331 0 0 0 62915 98 0 0 25 0 1 0 546198114 108785664 17123 4294967295 134512640 134672761 3221224544 3218999664 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26559 17123 603 41 0 26518 0
vsize: 106236
[startup+640.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38457 0 0 0 63915 98 0 0 25 0 1 0 546198114 109191168 17249 4294967295 134512640 134672761 3221224544 3220533936 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26658 17249 603 41 0 26617 0
vsize: 106632
[startup+650.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38639 0 0 0 64915 98 0 0 25 0 1 0 546198114 108961792 17231 4294967295 134512640 134672761 3221224544 3218500368 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26602 17231 603 41 0 26561 0
vsize: 106408
[startup+660.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38860 0 0 0 65915 99 0 0 25 0 1 0 546198114 109436928 17410 4294967295 134512640 134672761 3221224544 3219936144 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26718 17410 603 41 0 26677 0
vsize: 106872
[startup+670.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38910 0 0 0 66915 99 0 0 25 0 1 0 546198114 109572096 17460 4294967295 134512640 134672761 3221224544 3220536816 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26751 17460 603 41 0 26710 0
vsize: 107004
[startup+680.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38946 0 0 0 67915 99 0 0 25 0 1 0 546198114 109707264 17496 4294967295 134512640 134672761 3221224544 3220980720 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26784 17496 603 41 0 26743 0
vsize: 107136
[startup+690.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38967 0 0 0 68916 99 0 0 25 0 1 0 546198114 109707264 17517 4294967295 134512640 134672761 3221224544 3219863104 134594084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26784 17517 603 41 0 26743 0
vsize: 107136
[startup+700.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38967 0 0 0 69916 99 0 0 25 0 1 0 546198114 109707264 17517 4294967295 134512640 134672761 3221224544 3219453184 134594124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26784 17517 603 41 0 26743 0
vsize: 107136
[startup+710.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38967 0 0 0 70916 99 0 0 25 0 1 0 546198114 109707264 17517 4294967295 134512640 134672761 3221224544 3218958592 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26784 17517 603 41 0 26743 0
vsize: 107136
[startup+720.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 38967 0 0 0 71916 99 0 0 25 0 1 0 546198114 109707264 17517 4294967295 134512640 134672761 3221224544 3218006848 134594124 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26784 17517 603 41 0 26743 0
vsize: 107136
[startup+730.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 39332 0 0 0 72916 100 0 0 25 0 1 0 546198114 110583808 17799 4294967295 134512640 134672761 3221224544 3220242192 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26998 17799 603 41 0 26957 0
vsize: 107992
[startup+740.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 39407 0 0 0 73916 100 0 0 25 0 1 0 546198114 110718976 17874 4294967295 134512640 134672761 3221224544 3221155536 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27031 17874 603 41 0 26990 0
vsize: 108124
[startup+750.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 39653 0 0 0 74915 101 0 0 25 0 1 0 546198114 110755840 17920 4294967295 134512640 134672761 3221224544 3219789264 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27040 17920 603 41 0 26999 0
vsize: 108160
[startup+760.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 39789 0 0 0 75915 101 0 0 25 0 1 0 546198114 111058944 18014 4294967295 134512640 134672761 3221224544 3220435056 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27114 18014 603 41 0 27073 0
vsize: 108456
[startup+770.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 39829 0 0 0 76916 101 0 0 25 0 1 0 546198114 111058944 18054 4294967295 134512640 134672761 3221224544 3220903824 134594234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27114 18054 603 41 0 27073 0
vsize: 108456
[startup+780.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 39854 0 0 0 77916 101 0 0 25 0 1 0 546198114 111194112 18079 4294967295 134512640 134672761 3221224544 3220307296 134594084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27147 18079 603 41 0 27106 0
vsize: 108588
[startup+790.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 39854 0 0 0 78916 101 0 0 25 0 1 0 546198114 111194112 18079 4294967295 134512640 134672761 3221224544 3219531712 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27147 18079 603 41 0 27106 0
vsize: 108588
[startup+800.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 39854 0 0 0 79916 101 0 0 25 0 1 0 546198114 111194112 18079 4294967295 134512640 134672761 3221224544 3219063136 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27147 18079 603 41 0 27106 0
vsize: 108588
[startup+810.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 39854 0 0 0 80916 101 0 0 25 0 1 0 546198114 111194112 18079 4294967295 134512640 134672761 3221224544 3218158912 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27147 18079 603 41 0 27106 0
vsize: 108588
[startup+820.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 40201 0 0 0 81917 102 0 0 25 0 1 0 546198114 111935488 18343 4294967295 134512640 134672761 3221224544 3220013616 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27328 18343 603 41 0 27287 0
vsize: 109312
[startup+830.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 40284 0 0 0 82917 102 0 0 25 0 1 0 546198114 112205824 18426 4294967295 134512640 134672761 3221224544 3221027568 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27394 18426 603 41 0 27353 0
vsize: 109576
[startup+840.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 40528 0 0 0 83916 103 0 0 25 0 1 0 546198114 124755968 18470 4294967295 134512640 134672761 3221224544 3219645168 134594220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30458 18470 603 41 0 30417 0
vsize: 121832
[startup+850.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 40669 0 0 0 84916 103 0 0 25 0 1 0 546198114 125059072 18569 4294967295 134512640 134672761 3221224544 3220350960 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30532 18569 603 41 0 30491 0
vsize: 122128
[startup+860.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 40710 0 0 0 85917 103 0 0 25 0 1 0 546198114 125194240 18610 4294967295 134512640 134672761 3221224544 3220843440 134594252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30565 18610 603 41 0 30524 0
vsize: 122260
[startup+870.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 40740 0 0 0 86917 103 0 0 25 0 1 0 546198114 125194240 18640 4294967295 134512640 134672761 3221224544 3221084416 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30565 18640 603 41 0 30524 0
vsize: 122260
[startup+880.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 40740 0 0 0 87918 103 0 0 25 0 1 0 546198114 125194240 18640 4294967295 134512640 134672761 3221224544 3219592864 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30565 18640 603 41 0 30524 0
vsize: 122260
[startup+890.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 40740 0 0 0 88918 103 0 0 25 0 1 0 546198114 125194240 18640 4294967295 134512640 134672761 3221224544 3219135232 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30565 18640 603 41 0 30524 0
vsize: 122260
[startup+900.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 40740 0 0 0 89919 103 0 0 25 0 1 0 546198114 125194240 18640 4294967295 134512640 134672761 3221224544 3218239072 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30565 18640 603 41 0 30524 0
vsize: 122260
[startup+910.081 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41077 0 0 0 90919 104 0 0 25 0 1 0 546198114 125935616 18894 4294967295 134512640 134672761 3221224544 3219896112 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30746 18894 603 41 0 30705 0
vsize: 122984
[startup+920.084 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41165 0 0 0 91919 104 0 0 25 0 1 0 546198114 126205952 18982 4294967295 134512640 134672761 3221224544 3220978704 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30812 18982 603 41 0 30771 0
vsize: 123248
[startup+930.086 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41535 0 0 0 92918 105 0 0 25 0 1 0 546198114 126595072 19145 4294967295 134512640 134672761 3221224544 3218948688 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30907 19145 603 41 0 30866 0
vsize: 123628
[startup+940.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41678 0 0 0 93918 105 0 0 25 0 1 0 546198114 126898176 19246 4294967295 134512640 134672761 3221224544 3219687408 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30981 19246 603 41 0 30940 0
vsize: 123924
[startup+950.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41719 0 0 0 94919 105 0 0 25 0 1 0 546198114 127033344 19287 4294967295 134512640 134672761 3221224544 3220187856 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31014 19287 603 41 0 30973 0
vsize: 124056
[startup+960.087 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41751 0 0 0 95919 105 0 0 25 0 1 0 546198114 127168512 19319 4294967295 134512640 134672761 3221224544 3220574256 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31047 19319 603 41 0 31006 0
vsize: 124188
[startup+970.091 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41777 0 0 0 96919 105 0 0 25 0 1 0 546198114 127168512 19345 4294967295 134512640 134672761 3221224544 3220887888 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31047 19345 603 41 0 31006 0
vsize: 124188
[startup+980.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41800 0 0 0 97920 105 0 0 25 0 1 0 546198114 127303680 19368 4294967295 134512640 134672761 3221224544 3221162736 134594259 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19368 603 41 0 31039 0
vsize: 124320
[startup+990.101 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41805 0 0 0 98920 105 0 0 25 0 1 0 546198114 127303680 19373 4294967295 134512640 134672761 3221224544 3219415360 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41805 0 0 0 99921 105 0 0 25 0 1 0 546198114 127303680 19373 4294967295 134512640 134672761 3221224544 3219010048 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41805 0 0 0 100922 105 0 0 25 0 1 0 546198114 127303680 19373 4294967295 134512640 134672761 3221224544 3218717824 134594131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41805 0 0 0 101922 105 0 0 25 0 1 0 546198114 127303680 19373 4294967295 134512640 134672761 3221224544 3218382880 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41805 0 0 0 102922 105 0 0 25 0 1 0 546198114 127303680 19373 4294967295 134512640 134672761 3221224544 3217842112 134594101 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 41805 0 0 0 103923 105 0 0 25 0 1 0 546198114 127303680 19373 4294967295 134512640 134672761 3221224544 3217350400 134594086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 42159 0 0 0 104922 106 0 0 25 0 1 0 546198114 128045056 19644 4294967295 134512640 134672761 3221224544 3219497712 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31261 19644 603 41 0 31220 0
vsize: 125044
[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 42249 0 0 0 105922 107 0 0 25 0 1 0 546198114 128315392 19734 4294967295 134512640 134672761 3221224544 3220498032 134594217 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31327 19734 603 41 0 31286 0
vsize: 125308
[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 42322 0 0 0 106922 107 0 0 25 0 1 0 546198114 128585728 19807 4294967295 134512640 134672761 3221224544 3221097168 134594214 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31393 19807 603 41 0 31352 0
vsize: 125572
[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 42910 0 0 0 107921 108 0 0 25 0 1 0 546198114 129081344 20104 4294967295 134512640 134672761 3221224544 3220797664 134594106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31514 20104 603 41 0 31473 0
vsize: 126056
[startup+1090.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 85940 0 0 0 108812 217 0 0 25 0 1 0 546198114 282791936 60528 4294967295 134512640 134672761 3221224544 3221097456 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69041 60529 603 41 0 69000 0
vsize: 276164
[startup+1091.41 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 4131
Raw data (stat): 4131 (minisat+) R 4130 26298 26297 0 -1 0 85940 0 0 0 108812 217 0 0 25 0 1 0 546198114 282791936 60528 4294967295 134512640 134672761 3221224544 3221097456 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69041 60529 603 41 0 69000 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1091.39
CPU time (s): 1091.18
CPU user time (s): 1088.73
CPU system time (s): 2.44863
CPU usage (%): 99.9803
Max. virtual memory (Kb): 276164
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####