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 25753

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-22 07:07:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17850 boxname=wulflinc31 idbench=1374 idsolver=1 numberseed=0
MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef  /oldhome/oroussel/solvers/bsolo_lpr
MD5SUM BENCH:  5a18ff1f45b144b201f1f80233dc9b6b  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-nw04.opb
REAL COMMAND:  bsolo_lpr /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-nw04.opb
IDLAUNCH: 17850
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        902148 kB
Buffers:         11596 kB
Cached:         100452 kB
SwapCached:        900 kB
Active:          76464 kB
Inactive:        37640 kB
HighTotal:      131008 kB
HighFree:        29428 kB
LowTotal:       903652 kB
LowFree:        872720 kB
SwapTotal:     2097892 kB
SwapFree:      2095960 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5096 kB
Slab:            12584 kB
Committed_AS:    63856 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-22 07:21:54 (client local time) WITH STATUS 0 IN 879.979 SECONDS
stats: 17850 7 879.979 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.93 0.98 0.97 2/55 21178
Raw data (stat): 21178 (runsolver) R 21177 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 811010418 1056768 100 4294967295 134512640 135381576 3221221680 3221216900 135158418 0 2147483391 1 90112 0 0 0 17 1 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0016 s]
Raw data (loadavg): 0.94 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 3332 0 0 0 985 10 0 0 25 0 1 0 811010418 25239552 3255 4294967295 134512640 134714508 3221221792 3221220020 1077414433 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 6162 3255 1111 63 0 6099 0
vsize: 24648
[startup+20.0024 s]
Raw data (loadavg): 0.95 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 5885 0 0 0 1981 14 0 0 25 0 1 0 811010418 35692544 5808 4294967295 134512640 134714508 3221221792 3221220020 1077414426 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 8714 5808 1111 63 0 8651 0
vsize: 34856
[startup+30.0026 s]
Raw data (loadavg): 0.95 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 8445 0 0 0 2977 19 0 0 25 0 1 0 811010418 46280704 8368 4294967295 134512640 134714508 3221221792 3221220020 1077414349 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 11299 8368 1111 63 0 11236 0
vsize: 45196
[startup+40.0032 s]
Raw data (loadavg): 0.96 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 11003 0 0 0 3972 24 0 0 25 0 1 0 811010418 56733696 10926 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13851 10926 1111 63 0 13788 0
vsize: 55404
[startup+50.0042 s]
Raw data (loadavg): 0.97 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 13595 0 0 0 4968 28 0 0 25 0 1 0 811010418 67305472 13518 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 16432 13518 1111 63 0 16369 0
vsize: 65728
[startup+60.0051 s]
Raw data (loadavg): 0.97 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 16185 0 0 0 5964 33 0 0 25 0 1 0 811010418 77901824 16108 4294967295 134512640 134714508 3221221792 3221220020 1077414351 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 19019 16108 1111 63 0 18956 0
vsize: 76076
[startup+70.0061 s]
Raw data (loadavg): 0.97 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 18778 0 0 0 6961 36 0 0 25 0 1 0 811010418 88506368 18701 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 21608 18701 1111 63 0 21545 0
vsize: 86432
[startup+80.006 s]
Raw data (loadavg): 0.98 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 21373 0 0 0 7956 41 0 0 25 0 1 0 811010418 99258368 21296 4294967295 134512640 134714508 3221221792 3221220020 1077414435 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 24233 21296 1111 63 0 24170 0
vsize: 96932
[startup+90.0072 s]
Raw data (loadavg): 0.98 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 23979 0 0 0 8952 45 0 0 25 0 1 0 811010418 109858816 23902 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 26821 23902 1111 63 0 26758 0
vsize: 107284
[startup+100.008 s]
Raw data (loadavg): 0.98 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 26580 0 0 0 9949 49 0 0 25 0 1 0 811010418 120582144 26503 4294967295 134512640 134714508 3221221792 3221220020 1077414420 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 29439 26503 1111 63 0 29376 0
vsize: 117756
[startup+110.009 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 29163 0 0 0 10945 53 0 0 25 0 1 0 811010418 131182592 29086 4294967295 134512640 134714508 3221221792 3221220020 1077414383 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 32027 29086 1111 63 0 31964 0
vsize: 128108
[startup+120.009 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 31752 0 0 0 11941 57 0 0 25 0 1 0 811010418 141783040 31675 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 34615 31675 1111 63 0 34552 0
vsize: 138460
[startup+130.01 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 34315 0 0 0 12937 61 0 0 25 0 1 0 811010418 152231936 34238 4294967295 134512640 134714508 3221221792 3221220020 1077414383 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 37166 34238 1111 63 0 37103 0
vsize: 148664
[startup+140.011 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 36873 0 0 0 13934 64 0 0 25 0 1 0 811010418 162680832 36796 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 39717 36796 1111 63 0 39654 0
vsize: 158868
[startup+150.012 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 39427 0 0 0 14930 69 0 0 25 0 1 0 811010418 173137920 39350 4294967295 134512640 134714508 3221221792 3221220020 1077414345 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 42270 39350 1111 63 0 42207 0
vsize: 169080
[startup+160.012 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 42015 0 0 0 15926 73 0 0 25 0 1 0 811010418 183734272 41938 4294967295 134512640 134714508 3221221792 3221220020 1077414358 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 44857 41938 1111 63 0 44794 0
vsize: 179428
[startup+170.012 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 44616 0 0 0 16920 79 0 0 25 0 1 0 811010418 194338816 44539 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 47446 44539 1111 63 0 47383 0
vsize: 189784
[startup+180.012 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 47191 0 0 0 17916 83 0 0 25 0 1 0 811010418 204935168 47114 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 50033 47114 1111 63 0 49970 0
vsize: 200132
[startup+190.013 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 49887 0 0 0 18911 88 0 0 25 0 1 0 811010418 215982080 49810 4294967295 134512640 134714508 3221221792 3221220020 1077414383 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 52730 49810 1111 63 0 52667 0
vsize: 210920
[startup+200.013 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 52526 0 0 0 19908 92 0 0 25 0 1 0 811010418 226885632 52449 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 55392 52449 1111 63 0 55329 0
vsize: 221568
[startup+210.014 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 55131 0 0 0 20904 95 0 0 25 0 1 0 811010418 237481984 55054 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 57979 55054 1111 63 0 57916 0
vsize: 231916
[startup+220.015 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 57686 0 0 0 21901 99 0 0 25 0 1 0 811010418 247930880 57609 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 60530 57609 1111 63 0 60467 0
vsize: 242120
[startup+230.015 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 60267 0 0 0 22897 103 0 0 25 0 1 0 811010418 258535424 60190 4294967295 134512640 134714508 3221221792 3221220020 1077414376 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 63119 60190 1111 63 0 63056 0
vsize: 252476
[startup+240.016 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 62825 0 0 0 23893 107 0 0 25 0 1 0 811010418 268984320 62748 4294967295 134512640 134714508 3221221792 3221220020 1077414407 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 65670 62748 1111 63 0 65607 0
vsize: 262680
[startup+250.017 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 65457 0 0 0 24889 112 0 0 25 0 1 0 811010418 279736320 65380 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 68295 65380 1111 63 0 68232 0
vsize: 273180
[startup+260.018 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 68089 0 0 0 25884 117 0 0 25 0 1 0 811010418 290635776 68012 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 70956 68012 1111 63 0 70893 0
vsize: 283824
[startup+270.019 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 70672 0 0 0 26880 121 0 0 25 0 1 0 811010418 301084672 70595 4294967295 134512640 134714508 3221221792 3221220020 1077414426 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 73507 70595 1111 63 0 73444 0
vsize: 294028
[startup+280.019 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 73204 0 0 0 27876 125 0 0 25 0 1 0 811010418 311533568 73127 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 76058 73127 1111 63 0 75995 0
vsize: 304232
[startup+290.02 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 75807 0 0 0 28871 130 0 0 25 0 1 0 811010418 322138112 75730 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 78647 75730 1111 63 0 78584 0
vsize: 314588
[startup+300.02 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 78352 0 0 0 29868 134 0 0 25 0 1 0 811010418 332587008 78275 4294967295 134512640 134714508 3221221792 3221220144 134567410 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 81198 78275 1111 63 0 81135 0
vsize: 324792
[startup+310.021 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 80875 0 0 0 30864 138 0 0 25 0 1 0 811010418 342892544 80798 4294967295 134512640 134714508 3221221792 3221220020 1077414401 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 83714 80798 1111 63 0 83651 0
vsize: 334856
[startup+320.021 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 83469 0 0 0 31861 142 0 0 25 0 1 0 811010418 353488896 83392 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 86301 83392 1111 63 0 86238 0
vsize: 345204
[startup+330.022 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 86096 0 0 0 32856 146 0 0 25 0 1 0 811010418 364240896 86019 4294967295 134512640 134714508 3221221792 3221220144 134567410 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 88926 86019 1111 63 0 88863 0
vsize: 355704
[startup+340.022 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 88623 0 0 0 33853 150 0 0 25 0 1 0 811010418 374689792 88546 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 91477 88546 1111 63 0 91414 0
vsize: 365908
[startup+350.022 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 91139 0 0 0 34849 153 0 0 25 0 1 0 811010418 384995328 91062 4294967295 134512640 134714508 3221221792 3221220020 1077414426 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 93993 91062 1111 63 0 93930 0
vsize: 375972
[startup+360.023 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 93721 0 0 0 35845 158 0 0 25 0 1 0 811010418 395595776 93644 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 96581 93644 1111 63 0 96518 0
vsize: 386324
[startup+370.024 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 96230 0 0 0 36841 163 0 0 25 0 1 0 811010418 405749760 96153 4294967295 134512640 134714508 3221221792 3221220020 1077414408 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 99060 96153 1111 63 0 98997 0
vsize: 396240
[startup+380.024 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 98733 0 0 0 37836 167 0 0 25 0 1 0 811010418 416116736 98656 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 101591 98656 1111 63 0 101528 0
vsize: 406364
[startup+390.025 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 101217 0 0 0 38834 170 0 0 25 0 1 0 811010418 426418176 101140 4294967295 134512640 134714508 3221221792 3221220020 1077414370 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 104106 101140 1111 63 0 104043 0
vsize: 416424
[startup+400.026 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 103746 0 0 0 39830 174 0 0 25 0 1 0 811010418 436723712 103669 4294967295 134512640 134714508 3221221792 3221220020 1077414426 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 106622 103669 1111 63 0 106559 0
vsize: 426488
[startup+410.027 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 106207 0 0 0 40827 177 0 0 25 0 1 0 811010418 446722048 106130 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 109063 106130 1111 63 0 109000 0
vsize: 436252
[startup+420.027 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 108924 0 0 0 41822 182 0 0 25 0 1 0 811010418 457924608 108847 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 111798 108847 1111 63 0 111735 0
vsize: 447192
[startup+430.027 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 111458 0 0 0 42818 186 0 0 25 0 1 0 811010418 468221952 111381 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 114312 111381 1111 63 0 114249 0
vsize: 457248
[startup+440.028 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 114071 0 0 0 43813 192 0 0 25 0 1 0 811010418 478973952 113994 4294967295 134512640 134714508 3221221792 3221220020 1077414351 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 116937 113994 1111 63 0 116874 0
vsize: 467748
[startup+450.028 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 116648 0 0 0 44809 196 0 0 25 0 1 0 811010418 489574400 116571 4294967295 134512640 134714508 3221221792 3221220020 1077414408 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 119525 116571 1111 63 0 119462 0
vsize: 478100
[startup+460.029 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 119176 0 0 0 45804 201 0 0 25 0 1 0 811010418 499879936 119099 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 122041 119099 1111 63 0 121978 0
vsize: 488164
[startup+470.029 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 121704 0 0 0 46801 204 0 0 25 0 1 0 811010418 510177280 121627 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 124555 121627 1111 63 0 124492 0
vsize: 498220
[startup+480.029 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 124269 0 0 0 47796 210 0 0 25 0 1 0 811010418 520781824 124192 4294967295 134512640 134714508 3221221792 3221220020 1077414382 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 127144 124192 1111 63 0 127081 0
vsize: 508576
[startup+490.03 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 126809 0 0 0 48791 215 0 0 25 0 1 0 811010418 531079168 126732 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 129658 126732 1111 63 0 129595 0
vsize: 518632
[startup+500.031 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 129332 0 0 0 49787 219 0 0 25 0 1 0 811010418 541536256 129255 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 132211 129255 1111 63 0 132148 0
vsize: 528844
[startup+510.032 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 132204 0 0 0 50783 223 0 0 25 0 1 0 811010418 553177088 132127 4294967295 134512640 134714508 3221221792 3221220020 1077414420 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 135053 132127 1111 63 0 134990 0
vsize: 540212
[startup+520.032 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 135062 0 0 0 51778 228 0 0 25 0 1 0 811010418 564973568 134985 4294967295 134512640 134714508 3221221792 3221220020 1077414383 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 137933 134985 1111 63 0 137870 0
vsize: 551732
[startup+530.033 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 137887 0 0 0 52774 233 0 0 25 0 1 0 811010418 576471040 137810 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 140740 137810 1111 63 0 140677 0
vsize: 562960
[startup+540.034 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 140921 0 0 0 53768 239 0 0 25 0 1 0 811010418 588865536 140844 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 143766 140844 1111 63 0 143703 0
vsize: 575064
[startup+550.034 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 143611 0 0 0 54764 243 0 0 25 0 1 0 811010418 599908352 143534 4294967295 134512640 134714508 3221221792 3221220020 1077414407 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 146462 143534 1111 63 0 146399 0
vsize: 585848
[startup+560.034 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 146317 0 0 0 55760 248 0 0 25 0 1 0 811010418 610959360 146240 4294967295 134512640 134714508 3221221792 3221220020 1077414358 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 149160 146240 1111 63 0 149097 0
vsize: 596640
[startup+570.035 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 148802 0 0 0 56756 251 0 0 25 0 1 0 811010418 621260800 148725 4294967295 134512640 134714508 3221221792 3221220020 1077414435 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 151675 148725 1111 63 0 151612 0
vsize: 606700
[startup+580.035 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 151330 0 0 0 57751 256 0 0 25 0 1 0 811010418 631566336 151253 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 154191 151253 1111 63 0 154128 0
vsize: 616764
[startup+590.036 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 153980 0 0 0 58747 261 0 0 25 0 1 0 811010418 642461696 153903 4294967295 134512640 134714508 3221221792 3221220020 1077414410 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 156851 153903 1111 63 0 156788 0
vsize: 627404
[startup+600.037 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 156684 0 0 0 59742 266 0 0 25 0 1 0 811010418 653512704 156607 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 159549 156607 1111 63 0 159486 0
vsize: 638196
[startup+610.037 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 159608 0 0 0 60737 271 0 0 25 0 1 0 811010418 665456640 159531 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 162465 159531 1111 63 0 162402 0
vsize: 649860
[startup+620.037 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 162396 0 0 0 61731 278 0 0 25 0 1 0 811010418 676798464 162319 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 165234 162319 1111 63 0 165171 0
vsize: 660936
[startup+630.038 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 164907 0 0 0 62727 282 0 0 25 0 1 0 811010418 687104000 164830 4294967295 134512640 134714508 3221221792 3221220020 1077414349 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 167750 164830 1111 63 0 167687 0
vsize: 671000
[startup+640.038 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 167495 0 0 0 63723 286 0 0 25 0 1 0 811010418 697704448 167418 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 170338 167418 1111 63 0 170275 0
vsize: 681352
[startup+650.038 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 170193 0 0 0 64718 291 0 0 25 0 1 0 811010418 708755456 170116 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 173036 170116 1111 63 0 172973 0
vsize: 692144
[startup+660.038 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 172722 0 0 0 65715 294 0 0 25 0 1 0 811010418 719204352 172645 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 175587 172645 1111 63 0 175524 0
vsize: 702348
[startup+670.039 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 175232 0 0 0 66711 298 0 0 25 0 1 0 811010418 729358336 175155 4294967295 134512640 134714508 3221221792 3221220020 1077414357 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 178066 175155 1111 63 0 178003 0
vsize: 712264
[startup+680.039 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 177706 0 0 0 67707 302 0 0 25 0 1 0 811010418 739508224 177629 4294967295 134512640 134714508 3221221792 3221220020 1077414351 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 180544 177629 1111 63 0 180481 0
vsize: 722176
[startup+690.039 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 180082 0 0 0 68703 306 0 0 25 0 1 0 811010418 749211648 180005 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 182913 180005 1111 63 0 182850 0
vsize: 731652
[startup+700.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 182415 0 0 0 69700 310 0 0 25 0 1 0 811010418 758771712 182338 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 185247 182338 1111 63 0 185184 0
vsize: 740988
[startup+710.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 184773 0 0 0 70696 314 0 0 25 0 1 0 811010418 768475136 184696 4294967295 134512640 134714508 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 187616 184696 1111 63 0 187553 0
vsize: 750464
[startup+720.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 187167 0 0 0 71691 319 0 0 25 0 1 0 811010418 778326016 187090 4294967295 134512640 134714508 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 190021 187090 1111 63 0 189958 0
vsize: 760084
[startup+730.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 189477 0 0 0 72687 323 0 0 25 0 1 0 811010418 787738624 189400 4294967295 134512640 134714508 3221221792 3221220144 134567410 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 192319 189400 1111 63 0 192256 0
vsize: 769276
[startup+740.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 192095 0 0 0 73683 327 0 0 25 0 1 0 811010418 798486528 192018 4294967295 134512640 134714508 3221221792 3221220448 134527935 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 194943 192018 1111 63 0 194880 0
vsize: 779772
[startup+750.041 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 194579 0 0 0 74678 333 0 0 25 0 1 0 811010418 808636416 194502 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 197421 194502 1111 63 0 197358 0
vsize: 789684
[startup+760.041 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 197214 0 0 0 75673 337 0 0 25 0 1 0 811010418 819752960 197137 4294967295 134512640 134714508 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 200135 197137 1111 63 0 200072 0
vsize: 800540
[startup+770.041 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 199637 0 0 0 76670 342 0 0 25 0 1 0 811010418 829603840 199560 4294967295 134512640 134714508 3221221792 3221220448 134527930 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 202540 199560 1111 63 0 202477 0
vsize: 810160
[startup+780.042 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 202307 0 0 0 77665 346 0 0 25 0 1 0 811010418 840507392 202230 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 205202 202230 1111 63 0 205139 0
vsize: 820808
[startup+790.042 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 204797 0 0 0 78661 351 0 0 25 0 1 0 811010418 850804736 204720 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 207716 204720 1111 63 0 207653 0
vsize: 830864
[startup+800.043 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 207423 0 0 0 79657 355 0 0 25 0 1 0 811010418 861556736 207346 4294967295 134512640 134714508 3221221792 3221220020 1077414345 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 210341 207346 1111 63 0 210278 0
vsize: 841364
[startup+810.044 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 209945 0 0 0 80653 359 0 0 25 0 1 0 811010418 871858176 209868 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 212856 209868 1111 63 0 212793 0
vsize: 851424
[startup+820.044 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 212541 0 0 0 81649 364 0 0 25 0 1 0 811010418 882462720 212464 4294967295 134512640 134714508 3221221792 3221220020 1077414357 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 215445 212464 1111 63 0 215382 0
vsize: 861780
[startup+830.044 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 215323 0 0 0 82645 367 0 0 25 0 1 0 811010418 893804544 215246 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 218214 215246 1111 63 0 218151 0
vsize: 872856
[startup+840.045 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 217766 0 0 0 83641 372 0 0 25 0 1 0 811010418 903811072 217689 4294967295 134512640 134714508 3221221792 3221220020 1077414351 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 220657 217689 1111 63 0 220594 0
vsize: 882628
[startup+850.045 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 220630 0 0 0 84636 377 0 0 25 0 1 0 811010418 915607552 220553 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 223537 220553 1111 63 0 223474 0
vsize: 894148
[startup+860.045 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 223169 0 0 0 85633 380 0 0 25 0 1 0 811010418 925908992 223092 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 226052 223092 1111 63 0 225989 0
vsize: 904208
[startup+870.046 s]
Raw data (loadavg): 0.99 0.98 0.97 2/55 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 225454 0 0 0 86626 387 0 0 25 0 1 0 811010418 935313408 225140 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 228348 225140 1111 63 0 228285 0
vsize: 913392
[startup+879.882 s]
Raw data (loadavg): 0.99 0.98 0.97 1/54 21178
Raw data (stat): 21178 (bsolo_lpr) R 21177 7876 7672 0 -1 0 225454 0 0 0 86626 387 0 0 25 0 1 0 811010418 935313408 225140 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 228348 225140 1111 63 0 228285 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 879.881
CPU time (s): 879.979
CPU user time (s): 875.619
CPU system time (s): 4.36034
CPU usage (%): 100.011
Max. virtual memory (Kb): 913392
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####