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/web/uclid_pb_benchmarks/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb
MD5SUM	dcb6d1c3f66e900ae345e6fa455bef2a
Bench Category	no optimization function (SAT)
Has Objective Function	NO
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 numbers	10
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	168111
Total number of constraints	487525
Number of constraints which are clauses	468727
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	18798
Minimum length of a constraint	1
Maximum length of a constraint	15
Trace number 24648

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-11 13:53:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2711 boxname=wulflinc31 idbench=302 idsolver=2 numberseed=0
MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7  /oldhome/oroussel/solvers/bsolo_lpr_cuts
MD5SUM BENCH:  dcb6d1c3f66e900ae345e6fa455bef2a  /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb
REAL COMMAND:  bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb
IDLAUNCH: 2711
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 3
cpu MHz		: 451.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        909888 kB
Buffers:          3492 kB
Cached:          96084 kB
SwapCached:       4396 kB
Active:          69812 kB
Inactive:        35364 kB
HighTotal:      131008 kB
HighFree:        34244 kB
LowTotal:       903652 kB
LowFree:        875644 kB
SwapTotal:     2097892 kB
SwapFree:      2092816 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            13856 kB
Committed_AS:    63652 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-11 14:06:01 (client local time) WITH STATUS 0 IN 736.016 SECONDS
stats: 2711 7 736.016 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
Raw data (loadavg): 0.92 0.97 0.99 2/54 30191
Raw data (stat): 30191 (runsolver) R 30190 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 718398828 1056768 100 4294967295 134512640 135381576 3221221664 3221216880 135158418 0 2147483391 1 90112 0 0 0 17 1 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 33338 0 0 0 917 77 0 0 25 0 1 0 718398828 40636416 6631 4294967295 134512640 134714508 3221221760 3221220040 1077378438 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9971 6632 1111 63 0 9908 0
vsize: 39684
[startup+20.0018 s]
Raw data (loadavg): 0.94 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 149498 0 0 0 1712 283 0 0 25 0 1 0 718398828 56741888 10559 4294967295 134512640 134714508 3221221760 3221219960 1077799185 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13853 10559 1111 63 0 13790 0
vsize: 55412
[startup+30.0028 s]
Raw data (loadavg): 0.95 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 370359 0 0 0 2321 673 0 0 25 0 1 0 718398828 67178496 13033 4294967295 134512640 134714508 3221221760 3221220064 134568032 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 16401 13033 1111 63 0 16338 0
vsize: 65604
[startup+40.0035 s]
Raw data (loadavg): 0.96 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 592912 0 0 0 2925 1069 0 0 25 0 1 0 718398828 75874304 15171 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18524 15179 1111 63 0 18461 0
vsize: 74096
[startup+50.0046 s]
Raw data (loadavg): 0.96 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 809175 0 0 0 3541 1454 0 0 25 0 1 0 718398828 83763200 17073 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20450 17073 1111 63 0 20387 0
vsize: 81800
[startup+60.0053 s]
Raw data (loadavg): 0.97 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 1025655 0 0 0 4138 1856 0 0 25 0 1 0 718398828 90832896 18797 4294967295 134512640 134714508 3221221760 3221219804 1077387418 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 22176 18804 1111 63 0 22113 0
vsize: 88704
[startup+70.0063 s]
Raw data (loadavg): 0.97 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 1239945 0 0 0 4744 2250 0 0 25 0 1 0 718398828 97345536 20423 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 23766 20428 1111 63 0 23703 0
vsize: 95064
[startup+80.0072 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 1449129 0 0 0 5356 2638 0 0 25 0 1 0 718398828 104181760 22099 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 25435 22106 1111 63 0 25372 0
vsize: 101740
[startup+90.0071 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 1658962 0 0 0 5963 3031 0 0 25 0 1 0 718398828 109883392 23473 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 26827 23478 1111 63 0 26764 0
vsize: 107308
[startup+100.008 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 1866334 0 0 0 6571 3424 0 0 25 0 1 0 718398828 115183616 24832 4294967295 134512640 134714508 3221221760 3221220064 134568032 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 28121 24832 1111 63 0 28058 0
vsize: 112484
[startup+110.009 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 2069967 0 0 0 7176 3818 0 0 25 0 1 0 718398828 120975360 26064 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 29535 26064 1111 63 0 29472 0
vsize: 118140
[startup+120.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 2271470 0 0 0 7784 4210 0 0 25 0 1 0 718398828 125431808 27170 4294967295 134512640 134714508 3221221760 3221220504 134569945 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 30623 27170 1111 63 0 30560 0
vsize: 122492
[startup+130.011 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 2471552 0 0 0 8395 4600 0 0 25 0 1 0 718398828 130347008 28359 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 31823 28359 1111 63 0 31760 0
vsize: 127292
[startup+140.012 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 2668234 0 0 0 9008 4987 0 0 25 0 1 0 718398828 134832128 29413 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 32918 29413 1111 63 0 32855 0
vsize: 131672
[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 2864585 0 0 0 9617 5378 0 0 25 0 1 0 718398828 139042816 30462 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 33946 30468 1111 63 0 33883 0
vsize: 135784
[startup+160.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 3058616 0 0 0 10228 5768 0 0 25 0 1 0 718398828 142987264 31417 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 34909 31417 1111 63 0 34846 0
vsize: 139636
[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 3250761 0 0 0 10844 6151 0 0 25 0 1 0 718398828 146788352 32363 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 35837 32363 1111 63 0 35774 0
vsize: 143348
[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 3443994 0 0 0 11459 6537 0 0 25 0 1 0 718398828 150589440 33276 4294967295 134512640 134714508 3221221760 3221220064 134568044 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 36765 33276 1111 63 0 36702 0
vsize: 147060
[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 3635403 0 0 0 12073 6923 0 0 25 0 1 0 718398828 154025984 34179 4294967295 134512640 134714508 3221221760 3221219420 1077272273 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 37604 34179 1111 63 0 37541 0
vsize: 150416
[startup+200.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 3825976 0 0 0 12696 7300 0 0 25 0 1 0 718398828 157921280 35146 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 38555 35146 1111 63 0 38492 0
vsize: 154220
[startup+210.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 4016022 0 0 0 13313 7682 0 0 25 0 1 0 718398828 161452032 36006 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 39417 36006 1111 63 0 39354 0
vsize: 157668
[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 4205523 0 0 0 13930 8066 0 0 25 0 1 0 718398828 164458496 36769 4294967295 134512640 134714508 3221221760 3221220352 134526826 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 40151 36769 1111 63 0 40088 0
vsize: 160604
[startup+230.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 4393267 0 0 0 14551 8445 0 0 25 0 1 0 718398828 167849984 37578 4294967295 134512640 134714508 3221221760 3221220344 1077377227 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 40979 37578 1111 63 0 40916 0
vsize: 163916
[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 4581666 0 0 0 15179 8817 0 0 25 0 1 0 718398828 171507712 38422 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 41872 38422 1111 63 0 41809 0
vsize: 167488
[startup+250.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 4771728 0 0 0 15792 9204 0 0 25 0 1 0 718398828 174354432 39178 4294967295 134512640 134714508 3221221760 3221219960 1077799185 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 42567 39178 1111 63 0 42504 0
vsize: 170268
[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 4960656 0 0 0 16416 9580 0 0 25 0 1 0 718398828 177893376 40036 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 43431 40041 1111 63 0 43368 0
vsize: 173724
[startup+270.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 5148720 0 0 0 17032 9965 0 0 25 0 1 0 718398828 181014528 40786 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 44193 40791 1111 63 0 44130 0
vsize: 176772
[startup+280.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 5336759 0 0 0 17659 10337 0 0 25 0 1 0 718398828 184139776 41555 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 44956 41560 1111 63 0 44893 0
vsize: 179824
[startup+290.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 5525113 0 0 0 18288 10709 0 0 25 0 1 0 718398828 188817408 42659 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 46098 42664 1111 63 0 46035 0
vsize: 184392
[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 5714351 0 0 0 18911 11086 0 0 25 0 1 0 718398828 191807488 43381 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 46828 43386 1111 63 0 46765 0
vsize: 187312
[startup+310.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 5903406 0 0 0 19533 11464 0 0 25 0 1 0 718398828 194789376 44092 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 47556 44097 1111 63 0 47493 0
vsize: 190224
[startup+320.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 6091438 0 0 0 20150 11847 0 0 25 0 1 0 718398828 197046272 44779 4294967295 134512640 134714508 3221221760 3221219960 1077799185 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 48107 44779 1111 63 0 48044 0
vsize: 192428
[startup+330.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 6278577 0 0 0 20778 12219 0 0 25 0 1 0 718398828 200355840 45559 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 48915 45563 1111 63 0 48852 0
vsize: 195660
[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 6465700 0 0 0 21399 12598 0 0 25 0 1 0 718398828 203075584 46214 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 49579 46219 1111 63 0 49516 0
vsize: 198316
[startup+350.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 6654616 0 0 0 22022 12975 0 0 25 0 1 0 718398828 205799424 46876 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 50244 46881 1111 63 0 50181 0
vsize: 200976
[startup+360.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 6841625 0 0 0 22640 13358 0 0 25 0 1 0 718398828 208510976 47542 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 50906 47547 1111 63 0 50843 0
vsize: 203624
[startup+370.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 7027499 0 0 0 23270 13728 0 0 25 0 1 0 718398828 211099648 48200 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 51538 48205 1111 63 0 51475 0
vsize: 206152
[startup+380.076 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 30191
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 7214682 0 0 0 23900 14103 0 0 25 0 1 0 718398828 213811200 48784 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 52200 48789 1111 63 0 52137 0
vsize: 208800
[startup+390.205 s]
Raw data (loadavg): 1.07 0.99 0.99 2/56 30230
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 7403916 0 0 0 24539 14476 0 0 25 0 1 0 718398828 216395776 49506 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 52831 49511 1111 63 0 52768 0
vsize: 211324
[startup+400.46 s]
Raw data (loadavg): 1.14 1.00 1.00 3/57 30239
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 7589720 0 0 0 25157 14856 0 0 25 0 1 0 718398828 218972160 50100 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 53460 50106 1111 63 0 53397 0
vsize: 213840
[startup+410.611 s]
Raw data (loadavg): 1.19 1.02 1.00 2/54 30244
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 7779480 0 0 0 25792 15237 0 0 25 0 1 0 718398828 221556736 50770 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 54091 50775 1111 63 0 54028 0
vsize: 216364
[startup+420.713 s]
Raw data (loadavg): 1.16 1.02 1.00 2/54 30244
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 7967339 0 0 0 26425 15614 0 0 25 0 1 0 718398828 223997952 51332 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 54687 51337 1111 63 0 54624 0
vsize: 218748
[startup+430.713 s]
Raw data (loadavg): 1.14 1.02 1.00 2/54 30244
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 8153503 0 0 0 27052 15987 0 0 25 0 1 0 718398828 227975168 51899 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 55658 51904 1111 63 0 55595 0
vsize: 222632
[startup+440.714 s]
Raw data (loadavg): 1.12 1.02 1.00 2/54 30244
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 8338119 0 0 0 27669 16370 0 0 25 0 1 0 718398828 230428672 52549 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 56257 52554 1111 63 0 56194 0
vsize: 225028
[startup+450.714 s]
Raw data (loadavg): 1.10 1.02 1.00 2/54 30244
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 8521365 0 0 0 28295 16744 0 0 25 0 1 0 718398828 232734720 53071 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 56820 53075 1111 63 0 56757 0
vsize: 227280
[startup+460.716 s]
Raw data (loadavg): 1.08 1.01 1.00 2/54 30244
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 8705055 0 0 0 28928 17112 0 0 25 0 1 0 718398828 234500096 53611 4294967295 134512640 134714508 3221221760 3221218236 1077198899 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 57251 53611 1111 63 0 57188 0
vsize: 229004
[startup+470.716 s]
Raw data (loadavg): 1.07 1.01 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 8888270 0 0 0 29552 17486 0 0 25 0 1 0 718398828 237359104 54183 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 57949 54188 1111 63 0 57886 0
vsize: 231796
[startup+480.717 s]
Raw data (loadavg): 1.06 1.01 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 9072031 0 0 0 30173 17866 0 0 25 0 1 0 718398828 239665152 54793 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 58512 54798 1111 63 0 58449 0
vsize: 234048
[startup+490.717 s]
Raw data (loadavg): 1.05 1.01 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 9256372 0 0 0 30799 18239 0 0 25 0 1 0 718398828 241975296 55399 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 59076 55404 1111 63 0 59013 0
vsize: 236304
[startup+500.718 s]
Raw data (loadavg): 1.04 1.01 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 9441120 0 0 0 31430 18609 0 0 25 0 1 0 718398828 244289536 55891 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 59641 55896 1111 63 0 59578 0
vsize: 238564
[startup+510.719 s]
Raw data (loadavg): 1.03 1.01 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 9625264 0 0 0 32050 18989 0 0 25 0 1 0 718398828 246460416 56442 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 60171 56447 1111 63 0 60108 0
vsize: 240684
[startup+520.72 s]
Raw data (loadavg): 1.03 1.01 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 9808004 0 0 0 32676 19363 0 0 25 0 1 0 718398828 248631296 56940 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 60701 56940 1111 63 0 60638 0
vsize: 242804
[startup+530.721 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 9993029 0 0 0 33300 19739 0 0 25 0 1 0 718398828 250810368 57533 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 61233 57538 1111 63 0 61170 0
vsize: 244932
[startup+540.721 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 10178299 0 0 0 33917 20122 0 0 25 0 1 0 718398828 253120512 58157 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 61653 58016 1111 63 0 61590 0
vsize: 247188
[startup+550.722 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 10363703 0 0 0 34545 20494 0 0 25 0 1 0 718398828 255156224 58666 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 62294 58671 1111 63 0 62231 0
vsize: 249176
[startup+560.723 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 10548930 0 0 0 35166 20873 0 0 25 0 1 0 718398828 257331200 59214 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 62825 59219 1111 63 0 62762 0
vsize: 251300
[startup+570.724 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 10732079 0 0 0 35775 21265 0 0 25 0 1 0 718398828 259510272 59685 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 63357 59689 1111 63 0 63294 0
vsize: 253428
[startup+580.724 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 10914448 0 0 0 36398 21641 0 0 25 0 1 0 718398828 261545984 60240 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 63854 60240 1111 63 0 63791 0
vsize: 255416
[startup+590.723 s]
Raw data (loadavg): 1.01 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 11099428 0 0 0 37021 22018 0 0 25 0 1 0 718398828 263716864 60626 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 64384 60630 1111 63 0 64321 0
vsize: 257536
[startup+600.724 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 11284568 0 0 0 37642 22397 0 0 25 0 1 0 718398828 265752576 61234 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 64881 61239 1111 63 0 64818 0
vsize: 259524
[startup+610.724 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 11468883 0 0 0 38263 22777 0 0 25 0 1 0 718398828 267792384 61714 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 65379 61720 1111 63 0 65316 0
vsize: 261516
[startup+620.726 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 11654201 0 0 0 38887 23152 0 0 25 0 1 0 718398828 269828096 62256 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 65876 62261 1111 63 0 65813 0
vsize: 263504
[startup+630.726 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 11838920 0 0 0 39513 23527 0 0 25 0 1 0 718398828 271872000 62651 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 66375 62655 1111 63 0 66312 0
vsize: 265500
[startup+640.726 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 12021178 0 0 0 40134 23905 0 0 25 0 1 0 718398828 273907712 63257 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 66872 63257 1111 63 0 66809 0
vsize: 267488
[startup+650.727 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 12204582 0 0 0 40770 24270 0 0 25 0 1 0 718398828 275808256 63693 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 67336 63697 1111 63 0 67273 0
vsize: 269344
[startup+660.727 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 12389260 0 0 0 41385 24655 0 0 25 0 1 0 718398828 277843968 64245 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 67833 64250 1111 63 0 67770 0
vsize: 271332
[startup+670.728 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 12573586 0 0 0 42018 25022 0 0 25 0 1 0 718398828 279883776 64721 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 68331 64725 1111 63 0 68268 0
vsize: 273324
[startup+680.729 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 12757502 0 0 0 42635 25405 0 0 25 0 1 0 718398828 281788416 65093 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 68796 65098 1111 63 0 68733 0
vsize: 275184
[startup+690.729 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 12941509 0 0 0 43259 25782 0 0 25 0 1 0 718398828 283688960 65570 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 69260 65575 1111 63 0 69197 0
vsize: 277040
[startup+700.73 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 13124610 0 0 0 43882 26159 0 0 25 0 1 0 718398828 285597696 66099 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 69726 66099 1111 63 0 69663 0
vsize: 278904
[startup+710.731 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 13308062 0 0 0 44508 26533 0 0 25 0 1 0 718398828 287498240 66515 4294967295 134512640 134714508 3221221760 3221220064 134568037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 70190 66520 1111 63 0 70127 0
vsize: 280760
[startup+720.732 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 13481436 0 0 0 45148 26892 0 0 25 0 1 0 718398828 290480128 67348 4294967295 134512640 134714508 3221221760 3221220088 1077378037 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 70918 67348 1111 63 0 70855 0
vsize: 283672
[startup+730.733 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 30246
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 13516671 0 0 0 46062 26979 0 0 25 0 1 0 718398828 429322240 102581 4294967295 134512640 134714508 3221221760 3221220400 134606488 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 104815 102581 1111 63 0 104752 0
vsize: 419260
[startup+736.345 s]
Raw data (loadavg): 1.00 1.00 1.00 1/53 30248
Raw data (stat): 30191 (bsolo_lpr_cuts) R 30190 7876 7672 0 -1 0 13516671 0 0 0 46062 26979 0 0 25 0 1 0 718398828 429322240 102581 4294967295 134512640 134714508 3221221760 3221220400 134606488 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 104815 102581 1111 63 0 104752 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 736.344
CPU time (s): 736.016
CPU user time (s): 462.592
CPU system time (s): 273.424
CPU usage (%): 99.9555
Max. virtual memory (Kb): 419260
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####