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-nw04.opb
MD5SUM	a5c401bba5afccf02c7b40cb1c595b15
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	30407
Optimality of the best value was proved	NO
Number of terms in the objective function	87482
Biggest coefficient in the objective function	5220
Number of bits for the biggest coefficient in the objective function	13
Sum of the numbers in the objective function	120189580
Number of bits of the sum of numbers in the objective function	27
Biggest number in a constraint	5220
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	120189580
Number of bits of the biggest sum of numbers	27
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1192.4
Number of variables	87482
Total number of constraints	87518
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	87518
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	42032
Trace number 25634

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-21 09:26:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18671 boxname=wulflinc31 idbench=1437 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  a5c401bba5afccf02c7b40cb1c595b15  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-nw04.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-nw04.opb
IDLAUNCH: 18671
/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:        526952 kB
Buffers:         35556 kB
Cached:         450764 kB
SwapCached:       1172 kB
Active:         337856 kB
Inactive:       150892 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        526700 kB
SwapTotal:     2097892 kB
SwapFree:      2095980 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5356 kB
Slab:            13348 kB
Committed_AS:    63860 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-21 09:41:24 (client local time) WITH STATUS 0 IN 878.685 SECONDS
stats: 18671 7 878.685 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.98 1.00 0.97 2/55 8573
Raw data (stat): 8573 (runsolver) R 8572 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 803206590 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.98 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 3187 0 0 0 987 10 0 0 25 0 1 0 803206590 25214976 3164 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 6156 3164 1111 63 0 6093 0
vsize: 24624
[startup+20.0013 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 5752 0 0 0 1982 15 0 0 25 0 1 0 803206590 35819520 5729 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8745 5729 1111 63 0 8682 0
vsize: 34980
[startup+30.0012 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 8318 0 0 0 2978 19 0 0 25 0 1 0 803206590 46256128 8295 4294967295 134512640 134714540 3221221792 3221220020 1077414433 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11293 8295 1111 63 0 11230 0
vsize: 45172
[startup+40.0015 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 10876 0 0 0 3973 24 0 0 25 0 1 0 803206590 56709120 10853 4294967295 134512640 134714540 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13845 10853 1111 63 0 13782 0
vsize: 55380
[startup+50.002 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 13462 0 0 0 4968 29 0 0 25 0 1 0 803206590 67305472 13439 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 16432 13439 1111 63 0 16369 0
vsize: 65728
[startup+60.0023 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 16052 0 0 0 5963 34 0 0 25 0 1 0 803206590 77910016 16029 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19021 16029 1111 63 0 18958 0
vsize: 76084
[startup+70.0022 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 18646 0 0 0 6958 39 0 0 25 0 1 0 803206590 88506368 18623 4294967295 134512640 134714540 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 21608 18623 1111 63 0 21545 0
vsize: 86432
[startup+80.0028 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 21240 0 0 0 7953 45 0 0 25 0 1 0 803206590 99258368 21217 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 24233 21217 1111 63 0 24170 0
vsize: 96932
[startup+90.0031 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 23840 0 0 0 8948 50 0 0 25 0 1 0 803206590 109858816 23817 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 26821 23817 1111 63 0 26758 0
vsize: 107284
[startup+100.004 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 26448 0 0 0 9944 54 0 0 25 0 1 0 803206590 120610816 26425 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 29446 26425 1111 63 0 29383 0
vsize: 117784
[startup+110.005 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 29024 0 0 0 10939 59 0 0 25 0 1 0 803206590 131055616 29001 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 31996 29001 1111 63 0 31933 0
vsize: 127984
[startup+120.005 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 31620 0 0 0 11934 64 0 0 25 0 1 0 803206590 141660160 31597 4294967295 134512640 134714540 3221221792 3221220020 1077414395 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 34585 31597 1111 63 0 34522 0
vsize: 138340
[startup+130.006 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 34177 0 0 0 12930 69 0 0 25 0 1 0 803206590 152260608 34154 4294967295 134512640 134714540 3221221792 3221220020 1077414357 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 37173 34154 1111 63 0 37110 0
vsize: 148692
[startup+140.005 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 36734 0 0 0 13925 74 0 0 25 0 1 0 803206590 162705408 36711 4294967295 134512640 134714540 3221221792 3221220020 1077414426 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 39723 36711 1111 63 0 39660 0
vsize: 158892
[startup+150.007 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 39288 0 0 0 14921 78 0 0 25 0 1 0 803206590 173162496 39265 4294967295 134512640 134714540 3221221792 3221220020 1077414426 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 42276 39265 1111 63 0 42213 0
vsize: 169104
[startup+160.008 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 41870 0 0 0 15916 83 0 0 25 0 1 0 803206590 183758848 41847 4294967295 134512640 134714540 3221221792 3221220020 1077414401 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 44863 41847 1111 63 0 44800 0
vsize: 179452
[startup+170.007 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 44471 0 0 0 16912 87 0 0 25 0 1 0 803206590 194363392 44448 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 47452 44448 1111 63 0 47389 0
vsize: 189808
[startup+180.008 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 47052 0 0 0 17908 91 0 0 25 0 1 0 803206590 204959744 47029 4294967295 134512640 134714540 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 50039 47029 1111 63 0 49976 0
vsize: 200156
[startup+190.008 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 49749 0 0 0 18903 97 0 0 25 0 1 0 803206590 216031232 49726 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 52742 49726 1111 63 0 52679 0
vsize: 210968
[startup+200.009 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 52381 0 0 0 19898 101 0 0 25 0 1 0 803206590 226787328 52358 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 55368 52358 1111 63 0 55305 0
vsize: 221472
[startup+210.009 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 54986 0 0 0 20894 107 0 0 25 0 1 0 803206590 237531136 54963 4294967295 134512640 134714540 3221221792 3221220020 1077414410 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 57991 54963 1111 63 0 57928 0
vsize: 231964
[startup+220.009 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 57541 0 0 0 21888 112 0 0 25 0 1 0 803206590 247988224 57518 4294967295 134512640 134714540 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 60544 57518 1111 63 0 60481 0
vsize: 242176
[startup+230.01 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 60122 0 0 0 22883 117 0 0 25 0 1 0 803206590 258437120 60099 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 63095 60099 1111 63 0 63032 0
vsize: 252380
[startup+240.01 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 62680 0 0 0 23878 122 0 0 25 0 1 0 803206590 269033472 62657 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 65682 62657 1111 63 0 65619 0
vsize: 262728
[startup+250.011 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 65306 0 0 0 24873 128 0 0 25 0 1 0 803206590 279785472 65283 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 68307 65283 1111 63 0 68244 0
vsize: 273228
[startup+260.012 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 67938 0 0 0 25868 133 0 0 25 0 1 0 803206590 290537472 67915 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 70932 67915 1111 63 0 70869 0
vsize: 283728
[startup+270.012 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 70527 0 0 0 26864 137 0 0 25 0 1 0 803206590 301137920 70504 4294967295 134512640 134714540 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 73520 70504 1111 63 0 73457 0
vsize: 294080
[startup+280.013 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 73053 0 0 0 27860 141 0 0 25 0 1 0 803206590 311435264 73030 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 76034 73030 1111 63 0 75971 0
vsize: 304136
[startup+290.013 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 75655 0 0 0 28857 145 0 0 25 0 1 0 803206590 322039808 75632 4294967295 134512640 134714540 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 78623 75632 1111 63 0 78560 0
vsize: 314492
[startup+300.015 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 78195 0 0 0 29853 149 0 0 25 0 1 0 803206590 332488704 78172 4294967295 134512640 134714540 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 81174 78172 1111 63 0 81111 0
vsize: 324696
[startup+310.016 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 80724 0 0 0 30848 154 0 0 25 0 1 0 803206590 342794240 80701 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 83690 80701 1111 63 0 83627 0
vsize: 334760
[startup+320.015 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 83318 0 0 0 31844 159 0 0 25 0 1 0 803206590 353538048 83295 4294967295 134512640 134714540 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 86313 83295 1111 63 0 86250 0
vsize: 345252
[startup+330.016 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 85939 0 0 0 32839 164 0 0 25 0 1 0 803206590 364142592 85916 4294967295 134512640 134714540 3221221792 3221220020 1077414395 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 88902 85916 1111 63 0 88839 0
vsize: 355608
[startup+340.016 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 88466 0 0 0 33835 168 0 0 25 0 1 0 803206590 374591488 88443 4294967295 134512640 134714540 3221221792 3221220020 1077414435 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 91453 88443 1111 63 0 91390 0
vsize: 365812
[startup+350.017 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 90982 0 0 0 34831 172 0 0 25 0 1 0 803206590 384897024 90959 4294967295 134512640 134714540 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 93969 90959 1111 63 0 93906 0
vsize: 375876
[startup+360.019 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 93557 0 0 0 35826 177 0 0 25 0 1 0 803206590 395345920 93534 4294967295 134512640 134714540 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 96520 93534 1111 63 0 96457 0
vsize: 386080
[startup+370.018 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 96067 0 0 0 36822 181 0 0 25 0 1 0 803206590 405651456 96044 4294967295 134512640 134714540 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 99036 96044 1111 63 0 98973 0
vsize: 396144
[startup+380.019 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 98564 0 0 0 37819 185 0 0 25 0 1 0 803206590 416018432 98541 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 101567 98546 1111 63 0 101504 0
vsize: 406268
[startup+390.019 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 101055 0 0 0 38813 190 0 0 25 0 1 0 803206590 426168320 101032 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 104045 101032 1111 63 0 103982 0
vsize: 416180
[startup+400.02 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 103584 0 0 0 39809 195 0 0 25 0 1 0 803206590 436625408 103561 4294967295 134512640 134714540 3221221792 3221220020 1077414433 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 106598 103561 1111 63 0 106535 0
vsize: 426392
[startup+410.02 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 106045 0 0 0 40804 200 0 0 25 0 1 0 803206590 446623744 106022 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 109039 106022 1111 63 0 108976 0
vsize: 436156
[startup+420.022 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 108756 0 0 0 41800 205 0 0 25 0 1 0 803206590 457826304 108733 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 111774 108733 1111 63 0 111711 0
vsize: 447096
[startup+430.023 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 111289 0 0 0 42796 209 0 0 25 0 1 0 803206590 468123648 111266 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 114288 111266 1111 63 0 114225 0
vsize: 457152
[startup+440.022 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 113902 0 0 0 43792 213 0 0 25 0 1 0 803206590 478875648 113879 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 116913 113879 1111 63 0 116850 0
vsize: 467652
[startup+450.024 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 116480 0 0 0 44787 218 0 0 25 0 1 0 803206590 489324544 116457 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 119464 116457 1111 63 0 119401 0
vsize: 477856
[startup+460.025 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 119002 0 0 0 45783 223 0 0 25 0 1 0 803206590 499781632 118979 4294967295 134512640 134714540 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 122017 118979 1111 63 0 121954 0
vsize: 488068
[startup+470.024 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 121529 0 0 0 46778 228 0 0 25 0 1 0 803206590 510078976 121506 4294967295 134512640 134714540 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 124531 121506 1111 63 0 124468 0
vsize: 498124
[startup+480.025 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 124095 0 0 0 47773 233 0 0 25 0 1 0 803206590 520536064 124072 4294967295 134512640 134714540 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 127084 124072 1111 63 0 127021 0
vsize: 508336
[startup+490.025 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 126627 0 0 0 48768 238 0 0 25 0 1 0 803206590 530980864 126604 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 129634 126604 1111 63 0 129571 0
vsize: 518536
[startup+500.026 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 129152 0 0 0 49764 242 0 0 25 0 1 0 803206590 541286400 129129 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 132150 129129 1111 63 0 132087 0
vsize: 528600
[startup+510.026 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 132006 0 0 0 50759 247 0 0 25 0 1 0 803206590 552927232 131983 4294967295 134512640 134714540 3221221792 3221220020 1077414376 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 134992 131983 1111 63 0 134929 0
vsize: 539968
[startup+520.026 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 134821 0 0 0 51753 252 0 0 25 0 1 0 803206590 564428800 134798 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 137800 134798 1111 63 0 137737 0
vsize: 551200
[startup+530.027 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 137604 0 0 0 52748 256 0 0 25 0 1 0 803206590 575926272 137581 4294967295 134512640 134714540 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 140607 137581 1111 63 0 140544 0
vsize: 562428
[startup+540.027 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 140589 0 0 0 53742 261 0 0 25 0 1 0 803206590 588169216 140566 4294967295 134512640 134714540 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 143596 140566 1111 63 0 143533 0
vsize: 574384
[startup+550.028 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 143310 0 0 0 54736 266 0 0 25 0 1 0 803206590 599216128 143287 4294967295 134512640 134714540 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 146293 143287 1111 63 0 146230 0
vsize: 585172
[startup+560.029 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 145948 0 0 0 55730 271 0 0 25 0 1 0 803206590 610115584 145925 4294967295 134512640 134714540 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 148954 145925 1111 63 0 148891 0
vsize: 595816
[startup+570.029 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 148452 0 0 0 56725 275 0 0 25 0 1 0 803206590 620265472 148429 4294967295 134512640 134714540 3221221792 3221220020 1077414360 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 151432 148429 1111 63 0 151369 0
vsize: 605728
[startup+580.03 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 150943 0 0 0 57719 280 0 0 25 0 1 0 803206590 630571008 150920 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 153948 150920 1111 63 0 153885 0
vsize: 615792
[startup+590.029 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 153520 0 0 0 58714 283 0 0 25 0 1 0 803206590 641019904 153497 4294967295 134512640 134714540 3221221792 3221220020 1077414382 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 156499 153497 1111 63 0 156436 0
vsize: 625996
[startup+600.031 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 156176 0 0 0 59709 287 0 0 25 0 1 0 803206590 651923456 156153 4294967295 134512640 134714540 3221221792 3221220020 1077414399 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 159161 156153 1111 63 0 159098 0
vsize: 636644
[startup+610.032 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 159075 0 0 0 60704 292 0 0 25 0 1 0 803206590 663863296 159052 4294967295 134512640 134714540 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 162076 159052 1111 63 0 162013 0
vsize: 648304
[startup+620.031 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 161815 0 0 0 61699 295 0 0 25 0 1 0 803206590 675061760 161792 4294967295 134512640 134714540 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 164810 161792 1111 63 0 164747 0
vsize: 659240
[startup+630.032 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 164348 0 0 0 62694 300 0 0 25 0 1 0 803206590 685359104 164325 4294967295 134512640 134714540 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 167324 164325 1111 63 0 167261 0
vsize: 669296
[startup+640.033 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 166878 0 0 0 63689 304 0 0 25 0 1 0 803206590 695816192 166855 4294967295 134512640 134714540 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 169877 166855 1111 63 0 169814 0
vsize: 679508
[startup+650.033 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 169600 0 0 0 64682 309 0 0 25 0 1 0 803206590 706867200 169577 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 172575 169577 1111 63 0 172512 0
vsize: 690300
[startup+660.033 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 172153 0 0 0 65676 315 0 0 25 0 1 0 803206590 717316096 172130 4294967295 134512640 134714540 3221221792 3221220020 1077414360 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 175126 172130 1111 63 0 175063 0
vsize: 700504
[startup+670.033 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 174558 0 0 0 66670 319 0 0 25 0 1 0 803206590 727166976 174535 4294967295 134512640 134714540 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 177531 174535 1111 63 0 177468 0
vsize: 710124
[startup+680.034 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 177082 0 0 0 67665 323 0 0 25 0 1 0 803206590 737472512 177059 4294967295 134512640 134714540 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 180047 177059 1111 63 0 179984 0
vsize: 720188
[startup+690.034 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 179397 0 0 0 68660 328 0 0 25 0 1 0 803206590 747028480 179374 4294967295 134512640 134714540 3221221792 3221220020 1077414385 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 182380 179374 1111 63 0 182317 0
vsize: 729520
[startup+700.035 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 181711 0 0 0 69655 332 0 0 25 0 1 0 803206590 756432896 181688 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 184676 181688 1111 63 0 184613 0
vsize: 738704
[startup+710.035 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 184096 0 0 0 70650 337 0 0 25 0 1 0 803206590 766287872 184073 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 187082 184073 1111 63 0 187019 0
vsize: 748328
[startup+720.035 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 186446 0 0 0 71644 342 0 0 25 0 1 0 803206590 775843840 186423 4294967295 134512640 134714540 3221221792 3221220020 1077414388 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 189415 186423 1111 63 0 189352 0
vsize: 757660
[startup+730.036 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 188724 0 0 0 72639 346 0 0 25 0 1 0 803206590 785248256 188701 4294967295 134512640 134714540 3221221792 3221220020 1077414413 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 191711 188701 1111 63 0 191648 0
vsize: 766844
[startup+740.035 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 191239 0 0 0 73634 350 0 0 25 0 1 0 803206590 795549696 191216 4294967295 134512640 134714540 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 194226 191216 1111 63 0 194163 0
vsize: 776904
[startup+750.036 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 193761 0 0 0 74629 355 0 0 25 0 1 0 803206590 805855232 193738 4294967295 134512640 134714540 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 196742 193738 1111 63 0 196679 0
vsize: 786968
[startup+760.038 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 196424 0 0 0 75623 359 0 0 25 0 1 0 803206590 816963584 196401 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 199454 196401 1111 63 0 199391 0
vsize: 797816
[startup+770.037 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 198886 0 0 0 76617 363 0 0 25 0 1 0 803206590 827121664 198831 4294967295 134512640 134714540 3221221792 3221220448 134527932 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 201934 198831 1111 63 0 201871 0
vsize: 807736
[startup+780.038 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 201639 0 0 0 77610 369 0 0 25 0 1 0 803206590 838311936 201488 4294967295 134512640 134714540 3221221792 3221220020 1077414338 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 204666 201488 1111 63 0 204603 0
vsize: 818664
[startup+790.038 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 204167 0 0 0 78604 375 0 0 25 0 1 0 803206590 848769024 203952 4294967295 134512640 134714540 3221221792 3221220020 1077414435 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 207219 203952 1111 63 0 207156 0
vsize: 828876
[startup+800.038 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 206798 0 0 0 79596 381 0 0 25 0 1 0 803206590 859512832 206455 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 209842 206455 1111 63 0 209779 0
vsize: 839368
[startup+810.038 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 209454 0 0 0 80590 386 0 0 25 0 1 0 803206590 870416384 208919 4294967295 134512640 134714540 3221221792 3221220124 1077399566 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 212504 208919 1111 63 0 212441 0
vsize: 850016
[startup+820.038 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 212158 0 0 0 81582 392 0 0 25 0 1 0 803206590 881467392 211211 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 215202 211211 1111 63 0 215139 0
vsize: 860808
[startup+830.039 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 214965 0 0 0 82575 397 0 0 25 0 1 0 803206590 892960768 213726 4294967295 134512640 134714540 3221221792 3221220144 134567410 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 218008 213727 1111 63 0 217945 0
vsize: 872032
[startup+840.039 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 217464 0 0 0 83568 402 0 0 25 0 1 0 803206590 903114752 216001 4294967295 134512640 134714540 3221221792 3221220144 134567410 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 220487 216001 1111 63 0 220424 0
vsize: 881948
[startup+850.04 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 220461 0 0 0 84560 408 0 0 25 0 1 0 803206590 915361792 218682 4294967295 134512640 134714540 3221221792 3221220448 134527946 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 223477 218682 1111 63 0 223414 0
vsize: 893908
[startup+860.041 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 223066 0 0 0 85551 416 0 0 25 0 1 0 803206590 926105600 221095 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 226100 221095 1111 63 0 226037 0
vsize: 904400
[startup+870.041 s]
Raw data (loadavg): 0.99 1.00 0.97 2/55 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 225406 0 0 0 86545 421 0 0 25 0 1 0 803206590 935661568 223207 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 228433 223207 1111 63 0 228370 0
vsize: 913732
[startup+879.083 s]
Raw data (loadavg): 0.99 1.00 0.97 1/54 8573
Raw data (stat): 8573 (bsolo_mis) R 8572 7876 7672 0 -1 0 225406 0 0 0 86545 421 0 0 25 0 1 0 803206590 935661568 223207 4294967295 134512640 134714540 3221221792 3221220020 1077414363 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 228433 223207 1111 63 0 228370 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 879.082
CPU time (s): 878.685
CPU user time (s): 873.997
CPU system time (s): 4.68829
CPU usage (%): 99.9548
Max. virtual memory (Kb): 913732
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####