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/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-n3702.opb
MD5SUM	1d23f02bf686681d1b293e114d3bb612
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	105000
Biggest coefficient in the objective function	4194304
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	39177236543
Number of bits of the sum of numbers in the objective function	36
Biggest number in a constraint	4194304
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	39177236543
Number of bits of the biggest sum of numbers	36
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	105000
Total number of constraints	5150
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	5150
Minimum length of a constraint	21
Maximum length of a constraint	2000

Trace number 35691

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-05-28 13:46:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24992 boxname=wulflinc15 idbench=1464 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1d23f02bf686681d1b293e114d3bb612  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-n3702.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-n3702.opb
IDLAUNCH: 24992
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        730304 kB
Buffers:         34252 kB
Cached:         247208 kB
SwapCached:        604 kB
Active:          66184 kB
Inactive:       217376 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        730052 kB
SwapTotal:     2097136 kB
SwapFree:      2095616 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5120 kB
Slab:            15148 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 13:53:39 (client local time) WITH STATUS 1 IN 410.746 SECONDS
stats: 24992 7 410.746 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified

	Unexpected exception :
	St9bad_alloc
#### 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
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.91 0.95 0.90 2/54 4606
Raw data (stat): 4606 (runsolver) R 4605 23514 23513 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 807046511 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+9.99999 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 2209 0 0 0 994 5 0 0 25 0 1 0 807046511 8089600 1533 4294967295 134512640 135726644 3221224576 3221221664 134556187 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1975 1533 300 300 0 1675 0
vsize: 7900
[startup+19.9998 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 2757 0 0 0 1992 7 0 0 25 0 1 0 807046511 9576448 2072 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2338 2072 300 300 0 2038 0
vsize: 9352
[startup+30 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 3883 0 0 0 2989 10 0 0 25 0 1 0 807046511 13410304 2486 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3274 2486 300 300 0 2974 0
vsize: 13096
[startup+40.0004 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 4140 0 0 0 3988 11 0 0 25 0 1 0 807046511 14086144 2738 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3439 2738 300 300 0 3139 0
vsize: 13756
[startup+50.0013 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 4400 0 0 0 4987 13 0 0 25 0 1 0 807046511 14761984 2994 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3604 2994 300 300 0 3304 0
vsize: 14416
[startup+60.0011 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 4633 0 0 0 5986 13 0 0 25 0 1 0 807046511 15437824 3223 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3769 3223 300 300 0 3469 0
vsize: 15076
[startup+70.0009 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 4840 0 0 0 6985 15 0 0 25 0 1 0 807046511 15978496 3427 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3901 3427 300 300 0 3601 0
vsize: 15604
[startup+80.0018 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 5033 0 0 0 7984 16 0 0 25 0 1 0 807046511 16519168 3617 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4033 3617 300 300 0 3733 0
vsize: 16132
[startup+90.1039 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 5216 0 0 0 8994 16 0 0 25 0 1 0 807046511 16924672 3797 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4132 3797 300 300 0 3832 0
vsize: 16528
[startup+100.104 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 5387 0 0 0 9993 17 0 0 25 0 1 0 807046511 17330176 3965 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4231 3965 300 300 0 3931 0
vsize: 16924
[startup+110.105 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 7453 0 0 0 10989 22 0 0 25 0 1 0 807046511 25403392 4619 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4619 300 300 0 5902 0
vsize: 24808
[startup+120.105 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 7510 0 0 0 11988 23 0 0 25 0 1 0 807046511 25403392 4673 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4673 300 300 0 5902 0
vsize: 24808
[startup+130.105 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 7564 0 0 0 12988 23 0 0 25 0 1 0 807046511 25403392 4725 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4725 300 300 0 5902 0
vsize: 24808
[startup+140.105 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 7618 0 0 0 13988 24 0 0 25 0 1 0 807046511 25403392 4776 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4776 300 300 0 5902 0
vsize: 24808
[startup+150.105 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 7695 0 0 0 14987 24 0 0 25 0 1 0 807046511 25403392 4851 4294967295 134512640 135726644 3221224576 3221221664 134556187 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4851 300 300 0 5902 0
vsize: 24808
[startup+160.104 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 7763 0 0 0 15987 25 0 0 25 0 1 0 807046511 25538560 4917 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6235 4917 300 300 0 5935 0
vsize: 24940
[startup+170.104 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 7898 0 0 0 16986 26 0 0 25 0 1 0 807046511 25944064 5050 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6334 5050 300 300 0 6034 0
vsize: 25336
[startup+180.104 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 8030 0 0 0 17985 26 0 0 25 0 1 0 807046511 26214400 5179 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6400 5179 300 300 0 6100 0
vsize: 25600
[startup+190.104 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 8157 0 0 0 18985 27 0 0 25 0 1 0 807046511 26619904 5304 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6499 5304 300 300 0 6199 0
vsize: 25996
[startup+200.105 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 8281 0 0 0 19985 27 0 0 25 0 1 0 807046511 26890240 5426 4294967295 134512640 135726644 3221224576 3221221312 134990311 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6565 5426 300 300 0 6265 0
vsize: 26260
[startup+210.105 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 8404 0 0 0 20985 28 0 0 25 0 1 0 807046511 27295744 5547 4294967295 134512640 135726644 3221224576 3221221664 134556192 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6664 5547 300 300 0 6364 0
vsize: 26656
[startup+220.104 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 8523 0 0 0 21984 29 0 0 25 0 1 0 807046511 27566080 5664 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6730 5664 300 300 0 6430 0
vsize: 26920
[startup+230.105 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 8638 0 0 0 22984 29 0 0 25 0 1 0 807046511 27836416 5778 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6796 5778 300 300 0 6496 0
vsize: 27184
[startup+240.105 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 8754 0 0 0 23983 30 0 0 25 0 1 0 807046511 28106752 5892 4294967295 134512640 135726644 3221224576 3221221888 134565202 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6862 5892 300 300 0 6562 0
vsize: 27448
[startup+250.106 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 8865 0 0 0 24983 30 0 0 25 0 1 0 807046511 28512256 6001 4294967295 134512640 135726644 3221224576 3221221664 134556195 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6961 6001 300 300 0 6661 0
vsize: 27844
[startup+260.107 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 8974 0 0 0 25982 31 0 0 25 0 1 0 807046511 28782592 6108 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7027 6108 300 300 0 6727 0
vsize: 28108
[startup+270.107 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 9083 0 0 0 26982 31 0 0 25 0 1 0 807046511 29052928 6215 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7093 6215 300 300 0 6793 0
vsize: 28372
[startup+280.107 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 9188 0 0 0 27982 32 0 0 25 0 1 0 807046511 29323264 6319 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7159 6319 300 300 0 6859 0
vsize: 28636
[startup+290.107 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 9291 0 0 0 28982 32 0 0 25 0 1 0 807046511 29593600 6420 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7225 6420 300 300 0 6925 0
vsize: 28900
[startup+300.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 10212 0 0 0 29980 34 0 0 25 0 1 0 807046511 33243136 7339 4294967295 134512640 135726644 3221224576 3221221040 134549658 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8116 7339 300 300 0 7816 0
vsize: 32464
[startup+310.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 50015 0 0 0 30898 116 0 0 25 0 1 0 807046511 167170048 33906 4294967295 134512640 135726644 3221224576 3180615180 135287483 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 40813 33906 300 300 0 40513 0
vsize: 163252
[startup+320.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 86293 0 0 0 31823 191 0 0 25 0 1 0 807046511 331792384 63337 4294967295 134512640 135726644 3221224576 3179244416 135279084 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 81004 63337 300 300 0 80704 0
vsize: 324016
[startup+330.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 111919 0 0 0 32767 248 0 0 25 0 1 0 807046511 353161216 67253 4294967295 134512640 135726644 3221224576 3184422528 134554546 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 86254 67254 300 300 0 85954 0
vsize: 344884
[startup+340.107 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 131347 0 0 0 33725 290 0 0 25 0 1 0 807046511 414965760 86457 4294967295 134512640 135726644 3221224576 3181125280 134782642 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 101310 86457 300 300 0 101010 0
vsize: 405240
[startup+350.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 171655 0 0 0 34648 367 0 0 25 0 1 0 807046511 545746944 107176 4294967295 134512640 135726644 3221224576 3179523708 134604400 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 133239 107176 300 300 0 132939 0
vsize: 532956
[startup+360.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 207809 0 0 0 35567 449 0 0 25 0 1 0 807046511 646410240 118551 4294967295 134512640 135726644 3221224576 3180732552 134784091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 157815 118551 300 300 0 157515 0
vsize: 631260
[startup+370.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 222284 0 0 0 36533 483 0 0 25 0 1 0 807046511 691183616 132822 4294967295 134512640 135726644 3221224576 3183314620 134607254 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 168746 132823 300 300 0 168446 0
vsize: 674984
[startup+380.108 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 242280 0 0 0 37490 526 0 0 25 0 1 0 807046511 719704064 152588 4294967295 134512640 135726644 3221224576 3180983432 135281806 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 175709 152588 300 300 0 175409 0
vsize: 702836
[startup+390.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 263291 0 0 0 38442 574 0 0 25 0 1 0 807046511 749846528 173350 4294967295 134512640 135726644 3221224576 3188521752 134784091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 183068 173351 300 300 0 182768 0
vsize: 732272
[startup+400.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 271156 0 0 0 39423 593 0 0 25 0 1 0 807046511 813256704 181122 4294967295 134512640 135726644 3221224576 3189062964 135138357 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 198549 181122 300 300 0 198249 0
vsize: 794196
[startup+410.109 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 271158 0 0 0 40409 607 0 0 25 0 1 0 807046511 450433024 109536 4294967295 134512640 135726644 3221224576 3221222928 135280446 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 109969 109536 300 300 0 109669 0
vsize: 439876
[startup+410.687 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 4606
Raw data (stat): 4606 (pb2sat) R 4605 23514 23513 0 -1 0 271158 0 0 0 40409 607 0 0 25 0 1 0 807046511 450433024 109536 4294967295 134512640 135726644 3221224576 3221222928 135280446 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 109969 109536 300 300 0 109669 0
vsize: 0

Child status: 1
Real time (s): 410.686
CPU time (s): 410.746
CPU user time (s): 404.447
CPU system time (s): 6.29804
CPU usage (%): 100.015
Max. virtual memory (Kb): 794196
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####