PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 23:31:21 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13687 boxname=wulflinc7 idbench=1053 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a5c401bba5afccf02c7b40cb1c595b15  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-nw04.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-nw04.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-nw04.opb
IDLAUNCH: 13687
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 2
cpu MHz		: 451.050
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:        317584 kB
Buffers:         31404 kB
Cached:         663228 kB
SwapCached:        328 kB
Active:         189596 kB
Inactive:       507628 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        317332 kB
SwapTotal:     2097136 kB
SwapFree:      2096520 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6456 kB
Slab:            14148 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 23:48:40 (client local time) WITH STATUS 0 IN 1038.66 SECONDS
stats: 13687 7 1038.66 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.92 0.95 0.90 2/54 21998
Raw data (stat): 21998 (runsolver) R 21997 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 490842778 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.0001 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 23768 0 0 0 938 60 0 0 25 0 1 0 490842778 69439488 8007 4294967295 134512640 134672761 3221224544 3220427088 134594220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16953 8007 603 41 0 16912 0
vsize: 67812
[startup+19.9999 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 23768 0 0 0 1938 60 0 0 25 0 1 0 490842778 69439488 8007 4294967295 134512640 134672761 3221224544 3220734672 134594231 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.0005 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 24113 0 0 0 2937 61 0 0 25 0 1 0 490842778 70852608 8352 4294967295 134512640 134672761 3221224544 3220527024 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.0009 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 24501 0 0 0 3936 62 0 0 25 0 1 0 490842778 73998336 8740 4294967295 134512640 134672761 3221224544 3220827328 134594084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18066 8740 603 41 0 18025 0
vsize: 72264
[startup+50.0005 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 24742 0 0 0 4936 63 0 0 25 0 1 0 490842778 74629120 8981 4294967295 134512640 134672761 3221224544 3220719616 134594106 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.0001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 25461 0 0 0 5934 64 0 0 25 0 1 0 490842778 75976704 9370 4294967295 134512640 134672761 3221224544 3220335120 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18549 9370 603 41 0 18508 0
vsize: 74196
[startup+69.9998 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 25556 0 0 0 6934 65 0 0 25 0 1 0 490842778 75976704 9465 4294967295 134512640 134672761 3221224544 3220770496 134594089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18549 9465 603 41 0 18508 0
vsize: 74196
[startup+80.0004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 25636 0 0 0 7934 65 0 0 25 0 1 0 490842778 75976704 9545 4294967295 134512640 134672761 3221224544 3220399648 134594086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18549 9545 603 41 0 18508 0
vsize: 74196
[startup+90 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 25876 0 0 0 8934 65 0 0 25 0 1 0 490842778 79294464 9702 4294967295 134512640 134672761 3221224544 3221157840 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19359 9702 603 41 0 19318 0
vsize: 77436
[startup+99.9997 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 26193 0 0 0 9933 66 0 0 25 0 1 0 490842778 79872000 9894 4294967295 134512640 134672761 3221224544 3220490832 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19500 9894 603 41 0 19459 0
vsize: 78000
[startup+110 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 26275 0 0 0 10933 67 0 0 25 0 1 0 490842778 80044032 9976 4294967295 134512640 134672761 3221224544 3219635200 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+120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 28228 0 0 0 11929 71 0 0 25 0 1 0 490842778 84406272 11145 4294967295 134512640 134672761 3221224544 3220197840 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20607 11146 603 41 0 20566 0
vsize: 82428
[startup+130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 28378 0 0 0 12929 71 0 0 25 0 1 0 490842778 84709376 11253 4294967295 134512640 134672761 3221224544 3221009424 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20681 11253 603 41 0 20640 0
vsize: 82724
[startup+139.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 28396 0 0 0 13929 71 0 0 25 0 1 0 490842778 84844544 11271 4294967295 134512640 134672761 3221224544 3220160512 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+149.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 28396 0 0 0 14929 71 0 0 25 0 1 0 490842778 84844544 11271 4294967295 134512640 134672761 3221224544 3218741824 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20714 11271 603 41 0 20673 0
vsize: 82856
[startup+159.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 28835 0 0 0 15928 72 0 0 25 0 1 0 490842778 85991424 11627 4294967295 134512640 134672761 3221224544 3221026320 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20994 11627 603 41 0 20953 0
vsize: 83976
[startup+169.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 29055 0 0 0 16927 73 0 0 25 0 1 0 490842778 85868544 11682 4294967295 134512640 134672761 3221224544 3220662096 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20964 11682 603 41 0 20923 0
vsize: 83856
[startup+179.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 29185 0 0 0 17927 73 0 0 25 0 1 0 490842778 86171648 11770 4294967295 134512640 134672761 3221224544 3220633312 134594124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21038 11770 603 41 0 20997 0
vsize: 84152
[startup+189.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 29185 0 0 0 18928 73 0 0 25 0 1 0 490842778 86171648 11770 4294967295 134512640 134672761 3221224544 3218967424 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+199.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 29695 0 0 0 19926 75 0 0 25 0 1 0 490842778 86896640 12032 4294967295 134512640 134672761 3221224544 3220163088 134594220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21215 12032 603 41 0 21174 0
vsize: 84860
[startup+209.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 29846 0 0 0 20926 75 0 0 25 0 1 0 490842778 87199744 12141 4294967295 134512640 134672761 3221224544 3221026816 134594084 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21289 12141 603 41 0 21248 0
vsize: 85156
[startup+219.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 29940 0 0 0 21926 75 0 0 25 0 1 0 490842778 87470080 12235 4294967295 134512640 134672761 3221224544 3220295760 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21355 12235 603 41 0 21314 0
vsize: 85420
[startup+229.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 30366 0 0 0 22925 76 0 0 25 0 1 0 490842778 87785472 12413 4294967295 134512640 134672761 3221224544 3220409904 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21432 12413 603 41 0 21391 0
vsize: 85728
[startup+239.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 30514 0 0 0 23925 77 0 0 25 0 1 0 490842778 88088576 12519 4294967295 134512640 134672761 3221224544 3221215152 134594234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 12519 603 41 0 21465 0
vsize: 86024
[startup+249.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 30516 0 0 0 24925 77 0 0 25 0 1 0 490842778 88223744 12521 4294967295 134512640 134672761 3221224544 3219867232 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+259.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 30854 0 0 0 25925 77 0 0 25 0 1 0 490842778 95256576 12776 4294967295 134512640 134672761 3221224544 3220808976 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23256 12776 603 41 0 23215 0
vsize: 93024
[startup+269.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 31073 0 0 0 26924 78 0 0 25 0 1 0 490842778 95150080 12830 4294967295 134512640 134672761 3221224544 3220372464 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23230 12830 603 41 0 23189 0
vsize: 92920
[startup+279.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 31222 0 0 0 27924 78 0 0 25 0 1 0 490842778 95588352 12937 4294967295 134512640 134672761 3221224544 3221170512 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23337 12937 603 41 0 23296 0
vsize: 93348
[startup+289.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 31226 0 0 0 28924 78 0 0 25 0 1 0 490842778 95588352 12941 4294967295 134512640 134672761 3221224544 3219965344 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+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 31541 0 0 0 29924 79 0 0 25 0 1 0 490842778 96194560 13173 4294967295 134512640 134672761 3221224544 3220479408 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23485 13173 603 41 0 23444 0
vsize: 93940
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 31767 0 0 0 30924 79 0 0 25 0 1 0 490842778 96231424 13234 4294967295 134512640 134672761 3221224544 3220078512 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23494 13234 603 41 0 23453 0
vsize: 93976
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 31925 0 0 0 31924 80 0 0 25 0 1 0 490842778 96534528 13350 4294967295 134512640 134672761 3221224544 3221003088 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23568 13350 603 41 0 23527 0
vsize: 94272
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 31944 0 0 0 32924 80 0 0 25 0 1 0 490842778 96669696 13369 4294967295 134512640 134672761 3221224544 3220208320 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23601 13369 603 41 0 23560 0
vsize: 94404
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 32010 0 0 0 33924 80 0 0 25 0 1 0 490842778 96804864 13435 4294967295 134512640 134672761 3221224544 3219431664 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23634 13435 603 41 0 23593 0
vsize: 94536
[startup+350.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 32409 0 0 0 34924 81 0 0 25 0 1 0 490842778 97046528 13586 4294967295 134512640 134672761 3221224544 3219328656 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23693 13586 603 41 0 23652 0
vsize: 94772
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 32624 0 0 0 35924 81 0 0 25 0 1 0 490842778 97656832 13759 4294967295 134512640 134672761 3221224544 3220671408 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23842 13759 603 41 0 23801 0
vsize: 95368
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 32669 0 0 0 36923 81 0 0 25 0 1 0 490842778 97792000 13804 4294967295 134512640 134672761 3221224544 3220490848 134594089 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 32669 0 0 0 37924 81 0 0 25 0 1 0 490842778 97792000 13804 4294967295 134512640 134672761 3221224544 3219690112 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+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 35625 0 0 0 38917 88 0 0 25 0 1 0 490842778 103936000 15359 4294967295 134512640 134672761 3221224544 3220406448 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25375 15359 603 41 0 25334 0
vsize: 101500
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 35887 0 0 0 39917 88 0 0 25 0 1 0 490842778 103997440 15456 4294967295 134512640 134672761 3221224544 3219711216 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25390 15456 603 41 0 25349 0
vsize: 101560
[startup+410.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 36048 0 0 0 40916 89 0 0 25 0 1 0 490842778 104300544 15575 4294967295 134512640 134672761 3221224544 3220724880 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25464 15575 603 41 0 25423 0
vsize: 101856
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 36089 0 0 0 41916 89 0 0 25 0 1 0 490842778 104435712 15616 4294967295 134512640 134672761 3221224544 3220380736 134594131 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 36089 0 0 0 42916 89 0 0 25 0 1 0 490842778 104435712 15616 4294967295 134512640 134672761 3221224544 3219648448 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+440.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 36396 0 0 0 43916 90 0 0 25 0 1 0 490842778 105177088 15840 4294967295 134512640 134672761 3221224544 3220143120 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25678 15840 603 41 0 25637 0
vsize: 102712
[startup+450.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 36765 0 0 0 44915 91 0 0 25 0 1 0 490842778 105648128 16009 4294967295 134512640 134672761 3221224544 3218718960 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25793 16009 603 41 0 25752 0
vsize: 103172
[startup+460.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 36974 0 0 0 45914 92 0 0 25 0 1 0 490842778 106123264 16176 4294967295 134512640 134672761 3221224544 3219977808 134594223 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25909 16176 603 41 0 25868 0
vsize: 103636
[startup+470.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 37026 0 0 0 46914 92 0 0 25 0 1 0 490842778 106258432 16228 4294967295 134512640 134672761 3221224544 3220623120 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25942 16228 603 41 0 25901 0
vsize: 103768
[startup+480.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 37065 0 0 0 47915 92 0 0 25 0 1 0 490842778 106393600 16267 4294967295 134512640 134672761 3221224544 3221094096 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25975 16267 603 41 0 25934 0
vsize: 103900
[startup+490.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 37076 0 0 0 48915 92 0 0 25 0 1 0 490842778 106393600 16278 4294967295 134512640 134672761 3221224544 3219694912 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+500.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 37076 0 0 0 49915 92 0 0 25 0 1 0 490842778 106393600 16278 4294967295 134512640 134672761 3221224544 3219225088 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+510.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 37076 0 0 0 50915 92 0 0 25 0 1 0 490842778 106393600 16278 4294967295 134512640 134672761 3221224544 3218193856 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25975 16278 603 41 0 25934 0
vsize: 103900
[startup+520 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 37430 0 0 0 51914 93 0 0 25 0 1 0 490842778 107270144 16549 4294967295 134512640 134672761 3221224544 3220090032 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26189 16549 603 41 0 26148 0
vsize: 104756
[startup+530.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 37546 0 0 0 52914 93 0 0 25 0 1 0 490842778 107540480 16665 4294967295 134512640 134672761 3221224544 3221025552 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26255 16665 603 41 0 26214 0
vsize: 105020
[startup+540.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 37829 0 0 0 53914 94 0 0 25 0 1 0 490842778 107606016 16746 4294967295 134512640 134672761 3221224544 3219440880 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26271 16746 603 41 0 26230 0
vsize: 105084
[startup+550 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 37976 0 0 0 54914 94 0 0 25 0 1 0 490842778 108044288 16851 4294967295 134512640 134672761 3221224544 3220223184 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26378 16851 603 41 0 26337 0
vsize: 105512
[startup+560.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38020 0 0 0 55914 94 0 0 25 0 1 0 490842778 108179456 16895 4294967295 134512640 134672761 3221224544 3220762512 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26411 16895 603 41 0 26370 0
vsize: 105644
[startup+570 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38053 0 0 0 56914 94 0 0 25 0 1 0 490842778 108179456 16928 4294967295 134512640 134672761 3221224544 3221166768 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26411 16928 603 41 0 26370 0
vsize: 105644
[startup+580 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38057 0 0 0 57914 94 0 0 25 0 1 0 490842778 108179456 16932 4294967295 134512640 134672761 3221224544 3219541216 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+590 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38057 0 0 0 58915 94 0 0 25 0 1 0 490842778 108179456 16932 4294967295 134512640 134672761 3221224544 3219123424 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38057 0 0 0 59915 94 0 0 25 0 1 0 490842778 108179456 16932 4294967295 134512640 134672761 3221224544 3218272480 134594095 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38373 0 0 0 60914 95 0 0 25 0 1 0 490842778 108920832 17165 4294967295 134512640 134672761 3221224544 3219514224 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26592 17165 603 41 0 26551 0
vsize: 106368
[startup+620 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38471 0 0 0 61914 95 0 0 25 0 1 0 490842778 109191168 17263 4294967295 134512640 134672761 3221224544 3220703088 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26658 17263 603 41 0 26617 0
vsize: 106632
[startup+630 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38708 0 0 0 62914 95 0 0 25 0 1 0 490842778 109133824 17300 4294967295 134512640 134672761 3221224544 3218902608 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26644 17300 603 41 0 26603 0
vsize: 106576
[startup+640 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38868 0 0 0 63914 96 0 0 25 0 1 0 490842778 109436928 17418 4294967295 134512640 134672761 3221224544 3220032528 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26718 17418 603 41 0 26677 0
vsize: 106872
[startup+650 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38920 0 0 0 64914 96 0 0 25 0 1 0 490842778 109572096 17470 4294967295 134512640 134672761 3221224544 3220661136 134594212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26751 17470 603 41 0 26710 0
vsize: 107004
[startup+659.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38957 0 0 0 65914 96 0 0 25 0 1 0 490842778 109707264 17507 4294967295 134512640 134672761 3221224544 3221120976 134594229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26784 17507 603 41 0 26743 0
vsize: 107136
[startup+670 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38967 0 0 0 66914 96 0 0 25 0 1 0 490842778 109707264 17517 4294967295 134512640 134672761 3221224544 3219664768 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38967 0 0 0 67914 96 0 0 25 0 1 0 490842778 109707264 17517 4294967295 134512640 134672761 3221224544 3219187264 134594131 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 38967 0 0 0 68914 96 0 0 25 0 1 0 490842778 109707264 17517 4294967295 134512640 134672761 3221224544 3218135776 134594131 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 39323 0 0 0 69914 97 0 0 25 0 1 0 490842778 110583808 17790 4294967295 134512640 134672761 3221224544 3220134192 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26998 17790 603 41 0 26957 0
vsize: 107992
[startup+710 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 39399 0 0 0 70914 97 0 0 25 0 1 0 490842778 110718976 17866 4294967295 134512640 134672761 3221224544 3221062704 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27031 17866 603 41 0 26990 0
vsize: 108124
[startup+720 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 39639 0 0 0 71914 97 0 0 25 0 1 0 490842778 110620672 17906 4294967295 134512640 134672761 3221224544 3219619632 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27007 17906 603 41 0 26966 0
vsize: 108028
[startup+730.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 39786 0 0 0 72914 98 0 0 25 0 1 0 490842778 111058944 18011 4294967295 134512640 134672761 3221224544 3220382640 134594252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27114 18011 603 41 0 27073 0
vsize: 108456
[startup+740.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 39829 0 0 0 73914 98 0 0 25 0 1 0 490842778 111058944 18054 4294967295 134512640 134672761 3221224544 3220913808 134594231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27114 18054 603 41 0 27073 0
vsize: 108456
[startup+750.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 39854 0 0 0 74914 98 0 0 25 0 1 0 490842778 111194112 18079 4294967295 134512640 134672761 3221224544 3219999904 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27147 18079 603 41 0 27106 0
vsize: 108588
[startup+760.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 39854 0 0 0 75914 98 0 0 25 0 1 0 490842778 111194112 18079 4294967295 134512640 134672761 3221224544 3219440800 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.004 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 39854 0 0 0 76915 98 0 0 25 0 1 0 490842778 111194112 18079 4294967295 134512640 134672761 3221224544 3218820064 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.004 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 40142 0 0 0 77914 98 0 0 25 0 1 0 490842778 111800320 18284 4294967295 134512640 134672761 3221224544 3219299856 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27295 18284 603 41 0 27254 0
vsize: 109180
[startup+790.004 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 40256 0 0 0 78915 98 0 0 25 0 1 0 490842778 112070656 18398 4294967295 134512640 134672761 3221224544 3220697232 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27361 18398 603 41 0 27320 0
vsize: 109444
[startup+800.004 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 40486 0 0 0 79914 99 0 0 25 0 1 0 490842778 124620800 18428 4294967295 134512640 134672761 3221224544 3218990640 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30425 18428 603 41 0 30384 0
vsize: 121700
[startup+810.005 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 40646 0 0 0 80913 100 0 0 25 0 1 0 490842778 124923904 18546 4294967295 134512640 134672761 3221224544 3220075344 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30499 18546 603 41 0 30458 0
vsize: 121996
[startup+820.004 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 40697 0 0 0 81914 100 0 0 25 0 1 0 490842778 125059072 18597 4294967295 134512640 134672761 3221224544 3220696368 134594217 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30532 18597 603 41 0 30491 0
vsize: 122128
[startup+830.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 40735 0 0 0 82914 100 0 0 25 0 1 0 490842778 125194240 18635 4294967295 134512640 134672761 3221224544 3221151120 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30565 18635 603 41 0 30524 0
vsize: 122260
[startup+840.004 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 40740 0 0 0 83914 100 0 0 25 0 1 0 490842778 125194240 18640 4294967295 134512640 134672761 3221224544 3219641536 134594131 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30565 18640 603 41 0 30524 0
vsize: 122260
[startup+850.003 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 40740 0 0 0 84914 100 0 0 25 0 1 0 490842778 125194240 18640 4294967295 134512640 134672761 3221224544 3219140800 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.003 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 40740 0 0 0 85914 100 0 0 25 0 1 0 490842778 125194240 18640 4294967295 134512640 134672761 3221224544 3218026240 134594101 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.003 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 41108 0 0 0 86914 100 0 0 25 0 1 0 490842778 126070784 18925 4294967295 134512640 134672761 3221224544 3220281936 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30779 18925 603 41 0 30738 0
vsize: 123116
[startup+880.003 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 41179 0 0 0 87914 100 0 0 25 0 1 0 490842778 126205952 18996 4294967295 134512640 134672761 3221224544 3221155056 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30812 18996 603 41 0 30771 0
vsize: 123248
[startup+890.003 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 41550 0 0 0 88913 101 0 0 25 0 1 0 490842778 126730240 19160 4294967295 134512640 134672761 3221224544 3219135408 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30940 19160 603 41 0 30899 0
vsize: 123760
[startup+900.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 41692 0 0 0 89913 102 0 0 25 0 1 0 490842778 127033344 19260 4294967295 134512640 134672761 3221224544 3219847440 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31014 19260 603 41 0 30973 0
vsize: 124056
[startup+910.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 41733 0 0 0 90913 102 0 0 25 0 1 0 490842778 127033344 19301 4294967295 134512640 134672761 3221224544 3220357584 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31014 19301 603 41 0 30973 0
vsize: 124056
[startup+920.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 41765 0 0 0 91913 102 0 0 25 0 1 0 490842778 127168512 19333 4294967295 134512640 134672761 3221224544 3220742544 134594259 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31047 19333 603 41 0 31006 0
vsize: 124188
[startup+930.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 41790 0 0 0 92913 102 0 0 25 0 1 0 490842778 127303680 19358 4294967295 134512640 134672761 3221224544 3221049456 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31080 19358 603 41 0 31039 0
vsize: 124320
[startup+940.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 41805 0 0 0 93913 102 0 0 25 0 1 0 490842778 127303680 19373 4294967295 134512640 134672761 3221224544 3219887104 134594095 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31080 19373 603 41 0 31039 0
vsize: 124320
[startup+950.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 41805 0 0 0 94913 102 0 0 25 0 1 0 490842778 127303680 19373 4294967295 134512640 134672761 3221224544 3219066496 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+960.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 41805 0 0 0 95914 102 0 0 25 0 1 0 490842778 127303680 19373 4294967295 134512640 134672761 3221224544 3218770912 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+970.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 41805 0 0 0 96914 102 0 0 25 0 1 0 490842778 127303680 19373 4294967295 134512640 134672761 3221224544 3218409760 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 41805 0 0 0 97914 102 0 0 25 0 1 0 490842778 127303680 19373 4294967295 134512640 134672761 3221224544 3217701472 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.003 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 42056 0 0 0 98914 103 0 0 25 0 1 0 490842778 127774720 19541 4294967295 134512640 134672761 3221224544 3218241264 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31195 19541 603 41 0 31154 0
vsize: 124780
[startup+1000 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 42197 0 0 0 99914 103 0 0 25 0 1 0 490842778 128180224 19682 4294967295 134512640 134672761 3221224544 3219962736 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31294 19682 603 41 0 31253 0
vsize: 125176
[startup+1010 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 42271 0 0 0 100914 103 0 0 25 0 1 0 490842778 128450560 19756 4294967295 134512640 134672761 3221224544 3220690224 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31360 19756 603 41 0 31319 0
vsize: 125440
[startup+1020 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 42339 0 0 0 101914 103 0 0 25 0 1 0 490842778 128585728 19824 4294967295 134512640 134672761 3221224544 3221223024 134594214 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31393 19824 603 41 0 31352 0
vsize: 125572
[startup+1030 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 43075 0 0 0 102912 105 0 0 25 0 1 0 490842778 129519616 20227 4294967295 134512640 134672761 3221224544 3221006368 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31621 20227 603 41 0 31580 0
vsize: 126484
[startup+1038.48 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 21998
Raw data (stat): 21998 (minisat+) R 21997 22932 22931 0 -1 0 43075 0 0 0 102912 105 0 0 25 0 1 0 490842778 129519616 20227 4294967295 134512640 134672761 3221224544 3221006368 134594106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31621 20227 603 41 0 31580 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 1038.48
CPU time (s): 1038.66
CPU user time (s): 1036.16
CPU system time (s): 2.49362
CPU usage (%): 100.017
Max. virtual memory (Kb): 126484
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####