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/web/uclid_pb_benchmarks/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb
MD5SUMdcb6d1c3f66e900ae345e6fa455bef2a
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 130
Number of bits of the biggest number in a constraint 8
Biggest sum of numbers in a constraint 512
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables168111
Total number of constraints487525
Number of constraints which are clauses468727
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints18798
Minimum length of a constraint1
Maximum length of a constraint15

Trace number 40858

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-06-08 23:08:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=28916 boxname=wulflinc6 idbench=302 idsolver=21 numberseed=0
MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb  /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2
MD5SUM BENCH:  dcb6d1c3f66e900ae345e6fa455bef2a  /oldhome/oroussel/tmp/wulflinc6/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb
REAL COMMAND:  bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc6/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb
IDLAUNCH: 28916
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        893924 kB
Buffers:         24280 kB
Cached:          93172 kB
SwapCached:       2432 kB
Active:          41216 kB
Inactive:        79796 kB
HighTotal:      131008 kB
HighFree:        39116 kB
LowTotal:       903652 kB
LowFree:        854808 kB
SwapTotal:     2097136 kB
SwapFree:      2093696 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            13912 kB
Committed_AS:    63736 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-08 23:20:50 (client local time) WITH STATUS 0 IN 717.097 SECONDS
stats: 28916 7 717.097 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c INFO: No cost function. Find solution and finish.
c Initial problem consists of 168111 variables and 487525 constraints.
#### 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.88 0.95 0.91 2/54 3817
Raw data (stat): 3817 (runsolver) R 3816 25568 25567 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 905477648 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.0001 s]
Raw data (loadavg): 0.90 0.96 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 34024 0 0 0 928 70 0 0 25 0 1 0 905477648 41046016 6697 4294967295 134512640 134716908 3221224560 3221221324 1077191044 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 9971 6679 1111 63 0 9908 0
vsize: 40084
[startup+20.0002 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 161416 0 0 0 1707 291 0 0 25 0 1 0 905477648 57155584 10637 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 13919 10607 1111 63 0 13856 0
vsize: 55816
[startup+30.0004 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 386785 0 0 0 2309 689 0 0 25 0 1 0 905477648 67690496 13171 4294967295 134512640 134716908 3221224560 3221222900 1077374114 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16526 13171 1111 63 0 16463 0
vsize: 66104
[startup+40.0005 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 611721 0 0 0 2910 1088 0 0 25 0 1 0 905477648 76689408 15355 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 18723 15362 1111 63 0 18660 0
vsize: 74892
[startup+50.0006 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 833415 0 0 0 3504 1494 0 0 25 0 1 0 905477648 84570112 17305 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 20647 17311 1111 63 0 20584 0
vsize: 82588
[startup+59.9997 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 1052140 0 0 0 4106 1893 0 0 25 0 1 0 905477648 91639808 19030 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 22373 19037 1111 63 0 22310 0
vsize: 89492
[startup+69.9989 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 1267530 0 0 0 4709 2289 0 0 25 0 1 0 905477648 98160640 20586 4294967295 134512640 134716908 3221224560 3221222604 1077387418 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 23965 20593 1111 63 0 23902 0
vsize: 95860
[startup+79.999 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 1482868 0 0 0 5317 2682 0 0 25 0 1 0 905477648 104873984 22280 4294967295 134512640 134716908 3221224560 3221223368 134674635 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 25665 22283 1111 63 0 25602 0
vsize: 102416
[startup+89.9982 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 1698253 0 0 0 5915 3084 0 0 25 0 1 0 905477648 110833664 23755 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 27059 23762 1111 63 0 26996 0
vsize: 108236
[startup+99.9974 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 1908754 0 0 0 6520 3479 0 0 25 0 1 0 905477648 116269056 25061 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 28386 25067 1111 63 0 28323 0
vsize: 113544
[startup+109.998 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 2118176 0 0 0 7119 3880 0 0 25 0 1 0 905477648 122195968 26348 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29833 26354 1111 63 0 29770 0
vsize: 119332
[startup+119.998 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 2324418 0 0 0 7733 4267 0 0 25 0 1 0 905477648 127078400 27477 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 31025 27483 1111 63 0 30962 0
vsize: 124100
[startup+129.997 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 2532175 0 0 0 8349 4651 0 0 25 0 1 0 905477648 131702784 28677 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 32154 28682 1111 63 0 32091 0
vsize: 128616
[startup+139.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 2736740 0 0 0 8960 5040 0 0 25 0 1 0 905477648 136323072 29739 4294967295 134512640 134716908 3221224560 3221222604 1077387418 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 33282 29745 1111 63 0 33219 0
vsize: 133128
[startup+149.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 2939958 0 0 0 9573 5428 0 0 25 0 1 0 905477648 140201984 30793 4294967295 134512640 134716908 3221224560 3221222968 1077378037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 34310 30798 1111 63 0 34247 0
vsize: 136916
[startup+159.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 3140328 0 0 0 10185 5815 0 0 25 0 1 0 905477648 144613376 31801 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 35306 31807 1111 63 0 35243 0
vsize: 141224
[startup+169.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 3341105 0 0 0 10800 6200 0 0 25 0 1 0 905477648 148684800 32822 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 36300 32826 1111 63 0 36237 0
vsize: 145200
[startup+179.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 3540938 0 0 0 11413 6587 0 0 25 0 1 0 905477648 152485888 33813 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 37140 33728 1111 63 0 37077 0
vsize: 148912
[startup+189.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 3739475 0 0 0 12026 6976 0 0 25 0 1 0 905477648 155918336 34666 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 38066 34666 1111 63 0 38003 0
vsize: 152264
[startup+199.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 3937881 0 0 0 12640 7361 0 0 25 0 1 0 905477648 160088064 35576 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 39084 35581 1111 63 0 39021 0
vsize: 156336
[startup+209.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 4136520 0 0 0 13256 7746 0 0 25 0 1 0 905477648 163618816 36485 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 39946 36490 1111 63 0 39883 0
vsize: 159784
[startup+219.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 4330968 0 0 0 13877 8124 0 0 25 0 1 0 905477648 167153664 37375 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 40809 37375 1111 63 0 40746 0
vsize: 163236
[startup+229.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 4527875 0 0 0 14486 8515 0 0 25 0 1 0 905477648 170549248 38178 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 41638 38183 1111 63 0 41575 0
vsize: 166552
[startup+239.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 4724130 0 0 0 15087 8915 0 0 25 0 1 0 905477648 173944832 39063 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 42467 39068 1111 63 0 42404 0
vsize: 169868
[startup+249.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 4918385 0 0 0 15704 9298 0 0 25 0 1 0 905477648 176787456 39777 4294967295 134512640 134716908 3221224560 3221222568 1077364239 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 43263 39782 1111 63 0 43200 0
vsize: 172644
[startup+259.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 5111767 0 0 0 16316 9686 0 0 25 0 1 0 905477648 180469760 40641 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 44060 40645 1111 63 0 43997 0
vsize: 176240
[startup+269.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 5306223 0 0 0 16937 10066 0 0 25 0 1 0 905477648 183595008 41433 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 44823 41438 1111 63 0 44760 0
vsize: 179292
[startup+279.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 5498434 0 0 0 17555 10448 0 0 25 0 1 0 905477648 188407808 42540 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 45998 42545 1111 63 0 45935 0
vsize: 183992
[startup+289.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 5691796 0 0 0 18167 10836 0 0 25 0 1 0 905477648 191389696 43274 4294967295 134512640 134716908 3221224560 3221222604 1077387418 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 46726 43280 1111 63 0 46663 0
vsize: 186904
[startup+299.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 5883556 0 0 0 18777 11226 0 0 25 0 1 0 905477648 194379776 44103 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 47456 44108 1111 63 0 47393 0
vsize: 189824
[startup+309.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 6075782 0 0 0 19395 11609 0 0 25 0 1 0 905477648 197369856 44822 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 48186 44828 1111 63 0 48123 0
vsize: 192744
[startup+319.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 6267958 0 0 0 20008 11997 0 0 25 0 1 0 905477648 199749632 45420 4294967295 134512640 134716908 3221224560 3221222220 1077244344 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 48881 45425 1111 63 0 48818 0
vsize: 195068
[startup+329.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 6460007 0 0 0 20619 12386 0 0 25 0 1 0 905477648 203071488 46197 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 49578 46201 1111 63 0 49515 0
vsize: 198312
[startup+339.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 6649873 0 0 0 21240 12764 0 0 25 0 1 0 905477648 205795328 46845 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 50243 46851 1111 63 0 50180 0
vsize: 200972
[startup+349.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 6841915 0 0 0 21851 13154 0 0 25 0 1 0 905477648 208019456 47467 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 50786 47467 1111 63 0 50723 0
vsize: 203144
[startup+359.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 7033100 0 0 0 22462 13543 0 0 25 0 1 0 905477648 211230720 48227 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 51570 48232 1111 63 0 51507 0
vsize: 206280
[startup+369.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 7224446 0 0 0 23081 13925 0 0 25 0 1 0 905477648 213942272 48902 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 52232 48907 1111 63 0 52169 0
vsize: 208928
[startup+379.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 7414570 0 0 0 23702 14305 0 0 25 0 1 0 905477648 216526848 49488 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 52863 49493 1111 63 0 52800 0
vsize: 211452
[startup+389.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 7605613 0 0 0 24322 14685 0 0 25 0 1 0 905477648 219103232 50110 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 53492 50115 1111 63 0 53429 0
vsize: 213968
[startup+399.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 7794357 0 0 0 24938 15069 0 0 25 0 1 0 905477648 221687808 50780 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 54123 50780 1111 63 0 54060 0
vsize: 216492
[startup+409.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 7982161 0 0 0 25552 15454 0 0 25 0 1 0 905477648 224264192 51426 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 54752 51431 1111 63 0 54689 0
vsize: 219008
[startup+419.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 8171518 0 0 0 26174 15833 0 0 25 0 1 0 905477648 228249600 51958 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 55725 51963 1111 63 0 55662 0
vsize: 222900
[startup+429.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 8361285 0 0 0 26792 16215 0 0 25 0 1 0 905477648 230694912 52651 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 56322 52656 1111 63 0 56259 0
vsize: 225288
[startup+439.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 8551202 0 0 0 27409 16598 0 0 25 0 1 0 905477648 233136128 53200 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 56918 53204 1111 63 0 56855 0
vsize: 227672
[startup+449.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 8740814 0 0 0 28025 16982 0 0 25 0 1 0 905477648 235589632 53752 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 57517 53757 1111 63 0 57454 0
vsize: 230068
[startup+459.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 8929411 0 0 0 28643 17365 0 0 25 0 1 0 905477648 237895680 54411 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 58080 54416 1111 63 0 58017 0
vsize: 232320
[startup+469.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 9118029 0 0 0 29266 17742 0 0 25 0 1 0 905477648 240201728 54951 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 58643 54956 1111 63 0 58580 0
vsize: 234572
[startup+479.999 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 9306816 0 0 0 29885 18123 0 0 25 0 1 0 905477648 242655232 55538 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 59242 55543 1111 63 0 59179 0
vsize: 236968
[startup+489.999 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 9496977 0 0 0 30502 18507 0 0 25 0 1 0 905477648 244961280 56140 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 59805 56145 1111 63 0 59742 0
vsize: 239220
[startup+499.999 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 9686333 0 0 0 31114 18895 0 0 25 0 1 0 905477648 247132160 56603 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 60335 56607 1111 63 0 60272 0
vsize: 241340
[startup+510 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 9875855 0 0 0 31736 19273 0 0 25 0 1 0 905477648 249446400 57271 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 60900 57276 1111 63 0 60837 0
vsize: 243600
[startup+520 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 10063062 0 0 0 32352 19656 0 0 25 0 1 0 905477648 251617280 57774 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 61430 57779 1111 63 0 61367 0
vsize: 245720
[startup+530 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 10252102 0 0 0 32964 20044 0 0 25 0 1 0 905477648 253337600 58224 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 61850 58224 1111 63 0 61787 0
vsize: 247400
[startup+540 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 10441846 0 0 0 33581 20428 0 0 25 0 1 0 905477648 256110592 58848 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 62527 58853 1111 63 0 62464 0
vsize: 250108
[startup+550 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 10630409 0 0 0 34198 20812 0 0 25 0 1 0 905477648 258281472 59452 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 62910 59306 1111 63 0 62847 0
vsize: 252228
[startup+560.001 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 10819099 0 0 0 34822 21187 0 0 25 0 1 0 905477648 260452352 59969 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 63587 59974 1111 63 0 63524 0
vsize: 254348
[startup+570 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 11008127 0 0 0 35447 21563 0 0 25 0 1 0 905477648 262623232 60488 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 64117 60493 1111 63 0 64054 0
vsize: 256468
[startup+580.001 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 11196461 0 0 0 36063 21948 0 0 25 0 1 0 905477648 264802304 61001 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 64649 61006 1111 63 0 64586 0
vsize: 258596
[startup+590.001 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 11385064 0 0 0 36678 22333 0 0 25 0 1 0 905477648 266838016 61487 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 65146 61492 1111 63 0 65083 0
vsize: 260584
[startup+600.001 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 11573596 0 0 0 37296 22714 0 0 25 0 1 0 905477648 268877824 61968 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 65644 61973 1111 63 0 65581 0
vsize: 262576
[startup+610.001 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 11763387 0 0 0 37916 23095 0 0 25 0 1 0 905477648 271048704 62572 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 66174 62577 1111 63 0 66111 0
vsize: 264696
[startup+620.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 11953716 0 0 0 38520 23491 0 0 25 0 1 0 905477648 273084416 63050 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 66671 63054 1111 63 0 66608 0
vsize: 266684
[startup+630.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 12142811 0 0 0 39139 23873 0 0 25 0 1 0 905477648 275128320 63458 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 67170 63463 1111 63 0 67107 0
vsize: 268680
[startup+640.001 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 12330952 0 0 0 39754 24257 0 0 25 0 1 0 905477648 277164032 64073 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 67667 64079 1111 63 0 67604 0
vsize: 270668
[startup+650.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 12519576 0 0 0 40367 24645 0 0 25 0 1 0 905477648 278552576 64445 4294967295 134512640 134716908 3221224560 3221222760 1077799185 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 68165 64446 1111 63 0 68102 0
vsize: 272024
[startup+660.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 12708685 0 0 0 40983 25029 0 0 25 0 1 0 905477648 281243648 65068 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 68663 65073 1111 63 0 68600 0
vsize: 274652
[startup+670.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 12897525 0 0 0 41595 25418 0 0 25 0 1 0 905477648 283279360 65531 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 69160 65536 1111 63 0 69097 0
vsize: 276640
[startup+680.002 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 13085739 0 0 0 42211 25802 0 0 25 0 1 0 905477648 285179904 65990 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 69624 65996 1111 63 0 69561 0
vsize: 278496
[startup+690.002 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 13274739 0 0 0 42828 26185 0 0 25 0 1 0 905477648 287215616 66423 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 70121 66428 1111 63 0 70058 0
vsize: 280484
[startup+700.002 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 13462429 0 0 0 43448 26565 0 0 25 0 1 0 905477648 289124352 66978 4294967295 134512640 134716908 3221224560 3221222864 134568037 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 70587 66983 1111 63 0 70524 0
vsize: 282348
[startup+710.003 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 13492530 0 0 0 44382 26631 0 0 25 0 1 0 905477648 330108928 78432 4294967295 134512640 134716908 3221224560 3221223488 134606504 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 80593 78438 1111 63 0 80530 0
vsize: 322372
[startup+716.97 s]
Raw data (loadavg): 1.17 1.03 0.93 1/53 3817
Raw data (stat): 3817 (bsolo_lpr_cuts-) R 3816 25568 25567 0 -1 0 13492530 0 0 0 44382 26631 0 0 25 0 1 0 905477648 330108928 78432 4294967295 134512640 134716908 3221224560 3221223488 134606504 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 80593 78438 1111 63 0 80530 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 716.97
CPU time (s): 717.097
CPU user time (s): 446.822
CPU system time (s): 270.275
CPU usage (%): 100.018
Max. virtual memory (Kb): 322372
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####