PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:

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

General information on the benchmark

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-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.74658
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 28363

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc10 THE 2005-05-25 02:04:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13041 boxname=wulflinc10 idbench=1004 idsolver=2 numberseed=0
MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7  /oldhome/oroussel/solvers/bsolo_lpr_cuts
MD5SUM BENCH:  bd41ba4f2ddbc80664ba643e2dc93b96  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-stp3d.opb
REAL COMMAND:  bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-stp3d.opb
IDLAUNCH: 13041
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        850828 kB
Buffers:          4988 kB
Cached:         157104 kB
SwapCached:        224 kB
Active:          50628 kB
Inactive:       114220 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        850576 kB
SwapTotal:     2097136 kB
SwapFree:      2096792 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6572 kB
Slab:            13228 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 02:15:49 (client local time) WITH STATUS 0 IN 677.857 SECONDS
stats: 13041 7 677.857 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.03 1.02 0.94 2/54 24688
Raw data (stat): 24688 (runsolver) R 24687 15547 15546 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 776928381 1052672 99 4294967295 134512640 135381576 3221224480 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 24688
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 3345 0 0 0 986 11 0 0 25 0 1 0 776928381 25382912 3269 4294967295 134512640 134714508 3221224576 3221222804 1077414401 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 6197 3269 1111 63 0 6134 0
vsize: 24788
[startup+20.0179 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 24688
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 5976 0 0 0 1984 16 0 0 25 0 1 0 776928381 36139008 5900 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 8823 5900 1111 63 0 8760 0
vsize: 35292
[startup+30.0179 s]
Raw data (loadavg): 1.02 1.02 0.94 2/54 24688
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 8615 0 0 0 2979 20 0 0 25 0 1 0 776928381 47022080 8539 4294967295 134512640 134714508 3221224576 3221222804 1077414357 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11480 8539 1111 63 0 11417 0
vsize: 45920
[startup+40.0183 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 24688
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 11258 0 0 0 3975 24 0 0 25 0 1 0 776928381 57774080 11182 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 14105 11182 1111 63 0 14042 0
vsize: 56420
[startup+50.0191 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 24688
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 13924 0 0 0 4971 29 0 0 25 0 1 0 776928381 68792320 13848 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16795 13848 1111 63 0 16732 0
vsize: 67180
[startup+60.0186 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 24688
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 16604 0 0 0 5966 34 0 0 25 0 1 0 776928381 79695872 16528 4294967295 134512640 134714508 3221224576 3221222804 1077414424 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 19457 16528 1111 63 0 19394 0
vsize: 77828
[startup+70.0179 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 24688
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 19290 0 0 0 6963 37 0 0 25 0 1 0 776928381 90746880 19214 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 22155 19214 1111 63 0 22092 0
vsize: 88620
[startup+80.0219 s]
Raw data (loadavg): 1.01 1.02 0.94 2/54 24688
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 21992 0 0 0 7959 42 0 0 25 0 1 0 776928381 101789696 21916 4294967295 134512640 134714508 3221224576 3221222804 1077414383 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 24851 21916 1111 63 0 24788 0
vsize: 99404
[startup+90.0213 s]
Raw data (loadavg): 1.00 1.02 0.94 2/54 24688
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 24708 0 0 0 8954 47 0 0 25 0 1 0 776928381 112840704 24632 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 27549 24632 1111 63 0 27486 0
vsize: 110196
[startup+100.029 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 27448 0 0 0 9951 51 0 0 25 0 1 0 776928381 124157952 27372 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30312 27372 1111 63 0 30249 0
vsize: 121248
[startup+110.038 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 30202 0 0 0 10949 54 0 0 25 0 1 0 776928381 135356416 30126 4294967295 134512640 134714508 3221224576 3221222804 1077414408 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 33046 30126 1111 63 0 32983 0
vsize: 132184
[startup+120.044 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 32961 0 0 0 11945 58 0 0 25 0 1 0 776928381 146706432 32885 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 35817 32885 1111 63 0 35754 0
vsize: 143268
[startup+130.044 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 35744 0 0 0 12942 62 0 0 25 0 1 0 776928381 158048256 35668 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 38586 35668 1111 63 0 38523 0
vsize: 154344
[startup+140.043 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 38534 0 0 0 13937 67 0 0 25 0 1 0 776928381 169545728 38458 4294967295 134512640 134714508 3221224576 3221222804 1077414383 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 41393 38458 1111 63 0 41330 0
vsize: 165572
[startup+150.044 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 41348 0 0 0 14933 71 0 0 25 0 1 0 776928381 181047296 41272 4294967295 134512640 134714508 3221224576 3221222804 1077414424 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 44201 41272 1111 63 0 44138 0
vsize: 176804
[startup+160.044 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 44173 0 0 0 15929 76 0 0 25 0 1 0 776928381 192692224 44097 4294967295 134512640 134714508 3221224576 3221222804 1077414383 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 47044 44097 1111 63 0 46981 0
vsize: 188176
[startup+170.044 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 47009 0 0 0 16925 80 0 0 25 0 1 0 776928381 204185600 46933 4294967295 134512640 134714508 3221224576 3221222804 1077414370 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 49850 46933 1111 63 0 49787 0
vsize: 199400
[startup+180.044 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 49888 0 0 0 17921 84 0 0 25 0 1 0 776928381 216125440 49812 4294967295 134512640 134714508 3221224576 3221222804 1077414410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 52765 49812 1111 63 0 52702 0
vsize: 211060
[startup+190.045 s]
Raw data (loadavg): 1.00 1.01 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 52763 0 0 0 18916 89 0 0 25 0 1 0 776928381 227921920 52687 4294967295 134512640 134714508 3221224576 3221222804 1077414357 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 55645 52687 1111 63 0 55582 0
vsize: 222580
[startup+200.045 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 55662 0 0 0 19910 95 0 0 25 0 1 0 776928381 239718400 55586 4294967295 134512640 134714508 3221224576 3221222804 1077414336 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 58525 55586 1111 63 0 58462 0
vsize: 234100
[startup+210.045 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 58572 0 0 0 20906 100 0 0 25 0 1 0 776928381 251658240 58496 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 61440 58496 1111 63 0 61377 0
vsize: 245760
[startup+220.046 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 61512 0 0 0 21901 105 0 0 25 0 1 0 776928381 263753728 61436 4294967295 134512640 134714508 3221224576 3221222928 134567410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 64393 61436 1111 63 0 64330 0
vsize: 257572
[startup+230.046 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 64491 0 0 0 22896 110 0 0 25 0 1 0 776928381 275849216 64415 4294967295 134512640 134714508 3221224576 3221222804 1077414376 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 67346 64415 1111 63 0 67283 0
vsize: 269384
[startup+240.046 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 67486 0 0 0 23891 115 0 0 25 0 1 0 776928381 288092160 67410 4294967295 134512640 134714508 3221224576 3221222804 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 70335 67410 1111 63 0 70272 0
vsize: 281340
[startup+250.046 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 70508 0 0 0 24886 120 0 0 25 0 1 0 776928381 300486656 70432 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 73361 70432 1111 63 0 73298 0
vsize: 293444
[startup+260.051 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 73546 0 0 0 25882 125 0 0 25 0 1 0 776928381 313028608 73470 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 76423 73470 1111 63 0 76360 0
vsize: 305692
[startup+270.05 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 76604 0 0 0 26877 130 0 0 25 0 1 0 776928381 325419008 76528 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 79448 76528 1111 63 0 79385 0
vsize: 317792
[startup+280.051 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 79684 0 0 0 27872 135 0 0 25 0 1 0 776928381 338112512 79608 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 82547 79608 1111 63 0 82484 0
vsize: 330188
[startup+290.051 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 82790 0 0 0 28867 141 0 0 25 0 1 0 776928381 350801920 82714 4294967295 134512640 134714508 3221224576 3221222804 1077414336 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 85645 82714 1111 63 0 85582 0
vsize: 342580
[startup+300.052 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 85919 0 0 0 29861 147 0 0 25 0 1 0 776928381 363642880 85843 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 88780 85843 1111 63 0 88717 0
vsize: 355120
[startup+310.052 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 89068 0 0 0 30855 153 0 0 25 0 1 0 776928381 376479744 88992 4294967295 134512640 134714508 3221224576 3221222804 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 91914 88992 1111 63 0 91851 0
vsize: 367656
[startup+320.051 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 92239 0 0 0 31849 159 0 0 25 0 1 0 776928381 389472256 92163 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 95086 92163 1111 63 0 95023 0
vsize: 380344
[startup+330.052 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 95447 0 0 0 32843 166 0 0 25 0 1 0 776928381 402608128 95371 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 98293 95371 1111 63 0 98230 0
vsize: 393172
[startup+340.052 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 98739 0 0 0 33837 171 0 0 25 0 1 0 776928381 416264192 98663 4294967295 134512640 134714508 3221224576 3221222804 1077414370 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 101627 98663 1111 63 0 101564 0
vsize: 406508
[startup+350.053 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 102044 0 0 0 34832 177 0 0 25 0 1 0 776928381 429846528 101968 4294967295 134512640 134714508 3221224576 3221222804 1077414401 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 104943 101968 1111 63 0 104880 0
vsize: 419772
[startup+360.053 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 105388 0 0 0 35827 182 0 0 25 0 1 0 776928381 443432960 105312 4294967295 134512640 134714508 3221224576 3221222804 1077414349 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 108260 105312 1111 63 0 108197 0
vsize: 433040
[startup+370.053 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 108748 0 0 0 36821 189 0 0 25 0 1 0 776928381 457175040 108672 4294967295 134512640 134714508 3221224576 3221222804 1077414345 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 111615 108672 1111 63 0 111552 0
vsize: 446460
[startup+380.054 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 112145 0 0 0 37815 194 0 0 25 0 1 0 776928381 471207936 112069 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 115041 112069 1111 63 0 114978 0
vsize: 460164
[startup+390.053 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 115578 0 0 0 38809 201 0 0 25 0 1 0 776928381 485240832 115502 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 118467 115502 1111 63 0 118404 0
vsize: 473868
[startup+400.054 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 119030 0 0 0 39802 208 0 0 25 0 1 0 776928381 499277824 118954 4294967295 134512640 134714508 3221224576 3221222804 1077414401 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 121894 118954 1111 63 0 121831 0
vsize: 487576
[startup+410.054 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 122531 0 0 0 40797 214 0 0 25 0 1 0 776928381 513609728 122455 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 125393 122455 1111 63 0 125330 0
vsize: 501572
[startup+420.054 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 126066 0 0 0 41790 220 0 0 25 0 1 0 776928381 528089088 125990 4294967295 134512640 134714508 3221224576 3221222804 1077414426 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 128928 125990 1111 63 0 128865 0
vsize: 515712
[startup+430.054 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 129635 0 0 0 42784 227 0 0 25 0 1 0 776928381 542724096 129559 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 132501 129559 1111 63 0 132438 0
vsize: 530004
[startup+440.054 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 133221 0 0 0 43777 234 0 0 25 0 1 0 776928381 557502464 133145 4294967295 134512640 134714508 3221224576 3221222696 1077378037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 136109 133150 1111 63 0 136046 0
vsize: 544436
[startup+450.059 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 136861 0 0 0 44771 241 0 0 25 0 1 0 776928381 572284928 136785 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 139718 136785 1111 63 0 139655 0
vsize: 558872
[startup+460.059 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 140518 0 0 0 45766 246 0 0 25 0 1 0 776928381 587362304 140442 4294967295 134512640 134714508 3221224576 3221222804 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 143399 140442 1111 63 0 143336 0
vsize: 573596
[startup+470.059 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 144214 0 0 0 46759 253 0 0 25 0 1 0 776928381 602443776 144138 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 147081 144142 1111 63 0 147018 0
vsize: 588324
[startup+480.067 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 147965 0 0 0 47754 259 0 0 25 0 1 0 776928381 617828352 147889 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 150837 147889 1111 63 0 150774 0
vsize: 603348
[startup+490.07 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 151737 0 0 0 48747 266 0 0 25 0 1 0 776928381 633200640 151661 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 154590 151661 1111 63 0 154527 0
vsize: 618360
[startup+500.072 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 155548 0 0 0 49742 272 0 0 25 0 1 0 776928381 648880128 155472 4294967295 134512640 134714508 3221224576 3221222804 1077414345 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 158418 155472 1111 63 0 158355 0
vsize: 633672
[startup+510.073 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 159426 0 0 0 50735 279 0 0 25 0 1 0 776928381 664707072 159350 4294967295 134512640 134714508 3221224576 3221222928 134567410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 162282 159350 1111 63 0 162219 0
vsize: 649128
[startup+520.077 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 163326 0 0 0 51729 286 0 0 25 0 1 0 776928381 680677376 163250 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 166181 163250 1111 63 0 166118 0
vsize: 664724
[startup+530.078 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 167283 0 0 0 52724 291 0 0 25 0 1 0 776928381 696954880 167207 4294967295 134512640 134714508 3221224576 3221222804 1077414351 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 170155 167207 1111 63 0 170092 0
vsize: 680620
[startup+540.078 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 171301 0 0 0 53717 299 0 0 25 0 1 0 776928381 713379840 171225 4294967295 134512640 134714508 3221224576 3221222804 1077414385 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 174165 171225 1111 63 0 174102 0
vsize: 696660
[startup+550.079 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 175347 0 0 0 54710 305 0 0 25 0 1 0 776928381 729952256 175271 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 178211 175271 1111 63 0 178148 0
vsize: 712844
[startup+560.087 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 179468 0 0 0 55703 314 0 0 25 0 1 0 776928381 746823680 179392 4294967295 134512640 134714508 3221224576 3221222804 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 182330 179392 1111 63 0 182267 0
vsize: 729320
[startup+570.097 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 183516 0 0 0 56697 320 0 0 25 0 1 0 776928381 763396096 183440 4294967295 134512640 134714508 3221224576 3221222804 1077414395 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 186376 183440 1111 63 0 186313 0
vsize: 745504
[startup+580.101 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 187252 0 0 0 57692 326 0 0 25 0 1 0 776928381 778620928 187176 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 190093 187176 1111 63 0 190030 0
vsize: 760372
[startup+590.105 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 191080 0 0 0 58687 331 0 0 25 0 1 0 776928381 794300416 191004 4294967295 134512640 134714508 3221224576 3221222804 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 193921 191004 1111 63 0 193858 0
vsize: 775684
[startup+600.105 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 194896 0 0 0 59681 338 0 0 25 0 1 0 776928381 809979904 194820 4294967295 134512640 134714508 3221224576 3221222804 1077414358 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 197749 194820 1111 63 0 197686 0
vsize: 790996
[startup+610.108 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 198946 0 0 0 60673 346 0 0 25 0 1 0 776928381 826765312 198870 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 201847 198870 1111 63 0 201784 0
vsize: 807388
[startup+620.107 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 203018 0 0 0 61666 354 0 0 25 0 1 0 776928381 843489280 202942 4294967295 134512640 134714508 3221224576 3221222804 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 205930 202942 1111 63 0 205867 0
vsize: 823720
[startup+630.107 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 207187 0 0 0 62656 364 0 0 25 0 1 0 776928381 860508160 207111 4294967295 134512640 134714508 3221224576 3221223232 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 210085 207111 1111 63 0 210022 0
vsize: 840340
[startup+640.128 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 211374 0 0 0 63650 372 0 0 25 0 1 0 776928381 877678592 211298 4294967295 134512640 134714508 3221224576 3221222908 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 214277 211298 1111 63 0 214214 0
vsize: 857108
[startup+650.138 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 215610 0 0 0 64641 382 0 0 25 0 1 0 776928381 895000576 215085 4294967295 134512640 134714508 3221224576 3221222804 1077414410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 218506 215085 1111 63 0 218443 0
vsize: 874024
[startup+660.175 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 219986 0 0 0 65633 395 0 0 25 0 1 0 776928381 912912384 218279 4294967295 134512640 134714508 3221224576 3221222928 134567410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 222879 218279 1111 63 0 222816 0
vsize: 891516
[startup+670.177 s]
Raw data (loadavg): 1.00 1.00 0.94 2/54 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 224366 0 0 0 66622 406 0 0 25 0 1 0 776928381 930979840 221417 4294967295 134512640 134714508 3221224576 3221222804 1077414435 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 227290 221417 1111 63 0 227227 0
vsize: 909160
[startup+677.827 s]
Raw data (loadavg): 1.00 1.00 0.94 1/53 24690
Raw data (stat): 24688 (bsolo_lpr_cuts) R 24687 15547 15546 0 -1 0 224366 0 0 0 66622 406 0 0 25 0 1 0 776928381 930979840 221417 4294967295 134512640 134714508 3221224576 3221222804 1077414435 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 227290 221417 1111 63 0 227227 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 677.827
CPU time (s): 677.857
CPU user time (s): 673.302
CPU system time (s): 4.55531
CPU usage (%): 100.004
Max. virtual memory (Kb): 909160
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####