PB'05 competition: run trace

Some explanations

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

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

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-21 09:41:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18669 boxname=wulflinc31 idbench=1437 idsolver=1 numberseed=0
MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef  /oldhome/oroussel/solvers/bsolo_lpr
MD5SUM BENCH:  a5c401bba5afccf02c7b40cb1c595b15  /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: 18669
/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:        893008 kB
Buffers:          3948 kB
Cached:         116488 kB
SwapCached:       1080 kB
Active:          52260 kB
Inactive:        70508 kB
HighTotal:      131008 kB
HighFree:        58100 kB
LowTotal:       903652 kB
LowFree:        834908 kB
SwapTotal:     2097892 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5344 kB
Slab:            13180 kB
Committed_AS:    63860 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-21 09:56:18 (client local time) WITH STATUS 0 IN 877.573 SECONDS
stats: 18669 7 877.573 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): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (runsolver) R 8665 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 803296139 1056768 100 4294967295 134512640 135381576 3221221680 3221216900 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0014 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 3302 0 0 0 974 11 0 0 25 0 1 0 803296139 25239552 3225 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 6162 3225 1111 63 0 6099 0
vsize: 24648
[startup+20.0015 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 5861 0 0 0 1969 16 0 0 25 0 1 0 803296139 35692544 5784 4294967295 134512640 134714508 3221221792 3221220020 1077414351 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8714 5784 1111 63 0 8651 0
vsize: 34856
[startup+30.0025 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 8414 0 0 0 2966 20 0 0 25 0 1 0 803296139 46129152 8337 4294967295 134512640 134714508 3221221792 3221220020 1077414410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11262 8337 1111 63 0 11199 0
vsize: 45048
[startup+40.0037 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 10965 0 0 0 3960 25 0 0 25 0 1 0 803296139 56578048 10888 4294967295 134512640 134714508 3221221792 3221220020 1077414410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13813 10888 1111 63 0 13750 0
vsize: 55252
[startup+50.0033 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 13547 0 0 0 4956 30 0 0 25 0 1 0 803296139 67158016 13470 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 16396 13470 1111 63 0 16333 0
vsize: 65584
[startup+60.0033 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 16129 0 0 0 5952 34 0 0 25 0 1 0 803296139 77754368 16052 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18983 16052 1111 63 0 18920 0
vsize: 75932
[startup+70.0038 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 18724 0 0 0 6947 39 0 0 25 0 1 0 803296139 88358912 18647 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 21572 18647 1111 63 0 21509 0
vsize: 86288
[startup+80.0051 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 21317 0 0 0 7942 44 0 0 25 0 1 0 803296139 98955264 21240 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 24159 21240 1111 63 0 24096 0
vsize: 96636
[startup+90.0051 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 23918 0 0 0 8937 49 0 0 25 0 1 0 803296139 109559808 23841 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 26748 23841 1111 63 0 26685 0
vsize: 106992
[startup+100.005 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 26524 0 0 0 9933 54 0 0 25 0 1 0 803296139 120279040 26447 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 29365 26447 1111 63 0 29302 0
vsize: 117460
[startup+110.006 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 29108 0 0 0 10929 58 0 0 25 0 1 0 803296139 130883584 29031 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 31954 29031 1111 63 0 31891 0
vsize: 127816
[startup+120.006 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 31696 0 0 0 11925 62 0 0 25 0 1 0 803296139 141479936 31619 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 34541 31619 1111 63 0 34478 0
vsize: 138164
[startup+130.008 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 34261 0 0 0 12922 66 0 0 25 0 1 0 803296139 151932928 34184 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 37093 34184 1111 63 0 37030 0
vsize: 148372
[startup+140.008 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 36819 0 0 0 13917 70 0 0 25 0 1 0 803296139 162533376 36742 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 39681 36742 1111 63 0 39618 0
vsize: 158724
[startup+150.008 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 39372 0 0 0 14914 74 0 0 25 0 1 0 803296139 172986368 39295 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 42233 39295 1111 63 0 42170 0
vsize: 168932
[startup+160.008 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 41954 0 0 0 15910 78 0 0 25 0 1 0 803296139 183435264 41877 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 44784 41877 1111 63 0 44721 0
vsize: 179136
[startup+170.009 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 44555 0 0 0 16906 83 0 0 25 0 1 0 803296139 194187264 44478 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 47409 44478 1111 63 0 47346 0
vsize: 189636
[startup+180.009 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 47137 0 0 0 17902 87 0 0 25 0 1 0 803296139 204787712 47060 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 49997 47060 1111 63 0 49934 0
vsize: 199988
[startup+190.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 49827 0 0 0 18897 91 0 0 25 0 1 0 803296139 215834624 49750 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 52694 49750 1111 63 0 52631 0
vsize: 210776
[startup+200.01 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 52470 0 0 0 19894 95 0 0 25 0 1 0 803296139 226578432 52393 4294967295 134512640 134714508 3221221792 3221220020 1077414426 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 55317 52393 1111 63 0 55254 0
vsize: 221268
[startup+210.011 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 55077 0 0 0 20890 99 0 0 25 0 1 0 803296139 237334528 55000 4294967295 134512640 134714508 3221221792 3221220144 134567410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 57943 55000 1111 63 0 57880 0
vsize: 231772
[startup+220.012 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 57630 0 0 0 21887 102 0 0 25 0 1 0 803296139 247779328 57553 4294967295 134512640 134714508 3221221792 3221220020 1077414383 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 60493 57553 1111 63 0 60430 0
vsize: 241972
[startup+230.012 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 60218 0 0 0 22880 109 0 0 25 0 1 0 803296139 258383872 60141 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 63082 60141 1111 63 0 63019 0
vsize: 252328
[startup+240.013 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 62764 0 0 0 23878 112 0 0 25 0 1 0 803296139 268832768 62687 4294967295 134512640 134714508 3221221792 3221220020 1077414420 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 65633 62687 1111 63 0 65570 0
vsize: 262532
[startup+250.014 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 65403 0 0 0 24873 117 0 0 25 0 1 0 803296139 279584768 65326 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 68258 65326 1111 63 0 68195 0
vsize: 273032
[startup+260.014 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 68033 0 0 0 25868 122 0 0 25 0 1 0 803296139 290332672 67956 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 70882 67956 1111 63 0 70819 0
vsize: 283528
[startup+270.014 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 70617 0 0 0 26864 126 0 0 25 0 1 0 803296139 300937216 70540 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 73471 70540 1111 63 0 73408 0
vsize: 293884
[startup+280.015 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 73150 0 0 0 27860 130 0 0 25 0 1 0 803296139 311234560 73073 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 75985 73073 1111 63 0 75922 0
vsize: 303940
[startup+290.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 75753 0 0 0 28855 136 0 0 25 0 1 0 803296139 321990656 75676 4294967295 134512640 134714508 3221221792 3221220448 134527930 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 78611 75676 1111 63 0 78548 0
vsize: 314444
[startup+300.016 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 78297 0 0 0 29850 141 0 0 25 0 1 0 803296139 332435456 78220 4294967295 134512640 134714508 3221221792 3221220020 1077414435 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 81161 78220 1111 63 0 81098 0
vsize: 324644
[startup+310.017 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 80814 0 0 0 30846 145 0 0 25 0 1 0 803296139 342740992 80737 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 83677 80737 1111 63 0 83614 0
vsize: 334708
[startup+320.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 83421 0 0 0 31842 150 0 0 25 0 1 0 803296139 353341440 83344 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 86265 83344 1111 63 0 86202 0
vsize: 345060
[startup+330.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 86047 0 0 0 32837 154 0 0 25 0 1 0 803296139 364093440 85970 4294967295 134512640 134714508 3221221792 3221220144 134567410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 88890 85970 1111 63 0 88827 0
vsize: 355560
[startup+340.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 88575 0 0 0 33833 158 0 0 25 0 1 0 803296139 374390784 88498 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 91404 88498 1111 63 0 91341 0
vsize: 365616
[startup+350.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 91091 0 0 0 34828 163 0 0 25 0 1 0 803296139 384696320 91014 4294967295 134512640 134714508 3221221792 3221220144 134567410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 93920 91014 1111 63 0 93857 0
vsize: 375680
[startup+360.018 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 93672 0 0 0 35824 168 0 0 25 0 1 0 803296139 395296768 93595 4294967295 134512640 134714508 3221221792 3221220020 1077414420 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 96508 93595 1111 63 0 96445 0
vsize: 386032
[startup+370.019 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 96182 0 0 0 36820 172 0 0 25 0 1 0 803296139 405602304 96105 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 99024 96105 1111 63 0 98961 0
vsize: 396096
[startup+380.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 98684 0 0 0 37815 177 0 0 25 0 1 0 803296139 415969280 98607 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 101555 98607 1111 63 0 101492 0
vsize: 406220
[startup+390.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 101180 0 0 0 38811 182 0 0 25 0 1 0 803296139 426266624 101103 4294967295 134512640 134714508 3221221792 3221220448 134527930 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 104069 101103 1111 63 0 104006 0
vsize: 416276
[startup+400.02 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 103709 0 0 0 39808 185 0 0 25 0 1 0 803296139 436572160 103632 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 106585 103632 1111 63 0 106522 0
vsize: 426340
[startup+410.021 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 106170 0 0 0 40803 190 0 0 25 0 1 0 803296139 446574592 106093 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 109027 106093 1111 63 0 108964 0
vsize: 436108
[startup+420.021 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 108881 0 0 0 41798 195 0 0 25 0 1 0 803296139 457773056 108804 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 111761 108804 1111 63 0 111698 0
vsize: 447044
[startup+430.022 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 111421 0 0 0 42793 200 0 0 25 0 1 0 803296139 468074496 111344 4294967295 134512640 134714508 3221221792 3221220020 1077414426 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 114276 111344 1111 63 0 114213 0
vsize: 457104
[startup+440.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 114028 0 0 0 43790 204 0 0 25 0 1 0 803296139 478826496 113951 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 116901 113951 1111 63 0 116838 0
vsize: 467604
[startup+450.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 116617 0 0 0 44786 207 0 0 25 0 1 0 803296139 489422848 116540 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 119488 116540 1111 63 0 119425 0
vsize: 477952
[startup+460.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 119146 0 0 0 45782 212 0 0 25 0 1 0 803296139 499728384 119069 4294967295 134512640 134714508 3221221792 3221220144 134567410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 122004 119069 1111 63 0 121941 0
vsize: 488016
[startup+470.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 121667 0 0 0 46777 217 0 0 25 0 1 0 803296139 510029824 121590 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 124519 121590 1111 63 0 124456 0
vsize: 498076
[startup+480.024 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 124233 0 0 0 47773 221 0 0 25 0 1 0 803296139 520634368 124156 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 127108 124156 1111 63 0 127045 0
vsize: 508432
[startup+490.024 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 126779 0 0 0 48769 226 0 0 25 0 1 0 803296139 531079168 126702 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 129658 126702 1111 63 0 129595 0
vsize: 518632
[startup+500.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 129302 0 0 0 49765 230 0 0 25 0 1 0 803296139 541384704 129225 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 132174 129225 1111 63 0 132111 0
vsize: 528696
[startup+510.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 132180 0 0 0 50759 235 0 0 25 0 1 0 803296139 553177088 132103 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 135053 132103 1111 63 0 134990 0
vsize: 540212
[startup+520.025 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 135032 0 0 0 51755 240 0 0 25 0 1 0 803296139 564826112 134955 4294967295 134512640 134714508 3221221792 3221220020 1077414383 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 137897 134955 1111 63 0 137834 0
vsize: 551588
[startup+530.025 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 137857 0 0 0 52751 244 0 0 25 0 1 0 803296139 576323584 137780 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 140704 137780 1111 63 0 140641 0
vsize: 562816
[startup+540.025 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 140891 0 0 0 53746 249 0 0 25 0 1 0 803296139 588865536 140814 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 143766 140814 1111 63 0 143703 0
vsize: 575064
[startup+550.026 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 143587 0 0 0 54743 253 0 0 25 0 1 0 803296139 599908352 143510 4294967295 134512640 134714508 3221221792 3221220020 1077414433 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 146462 143510 1111 63 0 146399 0
vsize: 585848
[startup+560.026 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 146292 0 0 0 55739 257 0 0 25 0 1 0 803296139 610959360 146215 4294967295 134512640 134714508 3221221792 3221220020 1077414351 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 149160 146215 1111 63 0 149097 0
vsize: 596640
[startup+570.026 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 148784 0 0 0 56736 260 0 0 25 0 1 0 803296139 621109248 148707 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 151638 148707 1111 63 0 151575 0
vsize: 606552
[startup+580.027 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 151312 0 0 0 57732 264 0 0 25 0 1 0 803296139 631414784 151235 4294967295 134512640 134714508 3221221792 3221220020 1077414435 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 154154 151235 1111 63 0 154091 0
vsize: 616616
[startup+590.028 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 153962 0 0 0 58727 270 0 0 25 0 1 0 803296139 642310144 153885 4294967295 134512640 134714508 3221221792 3221220448 134527928 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 156814 153885 1111 63 0 156751 0
vsize: 627256
[startup+600.028 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 156666 0 0 0 59723 274 0 0 25 0 1 0 803296139 653361152 156589 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 159512 156589 1111 63 0 159449 0
vsize: 638048
[startup+610.028 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 159590 0 0 0 60718 279 0 0 25 0 1 0 803296139 665309184 159513 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 162429 159513 1111 63 0 162366 0
vsize: 649716
[startup+620.029 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 162372 0 0 0 61714 283 0 0 25 0 1 0 803296139 676798464 162295 4294967295 134512640 134714508 3221221792 3221218460 1077253729 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 165234 162299 1111 63 0 165171 0
vsize: 660936
[startup+630.029 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 164889 0 0 0 62710 288 0 0 25 0 1 0 803296139 687104000 164812 4294967295 134512640 134714508 3221221792 3221219912 1077378037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 167750 164818 1111 63 0 167687 0
vsize: 671000
[startup+640.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 167483 0 0 0 63705 292 0 0 25 0 1 0 803296139 697704448 167406 4294967295 134512640 134714508 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 170338 167406 1111 63 0 170275 0
vsize: 681352
[startup+650.029 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 170181 0 0 0 64701 297 0 0 25 0 1 0 803296139 708755456 170104 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 173036 170104 1111 63 0 172973 0
vsize: 692144
[startup+660.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 172716 0 0 0 65697 301 0 0 25 0 1 0 803296139 719052800 172639 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 175550 172639 1111 63 0 175487 0
vsize: 702200
[startup+670.031 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 175226 0 0 0 66693 305 0 0 25 0 1 0 803296139 729358336 175149 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 178066 175149 1111 63 0 178003 0
vsize: 712264
[startup+680.031 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 177700 0 0 0 67690 308 0 0 25 0 1 0 803296139 739508224 177623 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 180544 177623 1111 63 0 180481 0
vsize: 722176
[startup+690.032 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 180076 0 0 0 68686 312 0 0 25 0 1 0 803296139 749211648 179999 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 182913 179999 1111 63 0 182850 0
vsize: 731652
[startup+700.032 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 182415 0 0 0 69683 316 0 0 25 0 1 0 803296139 758771712 182338 4294967295 134512640 134714508 3221221792 3221220448 134527930 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 185247 182338 1111 63 0 185184 0
vsize: 740988
[startup+710.033 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 184767 0 0 0 70678 321 0 0 25 0 1 0 803296139 768475136 184690 4294967295 134512640 134714508 3221221792 3221220020 1077414395 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 187616 184690 1111 63 0 187553 0
vsize: 750464
[startup+720.033 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 187167 0 0 0 71674 325 0 0 25 0 1 0 803296139 778326016 187090 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 190021 187090 1111 63 0 189958 0
vsize: 760084
[startup+730.035 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 189495 0 0 0 72671 329 0 0 25 0 1 0 803296139 787886080 189418 4294967295 134512640 134714508 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 192355 189418 1111 63 0 192292 0
vsize: 769420
[startup+740.035 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 192143 0 0 0 73666 334 0 0 25 0 1 0 803296139 798633984 192066 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 194979 192066 1111 63 0 194916 0
vsize: 779916
[startup+750.035 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 194653 0 0 0 74662 338 0 0 25 0 1 0 803296139 808939520 194576 4294967295 134512640 134714508 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 197495 194576 1111 63 0 197432 0
vsize: 789980
[startup+760.036 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 197317 0 0 0 75658 342 0 0 25 0 1 0 803296139 820047872 197240 4294967295 134512640 134714508 3221221792 3221220144 134567410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 200207 197240 1111 63 0 200144 0
vsize: 800828
[startup+770.036 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 199759 0 0 0 76655 345 0 0 25 0 1 0 803296139 830050304 199682 4294967295 134512640 134714508 3221221792 3221220020 1077414383 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 202649 199682 1111 63 0 202586 0
vsize: 810596
[startup+780.037 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 202452 0 0 0 77651 349 0 0 25 0 1 0 803296139 841101312 202375 4294967295 134512640 134714508 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 205347 202375 1111 63 0 205284 0
vsize: 821388
[startup+790.038 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 204955 0 0 0 78647 354 0 0 25 0 1 0 803296139 851402752 204878 4294967295 134512640 134714508 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 207862 204878 1111 63 0 207799 0
vsize: 831448
[startup+800.038 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 207643 0 0 0 79643 358 0 0 25 0 1 0 803296139 862453760 207566 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 210560 207566 1111 63 0 210497 0
vsize: 842240
[startup+810.038 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 210268 0 0 0 80640 361 0 0 25 0 1 0 803296139 873205760 210191 4294967295 134512640 134714508 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 213185 210191 1111 63 0 213122 0
vsize: 852740
[startup+820.039 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 212917 0 0 0 81635 366 0 0 25 0 1 0 803296139 883953664 212840 4294967295 134512640 134714508 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 215809 212840 1111 63 0 215746 0
vsize: 863236
[startup+830.038 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 215658 0 0 0 82631 371 0 0 25 0 1 0 803296139 895152128 215581 4294967295 134512640 134714508 3221221792 3221220020 1077414408 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 218543 215581 1111 63 0 218480 0
vsize: 874172
[startup+840.038 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 218258 0 0 0 83626 376 0 0 25 0 1 0 803296139 905900032 218181 4294967295 134512640 134714508 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 221167 218181 1111 63 0 221104 0
vsize: 884668
[startup+850.039 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 221091 0 0 0 84620 381 0 0 25 0 1 0 803296139 917397504 221014 4294967295 134512640 134714508 3221221792 3221220020 1077414420 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 223974 221014 1111 63 0 223911 0
vsize: 895896
[startup+860.039 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 223636 0 0 0 85614 388 0 0 25 0 1 0 803296139 927846400 223559 4294967295 134512640 134714508 3221221792 3221220448 134527930 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 226525 223559 1111 63 0 226462 0
vsize: 906100
[startup+870.039 s]
Raw data (loadavg): 1.00 1.00 0.97 2/55 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 225911 0 0 0 86607 395 0 0 25 0 1 0 803296139 937254912 225834 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 228822 225834 1111 63 0 228759 0
vsize: 915288
[startup+877.583 s]
Raw data (loadavg): 1.00 1.00 0.97 1/54 8666
Raw data (stat): 8666 (bsolo_lpr) R 8665 7876 7672 0 -1 0 225911 0 0 0 86607 395 0 0 25 0 1 0 803296139 937254912 225834 4294967295 134512640 134714508 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 228822 225834 1111 63 0 228759 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 877.583
CPU time (s): 877.573
CPU user time (s): 873.164
CPU system time (s): 4.40833
CPU usage (%): 99.9988
Max. virtual memory (Kb): 915288
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####