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 28235

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-05-25 01:22:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13677 boxname=wulflinc17 idbench=1053 idsolver=1 numberseed=0
MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef  /oldhome/oroussel/solvers/bsolo_lpr
MD5SUM BENCH:  a5c401bba5afccf02c7b40cb1c595b15  /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-nw04.opb
REAL COMMAND:  bsolo_lpr /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-20-10-nw04.opb
IDLAUNCH: 13677
/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	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        644044 kB
Buffers:         23732 kB
Cached:         328736 kB
SwapCached:        452 kB
Active:          39136 kB
Inactive:       330160 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        643792 kB
SwapTotal:     2097892 kB
SwapFree:      2096860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            15616 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 01:36:59 (client local time) WITH STATUS 0 IN 872.459 SECONDS
stats: 13677 7 872.459 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
#### 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.86 0.95 0.92 2/54 15397
Raw data (stat): 15397 (runsolver) R 15396 7475 7474 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 834896008 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99989 s]
Raw data (loadavg): 0.88 0.96 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 3330 0 0 0 991 6 0 0 25 0 1 0 834896008 25235456 3254 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6161 3254 1111 63 0 6098 0
vsize: 24644
[startup+19.9994 s]
Raw data (loadavg): 0.90 0.96 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 5872 0 0 0 1987 11 0 0 25 0 1 0 834896008 35688448 5796 4294967295 134512640 134714508 3221224592 3221222712 1077378037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 8713 5801 1111 63 0 8650 0
vsize: 34852
[startup+29.9992 s]
Raw data (loadavg): 0.91 0.96 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 8424 0 0 0 2982 15 0 0 25 0 1 0 834896008 46125056 8348 4294967295 134512640 134714508 3221224592 3221222820 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11261 8348 1111 63 0 11198 0
vsize: 45044
[startup+39.9986 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 10963 0 0 0 3979 19 0 0 25 0 1 0 834896008 56573952 10887 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 13812 10887 1111 63 0 13749 0
vsize: 55248
[startup+49.9991 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 13539 0 0 0 4974 24 0 0 25 0 1 0 834896008 67153920 13463 4294967295 134512640 134714508 3221224592 3221222820 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16395 13463 1111 63 0 16332 0
vsize: 65580
[startup+59.999 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 16115 0 0 0 5969 29 0 0 25 0 1 0 834896008 77598720 16039 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 18945 16039 1111 63 0 18882 0
vsize: 75780
[startup+69.9983 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 18692 0 0 0 6963 35 0 0 25 0 1 0 834896008 88203264 18616 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 21534 18616 1111 63 0 21471 0
vsize: 86136
[startup+79.9989 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 21273 0 0 0 7959 40 0 0 25 0 1 0 834896008 98803712 21197 4294967295 134512640 134714508 3221224592 3221222820 1077414358 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 24122 21197 1111 63 0 24059 0
vsize: 96488
[startup+89.9988 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 23855 0 0 0 8955 44 0 0 25 0 1 0 834896008 109404160 23779 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 26710 23779 1111 63 0 26647 0
vsize: 106840
[startup+99.9992 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 26449 0 0 0 9950 49 0 0 25 0 1 0 834896008 119975936 26373 4294967295 134512640 134714508 3221224592 3221222820 1077414370 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29291 26373 1111 63 0 29228 0
vsize: 117164
[startup+109.999 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 29021 0 0 0 10945 54 0 0 25 0 1 0 834896008 130580480 28945 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 31880 28945 1111 63 0 31817 0
vsize: 127520
[startup+119.999 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 31597 0 0 0 11941 59 0 0 25 0 1 0 834896008 141029376 31521 4294967295 134512640 134714508 3221224592 3221222820 1077414433 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 34431 31521 1111 63 0 34368 0
vsize: 137724
[startup+129.999 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 34156 0 0 0 12936 64 0 0 25 0 1 0 834896008 151633920 34080 4294967295 134512640 134714508 3221224592 3221222820 1077414376 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 37020 34080 1111 63 0 36957 0
vsize: 148080
[startup+139.999 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 36708 0 0 0 13931 69 0 0 25 0 1 0 834896008 162082816 36632 4294967295 134512640 134714508 3221224592 3221222820 1077414347 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 39571 36632 1111 63 0 39508 0
vsize: 158284
[startup+149.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 39249 0 0 0 14927 73 0 0 25 0 1 0 834896008 172388352 39173 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 42087 39173 1111 63 0 42024 0
vsize: 168348
[startup+159.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 41819 0 0 0 15923 78 0 0 25 0 1 0 834896008 182984704 41743 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 44674 41743 1111 63 0 44611 0
vsize: 178696
[startup+169.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 44408 0 0 0 16918 82 0 0 25 0 1 0 834896008 193589248 44332 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 47263 44332 1111 63 0 47200 0
vsize: 189052
[startup+179.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 46989 0 0 0 17914 87 0 0 25 0 1 0 834896008 204185600 46913 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 49850 46913 1111 63 0 49787 0
vsize: 199400
[startup+189.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 49661 0 0 0 18910 90 0 0 25 0 1 0 834896008 215085056 49585 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 52511 49585 1111 63 0 52448 0
vsize: 210044
[startup+199.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 52298 0 0 0 19906 95 0 0 25 0 1 0 834896008 225980416 52222 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 55171 52222 1111 63 0 55108 0
vsize: 220684
[startup+209.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 54893 0 0 0 20902 99 0 0 25 0 1 0 834896008 236584960 54817 4294967295 134512640 134714508 3221224592 3221222820 1077414370 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 57760 54817 1111 63 0 57697 0
vsize: 231040
[startup+219.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 57446 0 0 0 21898 103 0 0 25 0 1 0 834896008 247029760 57370 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 60310 57370 1111 63 0 60247 0
vsize: 241240
[startup+229.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 60034 0 0 0 22893 108 0 0 25 0 1 0 834896008 257634304 59958 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 62899 59958 1111 63 0 62836 0
vsize: 251596
[startup+239.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 62574 0 0 0 23888 114 0 0 25 0 1 0 834896008 267935744 62498 4294967295 134512640 134714508 3221224592 3221222820 1077414382 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 65414 62498 1111 63 0 65351 0
vsize: 261656
[startup+249.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 65206 0 0 0 24883 119 0 0 25 0 1 0 834896008 278835200 65130 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 68075 65130 1111 63 0 68012 0
vsize: 272300
[startup+259.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 67825 0 0 0 25877 125 0 0 25 0 1 0 834896008 289435648 67749 4294967295 134512640 134714508 3221224592 3221222820 1077414383 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 70663 67749 1111 63 0 70600 0
vsize: 282652
[startup+269.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 70421 0 0 0 26871 131 0 0 25 0 1 0 834896008 300187648 70345 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 73288 70345 1111 63 0 73225 0
vsize: 293152
[startup+279.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 72954 0 0 0 27867 135 0 0 25 0 1 0 834896008 310484992 72878 4294967295 134512640 134714508 3221224592 3221222820 1077414351 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 75802 72878 1111 63 0 75739 0
vsize: 303208
[startup+289.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 75557 0 0 0 28862 140 0 0 25 0 1 0 834896008 321089536 75481 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 78391 75481 1111 63 0 78328 0
vsize: 313564
[startup+299.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 78107 0 0 0 29858 145 0 0 25 0 1 0 834896008 331538432 78031 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 80942 78031 1111 63 0 80879 0
vsize: 323768
[startup+309.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 80630 0 0 0 30854 149 0 0 25 0 1 0 834896008 341991424 80554 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 83494 80554 1111 63 0 83431 0
vsize: 333976
[startup+319.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 83243 0 0 0 31849 154 0 0 25 0 1 0 834896008 352591872 83167 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 86082 83167 1111 63 0 86019 0
vsize: 344328
[startup+329.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 85862 0 0 0 32845 158 0 0 25 0 1 0 834896008 363343872 85786 4294967295 134512640 134714508 3221224592 3221222820 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 88707 85786 1111 63 0 88644 0
vsize: 354828
[startup+339.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 88427 0 0 0 33841 162 0 0 25 0 1 0 834896008 373792768 88351 4294967295 134512640 134714508 3221224592 3221222820 1077414407 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 91258 88351 1111 63 0 91195 0
vsize: 365032
[startup+349.996 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 90937 0 0 0 34837 167 0 0 25 0 1 0 834896008 384098304 90861 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 93774 90861 1111 63 0 93711 0
vsize: 375096
[startup+359.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 93543 0 0 0 35833 171 0 0 25 0 1 0 834896008 394846208 93467 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 96398 93467 1111 63 0 96335 0
vsize: 385592
[startup+369.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 96053 0 0 0 36829 175 0 0 25 0 1 0 834896008 405151744 95977 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 98914 95977 1111 63 0 98851 0
vsize: 395656
[startup+379.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 98567 0 0 0 37825 179 0 0 25 0 1 0 834896008 415518720 98491 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 101445 98491 1111 63 0 101382 0
vsize: 405780
[startup+389.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 101087 0 0 0 38820 184 0 0 25 0 1 0 834896008 425816064 101011 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 103959 101011 1111 63 0 103896 0
vsize: 415836
[startup+399.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 103635 0 0 0 39815 189 0 0 25 0 1 0 834896008 436269056 103559 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 106511 103559 1111 63 0 106448 0
vsize: 426044
[startup+409.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 106114 0 0 0 40811 193 0 0 25 0 1 0 834896008 446423040 106038 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 108990 106038 1111 63 0 108927 0
vsize: 435960
[startup+419.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 108813 0 0 0 41807 197 0 0 25 0 1 0 834896008 457474048 108737 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 111688 108737 1111 63 0 111625 0
vsize: 446752
[startup+429.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 111377 0 0 0 42803 202 0 0 25 0 1 0 834896008 467918848 111301 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 114238 111301 1111 63 0 114175 0
vsize: 456952
[startup+439.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 113990 0 0 0 43799 206 0 0 25 0 1 0 834896008 478674944 113914 4294967295 134512640 134714508 3221224592 3221222820 1077414376 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 116864 113914 1111 63 0 116801 0
vsize: 467456
[startup+449.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 116603 0 0 0 44795 210 0 0 25 0 1 0 834896008 489418752 116527 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 119487 116527 1111 63 0 119424 0
vsize: 477948
[startup+459.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 119144 0 0 0 45790 215 0 0 25 0 1 0 834896008 499724288 119068 4294967295 134512640 134714508 3221224592 3221222820 1077414336 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 122003 119068 1111 63 0 121940 0
vsize: 488012
[startup+469.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 121689 0 0 0 46786 219 0 0 25 0 1 0 834896008 510173184 121613 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 124554 121613 1111 63 0 124491 0
vsize: 498216
[startup+479.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 124279 0 0 0 47782 224 0 0 25 0 1 0 834896008 520777728 124203 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 127143 124203 1111 63 0 127080 0
vsize: 508572
[startup+489.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 126843 0 0 0 48777 229 0 0 25 0 1 0 834896008 531226624 126767 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 129694 126767 1111 63 0 129631 0
vsize: 518776
[startup+499.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 129397 0 0 0 49773 233 0 0 25 0 1 0 834896008 541679616 129321 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 132246 129321 1111 63 0 132183 0
vsize: 528984
[startup+509.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 132269 0 0 0 50769 237 0 0 25 0 1 0 834896008 553472000 132193 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 135125 132193 1111 63 0 135062 0
vsize: 540500
[startup+519.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 135133 0 0 0 51765 242 0 0 25 0 1 0 834896008 565268480 135057 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 138005 135057 1111 63 0 137942 0
vsize: 552020
[startup+529.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 137989 0 0 0 52760 246 0 0 25 0 1 0 834896008 576913408 137913 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 140848 137913 1111 63 0 140785 0
vsize: 563392
[startup+539.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 141010 0 0 0 53756 251 0 0 25 0 1 0 834896008 589307904 140934 4294967295 134512640 134714508 3221224592 3221222820 1077414401 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 143874 140934 1111 63 0 143811 0
vsize: 575496
[startup+549.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 143700 0 0 0 54753 255 0 0 25 0 1 0 834896008 600350720 143624 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 146570 143624 1111 63 0 146507 0
vsize: 586280
[startup+559.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 146430 0 0 0 55748 259 0 0 25 0 1 0 834896008 611553280 146354 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 149305 146354 1111 63 0 149242 0
vsize: 597220
[startup+569.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 148933 0 0 0 56744 264 0 0 25 0 1 0 834896008 621703168 148857 4294967295 134512640 134714508 3221224592 3221222820 1077414408 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 151783 148857 1111 63 0 151720 0
vsize: 607132
[startup+579.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 151498 0 0 0 57741 267 0 0 25 0 1 0 834896008 632307712 151422 4294967295 134512640 134714508 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 154372 151422 1111 63 0 154309 0
vsize: 617488
[startup+589.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 154173 0 0 0 58736 272 0 0 25 0 1 0 834896008 643207168 154097 4294967295 134512640 134714508 3221224592 3221222820 1077414360 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 157033 154097 1111 63 0 156970 0
vsize: 628132
[startup+599.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 156931 0 0 0 59731 277 0 0 25 0 1 0 834896008 654553088 156855 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 159803 156855 1111 63 0 159740 0
vsize: 639212
[startup+609.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 159873 0 0 0 60726 283 0 0 25 0 1 0 834896008 666497024 159797 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 162719 159797 1111 63 0 162656 0
vsize: 650876
[startup+619.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 162656 0 0 0 61720 287 0 0 25 0 1 0 834896008 677994496 162580 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 165526 162580 1111 63 0 165463 0
vsize: 662104
[startup+629.997 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 165197 0 0 0 62714 293 0 0 25 0 1 0 834896008 688295936 165121 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 168041 165121 1111 63 0 167978 0
vsize: 672164
[startup+639.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 167846 0 0 0 63709 297 0 0 25 0 1 0 834896008 699195392 167770 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 170702 167770 1111 63 0 170639 0
vsize: 682808
[startup+649.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 170550 0 0 0 64704 301 0 0 25 0 1 0 834896008 710242304 170474 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 173399 170474 1111 63 0 173336 0
vsize: 693596
[startup+659.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 173091 0 0 0 65698 306 0 0 25 0 1 0 834896008 720695296 173015 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 175951 173015 1111 63 0 175888 0
vsize: 703804
[startup+669.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 175624 0 0 0 66691 311 0 0 25 0 1 0 834896008 730996736 175548 4294967295 134512640 134714508 3221224592 3221222820 1077414426 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 178466 175548 1111 63 0 178403 0
vsize: 713864
[startup+679.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 178148 0 0 0 67686 315 0 0 25 0 1 0 834896008 741302272 178072 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 180982 178072 1111 63 0 180919 0
vsize: 723928
[startup+689.998 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 180523 0 0 0 68680 321 0 0 25 0 1 0 834896008 751153152 180447 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 183387 180447 1111 63 0 183324 0
vsize: 733548
[startup+699.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 182917 0 0 0 69674 326 0 0 25 0 1 0 834896008 760856576 182841 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 185756 182841 1111 63 0 185693 0
vsize: 743024
[startup+709.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 185331 0 0 0 70668 331 0 0 25 0 1 0 834896008 770715648 185255 4294967295 134512640 134714508 3221224592 3221222864 134524935 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 188163 185255 1111 63 0 188100 0
vsize: 752652
[startup+719.999 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 187712 0 0 0 71663 334 0 0 25 0 1 0 834896008 780566528 187636 4294967295 134512640 134714508 3221224592 3221222820 1077414358 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 190568 187636 1111 63 0 190505 0
vsize: 762272
[startup+730 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 190106 0 0 0 72659 338 0 0 25 0 1 0 834896008 790269952 190030 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 192937 190030 1111 63 0 192874 0
vsize: 771748
[startup+740 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 192859 0 0 0 73653 343 0 0 25 0 1 0 834896008 801619968 192783 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 195708 192783 1111 63 0 195645 0
vsize: 782832
[startup+750.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 195396 0 0 0 74647 347 0 0 25 0 1 0 834896008 812285952 195320 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198312 195320 1111 63 0 198249 0
vsize: 793248
[startup+760.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 198026 0 0 0 75641 352 0 0 25 0 1 0 834896008 823033856 197854 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 200936 197854 1111 63 0 200873 0
vsize: 803744
[startup+770.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 200669 0 0 0 76636 356 0 0 25 0 1 0 834896008 833781760 200369 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 203560 200369 1111 63 0 203497 0
vsize: 814240
[startup+780.002 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 203247 0 0 0 77629 362 0 0 25 0 1 0 834896008 844382208 202787 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 206148 202787 1111 63 0 206085 0
vsize: 824592
[startup+790.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 205779 0 0 0 78623 367 0 0 25 0 1 0 834896008 854831104 205159 4294967295 134512640 134714508 3221224592 3221222820 1077414395 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 208699 205159 1111 63 0 208636 0
vsize: 834796
[startup+800.001 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 208552 0 0 0 79616 372 0 0 25 0 1 0 834896008 866181120 207580 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 211470 207580 1111 63 0 211407 0
vsize: 845880
[startup+810.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 211341 0 0 0 80608 379 0 0 25 0 1 0 834896008 877531136 210113 4294967295 134512640 134714508 3221224592 3221222820 1077414376 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214241 210113 1111 63 0 214178 0
vsize: 856964
[startup+820.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 213961 0 0 0 81601 385 0 0 25 0 1 0 834896008 888279040 212445 4294967295 134512640 134714508 3221224592 3221222820 1077414360 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 216865 212445 1111 63 0 216802 0
vsize: 867460
[startup+830.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 216719 0 0 0 82593 392 0 0 25 0 1 0 834896008 899624960 214883 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 219635 214883 1111 63 0 219572 0
vsize: 878540
[startup+840.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 219508 0 0 0 83585 398 0 0 25 0 1 0 834896008 910970880 217288 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 222405 217288 1111 63 0 222342 0
vsize: 889620
[startup+850.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 222255 0 0 0 84577 404 0 0 25 0 1 0 834896008 922169344 219619 4294967295 134512640 134714508 3221224592 3221222820 1077414395 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 225139 219619 1111 63 0 225076 0
vsize: 900556
[startup+860.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 224679 0 0 0 85570 409 0 0 25 0 1 0 834896008 932171776 221693 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 227581 221693 1111 63 0 227518 0
vsize: 910324
[startup+870.004 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 226972 0 0 0 86564 415 0 0 25 0 1 0 834896008 941580288 223602 4294967295 134512640 134714508 3221224592 3221222820 1077414410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 229878 223602 1111 63 0 229815 0
vsize: 919512
[startup+872.676 s]
Raw data (loadavg): 1.06 0.99 0.93 1/53 15397
Raw data (stat): 15397 (bsolo_lpr) R 15396 7475 7474 0 -1 0 226972 0 0 0 86564 415 0 0 25 0 1 0 834896008 941580288 223602 4294967295 134512640 134714508 3221224592 3221222820 1077414410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 229878 223602 1111 63 0 229815 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 872.676
CPU time (s): 872.459
CPU user time (s): 867.879
CPU system time (s): 4.5803
CPU usage (%): 99.9752
Max. virtual memory (Kb): 919512
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####