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 41538

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-06-09 15:17:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=29604 boxname=wulflinc3 idbench=1388 idsolver=21 numberseed=0
MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb  /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2
MD5SUM BENCH:  bd41ba4f2ddbc80664ba643e2dc93b96  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-stp3d.opb
REAL COMMAND:  bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-stp3d.opb
IDLAUNCH: 29604
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        851888 kB
Buffers:         11960 kB
Cached:         150228 kB
SwapCached:        672 kB
Active:          58244 kB
Inactive:       105952 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        851636 kB
SwapTotal:     2097136 kB
SwapFree:      2095392 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5012 kB
Slab:            12872 kB
Committed_AS:    71796 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-09 15:29:03 (client local time) WITH STATUS 0 IN 679.651 SECONDS
stats: 29604 7 679.651 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
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.93 0.97 0.91 2/54 11877
Raw data (stat): 11877 (runsolver) R 11876 20224 20223 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 911283756 884736 94 4294967295 134512640 135332820 3221224448 3221219628 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0012 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 3347 0 0 0 987 10 0 0 25 0 1 0 911283756 25382912 3267 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6197 3267 1111 63 0 6134 0
vsize: 24788
[startup+20.0015 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 5972 0 0 0 1981 16 0 0 25 0 1 0 911283756 36139008 5892 4294967295 134512640 134716908 3221224560 3221222788 1077414395 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 8823 5892 1111 63 0 8760 0
vsize: 35292
[startup+30.003 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 8611 0 0 0 2976 22 0 0 25 0 1 0 911283756 47022080 8531 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11480 8531 1111 63 0 11417 0
vsize: 45920
[startup+40.0035 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 11260 0 0 0 3971 26 0 0 25 0 1 0 911283756 57774080 11180 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 14105 11180 1111 63 0 14042 0
vsize: 56420
[startup+50.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 13926 0 0 0 4967 31 0 0 25 0 1 0 911283756 68792320 13846 4294967295 134512640 134716908 3221224560 3221223260 1076648036 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16795 13846 1111 63 0 16732 0
vsize: 67180
[startup+60.0042 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 16600 0 0 0 5962 36 0 0 25 0 1 0 911283756 79695872 16520 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 19457 16520 1111 63 0 19394 0
vsize: 77828
[startup+70.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 19286 0 0 0 6958 40 0 0 25 0 1 0 911283756 90746880 19206 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 22155 19206 1111 63 0 22092 0
vsize: 88620
[startup+80.0045 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 21988 0 0 0 7953 45 0 0 25 0 1 0 911283756 101789696 21908 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 24851 21908 1111 63 0 24788 0
vsize: 99404
[startup+90.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 24704 0 0 0 8949 50 0 0 25 0 1 0 911283756 112840704 24624 4294967295 134512640 134716908 3221224560 3221222788 1077414383 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 27549 24624 1111 63 0 27486 0
vsize: 110196
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 27438 0 0 0 9944 55 0 0 25 0 1 0 911283756 124157952 27358 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30312 27358 1111 63 0 30249 0
vsize: 121248
[startup+110.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 30185 0 0 0 10939 60 0 0 25 0 1 0 911283756 135356416 30105 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 33046 30105 1111 63 0 32983 0
vsize: 132184
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 32951 0 0 0 11934 65 0 0 25 0 1 0 911283756 146706432 32871 4294967295 134512640 134716908 3221224560 3221222788 1077414401 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 35817 32871 1111 63 0 35754 0
vsize: 143268
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 35727 0 0 0 12929 70 0 0 25 0 1 0 911283756 158048256 35647 4294967295 134512640 134716908 3221224560 3221222788 1077414385 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 38586 35647 1111 63 0 38523 0
vsize: 154344
[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 38517 0 0 0 13925 75 0 0 25 0 1 0 911283756 169398272 38437 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 41393 38439 1111 63 0 41330 0
vsize: 165428
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 41332 0 0 0 14920 80 0 0 25 0 1 0 911283756 181047296 41252 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 44201 41252 1111 63 0 44138 0
vsize: 176804
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 44156 0 0 0 15915 85 0 0 25 0 1 0 911283756 192536576 44076 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 47006 44076 1111 63 0 46943 0
vsize: 188024
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 46993 0 0 0 16910 90 0 0 25 0 1 0 911283756 204185600 46913 4294967295 134512640 134716908 3221224560 3221222788 1077414357 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 49850 46913 1111 63 0 49787 0
vsize: 199400
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 49871 0 0 0 17905 95 0 0 25 0 1 0 911283756 215977984 49791 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 52729 49791 1111 63 0 52666 0
vsize: 210916
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 52746 0 0 0 18901 100 0 0 25 0 1 0 911283756 227774464 52666 4294967295 134512640 134716908 3221224560 3221222788 1077414345 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 55609 52666 1111 63 0 55546 0
vsize: 222436
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 55645 0 0 0 19895 105 0 0 25 0 1 0 911283756 239718400 55565 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 58525 55565 1111 63 0 58462 0
vsize: 234100
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 58555 0 0 0 20890 111 0 0 25 0 1 0 911283756 251510784 58475 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 61404 58475 1111 63 0 61341 0
vsize: 245616
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 61490 0 0 0 21885 116 0 0 25 0 1 0 911283756 263606272 61410 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 64357 61410 1111 63 0 64294 0
vsize: 257428
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 64469 0 0 0 22881 120 0 0 25 0 1 0 911283756 275849216 64389 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 67346 64389 1111 63 0 67283 0
vsize: 269384
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 67470 0 0 0 23876 125 0 0 25 0 1 0 911283756 288092160 67390 4294967295 134512640 134716908 3221224560 3221222912 134567410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 70335 67390 1111 63 0 70272 0
vsize: 281340
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 70486 0 0 0 24871 131 0 0 25 0 1 0 911283756 300486656 70406 4294967295 134512640 134716908 3221224560 3221222788 1077414410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 73361 70406 1111 63 0 73298 0
vsize: 293444
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 73523 0 0 0 25867 135 0 0 25 0 1 0 911283756 312877056 73443 4294967295 134512640 134716908 3221224560 3221222788 1077414383 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 76386 73443 1111 63 0 76323 0
vsize: 305544
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 76587 0 0 0 26862 140 0 0 25 0 1 0 911283756 325419008 76507 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 79448 76507 1111 63 0 79385 0
vsize: 317792
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 79668 0 0 0 27857 145 0 0 25 0 1 0 911283756 337960960 79588 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 82510 79588 1111 63 0 82447 0
vsize: 330040
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 82768 0 0 0 28851 151 0 0 25 0 1 0 911283756 350654464 82688 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 85609 82688 1111 63 0 85546 0
vsize: 342436
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 85897 0 0 0 29846 157 0 0 25 0 1 0 911283756 363491328 85817 4294967295 134512640 134716908 3221224560 3221222788 1077414407 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 88743 85817 1111 63 0 88680 0
vsize: 354972
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 89046 0 0 0 30842 161 0 0 25 0 1 0 911283756 376479744 88966 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 91914 88966 1111 63 0 91851 0
vsize: 367656
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 92217 0 0 0 31837 166 0 0 25 0 1 0 911283756 389472256 92137 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 95086 92137 1111 63 0 95023 0
vsize: 380344
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 95412 0 0 0 32832 171 0 0 25 0 1 0 911283756 402460672 95332 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 98257 95332 1111 63 0 98194 0
vsize: 393028
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 98656 0 0 0 33827 177 0 0 25 0 1 0 911283756 415965184 98576 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 101554 98576 1111 63 0 101491 0
vsize: 406216
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 101895 0 0 0 34821 183 0 0 25 0 1 0 911283756 429101056 101815 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 104761 101815 1111 63 0 104698 0
vsize: 419044
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 105176 0 0 0 35816 188 0 0 25 0 1 0 911283756 442540032 105096 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 108042 105096 1111 63 0 107979 0
vsize: 432168
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 108476 0 0 0 36810 194 0 0 25 0 1 0 911283756 456122368 108396 4294967295 134512640 134716908 3221224560 3221222788 1077414407 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 111358 108396 1111 63 0 111295 0
vsize: 445432
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 111813 0 0 0 37805 199 0 0 25 0 1 0 911283756 469716992 111733 4294967295 134512640 134716908 3221224560 3221222788 1077414408 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 114677 111733 1111 63 0 114614 0
vsize: 458708
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 115210 0 0 0 38798 206 0 0 25 0 1 0 911283756 483749888 115130 4294967295 134512640 134716908 3221224560 3221222788 1077414336 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 118103 115130 1111 63 0 118040 0
vsize: 472412
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 118637 0 0 0 39793 212 0 0 25 0 1 0 911283756 497782784 118557 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 121529 118557 1111 63 0 121466 0
vsize: 486116
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 122102 0 0 0 40788 217 0 0 25 0 1 0 911283756 511967232 122022 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 124992 122022 1111 63 0 124929 0
vsize: 499968
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 125607 0 0 0 41782 223 0 0 25 0 1 0 911283756 526299136 125527 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 128491 125527 1111 63 0 128428 0
vsize: 513964
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 129138 0 0 0 42776 229 0 0 25 0 1 0 911283756 540778496 129058 4294967295 134512640 134716908 3221224560 3221222788 1077414370 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 132026 129058 1111 63 0 131963 0
vsize: 528104
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 132693 0 0 0 43769 236 0 0 25 0 1 0 911283756 555266048 132613 4294967295 134512640 134716908 3221224560 3221223260 134565097 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 135563 132616 1111 63 0 135500 0
vsize: 542252
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 136291 0 0 0 44763 242 0 0 25 0 1 0 911283756 570044416 136211 4294967295 134512640 134716908 3221224560 3221222788 1077414432 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 139171 136211 1111 63 0 139108 0
vsize: 556684
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 139914 0 0 0 45758 248 0 0 25 0 1 0 911283756 584826880 139834 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 142780 139834 1111 63 0 142717 0
vsize: 571120
[startup+470.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 143577 0 0 0 46752 254 0 0 25 0 1 0 911283756 599904256 143497 4294967295 134512640 134716908 3221224560 3221222788 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 146461 143497 1111 63 0 146398 0
vsize: 585844
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 147280 0 0 0 47746 261 0 0 25 0 1 0 911283756 614985728 147200 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 150143 147200 1111 63 0 150080 0
vsize: 600572
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 151009 0 0 0 48739 267 0 0 25 0 1 0 911283756 630214656 150929 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 153861 150929 1111 63 0 153798 0
vsize: 615444
[startup+500.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 154790 0 0 0 49732 275 0 0 25 0 1 0 911283756 645742592 154710 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 157652 154710 1111 63 0 157589 0
vsize: 630608
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 158607 0 0 0 50725 281 0 0 25 0 1 0 911283756 661422080 158527 4294967295 134512640 134716908 3221224560 3221222788 1077414435 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 161480 158527 1111 63 0 161417 0
vsize: 645920
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 162466 0 0 0 51718 289 0 0 25 0 1 0 911283756 677249024 162386 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 165344 162386 1111 63 0 165281 0
vsize: 661376
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 166373 0 0 0 52711 296 0 0 25 0 1 0 911283756 693219328 166293 4294967295 134512640 134716908 3221224560 3221222788 1077414410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 169243 166293 1111 63 0 169180 0
vsize: 676972
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 170336 0 0 0 53706 302 0 0 25 0 1 0 911283756 709345280 170256 4294967295 134512640 134716908 3221224560 3221223280 134564419 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 173180 170256 1111 63 0 173117 0
vsize: 692720
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 174334 0 0 0 54697 310 0 0 25 0 1 0 911283756 725770240 174254 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 177190 174254 1111 63 0 177127 0
vsize: 708760
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 178407 0 0 0 55691 317 0 0 25 0 1 0 911283756 742494208 178327 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 181273 178327 1111 63 0 181210 0
vsize: 725092
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 182550 0 0 0 56683 325 0 0 25 0 1 0 911283756 759365632 182470 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 185392 182470 1111 63 0 185329 0
vsize: 741568
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 186281 0 0 0 57676 332 0 0 25 0 1 0 911283756 774737920 186201 4294967295 134512640 134716908 3221224560 3221222788 1077414401 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 189145 186201 1111 63 0 189082 0
vsize: 756580
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 190074 0 0 0 58670 339 0 0 25 0 1 0 911283756 790269952 189994 4294967295 134512640 134716908 3221224560 3221222788 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 192937 189994 1111 63 0 192874 0
vsize: 771748
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 193956 0 0 0 59662 346 0 0 25 0 1 0 911283756 806096896 193876 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 196801 193876 1111 63 0 196738 0
vsize: 787204
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 197957 0 0 0 60656 353 0 0 25 0 1 0 911283756 822734848 197877 4294967295 134512640 134716908 3221224560 3221222788 1077414410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 200863 197877 1111 63 0 200800 0
vsize: 803452
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 202072 0 0 0 61649 360 0 0 25 0 1 0 911283756 839606272 201992 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 204982 201992 1111 63 0 204919 0
vsize: 819928
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 206259 0 0 0 62642 367 0 0 25 0 1 0 911283756 856776704 206179 4294967295 134512640 134716908 3221224560 3221222788 1077414358 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 209174 206179 1111 63 0 209111 0
vsize: 836696
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 210458 0 0 0 63635 374 0 0 25 0 1 0 911283756 873947136 210378 4294967295 134512640 134716908 3221224560 3221222788 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 213366 210378 1111 63 0 213303 0
vsize: 853464
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 214725 0 0 0 64624 384 0 0 25 0 1 0 911283756 891412480 214332 4294967295 134512640 134716908 3221224560 3221223216 134527932 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 217630 214332 1111 63 0 217567 0
vsize: 870520
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 219057 0 0 0 65612 395 0 0 25 0 1 0 911283756 909180928 217537 4294967295 134512640 134716908 3221224560 3221222788 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 221968 217537 1111 63 0 221905 0
vsize: 887872
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 223462 0 0 0 66599 407 0 0 25 0 1 0 911283756 927244288 220766 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 226378 220766 1111 63 0 226315 0
vsize: 905512
[startup+679.643 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 11877
Raw data (stat): 11877 (bsolo_lpr_cuts-) R 11876 20224 20223 0 -1 0 223462 0 0 0 66599 407 0 0 25 0 1 0 911283756 927244288 220766 4294967295 134512640 134716908 3221224560 3221222788 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 226378 220766 1111 63 0 226315 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 679.642
CPU time (s): 679.651
CPU user time (s): 675.035
CPU system time (s): 4.6153
CPU usage (%): 100.001
Max. virtual memory (Kb): 905512
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####