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 24649

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-11 14:06:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2712 boxname=wulflinc31 idbench=302 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  dcb6d1c3f66e900ae345e6fa455bef2a  /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.ex.mem.LsqHdStrong.ucl.opb
IDLAUNCH: 2712
/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:        917024 kB
Buffers:          1588 kB
Cached:          93764 kB
SwapCached:       1956 kB
Active:          66900 kB
Inactive:        31556 kB
HighTotal:      131008 kB
HighFree:        36652 kB
LowTotal:       903652 kB
LowFree:        880372 kB
SwapTotal:     2097892 kB
SwapFree:      2095248 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            13244 kB
Committed_AS:    63648 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-11 14:18:34 (client local time) WITH STATUS 0 IN 741.188 SECONDS
stats: 2712 7 741.188 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
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.93 0.98 0.99 1/54 30341
Raw data (stat): 30341 (runsolver) R 30340 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 718473676 1056768 100 4294967295 134512640 135381576 3221221664 3221216884 135158418 0 0 1 90112 0 0 0 17 1 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0007 s]
Raw data (loadavg): 0.94 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 34126 0 0 0 925 71 0 0 25 0 1 0 718473676 40964096 6618 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10001 6624 1111 63 0 9938 0
vsize: 40004
[startup+20.0014 s]
Raw data (loadavg): 0.95 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 160127 0 0 0 1693 303 0 0 25 0 1 0 718473676 56639488 10460 4294967295 134512640 134714540 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13828 10460 1111 63 0 13765 0
vsize: 55312
[startup+30.0024 s]
Raw data (loadavg): 0.95 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 382390 0 0 0 2304 693 0 0 25 0 1 0 718473676 67354624 12974 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 16444 12981 1111 63 0 16381 0
vsize: 65776
[startup+40.0033 s]
Raw data (loadavg): 0.96 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 603970 0 0 0 2918 1079 0 0 25 0 1 0 718473676 76046336 15139 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18521 15096 1111 63 0 18458 0
vsize: 74264
[startup+50.0043 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 821735 0 0 0 3534 1463 0 0 25 0 1 0 718473676 83931136 17023 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20491 17028 1111 63 0 20428 0
vsize: 81964
[startup+60.0042 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 1032628 0 0 0 4136 1861 0 0 25 0 1 0 718473676 90726400 18712 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 22150 18719 1111 63 0 22087 0
vsize: 88600
[startup+70.0041 s]
Raw data (loadavg): 0.97 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 1245378 0 0 0 4742 2256 0 0 25 0 1 0 718473676 97239040 20301 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 23740 20307 1111 63 0 23677 0
vsize: 94960
[startup+80.0052 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 1455357 0 0 0 5349 2649 0 0 25 0 1 0 718473676 104075264 21978 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 25409 21984 1111 63 0 25346 0
vsize: 101636
[startup+90.005 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 1661535 0 0 0 5956 3042 0 0 25 0 1 0 718473676 109641728 23348 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 26768 23353 1111 63 0 26705 0
vsize: 107072
[startup+100.006 s]
Raw data (loadavg): 0.98 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 1868680 0 0 0 6566 3432 0 0 25 0 1 0 718473676 115077120 24654 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 28095 24659 1111 63 0 28032 0
vsize: 112380
[startup+110.007 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 2072041 0 0 0 7186 3812 0 0 25 0 1 0 718473676 120864768 25928 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 29508 25933 1111 63 0 29445 0
vsize: 118032
[startup+120.008 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 2271395 0 0 0 7802 4197 0 0 25 0 1 0 718473676 125321216 27036 4294967295 134512640 134714540 3221221776 3221220056 1077378037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 30669 27039 1111 63 0 30606 0
vsize: 122384
[startup+130.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 2469961 0 0 0 8424 4575 0 0 25 0 1 0 718473676 129789952 28158 4294967295 134512640 134714540 3221221776 3221219428 1077360673 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 31762 28159 1111 63 0 31699 0
vsize: 126748
[startup+140.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 2667945 0 0 0 9039 4960 0 0 25 0 1 0 718473676 134582272 29266 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 32857 29271 1111 63 0 32794 0
vsize: 131428
[startup+150.01 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 2865605 0 0 0 9653 5346 0 0 25 0 1 0 718473676 138788864 30352 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 33884 30356 1111 63 0 33821 0
vsize: 135536
[startup+160.01 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 3061547 0 0 0 10270 5729 0 0 25 0 1 0 718473676 142868480 31341 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 34880 31347 1111 63 0 34817 0
vsize: 139520
[startup+170.009 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 3255782 0 0 0 10896 6103 0 0 25 0 1 0 718473676 146669568 32250 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 35808 32254 1111 63 0 35745 0
vsize: 143232
[startup+180.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 3449538 0 0 0 11511 6489 0 0 25 0 1 0 718473676 150470656 33193 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 36736 33198 1111 63 0 36673 0
vsize: 146944
[startup+190.011 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 3643886 0 0 0 12126 6874 0 0 25 0 1 0 718473676 154271744 34116 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 37664 34120 1111 63 0 37601 0
vsize: 150656
[startup+200.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 3835415 0 0 0 12747 7253 0 0 25 0 1 0 718473676 157937664 34990 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 38559 34994 1111 63 0 38496 0
vsize: 154236
[startup+210.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 4028408 0 0 0 13374 7626 0 0 25 0 1 0 718473676 161468416 35937 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 39421 35941 1111 63 0 39358 0
vsize: 157684
[startup+220.012 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 4218940 0 0 0 13998 8002 0 0 25 0 1 0 718473676 164999168 36746 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 40283 36751 1111 63 0 40220 0
vsize: 161132
[startup+230.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 4408683 0 0 0 14616 8385 0 0 25 0 1 0 718473676 168259584 37563 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 41079 37567 1111 63 0 41016 0
vsize: 164316
[startup+240.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 4597487 0 0 0 15239 8762 0 0 25 0 1 0 718473676 171520000 38329 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 41875 38334 1111 63 0 41812 0
vsize: 167500
[startup+250.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 4784865 0 0 0 15863 9138 0 0 25 0 1 0 718473676 174780416 39138 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 42671 39143 1111 63 0 42608 0
vsize: 170684
[startup+260.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 4971855 0 0 0 16482 9519 0 0 25 0 1 0 718473676 177483776 39881 4294967295 134512640 134714540 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 43331 39881 1111 63 0 43268 0
vsize: 173324
[startup+270.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 5158410 0 0 0 17103 9898 0 0 25 0 1 0 718473676 180600832 40634 4294967295 134512640 134714540 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 44092 40634 1111 63 0 44029 0
vsize: 176368
[startup+280.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 5344959 0 0 0 17728 10274 0 0 25 0 1 0 718473676 184016896 41437 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 44926 41442 1111 63 0 44863 0
vsize: 179704
[startup+290.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 5531338 0 0 0 18350 10652 0 0 25 0 1 0 718473676 188694528 42582 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 46068 42587 1111 63 0 46005 0
vsize: 184272
[startup+300.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 5716920 0 0 0 18979 11023 0 0 25 0 1 0 718473676 191229952 43248 4294967295 134512640 134714540 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 46687 43249 1111 63 0 46624 0
vsize: 186748
[startup+310.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 5901655 0 0 0 19618 11384 0 0 25 0 1 0 718473676 194531328 44034 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 47493 44039 1111 63 0 47430 0
vsize: 189972
[startup+320.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 6087234 0 0 0 20238 11765 0 0 25 0 1 0 718473676 197390336 44674 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 48191 44679 1111 63 0 48128 0
vsize: 192764
[startup+330.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 6271263 0 0 0 20862 12140 0 0 25 0 1 0 718473676 200101888 45401 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 48853 45405 1111 63 0 48790 0
vsize: 195412
[startup+340.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 6455584 0 0 0 21485 12518 0 0 25 0 1 0 718473676 202821632 46044 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 49517 46048 1111 63 0 49454 0
vsize: 198068
[startup+350.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 6640664 0 0 0 22108 12895 0 0 25 0 1 0 718473676 205402112 46699 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 50147 46704 1111 63 0 50084 0
vsize: 200588
[startup+360.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 6824927 0 0 0 22732 13271 0 0 25 0 1 0 718473676 207634432 47282 4294967295 134512640 134714540 3221221776 3221220528 134566218 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 50811 47286 1111 63 0 50748 0
vsize: 202768
[startup+370.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 7008833 0 0 0 23359 13644 0 0 25 0 1 0 718473676 210698240 47953 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 51440 47957 1111 63 0 51377 0
vsize: 205760
[startup+380.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 7191305 0 0 0 23987 14016 0 0 25 0 1 0 718473676 213282816 48643 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 52071 48648 1111 63 0 52008 0
vsize: 208284
[startup+390.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 7375017 0 0 0 24615 14389 0 0 25 0 1 0 718473676 215859200 49238 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 52700 49242 1111 63 0 52637 0
vsize: 210800
[startup+400.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 7558817 0 0 0 25241 14763 0 0 25 0 1 0 718473676 218308608 49912 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 53298 49916 1111 63 0 53235 0
vsize: 213192
[startup+410.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 7742520 0 0 0 25864 15140 0 0 25 0 1 0 718473676 220749824 50526 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 53768 50402 1111 63 0 53705 0
vsize: 215576
[startup+420.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 7926613 0 0 0 26483 15521 0 0 25 0 1 0 718473676 223334400 51044 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 54525 51049 1111 63 0 54462 0
vsize: 218100
[startup+430.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 8109470 0 0 0 27106 15898 0 0 25 0 1 0 718473676 227315712 51637 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 55497 51641 1111 63 0 55434 0
vsize: 221988
[startup+440.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 8291457 0 0 0 27738 16267 0 0 25 0 1 0 718473676 229621760 52265 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 56060 52269 1111 63 0 55997 0
vsize: 224240
[startup+450.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 8474719 0 0 0 28368 16637 0 0 25 0 1 0 718473676 231936000 52815 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 56625 52819 1111 63 0 56562 0
vsize: 226500
[startup+460.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 8657735 0 0 0 28983 17022 0 0 25 0 1 0 718473676 233832448 53347 4294967295 134512640 134714540 3221221776 3221220264 1077378037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 57221 53350 1111 63 0 57158 0
vsize: 228352
[startup+470.025 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 8840103 0 0 0 29604 17401 0 0 25 0 1 0 718473676 236134400 53911 4294967295 134512640 134714540 3221221776 3221219976 1077799185 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 57650 53911 1111 63 0 57587 0
vsize: 230600
[startup+480.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 9022625 0 0 0 30221 17784 0 0 25 0 1 0 718473676 238862336 54601 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 58180 54469 1111 63 0 58117 0
vsize: 233264
[startup+490.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 9205930 0 0 0 30843 18163 0 0 25 0 1 0 718473676 241168384 55128 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 58879 55132 1111 63 0 58816 0
vsize: 235516
[startup+500.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 9388724 0 0 0 31467 18539 0 0 25 0 1 0 718473676 243474432 55696 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 59442 55700 1111 63 0 59379 0
vsize: 237768
[startup+510.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 9570893 0 0 0 32089 18917 0 0 25 0 1 0 718473676 245653504 56141 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 59974 56146 1111 63 0 59911 0
vsize: 239896
[startup+520.028 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 9753994 0 0 0 32716 19290 0 0 25 0 1 0 718473676 247824384 56727 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 60504 56731 1111 63 0 60441 0
vsize: 242016
[startup+530.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 9936272 0 0 0 33339 19667 0 0 25 0 1 0 718473676 249999360 57326 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 61035 57331 1111 63 0 60972 0
vsize: 244140
[startup+540.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 10117621 0 0 0 33976 20031 0 0 25 0 1 0 718473676 252170240 57740 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 61565 57744 1111 63 0 61502 0
vsize: 246260
[startup+550.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 10299396 0 0 0 34606 20401 0 0 25 0 1 0 718473676 254349312 58274 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 62097 58278 1111 63 0 62034 0
vsize: 248388
[startup+560.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 10482390 0 0 0 35235 20772 0 0 25 0 1 0 718473676 256385024 58826 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 62594 58830 1111 63 0 62531 0
vsize: 250376
[startup+570.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 10664965 0 0 0 35856 21151 0 0 25 0 1 0 718473676 258555904 59382 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 63124 59386 1111 63 0 63061 0
vsize: 252496
[startup+580.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 10847326 0 0 0 36484 21524 0 0 25 0 1 0 718473676 260591616 59890 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 63621 59895 1111 63 0 63558 0
vsize: 254484
[startup+590.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 11030121 0 0 0 37106 21901 0 0 25 0 1 0 718473676 262762496 60435 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 64151 60439 1111 63 0 64088 0
vsize: 256604
[startup+600.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 11213171 0 0 0 37732 22276 0 0 25 0 1 0 718473676 264806400 60890 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 64650 60894 1111 63 0 64587 0
vsize: 258600
[startup+610.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 11395453 0 0 0 38362 22646 0 0 25 0 1 0 718473676 266842112 61370 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 65147 61374 1111 63 0 65084 0
vsize: 260588
[startup+620.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 11577647 0 0 0 38995 23013 0 0 25 0 1 0 718473676 268877824 61912 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 65644 61916 1111 63 0 65581 0
vsize: 262576
[startup+630.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 11760161 0 0 0 39617 23391 0 0 25 0 1 0 718473676 270778368 62338 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 66108 62342 1111 63 0 66045 0
vsize: 264432
[startup+640.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 11942372 0 0 0 40237 23771 0 0 25 0 1 0 718473676 272814080 62818 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 66605 62822 1111 63 0 66542 0
vsize: 266420
[startup+650.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 12124563 0 0 0 40870 24139 0 0 25 0 1 0 718473676 274849792 63356 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 67102 63361 1111 63 0 67039 0
vsize: 268408
[startup+660.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 12306696 0 0 0 41501 24508 0 0 25 0 1 0 718473676 276758528 63909 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 67568 63913 1111 63 0 67505 0
vsize: 270272
[startup+670.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 12488199 0 0 0 42126 24883 0 0 25 0 1 0 718473676 278798336 64349 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 68066 64353 1111 63 0 68003 0
vsize: 272264
[startup+680.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 12670516 0 0 0 42753 25257 0 0 25 0 1 0 718473676 280698880 64817 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 68530 64821 1111 63 0 68467 0
vsize: 274120
[startup+690.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 12853044 0 0 0 43388 25622 0 0 25 0 1 0 718473676 281939968 65202 4294967295 134512640 134714540 3221221776 3221220544 134566030 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 68994 65205 1111 63 0 68931 0
vsize: 275332
[startup+700.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 13034983 0 0 0 44012 25998 0 0 25 0 1 0 718473676 284499968 65694 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 69458 65698 1111 63 0 69395 0
vsize: 277832
[startup+710.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 13217050 0 0 0 44642 26368 0 0 25 0 1 0 718473676 286400512 66228 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 69922 66232 1111 63 0 69859 0
vsize: 279688
[startup+720.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 13398697 0 0 0 45280 26730 0 0 25 0 1 0 718473676 288301056 66608 4294967295 134512640 134714540 3221221776 3221220080 134568037 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 70386 66612 1111 63 0 70323 0
vsize: 281544
[startup+730.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 13490609 0 0 0 46088 26923 0 0 25 0 1 0 718473676 302096384 70111 4294967295 134512640 134714540 3221221776 3221220072 1077364234 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 73754 70111 1111 63 0 73691 0
vsize: 295016
[startup+740.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/54 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 13635719 0 0 0 46731 27280 0 0 25 0 1 0 718473676 891592704 215219 4294967295 134512640 134714540 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 217674 215225 1111 63 0 217611 0
vsize: 870696
[startup+741.115 s]
Raw data (loadavg): 0.99 0.98 0.99 1/53 30341
Raw data (stat): 30341 (bsolo_mis) R 30340 7876 7672 0 -1 0 13635719 0 0 0 46731 27280 0 0 25 0 1 0 718473676 891592704 215219 4294967295 134512640 134714540 3221221776 3221220416 134606488 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 217674 215225 1111 63 0 217611 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 741.114
CPU time (s): 741.188
CPU user time (s): 467.608
CPU system time (s): 273.58
CPU usage (%): 100.01
Max. virtual memory (Kb): 870696
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####