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-dano3mip.opb
MD5SUM	a9d7b9b5569d1dec981f274df34ef66e
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	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	65536000
Number of bits of the biggest number in a constraint	26
Biggest sum of numbers in a constraint	555744750
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	35.1067
Number of variables	266924
Total number of constraints	3778
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	600
Number of constraints which are nor clauses,nor cardinality constraints	3178
Minimum length of a constraint	1
Maximum length of a constraint	10600

Trace number 41555

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-06-09 15:42:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=29621 boxname=wulflinc1 idbench=1405 idsolver=21 numberseed=0
MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb  /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2
MD5SUM BENCH:  a9d7b9b5569d1dec981f274df34ef66e  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-dano3mip.opb
REAL COMMAND:  bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-13-7-dano3mip.opb
IDLAUNCH: 29621
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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	: 2
cpu MHz		: 451.053
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:        871440 kB
Buffers:         14976 kB
Cached:         123756 kB
SwapCached:       1144 kB
Active:          48272 kB
Inactive:        92600 kB
HighTotal:      131008 kB
HighFree:        14588 kB
LowTotal:       903652 kB
LowFree:        856852 kB
SwapTotal:     2097136 kB
SwapFree:      2094824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5268 kB
Slab:            16448 kB
Committed_AS:    92716 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-09 15:51:38 (client local time) WITH STATUS 0 IN 521.475 SECONDS
stats: 29621 7 521.475 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.82 0.93 0.90 2/55 7729
Raw data (stat): 7729 (runsolver) R 7728 8378 8377 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 854586764 884736 94 4294967295 134512640 135332820 3221224448 3221219628 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.001 s]
Raw data (loadavg): 0.85 0.93 0.90 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 28820 0 0 0 936 62 0 0 25 0 1 0 854586764 131420160 28740 4294967295 134512640 134716908 3221224560 3221222836 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 32085 28740 1111 63 0 32022 0
vsize: 128340
[startup+20.0017 s]
Raw data (loadavg): 0.87 0.93 0.90 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 48905 0 0 0 1892 106 0 0 25 0 1 0 854586764 212631552 48605 4294967295 134512640 134716908 3221224560 3221223144 134558582 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 51912 48605 1111 63 0 51849 0
vsize: 207648
[startup+30.0014 s]
Raw data (loadavg): 0.89 0.93 0.90 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 67263 0 0 0 2854 144 0 0 25 0 1 0 854586764 287719424 66837 4294967295 134512640 134716908 3221224560 3221221036 1077196200 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 70244 66837 1111 63 0 70181 0
vsize: 280976
[startup+40.0022 s]
Raw data (loadavg): 0.90 0.93 0.90 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 82495 0 0 0 3824 174 0 0 25 0 1 0 854586764 349859840 82069 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 85415 82069 1111 63 0 85352 0
vsize: 341660
[startup+50.002 s]
Raw data (loadavg): 0.92 0.93 0.90 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 97200 0 0 0 4797 202 0 0 25 0 1 0 854586764 408051712 96334 4294967295 134512640 134716908 3221224560 3221222836 1077414376 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 99622 96334 1111 63 0 99559 0
vsize: 398488
[startup+60.0028 s]
Raw data (loadavg): 0.93 0.94 0.90 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 111817 0 0 0 5771 228 0 0 25 0 1 0 854586764 467701760 110573 4294967295 134512640 134716908 3221224560 3221222848 134566780 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 114185 110573 1111 63 0 114122 0
vsize: 456740
[startup+70.0026 s]
Raw data (loadavg): 0.94 0.94 0.90 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 124300 0 0 0 6746 253 0 0 25 0 1 0 854586764 518639616 123056 4294967295 134512640 134716908 3221224560 3221222848 134566780 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 126621 123056 1111 63 0 126558 0
vsize: 506484
[startup+80.0024 s]
Raw data (loadavg): 0.95 0.94 0.90 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 136318 0 0 0 7724 275 0 0 25 0 1 0 854586764 567619584 135074 4294967295 134512640 134716908 3221224560 3221222864 134567410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 138615 135078 1111 63 0 138552 0
vsize: 554316
[startup+90.0022 s]
Raw data (loadavg): 0.96 0.94 0.90 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 148208 0 0 0 8703 297 0 0 25 0 1 0 854586764 616189952 146964 4294967295 134512640 134716908 3221224560 3221222864 134567543 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 150437 146965 1111 63 0 150374 0
vsize: 601748
[startup+100.002 s]
Raw data (loadavg): 0.96 0.94 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 159702 0 0 0 9679 320 0 0 25 0 1 0 854586764 663085056 158458 4294967295 134512640 134716908 3221224560 3221222844 1077399570 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 161886 158458 1111 63 0 161823 0
vsize: 647544
[startup+110.003 s]
Raw data (loadavg): 0.97 0.94 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 170535 0 0 0 10658 342 0 0 25 0 1 0 854586764 707289088 169291 4294967295 134512640 134716908 3221224560 3221222848 134566780 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 172678 169291 1111 63 0 172615 0
vsize: 690712
[startup+120.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 183559 0 0 0 11633 367 0 0 25 0 1 0 854586764 756842496 181435 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 184776 181435 1111 63 0 184713 0
vsize: 739104
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 193655 0 0 0 12613 387 0 0 25 0 1 0 854586764 797982720 191531 4294967295 134512640 134716908 3221224560 3221222848 134566780 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 194820 191531 1111 63 0 194757 0
vsize: 779280
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 207842 0 0 0 13582 419 0 0 25 0 1 0 854586764 855994368 204965 4294967295 134512640 134716908 3221224560 3221223208 134558485 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 208983 204965 1111 63 0 208920 0
vsize: 835932
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 209360 0 0 0 14577 424 0 0 25 0 1 0 854586764 862212096 206483 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 210501 206483 1111 63 0 210438 0
vsize: 842004
[startup+160.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 210914 0 0 0 15573 427 0 0 25 0 1 0 854586764 868564992 208037 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 212052 208037 1111 63 0 211989 0
vsize: 848208
[startup+170.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 212565 0 0 0 16570 431 0 0 25 0 1 0 854586764 875323392 209688 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 213702 209688 1111 63 0 213639 0
vsize: 854808
[startup+180.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 214357 0 0 0 17565 437 0 0 25 0 1 0 854586764 882622464 211480 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 215484 211480 1111 63 0 215421 0
vsize: 861936
[startup+190.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 216546 0 0 0 18560 441 0 0 25 0 1 0 854586764 891678720 213669 4294967295 134512640 134716908 3221224560 3221222864 134566804 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 217695 213669 1111 63 0 217632 0
vsize: 870780
[startup+200.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 218001 0 0 0 19557 445 0 0 25 0 1 0 854586764 897490944 215124 4294967295 134512640 134716908 3221224560 3221222836 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 219114 215124 1111 63 0 219051 0
vsize: 876456
[startup+210.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 218478 0 0 0 20555 447 0 0 25 0 1 0 854586764 899567616 215588 4294967295 134512640 134716908 3221224560 3221222836 1077414351 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 219621 215588 1111 63 0 219558 0
vsize: 878484
[startup+220.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 218809 0 0 0 21554 448 0 0 25 0 1 0 854586764 901038080 215905 4294967295 134512640 134716908 3221224560 3221222836 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 219980 215905 1111 63 0 219917 0
vsize: 879920
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 219135 0 0 0 22554 448 0 0 25 0 1 0 854586764 902512640 216216 4294967295 134512640 134716908 3221224560 3221222836 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 220340 216216 1111 63 0 220277 0
vsize: 881360
[startup+240.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 219464 0 0 0 23553 449 0 0 25 0 1 0 854586764 903983104 216531 4294967295 134512640 134716908 3221224560 3221222836 1077414336 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 220699 216531 1111 63 0 220636 0
vsize: 882796
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 219731 0 0 0 24552 450 0 0 25 0 1 0 854586764 905150464 216788 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 220984 216788 1111 63 0 220921 0
vsize: 883936
[startup+260.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 219950 0 0 0 25552 450 0 0 25 0 1 0 854586764 906207232 216994 4294967295 134512640 134716908 3221224560 3221223056 134539126 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 221242 216994 1111 63 0 221179 0
vsize: 884968
[startup+270.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 220118 0 0 0 26551 451 0 0 25 0 1 0 854586764 906928128 217154 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 221418 217154 1111 63 0 221355 0
vsize: 885672
[startup+280.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 220446 0 0 0 27551 452 0 0 25 0 1 0 854586764 908398592 217467 4294967295 134512640 134716908 3221224560 3221222836 1077414372 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 221777 217467 1111 63 0 221714 0
vsize: 887108
[startup+290.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 220771 0 0 0 28549 454 0 0 25 0 1 0 854586764 909873152 217778 4294967295 134512640 134716908 3221224560 3221222836 1077414360 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 222137 217778 1111 63 0 222074 0
vsize: 888548
[startup+300.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 221096 0 0 0 29548 455 0 0 25 0 1 0 854586764 911343616 217961 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 222496 217961 1111 63 0 222433 0
vsize: 889984
[startup+310.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 221272 0 0 0 30548 456 0 0 25 0 1 0 854586764 912097280 218130 4294967295 134512640 134716908 3221224560 3221222864 134566796 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 222680 218130 1111 63 0 222617 0
vsize: 890720
[startup+320.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 221428 0 0 0 31547 457 0 0 25 0 1 0 854586764 912818176 218279 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 222856 218279 1111 63 0 222793 0
vsize: 891424
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 221759 0 0 0 32546 458 0 0 25 0 1 0 854586764 914288640 218596 4294967295 134512640 134716908 3221224560 3221222836 1077414336 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 223215 218596 1111 63 0 223152 0
vsize: 892860
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 222084 0 0 0 33546 458 0 0 25 0 1 0 854586764 915763200 218681 4294967295 134512640 134716908 3221224560 3221222836 1077414385 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 223575 218681 1111 63 0 223512 0
vsize: 894300
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 222335 0 0 0 34545 459 0 0 25 0 1 0 854586764 916791296 218923 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 223826 218923 1111 63 0 223763 0
vsize: 895304
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 222509 0 0 0 35544 460 0 0 25 0 1 0 854586764 917647360 219089 4294967295 134512640 134716908 3221224560 3221221180 1077255876 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 224035 219089 1111 63 0 223972 0
vsize: 896140
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 222743 0 0 0 36544 461 0 0 25 0 1 0 854586764 918704128 219310 4294967295 134512640 134716908 3221224560 3221222836 1077414336 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 224293 219310 1111 63 0 224230 0
vsize: 897172
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 223071 0 1 0 37541 462 0 0 25 0 1 0 854586764 920178688 219368 4294967295 134512640 134716908 3221224560 3221221324 1077195936 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 224653 219368 1111 63 0 224590 0
vsize: 898612
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 223387 0 1 0 38540 463 0 0 25 0 1 0 854586764 921513984 219670 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 224979 219670 1111 63 0 224916 0
vsize: 899916
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 223515 0 1 0 39539 464 0 0 25 0 1 0 854586764 922062848 219797 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 225113 219797 1111 63 0 225050 0
vsize: 900452
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 223727 0 1 0 40538 465 0 0 25 0 1 0 854586764 923123712 219997 4294967295 134512640 134716908 3221224560 3221222836 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 225372 219997 1111 63 0 225309 0
vsize: 901488
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 224058 0 1 0 41537 467 0 0 25 0 1 0 854586764 924594176 219962 4294967295 134512640 134716908 3221224560 3221222836 1077414385 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 225731 219962 1111 63 0 225668 0
vsize: 902924
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 224320 0 1 0 42535 468 0 0 25 0 1 0 854586764 925761536 220215 4294967295 134512640 134716908 3221224560 3221222848 134566780 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 226016 220215 1111 63 0 225953 0
vsize: 904064
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 224483 0 1 0 43535 469 0 0 25 0 1 0 854586764 926482432 220371 4294967295 134512640 134716908 3221224560 3221223056 134539126 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 226192 220371 1111 63 0 226129 0
vsize: 904768
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 224714 0 1 0 44534 470 0 0 25 0 1 0 854586764 927539200 220588 4294967295 134512640 134716908 3221224560 3221222836 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 226450 220588 1111 63 0 226387 0
vsize: 905800
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 225044 0 1 0 45532 472 0 0 25 0 1 0 854586764 929017856 220519 4294967295 134512640 134716908 3221224560 3221222836 1077414360 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 226811 220519 1111 63 0 226748 0
vsize: 907244
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 225255 0 1 0 46532 473 0 0 25 0 1 0 854586764 929906688 220722 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 227028 220722 1111 63 0 226965 0
vsize: 908112
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 225399 0 1 0 47531 474 0 0 25 0 1 0 854586764 930488320 220859 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 227170 220859 1111 63 0 227107 0
vsize: 908680
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 225699 0 1 0 48530 475 0 0 25 0 1 0 854586764 931962880 221145 4294967295 134512640 134716908 3221224560 3221222836 1077414407 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 227530 221145 1111 63 0 227467 0
vsize: 910120
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 226030 0 1 0 49529 475 0 0 25 0 1 0 854586764 933433344 221462 4294967295 134512640 134716908 3221224560 3221222604 1076999584 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 227889 221462 1111 63 0 227826 0
vsize: 911556
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 227102 0 1 0 50525 479 0 0 25 0 1 0 854586764 937758720 221990 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 228945 221990 1111 63 0 228882 0
vsize: 915780
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 227994 0 1 0 51522 481 0 0 25 0 1 0 854586764 941408256 222470 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 229836 222470 1111 63 0 229773 0
vsize: 919344
[startup+521.449 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 7729
Raw data (stat): 7729 (bsolo_lpr_cuts-) R 7728 8378 8377 0 -1 0 227994 0 1 0 51522 481 0 0 25 0 1 0 854586764 941408256 222470 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 229836 222470 1111 63 0 229773 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 521.449
CPU time (s): 521.475
CPU user time (s): 516.234
CPU system time (s): 5.2412
CPU usage (%): 100.005
Max. virtual memory (Kb): 919344
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####