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/miplib2003/normalized-mps-v2-20-10-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.17
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 28482

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-05-25 02:44:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12522 boxname=wulflinc7 idbench=964 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  38504d32a17a57a658eee171614b901e  /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: 12522
/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:        833732 kB
Buffers:         10452 kB
Cached:         169716 kB
SwapCached:        644 kB
Active:          47988 kB
Inactive:       134444 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        833480 kB
SwapTotal:     2097136 kB
SwapFree:      2095780 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5492 kB
Slab:            12636 kB
Committed_AS:    63564 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 02:50:44 (client local time) WITH STATUS 0 IN 370.308 SECONDS
stats: 12522 7 370.308 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.88 0.94 0.90 2/54 4327
Raw data (stat): 4327 (runsolver) R 4326 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 777163479 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.0007 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 4867 0 0 0 990 8 0 0 25 0 1 0 777163479 32681984 4845 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 7979 4845 1111 63 0 7916 0
vsize: 31916
[startup+20.0009 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 9305 0 0 0 1982 16 0 0 25 0 1 0 777163479 50884608 9283 4294967295 134512640 134714540 3221224592 3221222820 1077414426 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12423 9283 1111 63 0 12360 0
vsize: 49692
[startup+30.0012 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 13806 0 0 0 2975 24 0 0 25 0 1 0 777163479 69398528 13784 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 16943 13784 1111 63 0 16880 0
vsize: 67772
[startup+40.0021 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 18345 0 0 0 3969 31 0 0 25 0 1 0 777163479 87912448 18323 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 21463 18323 1111 63 0 21400 0
vsize: 85852
[startup+50.0018 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 22931 0 0 0 4960 39 0 0 25 0 1 0 777163479 106721280 22909 4294967295 134512640 134714540 3221224592 3221222820 1077414351 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 26055 22909 1111 63 0 25992 0
vsize: 104220
[startup+60.0021 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 27592 0 0 0 5951 48 0 0 25 0 1 0 777163479 125833216 27570 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 30721 27570 1111 63 0 30658 0
vsize: 122884
[startup+70.0023 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 32344 0 0 0 6944 56 0 0 25 0 1 0 777163479 145240064 32322 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 35459 32322 1111 63 0 35396 0
vsize: 141836
[startup+80.0037 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 37146 0 0 0 7936 64 0 0 25 0 1 0 777163479 164950016 37124 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 40271 37124 1111 63 0 40208 0
vsize: 161084
[startup+90.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 41983 0 0 0 8927 73 0 0 25 0 1 0 777163479 184807424 41961 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 45119 41961 1111 63 0 45056 0
vsize: 180476
[startup+100.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 46861 0 0 0 9920 81 0 0 25 0 1 0 777163479 204812288 46839 4294967295 134512640 134714540 3221224592 3221222820 1077414407 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 50003 46839 1111 63 0 49940 0
vsize: 200012
[startup+110.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 51830 0 0 0 10913 88 0 0 25 0 1 0 777163479 225140736 51808 4294967295 134512640 134714540 3221224592 3221222820 1077414433 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 54966 51808 1111 63 0 54903 0
vsize: 219864
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 56880 0 0 0 11903 98 0 0 25 0 1 0 777163479 245895168 56858 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 60033 56858 1111 63 0 59970 0
vsize: 240132
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 62009 0 0 0 12893 108 0 0 25 0 1 0 777163479 266797056 61987 4294967295 134512640 134714540 3221224592 3221222820 1077414401 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 65136 61987 1111 63 0 65073 0
vsize: 260544
[startup+140.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 67308 0 0 0 13883 118 0 0 25 0 1 0 777163479 288595968 67286 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 70458 67291 1111 63 0 70395 0
vsize: 281832
[startup+150.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 72753 0 0 0 14874 128 0 0 25 0 1 0 777163479 310837248 72731 4294967295 134512640 134714540 3221224592 3221222820 1077414420 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 75888 72731 1111 63 0 75825 0
vsize: 303552
[startup+160.006 s]
Raw data (loadavg): 1.06 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 78302 0 0 0 15862 140 0 0 25 0 1 0 777163479 333537280 78280 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 81430 78280 1111 63 0 81367 0
vsize: 325720
[startup+170.006 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 83917 0 0 0 16852 150 0 0 25 0 1 0 777163479 356528128 83895 4294967295 134512640 134714540 3221224592 3221222820 1077414376 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 87043 83895 1111 63 0 86980 0
vsize: 348172
[startup+180.006 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 89606 0 0 0 17841 161 0 0 25 0 1 0 777163479 379822080 89584 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 92730 89584 1111 63 0 92667 0
vsize: 370920
[startup+190.007 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 95413 0 0 0 18831 172 0 0 25 0 1 0 777163479 403558400 95391 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 98525 95391 1111 63 0 98462 0
vsize: 394100
[startup+200.006 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 101350 0 0 0 19821 182 0 0 25 0 1 0 777163479 428113920 101328 4294967295 134512640 134714540 3221224592 3221222820 1077414435 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 104520 101328 1111 63 0 104457 0
vsize: 418080
[startup+210.007 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 107439 0 0 0 20810 193 0 0 25 0 1 0 777163479 453046272 107417 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 110607 107417 1111 63 0 110544 0
vsize: 442428
[startup+220.007 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 113656 0 0 0 21798 204 0 0 25 0 1 0 777163479 478429184 113634 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 116804 113634 1111 63 0 116741 0
vsize: 467216
[startup+230.007 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 119989 0 0 0 22788 215 0 0 25 0 1 0 777163479 504406016 119967 4294967295 134512640 134714540 3221224592 3221222820 1077414407 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 123146 119967 1111 63 0 123083 0
vsize: 492584
[startup+240.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 126576 0 0 0 23776 227 0 0 25 0 1 0 777163479 531279872 126554 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 129707 126554 1111 63 0 129644 0
vsize: 518828
[startup+250.007 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 133268 0 0 0 24764 240 0 0 25 0 1 0 777163479 558755840 133246 4294967295 134512640 134714540 3221224592 3221222820 1077414407 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 136415 133246 1111 63 0 136352 0
vsize: 545660
[startup+260.007 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 140086 0 0 0 25752 252 0 0 25 0 1 0 777163479 586674176 140064 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 143231 140064 1111 63 0 143168 0
vsize: 572924
[startup+270.006 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 147106 0 0 0 26741 263 0 0 25 0 1 0 777163479 615342080 147084 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 150230 147084 1111 63 0 150167 0
vsize: 600920
[startup+280.007 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 154222 0 0 0 27729 275 0 0 25 0 1 0 777163479 644603904 154200 4294967295 134512640 134714540 3221224592 3221222944 134567410 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 157374 154200 1111 63 0 157311 0
vsize: 629496
[startup+290.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 161533 0 0 0 28718 287 0 0 25 0 1 0 777163479 674463744 161511 4294967295 134512640 134714540 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 164664 161511 1111 63 0 164601 0
vsize: 658656
[startup+300.007 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 169189 0 0 0 29704 300 0 0 25 0 1 0 777163479 705818624 169167 4294967295 134512640 134714540 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 172319 169167 1111 63 0 172256 0
vsize: 689276
[startup+310.008 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 177000 0 0 0 30692 313 0 0 25 0 1 0 777163479 737771520 176978 4294967295 134512640 134714540 3221224592 3221222820 1077414426 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 180120 176978 1111 63 0 180057 0
vsize: 720480
[startup+320.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 185016 0 0 0 31677 328 0 0 25 0 1 0 777163479 770621440 184994 4294967295 134512640 134714540 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 188140 184994 1111 63 0 188077 0
vsize: 752560
[startup+330.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 193155 0 0 0 32666 339 0 0 25 0 1 0 777163479 803909632 193133 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 196267 193133 1111 63 0 196204 0
vsize: 785068
[startup+340.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 201508 0 0 0 33653 353 0 0 25 0 1 0 777163479 838463488 201486 4294967295 134512640 134714540 3221224592 3221222820 1077414336 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 204703 201486 1111 63 0 204640 0
vsize: 818812
[startup+350.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 210022 0 0 0 34636 368 0 0 25 0 1 0 777163479 873254912 209936 4294967295 134512640 134714540 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 213197 209936 1111 63 0 213134 0
vsize: 852788
[startup+360.009 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 0 218524 0 1 0 35610 391 0 0 25 0 1 0 777163479 908042240 216624 4294967295 134512640 134714540 3221224592 3221222820 1077414370 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 221690 216624 1111 63 0 221627 0
vsize: 886760
[startup+370.012 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 1028 227235 0 5 0 36573 424 0 0 25 0 1 0 777163479 0 0 4294967295 0 0 0 0 0 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
[startup+370.342 s]
Raw data (loadavg): 1.00 0.97 0.91 1/53 4327
Raw data (stat): 4327 (bsolo_mis) R 4326 24300 24299 0 -1 1028 227235 0 5 0 36573 424 0 0 25 0 1 0 777163479 0 0 4294967295 0 0 0 0 0 0 0 7 0 0 0 0 17 0 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): 370.341
CPU time (s): 370.308
CPU user time (s): 365.735
CPU system time (s): 4.5723
CPU usage (%): 99.9909
Max. virtual memory (Kb): 886760
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####