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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-dano3_4.opb
MD5SUM53ae35dd3424f79abe62dc18aab624bf
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableNO
(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 131072000
Number of bits of the biggest number in a constraint 27
Biggest sum of numbers in a constraint 576307709
Number of bits of the biggest sum of numbers30
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark35.0387
Number of variables270144
Total number of constraints3778
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)96
Number of constraints which are nor clauses,nor cardinality constraints3682
Minimum length of a constraint1
Maximum length of a constraint10600

Trace number 41646

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-06-09 18:57:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=29713 boxname=wulflinc4 idbench=1497 idsolver=21 numberseed=0
MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb  /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2
MD5SUM BENCH:  53ae35dd3424f79abe62dc18aab624bf  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-dano3_4.opb
REAL COMMAND:  bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-dano3_4.opb
IDLAUNCH: 29713
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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.169
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:        821328 kB
Buffers:         14848 kB
Cached:         177696 kB
SwapCached:        916 kB
Active:          49196 kB
Inactive:       145396 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        821076 kB
SwapTotal:     2097136 kB
SwapFree:      2095168 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4908 kB
Slab:            13124 kB
Committed_AS:    71796 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-09 19:06:09 (client local time) WITH STATUS 0 IN 505.02 SECONDS
stats: 29713 7 505.02 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.98 0.91 2/54 19373
Raw data (stat): 19373 (runsolver) R 19372 21152 21151 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 912602940 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.0004 s]
Raw data (loadavg): 0.94 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 33062 0 0 0 924 73 0 0 25 0 1 0 912602940 148836352 32982 4294967295 134512640 134716908 3221224560 3221222864 134567410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 36337 32986 1111 63 0 36274 0
vsize: 145348
[startup+20.0008 s]
Raw data (loadavg): 0.95 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 54139 0 0 0 1880 116 0 0 25 0 1 0 912602940 234393600 53769 4294967295 134512640 134716908 3221224560 3221221180 1077253700 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 57225 53769 1111 63 0 57162 0
vsize: 228900
[startup+30.0011 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 71187 0 0 0 2848 148 0 0 25 0 1 0 912602940 302608384 70485 4294967295 134512640 134716908 3221224560 3221223048 1077378037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 73879 70485 1111 63 0 73816 0
vsize: 295516
[startup+40.0017 s]
Raw data (loadavg): 0.96 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 86910 0 0 0 3819 176 0 0 25 0 1 0 912602940 366854144 86208 4294967295 134512640 134716908 3221224560 3221222848 134566780 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 89564 86208 1111 63 0 89501 0
vsize: 358256
[startup+50.0023 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 102088 0 0 0 4789 206 0 0 25 0 1 0 912602940 428744704 101008 4294967295 134512640 134716908 3221224560 3221223220 134568431 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 104674 101008 1111 63 0 104611 0
vsize: 418696
[startup+60.0024 s]
Raw data (loadavg): 0.97 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 115475 0 0 0 5765 230 0 0 25 0 1 0 912602940 483328000 114395 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 118000 114395 1111 63 0 117937 0
vsize: 472000
[startup+70.0033 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 126861 0 0 0 6746 250 0 0 25 0 1 0 912602940 529760256 125781 4294967295 134512640 134716908 3221224560 3221222836 1077414370 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 129336 125781 1111 63 0 129273 0
vsize: 517344
[startup+80.0042 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 141646 0 0 0 7717 278 0 0 25 0 1 0 912602940 587382784 139906 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 143404 139907 1111 63 0 143341 0
vsize: 573616
[startup+90.0051 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 152310 0 0 0 8698 298 0 0 25 0 1 0 912602940 631013376 150570 4294967295 134512640 134716908 3221224560 3221222864 134567410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 154056 150570 1111 63 0 153993 0
vsize: 616224
[startup+100.006 s]
Raw data (loadavg): 0.98 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 164557 0 0 0 9676 320 0 0 25 0 1 0 912602940 680878080 162817 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 166230 162817 1111 63 0 166167 0
vsize: 664920
[startup+110.005 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 175051 0 0 0 10656 339 0 0 25 0 1 0 912602940 723693568 173311 4294967295 134512640 134716908 3221224560 3221222220 1077244344 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 176683 173311 1111 63 0 176620 0
vsize: 706732
[startup+120.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 185892 0 0 0 11636 360 0 0 25 0 1 0 912602940 767909888 184152 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 187478 184152 1111 63 0 187415 0
vsize: 749912
[startup+130.007 s]
Raw data (loadavg): 0.99 0.98 0.91 2/54 19373
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 196903 0 0 0 12615 381 0 0 25 0 1 0 912602940 812855296 195163 4294967295 134512640 134716908 3221224560 3221222836 1077414383 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 198451 195163 1111 63 0 198388 0
vsize: 793804
[startup+140.008 s]
Raw data (loadavg): 0.99 0.98 0.91 2/57 19376
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 209891 0 0 0 13585 411 0 0 25 0 1 0 912602940 865927168 207302 4294967295 134512640 134716908 3221224560 3221222844 1077399567 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 211408 207302 1111 63 0 211345 0
vsize: 845632
[startup+150.008 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 19426
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 211431 0 0 0 14580 416 0 0 25 0 1 0 912602940 872144896 208618 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 212926 208618 1111 63 0 212863 0
vsize: 851704
[startup+160.008 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 19426
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 212949 0 0 0 15576 421 0 0 25 0 1 0 912602940 878362624 209816 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 214444 209816 1111 63 0 214381 0
vsize: 857776
[startup+170.009 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 19426
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 214553 0 0 0 16571 426 0 0 25 0 1 0 912602940 884985856 211038 4294967295 134512640 134716908 3221224560 3221222844 1077399556 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 216061 211038 1111 63 0 215998 0
vsize: 864244
[startup+180.009 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 19426
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 216278 0 0 0 17566 431 0 0 25 0 1 0 912602940 892014592 212378 4294967295 134512640 134716908 3221224560 3221222848 134566780 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 217777 212378 1111 63 0 217714 0
vsize: 871108
[startup+190.01 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 19426
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 218268 0 0 0 18559 438 0 0 25 0 1 0 912602940 900259840 214283 4294967295 134512640 134716908 3221224560 3221222476 1077246007 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 219790 214283 1111 63 0 219727 0
vsize: 879160
[startup+200.011 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 19426
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 220222 0 0 0 19553 444 0 0 25 0 1 0 912602940 908099584 215940 4294967295 134512640 134716908 3221224560 3221222836 1077414360 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 221704 215940 1111 63 0 221641 0
vsize: 886816
[startup+210.01 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 19426
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 220883 0 0 0 20551 446 0 0 25 0 1 0 912602940 910925824 216285 4294967295 134512640 134716908 3221224560 3221222836 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 222394 216285 1111 63 0 222331 0
vsize: 889576
[startup+220.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 221199 0 0 0 21550 448 0 0 25 0 1 0 912602940 912265216 216585 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 222721 216585 1111 63 0 222658 0
vsize: 890884
[startup+230.011 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 221402 0 0 0 22549 449 0 0 25 0 1 0 912602940 913149952 216643 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 222937 216643 1111 63 0 222874 0
vsize: 891748
[startup+240.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 221636 0 0 0 23549 450 0 0 25 0 1 0 912602940 914284544 216867 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 223214 216867 1111 63 0 223151 0
vsize: 892856
[startup+250.013 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 221865 0 0 0 24548 451 0 0 25 0 1 0 912602940 915341312 217083 4294967295 134512640 134716908 3221224560 3221222836 1077414345 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 223472 217083 1111 63 0 223409 0
vsize: 893888
[startup+260.014 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 222192 0 0 0 25547 451 0 0 25 0 1 0 912602940 916815872 217086 4294967295 134512640 134716908 3221224560 3221222836 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 223832 217086 1111 63 0 223769 0
vsize: 895328
[startup+270.015 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 222523 0 0 0 26546 453 0 0 25 0 1 0 912602940 918286336 217403 4294967295 134512640 134716908 3221224560 3221222836 1077414336 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 224191 217403 1111 63 0 224128 0
vsize: 896764
[startup+280.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 222835 0 0 0 27545 454 0 0 25 0 1 0 912602940 919625728 217702 4294967295 134512640 134716908 3221224560 3221223056 134539144 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 224518 217702 1111 63 0 224455 0
vsize: 898072
[startup+290.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 223007 0 0 0 28544 455 0 0 25 0 1 0 912602940 920510464 217867 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 224734 217867 1111 63 0 224671 0
vsize: 898936
[startup+300.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 223179 0 0 0 29543 456 0 0 25 0 1 0 912602940 921231360 217931 4294967295 134512640 134716908 3221224560 3221222836 1077414395 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 224910 217931 1111 63 0 224847 0
vsize: 899640
[startup+310.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 223504 0 0 0 30541 457 0 0 25 0 1 0 912602940 922705920 218241 4294967295 134512640 134716908 3221224560 3221222836 1077414424 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 225270 218241 1111 63 0 225207 0
vsize: 901080
[startup+320.016 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 223835 0 0 0 31540 459 0 0 25 0 1 0 912602940 924176384 218274 4294967295 134512640 134716908 3221224560 3221222836 1077414360 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 225629 218274 1111 63 0 225566 0
vsize: 902516
[startup+330.017 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 224051 0 0 0 32540 459 0 0 25 0 1 0 912602940 925065216 218482 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 225846 218482 1111 63 0 225783 0
vsize: 903384
[startup+340.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 224220 0 0 0 33539 460 0 0 25 0 1 0 912602940 925921280 218643 4294967295 134512640 134716908 3221224560 3221222844 1077399562 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 226055 218643 1111 63 0 225992 0
vsize: 904220
[startup+350.018 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 224487 0 0 0 34538 461 0 0 25 0 1 0 912602940 927121408 218896 4294967295 134512640 134716908 3221224560 3221222836 1077414407 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 226348 218896 1111 63 0 226285 0
vsize: 905392
[startup+360.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 224818 0 0 0 35537 462 0 0 25 0 1 0 912602940 928591872 219112 4294967295 134512640 134716908 3221224560 3221222836 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 226707 219112 1111 63 0 226644 0
vsize: 906828
[startup+370.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 225075 0 0 0 36537 463 0 0 25 0 1 0 912602940 929759232 219361 4294967295 134512640 134716908 3221224560 3221222220 1077271527 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 226992 219361 1111 63 0 226929 0
vsize: 907968
[startup+380.019 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 225234 0 0 0 37536 464 0 0 25 0 1 0 912602940 930480128 219513 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 227168 219513 1111 63 0 227105 0
vsize: 908672
[startup+390.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 225474 0 0 0 38536 464 0 0 25 0 1 0 912602940 931536896 219741 4294967295 134512640 134716908 3221224560 3221222836 1077414397 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 227426 219741 1111 63 0 227363 0
vsize: 909704
[startup+400.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 225800 0 0 0 39534 466 0 0 25 0 1 0 912602940 933011456 219777 4294967295 134512640 134716908 3221224560 3221222836 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 227786 219777 1111 63 0 227723 0
vsize: 911144
[startup+410.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 226020 0 0 0 40534 466 0 0 25 0 1 0 912602940 933896192 219990 4294967295 134512640 134716908 3221224560 3221223120 134535026 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 228002 219990 1111 63 0 227939 0
vsize: 912008
[startup+420.023 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 226151 0 0 0 41534 467 0 0 25 0 1 0 912602940 934481920 220113 4294967295 134512640 134716908 3221224560 3221223160 134543609 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 228145 220113 1111 63 0 228082 0
vsize: 912580
[startup+430.022 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 226457 0 0 0 42533 467 0 0 25 0 1 0 912602940 935956480 220403 4294967295 134512640 134716908 3221224560 3221222836 1077414410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 228505 220403 1111 63 0 228442 0
vsize: 914020
[startup+440.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 226784 0 0 0 43532 469 0 0 25 0 1 0 912602940 937426944 220374 4294967295 134512640 134716908 3221224560 3221222836 1077414410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 228864 220374 1111 63 0 228801 0
vsize: 915456
[startup+450.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 226945 0 0 0 44531 469 0 0 25 0 1 0 912602940 938180608 220527 4294967295 134512640 134716908 3221224560 3221222588 1077364379 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 229048 220527 1111 63 0 228985 0
vsize: 916192
[startup+460.024 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19428
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 227112 0 0 0 45531 470 0 0 25 0 1 0 912602940 938897408 220687 4294967295 134512640 134716908 3221224560 3221222836 1077414433 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 229223 220687 1111 63 0 229160 0
vsize: 916892
[startup+470.025 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19430
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 227445 0 0 0 46529 472 0 0 25 0 1 0 912602940 940376064 221006 4294967295 134512640 134716908 3221224560 3221222836 1077414410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 229584 221006 1111 63 0 229521 0
vsize: 918336
[startup+480.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19430
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 227693 0 0 0 47528 473 0 0 25 0 1 0 912602940 941408256 220884 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 229836 220884 1111 63 0 229773 0
vsize: 919344
[startup+490.027 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19430
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 227822 0 0 0 48528 473 0 0 25 0 1 0 912602940 941985792 221008 4294967295 134512640 134716908 3221224560 3221223056 134539146 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 229977 221008 1111 63 0 229914 0
vsize: 919908
[startup+500.028 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 19430
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 228101 0 0 0 49526 475 0 0 25 0 1 0 912602940 943321088 221273 4294967295 134512640 134716908 3221224560 3221222836 1077414418 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 230303 221273 1111 63 0 230240 0
vsize: 921212
[startup+505.103 s]
Raw data (loadavg): 1.00 1.00 0.92 1/53 19430
Raw data (stat): 19373 (bsolo_lpr_cuts-) R 19372 21152 21151 0 -1 0 228101 0 0 0 49526 475 0 0 25 0 1 0 912602940 943321088 221273 4294967295 134512640 134716908 3221224560 3221222836 1077414418 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 230303 221273 1111 63 0 230240 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 505.103
CPU time (s): 505.02
CPU user time (s): 499.845
CPU system time (s): 5.17521
CPU usage (%): 99.9836
Max. virtual memory (Kb): 921212
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####