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-n3707.opb
MD5SUM	01e0877cc064d2a3c60da2ac822a983e
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	39195741828
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	39195741828
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	0.998847
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 35697

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-05-28 13:47:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24997 boxname=wulflinc7 idbench=1469 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  01e0877cc064d2a3c60da2ac822a983e  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-n3707.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-n3707.opb
IDLAUNCH: 24997
/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:        668344 kB
Buffers:         34236 kB
Cached:         310424 kB
SwapCached:        644 kB
Active:          25448 kB
Inactive:       321304 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        668092 kB
SwapTotal:     2097136 kB
SwapFree:      2095560 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            13832 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 13:54:42 (client local time) WITH STATUS 1 IN 411.626 SECONDS
stats: 24997 7 411.626 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.92 0.95 0.91 2/54 10615
Raw data (stat): 10615 (runsolver) R 10614 24300 24299 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 807067534 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.99984 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 2162 0 0 0 995 3 0 0 25 0 1 0 807067534 7954432 1486 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1942 1486 300 300 0 1642 0
vsize: 7768
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 2698 0 0 0 1994 5 0 0 25 0 1 0 807067534 9306112 2014 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 2272 2014 300 300 0 1972 0
vsize: 9088
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 3865 0 0 0 2991 7 0 0 25 0 1 0 807067534 13410304 2469 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3274 2469 300 300 0 2974 0
vsize: 13096
[startup+40.0018 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 4098 0 0 0 3990 8 0 0 25 0 1 0 807067534 13950976 2697 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3406 2697 300 300 0 3106 0
vsize: 13624
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 4351 0 0 0 4989 8 0 0 25 0 1 0 807067534 14626816 2946 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3571 2946 300 300 0 3271 0
vsize: 14284
[startup+60.0021 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 4583 0 0 0 5989 9 0 0 25 0 1 0 807067534 15302656 3174 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3736 3174 300 300 0 3436 0
vsize: 14944
[startup+70.0017 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 4793 0 0 0 6988 9 0 0 25 0 1 0 807067534 15843328 3381 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 3868 3381 300 300 0 3568 0
vsize: 15472
[startup+80.0014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 4989 0 0 0 7987 10 0 0 25 0 1 0 807067534 16384000 3574 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4000 3574 300 300 0 3700 0
vsize: 16000
[startup+90.0024 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 5174 0 0 0 8987 10 0 0 25 0 1 0 807067534 16789504 3756 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4099 3756 300 300 0 3799 0
vsize: 16396
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 5348 0 0 0 9986 11 0 0 25 0 1 0 807067534 17330176 3927 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4231 3927 300 300 0 3931 0
vsize: 16924
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 5516 0 0 0 10985 11 0 0 25 0 1 0 807067534 17735680 4092 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4330 4092 300 300 0 4030 0
vsize: 17320
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 7499 0 0 0 11983 14 0 0 25 0 1 0 807067534 25403392 4663 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4663 300 300 0 5902 0
vsize: 24808
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 7557 0 0 0 12982 15 0 0 25 0 1 0 807067534 25403392 4718 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4718 300 300 0 5902 0
vsize: 24808
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 7610 0 0 0 13983 15 0 0 25 0 1 0 807067534 25403392 4769 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4769 300 300 0 5902 0
vsize: 24808
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 7690 0 0 0 14983 15 0 0 25 0 1 0 807067534 25403392 4846 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6202 4846 300 300 0 5902 0
vsize: 24808
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 7749 0 0 0 15982 15 0 0 25 0 1 0 807067534 25538560 4903 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6235 4903 300 300 0 5935 0
vsize: 24940
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 7886 0 0 0 16981 16 0 0 25 0 1 0 807067534 25808896 5038 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6301 5038 300 300 0 6001 0
vsize: 25204
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 8017 0 0 0 17981 16 0 0 25 0 1 0 807067534 26214400 5167 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6400 5167 300 300 0 6100 0
vsize: 25600
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 8149 0 0 0 18981 16 0 0 25 0 1 0 807067534 26619904 5296 4294967295 134512640 135726644 3221224592 3221221680 134556168 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6499 5296 300 300 0 6199 0
vsize: 25996
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 8275 0 0 0 19981 17 0 0 25 0 1 0 807067534 26890240 5420 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6565 5420 300 300 0 6265 0
vsize: 26260
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 8398 0 0 0 20980 18 0 0 25 0 1 0 807067534 27160576 5541 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6631 5541 300 300 0 6331 0
vsize: 26524
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 8517 0 0 0 21980 18 0 0 25 0 1 0 807067534 27566080 5659 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6730 5659 300 300 0 6430 0
vsize: 26920
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 8634 0 0 0 22979 19 0 0 25 0 1 0 807067534 27836416 5774 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6796 5774 300 300 0 6496 0
vsize: 27184
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 8749 0 0 0 23979 19 0 0 25 0 1 0 807067534 28106752 5887 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6862 5887 300 300 0 6562 0
vsize: 27448
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 8861 0 0 0 24979 19 0 0 25 0 1 0 807067534 28512256 5997 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6961 5997 300 300 0 6661 0
vsize: 27844
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 8970 0 0 0 25979 20 0 0 25 0 1 0 807067534 28782592 6104 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7027 6104 300 300 0 6727 0
vsize: 28108
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 9079 0 0 0 26978 20 0 0 25 0 1 0 807067534 29052928 6211 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7093 6211 300 300 0 6793 0
vsize: 28372
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 9183 0 0 0 27978 20 0 0 25 0 1 0 807067534 29323264 6314 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7159 6314 300 300 0 6859 0
vsize: 28636
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 9287 0 0 0 28978 21 0 0 25 0 1 0 807067534 29593600 6416 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7225 6416 300 300 0 6925 0
vsize: 28900
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 9936 0 0 0 29977 21 0 0 25 0 1 0 807067534 32026624 7063 4294967295 134512640 135726644 3221224592 3221221384 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7819 7063 300 300 0 7519 0
vsize: 31276
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 46489 0 0 0 30898 100 0 0 25 0 1 0 807067534 154316800 33457 4294967295 134512640 135726644 3221224592 3179298400 135280446 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 37675 33458 300 300 0 37375 0
vsize: 150700
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 82682 0 0 0 31823 176 0 0 25 0 1 0 807067534 326250496 59857 4294967295 134512640 135726644 3221224592 3182733176 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 79651 59860 300 300 0 79351 0
vsize: 318604
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 106545 0 0 0 32771 228 0 0 25 0 1 0 807067534 403361792 74169 4294967295 134512640 135726644 3221224592 3179357008 134784885 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 98477 74173 300 300 0 98177 0
vsize: 393908
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 130004 0 0 0 33722 277 0 0 25 0 1 0 807067534 412803072 85132 4294967295 134512640 135726644 3221224592 3185172928 135288929 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 100782 85134 300 300 0 100482 0
vsize: 403128
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 170900 0 0 0 34641 359 0 0 25 0 1 0 807067534 545746944 106436 4294967295 134512640 135726644 3221224592 3179841280 134767091 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 133239 106437 300 300 0 132939 0
vsize: 532956
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 206913 0 0 0 35563 436 0 0 25 0 1 0 807067534 646410240 117671 4294967295 134512640 135726644 3221224592 3179822480 134766969 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 157815 117672 300 300 0 157515 0
vsize: 631260
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 221607 0 0 0 36527 472 0 0 25 0 1 0 807067534 690913280 132148 4294967295 134512640 135726644 3221224592 3180041248 134766492 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 168680 132148 300 300 0 168380 0
vsize: 674720
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 241605 0 0 0 37485 514 0 0 25 0 1 0 807067534 719298560 151919 4294967295 134512640 135726644 3221224592 3183115564 135287512 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 175610 151919 300 300 0 175310 0
vsize: 702440
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 261234 0 0 0 38443 557 0 0 25 0 1 0 807067534 747143168 171321 4294967295 134512640 135726644 3221224592 3181158880 134767234 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 182408 171321 300 300 0 182108 0
vsize: 729632
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 271746 0 0 0 39418 582 0 0 25 0 1 0 807067534 813662208 181712 4294967295 134512640 135726644 3221224592 3182587256 135131541 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 198648 181712 300 300 0 198348 0
vsize: 794592
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 271748 0 0 0 40403 596 0 0 25 0 1 0 807067534 450838528 109632 4294967295 134512640 135726644 3221224592 3221222848 135279084 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 110068 109632 300 300 0 109768 0
vsize: 440272
[startup+411.623 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 10615
Raw data (stat): 10615 (pb2sat) R 10614 24300 24299 0 -1 0 271748 0 0 0 40403 596 0 0 25 0 1 0 807067534 450838528 109632 4294967295 134512640 135726644 3221224592 3221222848 135279084 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 110068 109632 300 300 0 109768 0
vsize: 0

Child status: 1
Real time (s): 411.623
CPU time (s): 411.626
CPU user time (s): 405.431
CPU system time (s): 6.19506
CPU usage (%): 100.001
Max. virtual memory (Kb): 794592
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####