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/plato.asu.edu/pub/fctp/normalized-mps-v2-20-10-n3705.opb
MD5SUM	8eea845826d64e6d5753fad916c185c9
Bench Category	optimization, big integers (OPTBIGINT)
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	155000
Biggest coefficient in the objective function	4294967296
Number of bits for the biggest coefficient in the objective function	33
Sum of the numbers in the objective function	29593306649763
Number of bits of the sum of numbers in the objective function	45
Biggest number in a constraint	4294967296
Number of bits of the biggest number in a constraint	33
Biggest sum of numbers in a constraint	29593306649763
Number of bits of the biggest sum of numbers	45
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.43278
Number of variables	155000
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	31
Maximum length of a constraint	3000
Trace number 35327

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-05-28 12:43:54 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24611 boxname=wulflinc29 idbench=1083 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  8eea845826d64e6d5753fad916c185c9  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-n3705.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-20-10-n3705.opb
IDLAUNCH: 24611
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        680848 kB
Buffers:         34668 kB
Cached:         292664 kB
SwapCached:        632 kB
Active:          28188 kB
Inactive:       301244 kB
HighTotal:      131008 kB
HighFree:        31892 kB
LowTotal:       903652 kB
LowFree:        648956 kB
SwapTotal:     2097892 kB
SwapFree:      2096368 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5132 kB
Slab:            18576 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-28 12:57:00 (client local time) WITH STATUS 1 IN 785.771 SECONDS
stats: 24611 7 785.771 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 28226
Raw data (stat): 28226 (runsolver) R 28225 20001 20000 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 864892207 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 2144 0 0 0 994 5 0 0 25 0 1 0 864892207 7954432 1469 4294967295 134512640 135726644 3221224576 3221221664 134556192 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1942 1469 300 300 0 1642 0
vsize: 7768
[startup+20.0082 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 2701 0 0 0 1992 7 0 0 25 0 1 0 864892207 9306112 2017 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2272 2017 300 300 0 1972 0
vsize: 9088
[startup+30.0088 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 3867 0 0 0 2989 10 0 0 25 0 1 0 864892207 13410304 2471 4294967295 134512640 135726644 3221224576 3221221664 134556188 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3274 2471 300 300 0 2974 0
vsize: 13096
[startup+40.0101 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 4110 0 0 0 3989 11 0 0 25 0 1 0 864892207 14086144 2709 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3439 2709 300 300 0 3139 0
vsize: 13756
[startup+50.0108 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 4365 0 0 0 4988 12 0 0 25 0 1 0 864892207 14626816 2960 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3571 2960 300 300 0 3271 0
vsize: 14284
[startup+60.0116 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 4594 0 0 0 5987 13 0 0 25 0 1 0 864892207 15302656 3185 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3736 3185 300 300 0 3436 0
vsize: 14944
[startup+70.0124 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 4800 0 0 0 6986 14 0 0 25 0 1 0 864892207 15843328 3388 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3868 3388 300 300 0 3568 0
vsize: 15472
[startup+80.0142 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 4990 0 0 0 7986 15 0 0 25 0 1 0 864892207 16384000 3575 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4000 3575 300 300 0 3700 0
vsize: 16000
[startup+90.0149 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 5169 0 0 0 8985 16 0 0 25 0 1 0 864892207 16789504 3751 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4099 3751 300 300 0 3799 0
vsize: 16396
[startup+100.015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 5339 0 0 0 9984 16 0 0 25 0 1 0 864892207 17330176 3918 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4231 3918 300 300 0 3931 0
vsize: 16924
[startup+110.016 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 5501 0 0 0 10983 18 0 0 25 0 1 0 864892207 17735680 4077 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4330 4077 300 300 0 4030 0
vsize: 17320
[startup+120.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 7492 0 0 0 11979 22 0 0 25 0 1 0 864892207 25403392 4656 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4656 300 300 0 5902 0
vsize: 24808
[startup+130.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 7547 0 0 0 12979 22 0 0 25 0 1 0 864892207 25403392 4708 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4708 300 300 0 5902 0
vsize: 24808
[startup+140.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 7599 0 0 0 13978 23 0 0 25 0 1 0 864892207 25403392 4758 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4758 300 300 0 5902 0
vsize: 24808
[startup+150.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 7677 0 0 0 14978 24 0 0 25 0 1 0 864892207 25403392 4834 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4834 300 300 0 5902 0
vsize: 24808
[startup+160.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 7726 0 0 0 15977 24 0 0 25 0 1 0 864892207 25403392 4881 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4881 300 300 0 5902 0
vsize: 24808
[startup+170.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 7846 0 0 0 16977 25 0 0 25 0 1 0 864892207 25808896 4998 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6301 4998 300 300 0 6001 0
vsize: 25204
[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 7977 0 0 0 17977 25 0 0 25 0 1 0 864892207 26079232 5127 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6367 5127 300 300 0 6067 0
vsize: 25468
[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 8103 0 0 0 18976 26 0 0 25 0 1 0 864892207 26484736 5251 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6466 5251 300 300 0 6166 0
vsize: 25864
[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 8227 0 0 0 19976 27 0 0 25 0 1 0 864892207 26755072 5373 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6532 5373 300 300 0 6232 0
vsize: 26128
[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 8348 0 0 0 20975 27 0 0 25 0 1 0 864892207 27025408 5492 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6598 5492 300 300 0 6298 0
vsize: 26392
[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 8466 0 0 0 21975 28 0 0 25 0 1 0 864892207 27430912 5608 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6697 5608 300 300 0 6397 0
vsize: 26788
[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 8584 0 0 0 22974 28 0 0 25 0 1 0 864892207 27701248 5724 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6763 5724 300 300 0 6463 0
vsize: 27052
[startup+240.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 8698 0 0 0 23974 28 0 0 25 0 1 0 864892207 27971584 5837 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6829 5837 300 300 0 6529 0
vsize: 27316
[startup+250.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 8809 0 0 0 24974 29 0 0 25 0 1 0 864892207 28377088 5946 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6928 5946 300 300 0 6628 0
vsize: 27712
[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 8922 0 0 0 25974 29 0 0 25 0 1 0 864892207 28647424 6057 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 6994 6057 300 300 0 6694 0
vsize: 27976
[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 9030 0 0 0 26974 30 0 0 25 0 1 0 864892207 28917760 6163 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7060 6163 300 300 0 6760 0
vsize: 28240
[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 9135 0 0 0 27973 30 0 0 25 0 1 0 864892207 29188096 6267 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7126 6267 300 300 0 6826 0
vsize: 28504
[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 9240 0 0 0 28973 31 0 0 25 0 1 0 864892207 29458432 6370 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7192 6370 300 300 0 6892 0
vsize: 28768
[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 9344 0 0 0 29973 31 0 0 25 0 1 0 864892207 29728768 6472 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7258 6472 300 300 0 6958 0
vsize: 29032
[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 9444 0 0 0 30973 31 0 0 25 0 1 0 864892207 29999104 6571 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7324 6571 300 300 0 7024 0
vsize: 29296
[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 9545 0 0 0 31973 31 0 0 25 0 1 0 864892207 30269440 6670 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7390 6670 300 300 0 7090 0
vsize: 29560
[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 9643 0 0 0 32973 31 0 0 25 0 1 0 864892207 30539776 6766 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7456 6766 300 300 0 7156 0
vsize: 29824
[startup+340.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 9739 0 0 0 33973 31 0 0 25 0 1 0 864892207 30810112 6861 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7522 6861 300 300 0 7222 0
vsize: 30088
[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 9836 0 0 0 34972 32 0 0 25 0 1 0 864892207 31080448 6956 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7588 6956 300 300 0 7288 0
vsize: 30352
[startup+360.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 9929 0 0 0 35972 32 0 0 25 0 1 0 864892207 31215616 7048 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7621 7048 300 300 0 7321 0
vsize: 30484
[startup+370.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 10024 0 0 0 36972 32 0 0 25 0 1 0 864892207 31485952 7141 4294967295 134512640 135726644 3221224576 3221221208 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7687 7141 300 300 0 7387 0
vsize: 30748
[startup+380.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 10115 0 0 0 37972 33 0 0 25 0 1 0 864892207 31756288 7231 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7753 7231 300 300 0 7453 0
vsize: 31012
[startup+390.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 10205 0 0 0 38972 33 0 0 25 0 1 0 864892207 32026624 7319 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7819 7319 300 300 0 7519 0
vsize: 31276
[startup+400.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 10294 0 0 0 39972 33 0 0 25 0 1 0 864892207 32296960 7407 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7885 7407 300 300 0 7585 0
vsize: 31540
[startup+410.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 10382 0 0 0 40971 34 0 0 25 0 1 0 864892207 32432128 7493 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7918 7493 300 300 0 7618 0
vsize: 31672
[startup+420.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 10469 0 0 0 41971 34 0 0 25 0 1 0 864892207 32702464 7579 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 7984 7579 300 300 0 7684 0
vsize: 31936
[startup+430.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 10555 0 0 0 42970 35 0 0 25 0 1 0 864892207 32972800 7664 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 8050 7664 300 300 0 7750 0
vsize: 32200
[startup+440.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 10642 0 0 0 43970 35 0 0 25 0 1 0 864892207 33107968 7749 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 8083 7749 300 300 0 7783 0
vsize: 32332
[startup+450.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 10726 0 0 0 44970 35 0 0 25 0 1 0 864892207 33378304 7832 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 8149 7832 300 300 0 7849 0
vsize: 32596
[startup+460.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 10808 0 0 0 45970 35 0 0 25 0 1 0 864892207 33648640 7913 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8215 7913 300 300 0 7915 0
vsize: 32860
[startup+470.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 10892 0 0 0 46970 36 0 0 25 0 1 0 864892207 33783808 7995 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 8248 7995 300 300 0 7948 0
vsize: 32992
[startup+480.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 14809 0 0 0 47962 44 0 0 25 0 1 0 864892207 49254400 9093 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9093 300 300 0 11725 0
vsize: 48100
[startup+490.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 14837 0 0 0 48962 44 0 0 25 0 1 0 864892207 49254400 9120 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9120 300 300 0 11725 0
vsize: 48100
[startup+500.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 14866 0 0 0 49962 44 0 0 25 0 1 0 864892207 49254400 9147 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9147 300 300 0 11725 0
vsize: 48100
[startup+510.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 14894 0 0 0 50962 44 0 0 25 0 1 0 864892207 49254400 9174 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9174 300 300 0 11725 0
vsize: 48100
[startup+520.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 14922 0 0 0 51962 44 0 0 25 0 1 0 864892207 49254400 9201 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9201 300 300 0 11725 0
vsize: 48100
[startup+530.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 14949 0 0 0 52961 45 0 0 25 0 1 0 864892207 49254400 9227 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9227 300 300 0 11725 0
vsize: 48100
[startup+540.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 14977 0 0 0 53961 45 0 0 25 0 1 0 864892207 49254400 9253 4294967295 134512640 135726644 3221224576 3221221728 134606965 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9253 300 300 0 11725 0
vsize: 48100
[startup+550.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15004 0 0 0 54961 45 0 0 25 0 1 0 864892207 49254400 9279 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9279 300 300 0 11725 0
vsize: 48100
[startup+560.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15031 0 0 0 55961 45 0 0 25 0 1 0 864892207 49254400 9305 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9305 300 300 0 11725 0
vsize: 48100
[startup+570.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15058 0 0 0 56961 45 0 0 25 0 1 0 864892207 49254400 9331 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9331 300 300 0 11725 0
vsize: 48100
[startup+580.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15085 0 0 0 57961 45 0 0 25 0 1 0 864892207 49254400 9356 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9356 300 300 0 11725 0
vsize: 48100
[startup+590.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15112 0 0 0 58961 46 0 0 25 0 1 0 864892207 49254400 9382 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9382 300 300 0 11725 0
vsize: 48100
[startup+600.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15137 0 0 0 59961 46 0 0 25 0 1 0 864892207 49254400 9406 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9406 300 300 0 11725 0
vsize: 48100
[startup+610.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15167 0 0 0 60961 46 0 0 25 0 1 0 864892207 49254400 9435 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9435 300 300 0 11725 0
vsize: 48100
[startup+620.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15215 0 0 0 61961 46 0 0 25 0 1 0 864892207 49254400 9482 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9482 300 300 0 11725 0
vsize: 48100
[startup+630.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15239 0 0 0 62961 46 0 0 25 0 1 0 864892207 49254400 9505 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9505 300 300 0 11725 0
vsize: 48100
[startup+640.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15266 0 0 0 63962 46 0 0 25 0 1 0 864892207 49254400 9530 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9530 300 300 0 11725 0
vsize: 48100
[startup+650.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15290 0 0 0 64961 46 0 0 25 0 1 0 864892207 49254400 9553 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9553 300 300 0 11725 0
vsize: 48100
[startup+660.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15315 0 0 0 65961 46 0 0 25 0 1 0 864892207 49254400 9577 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9577 300 300 0 11725 0
vsize: 48100
[startup+670.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 15339 0 0 0 66962 47 0 0 25 0 1 0 864892207 49254400 9600 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 12025 9600 300 300 0 11725 0
vsize: 48100
[startup+680.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 43932 0 0 0 67899 109 0 0 25 0 1 0 864892207 158937088 32732 4294967295 134512640 135726644 3221224576 3168786192 134784885 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 38803 32737 300 300 0 38503 0
vsize: 155212
[startup+690.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 73971 0 0 0 68837 172 0 0 25 0 1 0 864892207 301457408 56988 4294967295 134512640 135726644 3221224576 3160452360 135282351 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 73598 56991 300 300 0 73298 0
vsize: 294392
[startup+700.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 100966 0 0 0 69780 228 0 0 25 0 1 0 864892207 327081984 68608 4294967295 134512640 135726644 3221224576 3166761264 134767123 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 79854 68608 300 300 0 79554 0
vsize: 319416
[startup+710.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 131195 0 0 0 70720 289 0 0 25 0 1 0 864892207 437055488 86340 4294967295 134512640 135726644 3221224576 3161459268 135289335 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 106703 86340 300 300 0 106403 0
vsize: 426812
[startup+720.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 172095 0 0 0 71642 367 0 0 25 0 1 0 864892207 570540032 107654 4294967295 134512640 135726644 3221224576 3162206464 134767231 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 139292 107654 300 300 0 138992 0
vsize: 557168
[startup+730.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 185492 0 0 0 72613 397 0 0 25 0 1 0 864892207 570540032 120816 4294967295 134512640 135726644 3221224576 3162760000 135284871 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 139292 120816 300 300 0 138992 0
vsize: 557168
[startup+740.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 224142 0 0 0 73529 481 0 0 25 0 1 0 864892207 716247040 134691 4294967295 134512640 135726644 3221224576 3162501600 134780348 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 174865 134691 300 300 0 174565 0
vsize: 699460
[startup+750.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 241541 0 0 0 74492 518 0 0 25 0 1 0 864892207 740982784 151891 4294967295 134512640 135726644 3221224576 3162209352 134784091 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 180904 151891 300 300 0 180604 0
vsize: 723616
[startup+760.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 262318 0 0 0 75442 568 0 0 25 0 1 0 864892207 771395584 172425 4294967295 134512640 135726644 3221224576 3160221352 134784091 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 188329 172426 300 300 0 188029 0
vsize: 753316
[startup+770.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 274687 0 0 0 76414 597 0 0 25 0 1 0 864892207 790016000 184653 4294967295 134512640 135726644 3221224576 3160789504 135298151 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 192875 184653 300 300 0 192575 0
vsize: 771500
[startup+780.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 274688 0 0 0 77414 597 0 0 25 0 1 0 864892207 790016000 184654 4294967295 134512640 135726644 3221224576 3221222556 134541595 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 192875 184654 300 300 0 192575 0
vsize: 771500
[startup+785.707 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 28226
Raw data (stat): 28226 (pb2sat) R 28225 20001 20000 0 -1 0 274688 0 0 0 77414 597 0 0 25 0 1 0 864892207 790016000 184654 4294967295 134512640 135726644 3221224576 3221222556 134541595 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 192875 184654 300 300 0 192575 0
vsize: 0

Child status: 1
Real time (s): 785.707
CPU time (s): 785.771
CPU user time (s): 779.418
CPU system time (s): 6.35203
CPU usage (%): 100.008
Max. virtual memory (Kb): 771500
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####