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-stp3d.opb
MD5SUM	bd41ba4f2ddbc80664ba643e2dc93b96
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	75648
Biggest coefficient in the objective function	100303
Number of bits for the biggest coefficient in the objective function	17
Sum of the numbers in the objective function	7576279200
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	100303
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	7576279200
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	2.75158
Number of variables	204880
Total number of constraints	364368
Number of constraints which are clauses	129232
Number of constraints which are cardinality constraints (but not clauses)	210685
Number of constraints which are nor clauses,nor cardinality constraints	24451
Minimum length of a constraint	1
Maximum length of a constraint	120

Trace number 25725

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-22 00:39:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18033 boxname=wulflinc31 idbench=1388 idsolver=2 numberseed=0
MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7  /oldhome/oroussel/solvers/bsolo_lpr_cuts
MD5SUM BENCH:  bd41ba4f2ddbc80664ba643e2dc93b96  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-stp3d.opb
REAL COMMAND:  bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-stp3d.opb
IDLAUNCH: 18033
/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:        837176 kB
Buffers:          6124 kB
Cached:         169508 kB
SwapCached:        896 kB
Active:         128668 kB
Inactive:        49056 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        836924 kB
SwapTotal:     2097892 kB
SwapFree:      2095964 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5096 kB
Slab:            14172 kB
Committed_AS:    63860 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-22 00:51:17 (client local time) WITH STATUS 0 IN 682.342 SECONDS
stats: 18033 7 682.342 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.96 2/55 18093
Raw data (stat): 18093 (runsolver) R 18092 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 808686177 1056768 100 4294967295 134512640 135381576 3221221680 3221216896 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.0004 s]
Raw data (loadavg): 0.94 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 3328 0 0 0 983 12 0 0 25 0 1 0 808686177 25387008 3251 4294967295 134512640 134714508 3221221776 3221220004 1077414357 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 6198 3251 1111 63 0 6135 0
vsize: 24792
[startup+20.0018 s]
Raw data (loadavg): 0.95 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 5942 0 0 0 1978 17 0 0 25 0 1 0 808686177 35991552 5865 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 8787 5865 1111 63 0 8724 0
vsize: 35148
[startup+30.0017 s]
Raw data (loadavg): 0.96 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 8568 0 0 0 2974 21 0 0 25 0 1 0 808686177 46727168 8491 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 11408 8491 1111 63 0 11345 0
vsize: 45632
[startup+40.0022 s]
Raw data (loadavg): 0.96 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 11205 0 0 0 3969 26 0 0 25 0 1 0 808686177 57626624 11128 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 14069 11128 1111 63 0 14006 0
vsize: 56276
[startup+50.0038 s]
Raw data (loadavg): 0.97 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 13859 0 0 0 4964 31 0 0 25 0 1 0 808686177 68497408 13782 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 16723 13782 1111 63 0 16660 0
vsize: 66892
[startup+60.0046 s]
Raw data (loadavg): 0.97 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 16521 0 0 0 5959 36 0 0 25 0 1 0 808686177 79400960 16444 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 19385 16444 1111 63 0 19322 0
vsize: 77540
[startup+70.005 s]
Raw data (loadavg): 0.98 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 19193 0 0 0 6954 41 0 0 25 0 1 0 808686177 90296320 19116 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 22045 19116 1111 63 0 21982 0
vsize: 88180
[startup+80.0053 s]
Raw data (loadavg): 0.98 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 21885 0 0 0 7950 46 0 0 25 0 1 0 808686177 101347328 21808 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 24743 21808 1111 63 0 24680 0
vsize: 98972
[startup+90.0063 s]
Raw data (loadavg): 0.98 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 24589 0 0 0 8944 52 0 0 25 0 1 0 808686177 112398336 24512 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 27441 24512 1111 63 0 27378 0
vsize: 109764
[startup+100.006 s]
Raw data (loadavg): 0.98 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 27317 0 0 0 9940 56 0 0 25 0 1 0 808686177 123564032 27240 4294967295 134512640 134714508 3221221776 3221220004 1077414351 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 30167 27240 1111 63 0 30104 0
vsize: 120668
[startup+110.007 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 30046 0 0 0 10935 61 0 0 25 0 1 0 808686177 134766592 29969 4294967295 134512640 134714508 3221221776 3221220004 1077414432 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 32902 29969 1111 63 0 32839 0
vsize: 131608
[startup+120.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 32793 0 0 0 11930 66 0 0 25 0 1 0 808686177 145960960 32716 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 35635 32716 1111 63 0 35572 0
vsize: 142540
[startup+130.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 35558 0 0 0 12924 72 0 0 25 0 1 0 808686177 157306880 35481 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 38405 35481 1111 63 0 38342 0
vsize: 153620
[startup+140.008 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 38342 0 0 0 13919 77 0 0 25 0 1 0 808686177 168804352 38265 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 41212 38265 1111 63 0 41149 0
vsize: 164848
[startup+150.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 41138 0 0 0 14914 83 0 0 25 0 1 0 808686177 180154368 41061 4294967295 134512640 134714508 3221221776 3221220004 1077414376 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 43983 41061 1111 63 0 43920 0
vsize: 175932
[startup+160.009 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 43949 0 0 0 15908 89 0 0 25 0 1 0 808686177 191647744 43872 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 46789 43872 1111 63 0 46726 0
vsize: 187156
[startup+170.01 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 46775 0 0 0 16903 94 0 0 25 0 1 0 808686177 203296768 46698 4294967295 134512640 134714508 3221221776 3221220004 1077414370 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 49633 46698 1111 63 0 49570 0
vsize: 198532
[startup+180.01 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 49629 0 0 0 17899 98 0 0 25 0 1 0 808686177 215089152 49552 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 52512 49552 1111 63 0 52449 0
vsize: 210048
[startup+190.01 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 52492 0 0 0 18893 104 0 0 25 0 1 0 808686177 226729984 52415 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 55354 52415 1111 63 0 55291 0
vsize: 221416
[startup+200.011 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 55370 0 0 0 19887 110 0 0 25 0 1 0 808686177 238526464 55293 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 58234 55293 1111 63 0 58171 0
vsize: 232936
[startup+210.011 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 58264 0 0 0 20880 117 0 0 25 0 1 0 808686177 250322944 58187 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 61114 58187 1111 63 0 61051 0
vsize: 244456
[startup+220.012 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 61180 0 0 0 21873 124 0 0 25 0 1 0 808686177 262266880 61103 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 64030 61103 1111 63 0 63967 0
vsize: 256120
[startup+230.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 64147 0 0 0 22868 129 0 0 25 0 1 0 808686177 274509824 64070 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 67019 64070 1111 63 0 66956 0
vsize: 268076
[startup+240.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 67124 0 0 0 23863 135 0 0 25 0 1 0 808686177 286605312 67047 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 69972 67047 1111 63 0 69909 0
vsize: 279888
[startup+250.013 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 70128 0 0 0 24856 142 0 0 25 0 1 0 808686177 298999808 70051 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 72998 70051 1111 63 0 72935 0
vsize: 291992
[startup+260.014 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 73146 0 0 0 25850 148 0 0 25 0 1 0 808686177 311386112 73069 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 76022 73069 1111 63 0 75959 0
vsize: 304088
[startup+270.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 76192 0 0 0 26845 153 0 0 25 0 1 0 808686177 323776512 76115 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 79047 76115 1111 63 0 78984 0
vsize: 316188
[startup+280.015 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 79254 0 0 0 27839 159 0 0 25 0 1 0 808686177 336318464 79177 4294967295 134512640 134714508 3221221776 3221220004 1077414435 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 82109 79177 1111 63 0 82046 0
vsize: 328436
[startup+290.016 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 82354 0 0 0 28834 165 0 0 25 0 1 0 808686177 349011968 82277 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 85208 82277 1111 63 0 85145 0
vsize: 340832
[startup+300.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 85495 0 0 0 29828 171 0 0 25 0 1 0 808686177 361848832 85418 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 88342 85418 1111 63 0 88279 0
vsize: 353368
[startup+310.017 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 88662 0 0 0 30823 176 0 0 25 0 1 0 808686177 374841344 88585 4294967295 134512640 134714508 3221221776 3221220004 1077414376 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 91514 88585 1111 63 0 91451 0
vsize: 366056
[startup+320.019 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 91851 0 0 0 31817 182 0 0 25 0 1 0 808686177 387977216 91774 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 94721 91774 1111 63 0 94658 0
vsize: 378884
[startup+330.019 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 95054 0 0 0 32811 188 0 0 25 0 1 0 808686177 400973824 94977 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 97894 94977 1111 63 0 97831 0
vsize: 391576
[startup+340.019 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 98316 0 0 0 33806 193 0 0 25 0 1 0 808686177 414478336 98239 4294967295 134512640 134714508 3221221776 3221220004 1077414435 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 101191 98239 1111 63 0 101128 0
vsize: 404764
[startup+350.02 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 101572 0 0 0 34800 199 0 0 25 0 1 0 808686177 427913216 101495 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 104471 101495 1111 63 0 104408 0
vsize: 417884
[startup+360.022 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 104873 0 0 0 35793 206 0 0 25 0 1 0 808686177 441348096 104796 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 107751 104796 1111 63 0 107688 0
vsize: 431004
[startup+370.022 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 108184 0 0 0 36787 212 0 0 25 0 1 0 808686177 454934528 108107 4294967295 134512640 134714508 3221221776 3221220004 1077414407 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 111068 108107 1111 63 0 111005 0
vsize: 444272
[startup+380.022 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 111533 0 0 0 37783 217 0 0 25 0 1 0 808686177 468668416 111456 4294967295 134512640 134714508 3221221776 3221220004 1077414376 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 114421 111456 1111 63 0 114358 0
vsize: 457684
[startup+390.023 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 114912 0 0 0 38776 223 0 0 25 0 1 0 808686177 482410496 114835 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 117776 114835 1111 63 0 117713 0
vsize: 471104
[startup+400.023 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 118315 0 0 0 39770 230 0 0 25 0 1 0 808686177 496443392 118238 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 121202 118238 1111 63 0 121139 0
vsize: 484808
[startup+410.024 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 121760 0 0 0 40763 237 0 0 25 0 1 0 808686177 510476288 121683 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 124628 121683 1111 63 0 124565 0
vsize: 498512
[startup+420.025 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 125249 0 0 0 41756 244 0 0 25 0 1 0 808686177 524812288 125172 4294967295 134512640 134714508 3221221776 3221220004 1077414408 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 128128 125172 1111 63 0 128065 0
vsize: 512512
[startup+430.026 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 128756 0 0 0 42750 251 0 0 25 0 1 0 808686177 539144192 128679 4294967295 134512640 134714508 3221221776 3221220004 1077414358 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 131627 128679 1111 63 0 131564 0
vsize: 526508
[startup+440.026 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 132297 0 0 0 43743 258 0 0 25 0 1 0 808686177 553623552 132220 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 135162 132220 1111 63 0 135099 0
vsize: 540648
[startup+450.025 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 135873 0 0 0 44736 265 0 0 25 0 1 0 808686177 568258560 135796 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 138735 135796 1111 63 0 138672 0
vsize: 554940
[startup+460.026 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 139469 0 0 0 45728 272 0 0 25 0 1 0 808686177 583036928 139392 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 142343 139392 1111 63 0 142280 0
vsize: 569372
[startup+470.027 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 143110 0 0 0 46723 278 0 0 25 0 1 0 808686177 597970944 143033 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 145989 143033 1111 63 0 145926 0
vsize: 583956
[startup+480.027 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 146787 0 0 0 47716 285 0 0 25 0 1 0 808686177 613048320 146710 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 149670 146710 1111 63 0 149607 0
vsize: 598680
[startup+490.027 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 150493 0 0 0 48708 293 0 0 25 0 1 0 808686177 628129792 150416 4294967295 134512640 134714508 3221221776 3221220004 1077414408 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 153352 150416 1111 63 0 153289 0
vsize: 613408
[startup+500.028 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 154250 0 0 0 49702 300 0 0 25 0 1 0 808686177 643510272 154173 4294967295 134512640 134714508 3221221776 3221220004 1077414349 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 157107 154173 1111 63 0 157044 0
vsize: 628428
[startup+510.028 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 158035 0 0 0 50694 308 0 0 25 0 1 0 808686177 659034112 157958 4294967295 134512640 134714508 3221221776 3221220004 1077414435 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 160897 157958 1111 63 0 160834 0
vsize: 643588
[startup+520.028 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 161870 0 0 0 51686 316 0 0 25 0 1 0 808686177 674713600 161793 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 164725 161793 1111 63 0 164662 0
vsize: 658900
[startup+530.029 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 165755 0 0 0 52679 322 0 0 25 0 1 0 808686177 690688000 165678 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 168625 165678 1111 63 0 168562 0
vsize: 674500
[startup+540.029 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 169672 0 0 0 53672 330 0 0 25 0 1 0 808686177 706662400 169595 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 172525 169595 1111 63 0 172462 0
vsize: 690100
[startup+550.029 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 173647 0 0 0 54665 337 0 0 25 0 1 0 808686177 722935808 173570 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 176498 173570 1111 63 0 176435 0
vsize: 705992
[startup+560.03 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 177696 0 0 0 55657 346 0 0 25 0 1 0 808686177 739508224 177619 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 180544 177619 1111 63 0 180481 0
vsize: 722176
[startup+570.031 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 181772 0 0 0 56651 352 0 0 25 0 1 0 808686177 756232192 181695 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 184627 181695 1111 63 0 184564 0
vsize: 738508
[startup+580.031 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 185505 0 0 0 57644 359 0 0 25 0 1 0 808686177 771465216 185428 4294967295 134512640 134714508 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 188346 185428 1111 63 0 188283 0
vsize: 753384
[startup+590.031 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 189247 0 0 0 58638 365 0 0 25 0 1 0 808686177 786837504 189170 4294967295 134512640 134714508 3221221776 3221220004 1077414408 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 192099 189170 1111 63 0 192036 0
vsize: 768396
[startup+600.031 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 193027 0 0 0 59630 373 0 0 25 0 1 0 808686177 802369536 192950 4294967295 134512640 134714508 3221221776 3221220432 134527928 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 195891 192950 1111 63 0 195828 0
vsize: 783564
[startup+610.032 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 196937 0 0 0 60622 381 0 0 25 0 1 0 808686177 818556928 196860 4294967295 134512640 134714508 3221221776 3221220004 1077414408 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 199843 196860 1111 63 0 199780 0
vsize: 799372
[startup+620.033 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 201081 0 0 0 61615 388 0 0 25 0 1 0 808686177 835579904 201004 4294967295 134512640 134714508 3221221776 3221220004 1077414433 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 203999 201004 1111 63 0 203936 0
vsize: 815996
[startup+630.032 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 205268 0 0 0 62608 396 0 0 25 0 1 0 808686177 852750336 205191 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 208191 205191 1111 63 0 208128 0
vsize: 832764
[startup+640.033 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 209492 0 0 0 63600 402 0 0 25 0 1 0 808686177 870068224 209415 4294967295 134512640 134714508 3221221776 3221220004 1077414336 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 212419 209415 1111 63 0 212356 0
vsize: 849676
[startup+650.034 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 213734 0 1 0 64589 411 0 0 25 0 1 0 808686177 887386112 212861 4294967295 134512640 134714508 3221221776 3221220004 1077414399 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 216647 212861 1111 63 0 216584 0
vsize: 866588
[startup+660.034 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 217981 0 1 0 65577 421 0 0 25 0 1 0 808686177 904704000 216339 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 220875 216339 1111 63 0 220812 0
vsize: 883500
[startup+670.035 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 222296 0 1 0 66562 435 0 0 25 0 1 0 808686177 922472448 219580 4294967295 134512640 134714508 3221221776 3221220004 1077414370 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 225213 219580 1111 63 0 225150 0
vsize: 900852
[startup+680.04 s]
Raw data (loadavg): 0.99 0.98 0.96 2/55 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 226676 0 6 0 67545 449 0 0 25 0 1 0 808686177 940236800 222278 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 229550 222278 1111 63 0 229487 0
vsize: 918200
[startup+682.446 s]
Raw data (loadavg): 0.99 0.98 0.96 1/54 18093
Raw data (stat): 18093 (bsolo_lpr_cuts) R 18092 7876 7672 0 -1 0 226676 0 6 0 67545 449 0 0 25 0 1 0 808686177 940236800 222278 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 229550 222278 1111 63 0 229487 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 682.445
CPU time (s): 682.342
CPU user time (s): 677.401
CPU system time (s): 4.94125
CPU usage (%): 99.9849
Max. virtual memory (Kb): 918200
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####