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/miplib3/normalized-mps-v2-13-7-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.18
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 25686

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-21 17:37:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18318 boxname=wulflinc31 idbench=1410 idsolver=1 numberseed=0
MD5SUM SOLVER: e973bb179fd0e01ec8c7277096f1c3ef  /oldhome/oroussel/solvers/bsolo_lpr
MD5SUM BENCH:  2854384016ebafb26c8bfb47f81aee87  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-fast0507.opb
REAL COMMAND:  bsolo_lpr /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-fast0507.opb
IDLAUNCH: 18318
/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:        857096 kB
Buffers:         29580 kB
Cached:         126968 kB
SwapCached:       1076 kB
Active:          96532 kB
Inactive:        62352 kB
HighTotal:      131008 kB
HighFree:        35308 kB
LowTotal:       903652 kB
LowFree:        821788 kB
SwapTotal:     2097892 kB
SwapFree:      2095984 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5356 kB
Slab:            13148 kB
Committed_AS:    63860 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-21 17:43:33 (client local time) WITH STATUS 0 IN 377.434 SECONDS
stats: 18318 7 377.434 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.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (runsolver) R 13987 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 806150013 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.0007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 4748 0 0 0 983 13 0 0 25 0 1 0 806150013 31662080 4671 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 7730 4671 1111 63 0 7667 0
vsize: 30920
[startup+20.0024 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 8919 0 0 0 1975 22 0 0 25 0 1 0 806150013 48820224 8842 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11919 8842 1111 63 0 11856 0
vsize: 47676
[startup+30.0033 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 13152 0 0 0 2968 28 0 0 25 0 1 0 806150013 66113536 13075 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 16141 13075 1111 63 0 16078 0
vsize: 64564
[startup+40.0033 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 17412 0 0 0 3962 35 0 0 25 0 1 0 806150013 83578880 17335 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20405 17335 1111 63 0 20342 0
vsize: 81620
[startup+50.0045 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 21713 0 0 0 4954 43 0 0 25 0 1 0 806150013 101195776 21636 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 24706 21636 1111 63 0 24643 0
vsize: 98824
[startup+60.0051 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 26063 0 0 0 5947 50 0 0 25 0 1 0 806150013 119087104 25986 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 29074 25986 1111 63 0 29011 0
vsize: 116296
[startup+70.0061 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 30456 0 0 0 6939 59 0 0 25 0 1 0 806150013 137003008 30379 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 33448 30379 1111 63 0 33385 0
vsize: 133792
[startup+80.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 34888 0 0 0 7933 65 0 0 25 0 1 0 806150013 155222016 34811 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 37896 34811 1111 63 0 37833 0
vsize: 151584
[startup+90.0069 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 39378 0 0 0 8924 74 0 0 25 0 1 0 806150013 173584384 39301 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 42379 39301 1111 63 0 42316 0
vsize: 169516
[startup+100.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 43983 0 0 0 9916 82 0 0 25 0 1 0 806150013 192393216 43906 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 46971 43906 1111 63 0 46908 0
vsize: 187884
[startup+110.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 48716 0 0 0 10908 91 0 0 25 0 1 0 806150013 211804160 48639 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 51710 48639 1111 63 0 51647 0
vsize: 206840
[startup+120.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 53582 0 0 0 11900 99 0 0 25 0 1 0 806150013 231809024 53505 4294967295 134512640 134714508 3221221776 3221220004 1077414401 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 56594 53505 1111 63 0 56531 0
vsize: 226376
[startup+130.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 58510 0 0 0 12891 108 0 0 25 0 1 0 806150013 251961344 58433 4294967295 134512640 134714508 3221221776 3221220128 134567410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 61514 58433 1111 63 0 61451 0
vsize: 246056
[startup+140.011 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 63537 0 0 0 13883 116 0 0 25 0 1 0 806150013 272568320 63460 4294967295 134512640 134714508 3221221776 3221220004 1077414410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 66545 63460 1111 63 0 66482 0
vsize: 266180
[startup+150.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 68653 0 0 0 14875 125 0 0 25 0 1 0 806150013 293470208 68576 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 71648 68576 1111 63 0 71585 0
vsize: 286592
[startup+160.012 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 73928 0 0 0 15866 134 0 0 25 0 1 0 806150013 315117568 73851 4294967295 134512640 134714508 3221221776 3221220004 1077414433 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 76933 73851 1111 63 0 76870 0
vsize: 307732
[startup+170.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 79374 0 0 0 16858 142 0 0 25 0 1 0 806150013 337371136 79297 4294967295 134512640 134714508 3221221776 3221220004 1077414345 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 82366 79297 1111 63 0 82303 0
vsize: 329464
[startup+180.014 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 84916 0 0 0 17851 149 0 0 25 0 1 0 806150013 360062976 84839 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 87906 84839 1111 63 0 87843 0
vsize: 351624
[startup+190.015 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 90537 0 0 0 18841 160 0 0 25 0 1 0 806150013 383053824 90460 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 93519 90460 1111 63 0 93456 0
vsize: 374076
[startup+200.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 96248 0 0 0 19831 169 0 0 25 0 1 0 806150013 406495232 96171 4294967295 134512640 134714508 3221221776 3221220004 1077414395 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 99242 96171 1111 63 0 99179 0
vsize: 396968
[startup+210.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 102080 0 0 0 20823 177 0 0 25 0 1 0 806150013 430448640 102003 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 105090 102003 1111 63 0 105027 0
vsize: 420360
[startup+220.016 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 108006 0 0 0 21812 189 0 0 25 0 1 0 806150013 454787072 107929 4294967295 134512640 134714508 3221221776 3221220004 1077414383 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 111032 107929 1111 63 0 110969 0
vsize: 444128
[startup+230.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 114058 0 0 0 22804 197 0 0 25 0 1 0 806150013 479571968 113981 4294967295 134512640 134714508 3221221776 3221220004 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 117083 113981 1111 63 0 117020 0
vsize: 468332
[startup+240.017 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 120245 0 0 0 23794 207 0 0 25 0 1 0 806150013 504803328 120168 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 123243 120168 1111 63 0 123180 0
vsize: 492972
[startup+250.018 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 126784 0 0 0 24781 221 0 0 25 0 1 0 806150013 531677184 126707 4294967295 134512640 134714508 3221221776 3221220004 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 129804 126707 1111 63 0 129741 0
vsize: 519216
[startup+260.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 133530 0 0 0 25770 232 0 0 25 0 1 0 806150013 559300608 133453 4294967295 134512640 134714508 3221221776 3221220004 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 136548 133453 1111 63 0 136485 0
vsize: 546192
[startup+270.019 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 140439 0 0 0 26759 243 0 0 25 0 1 0 806150013 587517952 140362 4294967295 134512640 134714508 3221221776 3221220004 1077414410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 143437 140362 1111 63 0 143374 0
vsize: 573748
[startup+280.02 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 147574 0 0 0 27746 257 0 0 25 0 1 0 806150013 616779776 147497 4294967295 134512640 134714508 3221221776 3221220004 1077414399 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 150581 147497 1111 63 0 150518 0
vsize: 602324
[startup+290.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 154794 0 0 0 28733 269 0 0 25 0 1 0 806150013 646344704 154717 4294967295 134512640 134714508 3221221776 3221220004 1077414336 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 157799 154717 1111 63 0 157736 0
vsize: 631196
[startup+300.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 162226 0 0 0 29722 281 0 0 25 0 1 0 806150013 676798464 162149 4294967295 134512640 134714508 3221221776 3221220004 1077414424 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 165234 162149 1111 63 0 165171 0
vsize: 660936
[startup+310.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 169968 0 0 0 30709 294 0 0 25 0 1 0 806150013 708456448 169891 4294967295 134512640 134714508 3221221776 3221220128 134567410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 172963 169891 1111 63 0 172900 0
vsize: 691852
[startup+320.021 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 177839 0 0 0 31696 307 0 0 25 0 1 0 806150013 740700160 177762 4294967295 134512640 134714508 3221221776 3221220004 1077414395 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 180835 177762 1111 63 0 180772 0
vsize: 723340
[startup+330.022 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 186042 0 0 0 32682 321 0 0 25 0 1 0 806150013 774295552 185965 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 189037 185965 1111 63 0 188974 0
vsize: 756148
[startup+340.022 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 194336 0 0 0 33665 339 0 0 25 0 1 0 806150013 808189952 194259 4294967295 134512640 134714508 3221221776 3221220004 1077414410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 197312 194259 1111 63 0 197249 0
vsize: 789248
[startup+350.023 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 202896 0 0 0 34649 354 0 0 25 0 1 0 806150013 843493376 202819 4294967295 134512640 134714508 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 205931 202819 1111 63 0 205868 0
vsize: 823724
[startup+360.024 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 211598 0 0 0 35635 369 0 0 25 0 1 0 806150013 879173632 211521 4294967295 134512640 134714508 3221221776 3221220432 134527946 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 214642 211521 1111 63 0 214579 0
vsize: 858568
[startup+370.024 s]
Raw data (loadavg): 0.99 0.98 0.95 2/55 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 220729 0 0 0 36613 391 0 0 25 0 1 0 806150013 916652032 220172 4294967295 134512640 134714508 3221221776 3221220128 134567410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 223792 220176 1111 63 0 223729 0
vsize: 895168
[startup+377.406 s]
Raw data (loadavg): 0.99 0.98 0.95 1/54 13988
Raw data (stat): 13988 (bsolo_lpr) R 13987 7876 7672 0 -1 0 220729 0 0 0 36613 391 0 0 25 0 1 0 806150013 916652032 220172 4294967295 134512640 134714508 3221221776 3221220128 134567410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 223792 220176 1111 63 0 223729 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 377.405
CPU time (s): 377.434
CPU user time (s): 372.919
CPU system time (s): 4.51431
CPU usage (%): 100.007
Max. virtual memory (Kb): 895168
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####