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-fast0507.opb
MD5SUM	38504d32a17a57a658eee171614b901e
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.19
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 27303

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-05-24 20:56:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17512 boxname=wulflinc18 idbench=1348 idsolver=1 numberseed=0
MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef  /oldhome/oroussel/solvers/bsolo_lpr
MD5SUM BENCH:  38504d32a17a57a658eee171614b901e  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-fast0507.opb
REAL COMMAND:  bsolo_lpr /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-fast0507.opb
IDLAUNCH: 17512
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        722396 kB
Buffers:          1784 kB
Cached:         288624 kB
SwapCached:        836 kB
Active:          36804 kB
Inactive:       256084 kB
HighTotal:      131008 kB
HighFree:        24808 kB
LowTotal:       903652 kB
LowFree:        697588 kB
SwapTotal:     2097892 kB
SwapFree:      2096620 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5660 kB
Slab:            13636 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-24 21:03:16 (client local time) WITH STATUS 0 IN 376.281 SECONDS
stats: 17512 7 376.281 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
#### 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.97 0.96 2/54 25957
Raw data (stat): 25957 (runsolver) R 25956 24172 24171 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 833277047 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0016 s]
Raw data (loadavg): 0.94 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 4781 0 0 0 987 11 0 0 25 0 1 0 833277047 31809536 4705 4294967295 134512640 134714508 3221224592 3221222820 1077414358 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7766 4705 1111 63 0 7703 0
vsize: 31064
[startup+20.002 s]
Raw data (loadavg): 0.95 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 8988 0 0 0 1979 19 0 0 25 0 1 0 833277047 49115136 8912 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11991 8912 1111 63 0 11928 0
vsize: 47964
[startup+30.0022 s]
Raw data (loadavg): 0.96 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 13263 0 0 0 2970 28 0 0 25 0 1 0 833277047 66555904 13187 4294967295 134512640 134714508 3221224592 3221222820 1077414401 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16249 13187 1111 63 0 16186 0
vsize: 64996
[startup+40.0028 s]
Raw data (loadavg): 0.96 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 17638 0 0 0 3964 34 0 0 25 0 1 0 833277047 84471808 17562 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 20623 17562 1111 63 0 20560 0
vsize: 82492
[startup+50.0027 s]
Raw data (loadavg): 0.97 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 22121 0 0 0 4956 42 0 0 25 0 1 0 833277047 102834176 22045 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 25106 22045 1111 63 0 25043 0
vsize: 100424
[startup+60.0029 s]
Raw data (loadavg): 0.97 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 26734 0 0 0 5949 49 0 0 25 0 1 0 833277047 121769984 26658 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 29729 26658 1111 63 0 29666 0
vsize: 118916
[startup+70.0026 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 31461 0 0 0 6941 58 0 0 25 0 1 0 833277047 141176832 31385 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 34467 31385 1111 63 0 34404 0
vsize: 137868
[startup+80.0025 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 36317 0 0 0 7932 67 0 0 25 0 1 0 833277047 161038336 36241 4294967295 134512640 134714508 3221224592 3221222820 1077414358 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 39316 36241 1111 63 0 39253 0
vsize: 157264
[startup+90.0027 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 41307 0 0 0 8923 76 0 0 25 0 1 0 833277047 181493760 41231 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 44310 41231 1111 63 0 44247 0
vsize: 177240
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 46356 0 0 0 9915 84 0 0 25 0 1 0 833277047 202096640 46280 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 49340 46280 1111 63 0 49277 0
vsize: 197360
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 51476 0 0 0 10908 92 0 0 25 0 1 0 833277047 223145984 51400 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 54479 51400 1111 63 0 54416 0
vsize: 217916
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 56654 0 0 0 11899 101 0 0 25 0 1 0 833277047 244346880 56578 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 59655 56578 1111 63 0 59592 0
vsize: 238620
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 61917 0 0 0 12890 109 0 0 25 0 1 0 833277047 265846784 61841 4294967295 134512640 134714508 3221224592 3221222820 1077414395 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 64904 61841 1111 63 0 64841 0
vsize: 259616
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 67373 0 0 0 13881 119 0 0 25 0 1 0 833277047 288239616 67297 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 70371 67297 1111 63 0 70308 0
vsize: 281484
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 72897 0 0 0 14872 128 0 0 25 0 1 0 833277047 310935552 72821 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 75912 72821 1111 63 0 75849 0
vsize: 303648
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 78501 0 0 0 15862 138 0 0 25 0 1 0 833277047 333783040 78425 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 81490 78425 1111 63 0 81427 0
vsize: 325960
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 84170 0 0 0 16851 149 0 0 25 0 1 0 833277047 357068800 84094 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 87175 84094 1111 63 0 87112 0
vsize: 348700
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.96 2/54 25957
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 89926 0 0 0 17840 161 0 0 25 0 1 0 833277047 380661760 89850 4294967295 134512640 134714508 3221224592 3221222820 1077414432 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 92935 89850 1111 63 0 92872 0
vsize: 371740
[startup+190.006 s]
Raw data (loadavg): 1.07 0.99 0.96 3/57 26005
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 95806 0 0 0 18831 170 0 0 25 0 1 0 833277047 404697088 95730 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 98803 95730 1111 63 0 98740 0
vsize: 395212
[startup+200.006 s]
Raw data (loadavg): 1.06 0.99 0.96 2/54 26010
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 101773 0 0 0 19820 181 0 0 25 0 1 0 833277047 429252608 101697 4294967295 134512640 134714508 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 104798 101697 1111 63 0 104735 0
vsize: 419192
[startup+210.006 s]
Raw data (loadavg): 1.05 0.99 0.96 2/54 26010
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 107819 0 0 0 20810 191 0 0 25 0 1 0 833277047 454037504 107743 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 110849 107743 1111 63 0 110786 0
vsize: 443396
[startup+220.005 s]
Raw data (loadavg): 1.04 0.99 0.96 2/54 26010
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 114006 0 0 0 21798 203 0 0 25 0 1 0 833277047 479268864 113930 4294967295 134512640 134714508 3221224592 3221222820 1077414401 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 117009 113930 1111 63 0 116946 0
vsize: 468036
[startup+230.005 s]
Raw data (loadavg): 1.04 0.99 0.96 2/54 26010
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 120332 0 0 0 22786 216 0 0 25 0 1 0 833277047 505249792 120256 4294967295 134512640 134714508 3221224592 3221221308 1077191238 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 123352 120256 1111 63 0 123289 0
vsize: 493408
[startup+240.005 s]
Raw data (loadavg): 1.03 0.99 0.96 2/54 26010
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 126811 0 0 0 23775 227 0 0 25 0 1 0 833277047 531820544 126735 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 129839 126735 1111 63 0 129776 0
vsize: 519356
[startup+250.005 s]
Raw data (loadavg): 1.03 0.99 0.96 2/54 26010
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 133326 0 0 0 24765 236 0 0 25 0 1 0 833277047 558403584 133250 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 136329 133250 1111 63 0 136266 0
vsize: 545316
[startup+260.009 s]
Raw data (loadavg): 1.02 0.99 0.96 2/54 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 139925 0 0 0 25754 249 0 0 25 0 1 0 833277047 585424896 139849 4294967295 134512640 134714508 3221224592 3221222820 1077414351 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 142926 139849 1111 63 0 142863 0
vsize: 571704
[startup+270.009 s]
Raw data (loadavg): 1.02 0.99 0.96 2/54 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 146665 0 0 0 26742 261 0 0 25 0 1 0 833277047 613044224 146589 4294967295 134512640 134714508 3221224592 3221222820 1077414385 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 149669 146589 1111 63 0 149606 0
vsize: 598676
[startup+280.009 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 153484 0 0 0 27730 273 0 0 25 0 1 0 833277047 640966656 153408 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 156486 153408 1111 63 0 156423 0
vsize: 625944
[startup+290.01 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 160467 0 0 0 28719 284 0 0 25 0 1 0 833277047 669634560 160391 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 163485 160391 1111 63 0 163422 0
vsize: 653940
[startup+300.01 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 167668 0 0 0 29706 297 0 0 25 0 1 0 833277047 699047936 167592 4294967295 134512640 134714508 3221224592 3221222820 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 170666 167592 1111 63 0 170603 0
vsize: 682664
[startup+310.01 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 174991 0 0 0 30693 310 0 0 25 0 1 0 833277047 729055232 174915 4294967295 134512640 134714508 3221224592 3221222820 1077414433 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 177992 174915 1111 63 0 177929 0
vsize: 711968
[startup+320.01 s]
Raw data (loadavg): 1.01 0.99 0.96 2/54 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 182453 0 0 0 31680 322 0 0 25 0 1 0 833277047 759664640 182377 4294967295 134512640 134714508 3221224592 3221222820 1077414382 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 185465 182377 1111 63 0 185402 0
vsize: 741860
[startup+330.01 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 190079 0 0 0 32661 337 0 0 25 0 1 0 833277047 790863872 190003 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 193082 190003 1111 63 0 193019 0
vsize: 772328
[startup+340.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 197890 0 0 0 33646 353 0 0 25 0 1 0 833277047 823033856 197814 4294967295 134512640 134714508 3221224592 3221222820 1077414433 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 200936 197814 1111 63 0 200873 0
vsize: 803744
[startup+350.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 205813 0 0 0 34631 369 0 0 25 0 1 0 833277047 855576576 205639 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 208881 205639 1111 63 0 208818 0
vsize: 835524
[startup+360.021 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 214001 0 0 0 35612 388 0 0 25 0 1 0 833277047 889024512 213380 4294967295 134512640 134714508 3221224592 3221222820 1077414385 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 217047 213380 1111 63 0 216984 0
vsize: 868188
[startup+370.023 s]
Raw data (loadavg): 1.00 0.99 0.96 2/54 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 222332 0 2 0 36592 407 0 0 25 0 1 0 833277047 923213824 220723 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 225394 220723 1111 63 0 225331 0
vsize: 901576
[startup+376.32 s]
Raw data (loadavg): 1.00 0.99 0.96 1/53 26012
Raw data (stat): 25957 (bsolo_lpr) R 25956 24172 24171 0 -1 0 222332 0 2 0 36592 407 0 0 25 0 1 0 833277047 923213824 220723 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 225394 220723 1111 63 0 225331 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 376.319
CPU time (s): 376.281
CPU user time (s): 371.668
CPU system time (s): 4.6123
CPU usage (%): 99.9899
Max. virtual memory (Kb): 901576
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####