PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-t1717.opb
MD5SUM	bc46e72682d969c09e6f4028df473a45
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	201342
Optimality of the best value was proved	NO
Number of terms in the objective function	73885
Biggest coefficient in the objective function	4066
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	172074995
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	4066
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	172074995
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.34
Number of variables	73885
Total number of constraints	74436
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	74436
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	612
Trace number 25721

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-22 00:06:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18060 boxname=wulflinc31 idbench=1390 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  bc46e72682d969c09e6f4028df473a45  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-t1717.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-t1717.opb
IDLAUNCH: 18060
/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:        799232 kB
Buffers:         27436 kB
Cached:         184848 kB
SwapCached:        964 kB
Active:         156652 kB
Inactive:        57788 kB
HighTotal:      131008 kB
HighFree:        12684 kB
LowTotal:       903652 kB
LowFree:        786548 kB
SwapTotal:     2097892 kB
SwapFree:      2095964 kB
Dirty:               0 kB
Writeback:           0 kB
Mapped:           5096 kB
Slab:            15296 kB
Committed_AS:    63860 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-22 00:18:23 (client local time) WITH STATUS 0 IN 740.35 SECONDS
stats: 18060 7 740.35 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
#### 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.85 0.97 0.96 2/55 17714
Raw data (stat): 17714 (runsolver) R 17713 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 808482910 1056768 100 4294967295 134512640 135381576 3221221680 3221216900 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10 s]
Raw data (loadavg): 0.87 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 3559 0 0 0 986 10 0 0 25 0 1 0 808482910 27009024 3536 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 6594 3536 1111 63 0 6531 0
vsize: 26376
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 6546 0 0 0 1981 16 0 0 25 0 1 0 808482910 39247872 6523 4294967295 134512640 134714540 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9582 6523 1111 63 0 9519 0
vsize: 38328
[startup+30.0004 s]
Raw data (loadavg): 0.91 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 9544 0 0 0 2976 20 0 0 25 0 1 0 808482910 51478528 9521 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 12568 9521 1111 63 0 12505 0
vsize: 50272
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 12552 0 0 0 3972 25 0 0 25 0 1 0 808482910 63873024 12529 4294967295 134512640 134714540 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 15594 12529 1111 63 0 15531 0
vsize: 62376
[startup+50.0027 s]
Raw data (loadavg): 0.93 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 15559 0 0 0 4965 31 0 0 25 0 1 0 808482910 76115968 15536 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18583 15536 1111 63 0 18520 0
vsize: 74332
[startup+60.0022 s]
Raw data (loadavg): 0.94 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 18566 0 0 0 5961 36 0 0 25 0 1 0 808482910 88506368 18543 4294967295 134512640 134714540 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 21608 18543 1111 63 0 21545 0
vsize: 86432
[startup+70.0025 s]
Raw data (loadavg): 0.95 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 21574 0 0 0 6956 41 0 0 25 0 1 0 808482910 100749312 21551 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 24597 21551 1111 63 0 24534 0
vsize: 98388
[startup+80.0031 s]
Raw data (loadavg): 0.96 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 24575 0 0 0 7950 48 0 0 25 0 1 0 808482910 113143808 24552 4294967295 134512640 134714540 3221221776 3221220004 1077414435 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 27623 24552 1111 63 0 27560 0
vsize: 110492
[startup+90.003 s]
Raw data (loadavg): 0.96 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 27589 0 0 0 8944 54 0 0 25 0 1 0 808482910 125386752 27566 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 30612 27566 1111 63 0 30549 0
vsize: 122448
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 30598 0 0 0 9938 59 0 0 25 0 1 0 808482910 137777152 30575 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 33637 30575 1111 63 0 33574 0
vsize: 134548
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 33600 0 0 0 10932 66 0 0 25 0 1 0 808482910 150016000 33577 4294967295 134512640 134714540 3221221776 3221220004 1077414358 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 36625 33577 1111 63 0 36562 0
vsize: 146500
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 36601 0 0 0 11927 71 0 0 25 0 1 0 808482910 162410496 36578 4294967295 134512640 134714540 3221221776 3221220004 1077414385 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 39651 36578 1111 63 0 39588 0
vsize: 158604
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 39597 0 0 0 12921 77 0 0 25 0 1 0 808482910 174653440 39574 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 42640 39574 1111 63 0 42577 0
vsize: 170560
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 42593 0 0 0 13917 82 0 0 25 0 1 0 808482910 186896384 42570 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 45629 42570 1111 63 0 45566 0
vsize: 182516
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 45594 0 0 0 14912 87 0 0 25 0 1 0 808482910 199139328 45571 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 48618 45571 1111 63 0 48555 0
vsize: 194472
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 48590 0 0 0 15906 93 0 0 25 0 1 0 808482910 211382272 48567 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 51607 48567 1111 63 0 51544 0
vsize: 206428
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 51590 0 0 0 16901 98 0 0 25 0 1 0 808482910 223797248 51567 4294967295 134512640 134714540 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 54638 51567 1111 63 0 54575 0
vsize: 218552
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 54579 0 0 0 17895 104 0 0 25 0 1 0 808482910 236040192 54556 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 57627 54556 1111 63 0 57564 0
vsize: 230508
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 57571 0 0 0 18890 109 0 0 25 0 1 0 808482910 248283136 57548 4294967295 134512640 134714540 3221221776 3221220004 1077414376 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 60616 57548 1111 63 0 60553 0
vsize: 242464
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 60540 0 0 0 19884 116 0 0 25 0 1 0 808482910 260374528 60517 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 63568 60517 1111 63 0 63505 0
vsize: 254272
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 63556 0 0 0 20879 121 0 0 25 0 1 0 808482910 272764928 63533 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 66593 63533 1111 63 0 66530 0
vsize: 266372
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 66539 0 0 0 21875 125 0 0 25 0 1 0 808482910 285011968 66516 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 69583 66516 1111 63 0 69520 0
vsize: 278332
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 69559 0 0 0 22869 131 0 0 25 0 1 0 808482910 297402368 69536 4294967295 134512640 134714540 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 72608 69536 1111 63 0 72545 0
vsize: 290432
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 72531 0 0 0 23864 136 0 0 25 0 1 0 808482910 309497856 72508 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 75561 72508 1111 63 0 75498 0
vsize: 302244
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 75552 0 0 0 24858 142 0 0 25 0 1 0 808482910 321888256 75529 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 78586 75529 1111 63 0 78523 0
vsize: 314344
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 78542 0 0 0 25854 146 0 0 25 0 1 0 808482910 334135296 78519 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 81576 78519 1111 63 0 81513 0
vsize: 326304
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 81556 0 0 0 26850 150 0 0 25 0 1 0 808482910 346525696 81533 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 84601 81533 1111 63 0 84538 0
vsize: 338404
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 84540 0 0 0 27844 156 0 0 25 0 1 0 808482910 358768640 84517 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 87590 84517 1111 63 0 87527 0
vsize: 350360
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 87555 0 0 0 28839 162 0 0 25 0 1 0 808482910 371007488 87532 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 90578 87532 1111 63 0 90515 0
vsize: 362312
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 90550 0 0 0 29833 168 0 0 25 0 1 0 808482910 383250432 90527 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 93567 90527 1111 63 0 93504 0
vsize: 374268
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 93545 0 0 0 30828 174 0 0 25 0 1 0 808482910 395644928 93522 4294967295 134512640 134714540 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 96593 93522 1111 63 0 96530 0
vsize: 386372
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 96528 0 0 0 31823 179 0 0 25 0 1 0 808482910 407740416 96505 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 99546 96505 1111 63 0 99483 0
vsize: 398184
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 99554 0 0 0 32818 184 0 0 25 0 1 0 808482910 420347904 99531 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 102624 99531 1111 63 0 102561 0
vsize: 410496
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 102544 0 0 0 33812 190 0 0 25 0 1 0 808482910 432590848 102521 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 105613 102521 1111 63 0 105550 0
vsize: 422452
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 105528 0 0 0 34807 195 0 0 25 0 1 0 808482910 444833792 105505 4294967295 134512640 134714540 3221221776 3221220432 134527928 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 108602 105505 1111 63 0 108539 0
vsize: 434408
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 108507 0 0 0 35803 200 0 0 25 0 1 0 808482910 456929280 108484 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 111555 108484 1111 63 0 111492 0
vsize: 446220
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 111521 0 0 0 36797 205 0 0 25 0 1 0 808482910 469323776 111498 4294967295 134512640 134714540 3221221776 3221220004 1077414370 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 114581 111498 1111 63 0 114518 0
vsize: 458324
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 114534 0 0 0 37791 212 0 0 25 0 1 0 808482910 481714176 114511 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 117606 114511 1111 63 0 117543 0
vsize: 470424
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 117518 0 0 0 38786 217 0 0 25 0 1 0 808482910 493805568 117495 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 120558 117495 1111 63 0 120495 0
vsize: 482232
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 120507 0 0 0 39781 222 0 0 25 0 1 0 808482910 506048512 120484 4294967295 134512640 134714540 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 123547 120484 1111 63 0 123484 0
vsize: 494188
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 123523 0 0 0 40776 228 0 0 25 0 1 0 808482910 518438912 123500 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 126572 123500 1111 63 0 126509 0
vsize: 506288
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 126548 0 0 0 41771 232 0 0 25 0 1 0 808482910 530833408 126525 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 129598 126525 1111 63 0 129535 0
vsize: 518392
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 129515 0 0 0 42766 237 0 0 25 0 1 0 808482910 542928896 129492 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 132551 129492 1111 63 0 132488 0
vsize: 530204
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 132498 0 0 0 43762 242 0 0 25 0 1 0 808482910 555171840 132475 4294967295 134512640 134714540 3221221776 3221220004 1077414395 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 135540 132475 1111 63 0 135477 0
vsize: 542160
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 135514 0 0 0 44756 248 0 0 25 0 1 0 808482910 567566336 135491 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 138566 135491 1111 63 0 138503 0
vsize: 554264
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 138515 0 0 0 45751 253 0 0 25 0 1 0 808482910 579809280 138492 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 141555 138492 1111 63 0 141492 0
vsize: 566220
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 141506 0 0 0 46746 258 0 0 25 0 1 0 808482910 592044032 141483 4294967295 134512640 134714540 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 144542 141483 1111 63 0 144479 0
vsize: 578168
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 144488 0 0 0 47740 264 0 0 25 0 1 0 808482910 604291072 144465 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 147532 144465 1111 63 0 147469 0
vsize: 590128
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 147540 0 0 0 48735 270 0 0 25 0 1 0 808482910 616833024 147517 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 150594 147517 1111 63 0 150531 0
vsize: 602376
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 150565 0 0 0 49730 275 0 0 25 0 1 0 808482910 629223424 150542 4294967295 134512640 134714540 3221221776 3221220004 1077414408 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 153619 150542 1111 63 0 153556 0
vsize: 614476
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 153568 0 0 0 50726 279 0 0 25 0 1 0 808482910 641466368 153545 4294967295 134512640 134714540 3221221776 3221220128 134567410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 156608 153546 1111 63 0 156545 0
vsize: 626432
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 156576 0 0 0 51720 285 0 0 25 0 1 0 808482910 653860864 156553 4294967295 134512640 134714540 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 159634 156553 1111 63 0 159571 0
vsize: 638536
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 159603 0 0 0 52716 290 0 0 25 0 1 0 808482910 666251264 159580 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 162659 159580 1111 63 0 162596 0
vsize: 650636
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 162647 0 0 0 53711 295 0 0 25 0 1 0 808482910 678645760 162624 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 165685 162624 1111 63 0 165622 0
vsize: 662740
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 165711 0 0 0 54705 301 0 0 25 0 1 0 808482910 691187712 165688 4294967295 134512640 134714540 3221221776 3221220432 134527946 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 168747 165688 1111 63 0 168684 0
vsize: 674988
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 168773 0 0 0 55701 306 0 0 25 0 1 0 808482910 703729664 168750 4294967295 134512640 134714540 3221221776 3221220432 134527946 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 171809 168750 1111 63 0 171746 0
vsize: 687236
[startup+570.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 171825 0 0 0 56696 310 0 0 25 0 1 0 808482910 716271616 171802 4294967295 134512640 134714540 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 174871 171802 1111 63 0 174808 0
vsize: 699484
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 174869 0 0 0 57692 315 0 0 25 0 1 0 808482910 728666112 174846 4294967295 134512640 134714540 3221221776 3221220004 1077414382 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 177897 174846 1111 63 0 177834 0
vsize: 711588
[startup+590.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 177915 0 0 0 58688 319 0 0 25 0 1 0 808482910 741203968 177892 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 180958 177892 1111 63 0 180895 0
vsize: 723832
[startup+600.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 180995 0 0 0 59683 324 0 0 25 0 1 0 808482910 753745920 180972 4294967295 134512640 134714540 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 184020 180972 1111 63 0 183957 0
vsize: 736080
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 184101 0 0 0 60678 329 0 0 25 0 1 0 808482910 766439424 184078 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 187119 184078 1111 63 0 187056 0
vsize: 748476
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 187181 0 0 0 61673 335 0 0 25 0 1 0 808482910 779128832 187158 4294967295 134512640 134714540 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 190217 187158 1111 63 0 190154 0
vsize: 760868
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 190316 0 0 0 62667 340 0 0 25 0 1 0 808482910 791969792 190293 4294967295 134512640 134714540 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 193352 190293 1111 63 0 193289 0
vsize: 773408
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 193560 0 0 0 63662 346 0 0 25 0 1 0 808482910 805257216 193537 4294967295 134512640 134714540 3221221776 3221220004 1077414360 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 196596 193537 1111 63 0 196533 0
vsize: 786384
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 196838 0 0 0 64656 352 0 0 25 0 1 0 808482910 818909184 196815 4294967295 134512640 134714540 3221221776 3221220108 1077399562 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 199929 196821 1111 63 0 199866 0
vsize: 799716
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 200162 0 0 0 65650 357 0 0 25 0 1 0 808482910 832491520 200139 4294967295 134512640 134714540 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 203245 200139 1111 63 0 203182 0
vsize: 812980
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 203473 0 0 0 66642 363 0 0 25 0 1 0 808482910 846077952 203226 4294967295 134512640 134714540 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 206562 203226 1111 63 0 206499 0
vsize: 826248
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 206803 0 0 0 67634 370 0 0 25 0 1 0 808482910 859664384 206238 4294967295 134512640 134714540 3221221776 3221220004 1077414408 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 209879 206238 1111 63 0 209816 0
vsize: 839516
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 210226 0 0 0 68624 380 0 0 25 0 1 0 808482910 873701376 209309 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 213306 209309 1111 63 0 213243 0
vsize: 853224
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 213696 0 0 0 69614 388 0 0 25 0 1 0 808482910 887885824 212207 4294967295 134512640 134714540 3221221776 3221220432 134527946 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 216769 212207 1111 63 0 216706 0
vsize: 867076
[startup+710.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 217055 0 0 0 70606 396 0 0 25 0 1 0 808482910 901767168 215307 4294967295 134512640 134714540 3221221776 3221220004 1077414408 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 220158 215307 1111 63 0 220095 0
vsize: 880632
[startup+720.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 220473 0 0 0 71595 406 0 0 25 0 1 0 808482910 915656704 218373 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 223549 218373 1111 63 0 223486 0
vsize: 894196
[startup+730.027 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 0 223880 0 0 0 72584 416 0 0 25 0 1 0 808482910 929689600 221172 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 226975 221172 1111 63 0 226912 0
vsize: 907900
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.96 2/55 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 1028 227325 0 3 0 73567 431 0 0 25 0 1 0 808482910 0 0 4294967295 0 0 0 0 0 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
[startup+740.395 s]
Raw data (loadavg): 0.99 0.97 0.96 1/54 17714
Raw data (stat): 17714 (bsolo_mis) R 17713 7876 7672 0 -1 1028 227325 0 3 0 73567 431 0 0 25 0 1 0 808482910 0 0 4294967295 0 0 0 0 0 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 740.394
CPU time (s): 740.35
CPU user time (s): 735.676
CPU system time (s): 4.67429
CPU usage (%): 99.9941
Max. virtual memory (Kb): 907900
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####