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-20-10/MIPLIB/miplib3/normalized-mps-v2-20-10-fast0507.opb
MD5SUM	2854384016ebafb26c8bfb47f81aee87
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	324
Optimality of the best value was proved	NO
Number of terms in the objective function	63009
Biggest coefficient in the objective function	2
Number of bits for the biggest coefficient in the objective function	2
Sum of the numbers in the objective function	122425
Number of bits of the sum of numbers in the objective function	17
Biggest number in a constraint	2
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	122425
Number of bits of the biggest sum of numbers	17
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.16
Number of variables	63009
Total number of constraints	63516
Number of constraints which are clauses	507
Number of constraints which are cardinality constraints (but not clauses)	63009
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	7753

Trace number 28317

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-05-25 01:48:20 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13328 boxname=wulflinc7 idbench=1026 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  2854384016ebafb26c8bfb47f81aee87  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-fast0507.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-fast0507.opb
IDLAUNCH: 13328
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        906404 kB
Buffers:          5976 kB
Cached:         101892 kB
SwapCached:        524 kB
Active:          41876 kB
Inactive:        68108 kB
HighTotal:      131008 kB
HighFree:        59052 kB
LowTotal:       903652 kB
LowFree:        847352 kB
SwapTotal:     2097136 kB
SwapFree:      2095780 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5476 kB
Slab:            12452 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 01:54:46 (client local time) WITH STATUS 0 IN 385.788 SECONDS
stats: 13328 7 385.788 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.86 0.93 0.90 1/54 3601
Raw data (stat): 3601 (runsolver) D 3600 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 776826150 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 4584 0 0 0 987 10 0 0 25 0 1 0 776826150 31637504 4562 4294967295 134512640 134714540 3221224592 3221222820 1077414426 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 7724 4562 1111 63 0 7661 0
vsize: 30896
[startup+20.0003 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 8731 0 0 0 1980 17 0 0 25 0 1 0 776826150 48496640 8709 4294967295 134512640 134714540 3221224592 3221222820 1077414433 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11877 8712 1111 63 0 11814 0
vsize: 47360
[startup+30.0013 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 12921 0 0 0 2974 24 0 0 25 0 1 0 776826150 65667072 12899 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 16032 12899 1111 63 0 15969 0
vsize: 64128
[startup+40.0009 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 17199 0 0 0 3966 32 0 0 25 0 1 0 776826150 83283968 17177 4294967295 134512640 134714540 3221224592 3221222820 1077414395 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20333 17177 1111 63 0 20270 0
vsize: 81332
[startup+50.0017 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 21603 0 0 0 4958 40 0 0 25 0 1 0 776826150 101347328 21581 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 24743 21581 1111 63 0 24680 0
vsize: 98972
[startup+60.0012 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 26123 0 0 0 5951 47 0 0 25 0 1 0 776826150 119857152 26101 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 29262 26101 1111 63 0 29199 0
vsize: 117048
[startup+70.002 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 30766 0 0 0 6943 56 0 0 25 0 1 0 776826150 138821632 30744 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 33892 30744 1111 63 0 33829 0
vsize: 135568
[startup+80.0031 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 35530 0 0 0 7934 64 0 0 25 0 1 0 776826150 158375936 35508 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 38666 35508 1111 63 0 38603 0
vsize: 154664
[startup+90.0031 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 40435 0 0 0 8926 73 0 0 25 0 1 0 776826150 178384896 40413 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 43551 40413 1111 63 0 43488 0
vsize: 174204
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 45424 0 0 0 9918 81 0 0 25 0 1 0 776826150 198840320 45402 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 48545 45402 1111 63 0 48482 0
vsize: 194180
[startup+110.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 50483 0 0 0 10911 88 0 0 25 0 1 0 776826150 219615232 50461 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 53617 50461 1111 63 0 53554 0
vsize: 214468
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 55612 0 0 0 11903 96 0 0 25 0 1 0 776826150 240668672 55590 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 58757 55590 1111 63 0 58694 0
vsize: 235028
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 60814 0 0 0 12894 106 0 0 25 0 1 0 776826150 261869568 60792 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 63933 60792 1111 63 0 63870 0
vsize: 255732
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 66125 0 0 0 13885 116 0 0 25 0 1 0 776826150 283668480 66103 4294967295 134512640 134714540 3221224592 3221222820 1077414435 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 69255 66103 1111 63 0 69192 0
vsize: 277020
[startup+150.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 71479 0 0 0 14876 124 0 0 25 0 1 0 776826150 305614848 71457 4294967295 134512640 134714540 3221224592 3221222820 1077414433 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 74613 71457 1111 63 0 74550 0
vsize: 298452
[startup+160.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 76888 0 0 0 15867 133 0 0 25 0 1 0 776826150 327708672 76866 4294967295 134512640 134714540 3221224592 3221222820 1077414422 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 80007 76866 1111 63 0 79944 0
vsize: 320028
[startup+170.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 82371 0 0 0 16860 141 0 0 25 0 1 0 776826150 350261248 82349 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 85513 82349 1111 63 0 85450 0
vsize: 342052
[startup+180.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 87924 0 0 0 17852 149 0 0 25 0 1 0 776826150 372953088 87902 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 91053 87902 1111 63 0 90990 0
vsize: 364212
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 93574 0 0 0 18842 159 0 0 25 0 1 0 776826150 396091392 93552 4294967295 134512640 134714540 3221224592 3221222820 1077414426 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 96702 93552 1111 63 0 96639 0
vsize: 386808
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 99317 0 0 0 19833 168 0 0 25 0 1 0 776826150 419753984 99295 4294967295 134512640 134714540 3221224592 3221222820 1077414395 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 102479 99295 1111 63 0 102416 0
vsize: 409916
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 105109 0 0 0 20823 179 0 0 25 0 1 0 776826150 443494400 105087 4294967295 134512640 134714540 3221224592 3221222928 134566780 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108275 105087 1111 63 0 108212 0
vsize: 433100
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 110997 0 0 0 21811 190 0 0 25 0 1 0 776826150 467529728 110975 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 114143 110975 1111 63 0 114080 0
vsize: 456572
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 116995 0 0 0 22801 201 0 0 25 0 1 0 776826150 492163072 116973 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 120157 116973 1111 63 0 120094 0
vsize: 480628
[startup+240.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 123152 0 0 0 23791 211 0 0 25 0 1 0 776826150 517246976 123130 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 126281 123130 1111 63 0 126218 0
vsize: 505124
[startup+250.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 129369 0 0 0 24781 222 0 0 25 0 1 0 776826150 542777344 129347 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 132514 129347 1111 63 0 132451 0
vsize: 530056
[startup+260.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 135683 0 0 0 25769 234 0 0 25 0 1 0 776826150 568606720 135661 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 138820 135661 1111 63 0 138757 0
vsize: 555280
[startup+270.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 142106 0 0 0 26759 244 0 0 25 0 1 0 776826150 594882560 142084 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 145235 142084 1111 63 0 145172 0
vsize: 580940
[startup+280.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 148688 0 0 0 27747 256 0 0 25 0 1 0 776826150 621912064 148666 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 151834 148666 1111 63 0 151771 0
vsize: 607336
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 155366 0 0 0 28736 268 0 0 25 0 1 0 776826150 649232384 155344 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 158504 155344 1111 63 0 158441 0
vsize: 634016
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 162228 0 0 0 29725 279 0 0 25 0 1 0 776826150 677302272 162206 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 165357 162206 1111 63 0 165294 0
vsize: 661428
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 169306 0 0 0 30715 289 0 0 25 0 1 0 776826150 706265088 169284 4294967295 134512640 134714540 3221224592 3221222820 1077414383 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 172428 169284 1111 63 0 172365 0
vsize: 689712
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 176489 0 0 0 31704 300 0 0 25 0 1 0 776826150 735678464 176467 4294967295 134512640 134714540 3221224592 3221222820 1077414383 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 179609 176467 1111 63 0 179546 0
vsize: 718436
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 183838 0 0 0 32691 313 0 0 25 0 1 0 776826150 765837312 183816 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 186972 183816 1111 63 0 186909 0
vsize: 747888
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 191233 0 0 0 33679 325 0 0 25 0 1 0 776826150 796151808 191211 4294967295 134512640 134714540 3221224592 3221222924 1077399562 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 194373 191211 1111 63 0 194310 0
vsize: 777492
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 198739 0 0 0 34668 337 0 0 25 0 1 0 776826150 827121664 198717 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 201934 198717 1111 63 0 201871 0
vsize: 807736
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 206450 0 0 0 35653 352 0 0 25 0 1 0 776826150 858619904 206428 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 209624 206428 1111 63 0 209561 0
vsize: 838496
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 214425 0 0 0 36640 366 0 0 25 0 1 0 776826150 891318272 214403 4294967295 134512640 134714540 3221224592 3221222820 1077414426 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 217607 214403 1111 63 0 217544 0
vsize: 870428
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 222634 0 0 0 37625 380 0 0 25 0 1 0 776826150 924913664 222612 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 225809 222612 1111 63 0 225746 0
vsize: 903236
[startup+385.746 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 3601
Raw data (stat): 3601 (bsolo_mis) R 3600 24300 24299 0 -1 0 222634 0 0 0 37625 380 0 0 25 0 1 0 776826150 924913664 222612 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 225809 222612 1111 63 0 225746 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 385.745
CPU time (s): 385.788
CPU user time (s): 381.466
CPU system time (s): 4.32234
CPU usage (%): 100.011
Max. virtual memory (Kb): 903236
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####