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-n3700.opb
MD5SUM	bc3b48d8361bf44c5b17a3bc4d19364a
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	29631666774144
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	29631666774144
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.42678
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 35322

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-05-28 12:42:44 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24606 boxname=wulflinc27 idbench=1078 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  bc3b48d8361bf44c5b17a3bc4d19364a  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-n3700.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-20-10-n3700.opb
IDLAUNCH: 24606
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        691412 kB
Buffers:         34248 kB
Cached:         277984 kB
SwapCached:        704 kB
Active:          32056 kB
Inactive:       282308 kB
HighTotal:      131008 kB
HighFree:        23296 kB
LowTotal:       903652 kB
LowFree:        668116 kB
SwapTotal:     2097892 kB
SwapFree:      2096316 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5128 kB
Slab:            23104 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-28 12:55:54 (client local time) WITH STATUS 1 IN 789.377 SECONDS
stats: 24606 7 789.377 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.93 0.90 2/54 20180
Raw data (stat): 20180 (runsolver) R 20179 3394 3393 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 864884181 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.0002 s]
Raw data (loadavg): 0.93 0.93 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 2163 0 0 0 993 5 0 0 25 0 1 0 864884181 7954432 1487 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1942 1487 300 300 0 1642 0
vsize: 7768
[startup+20.001 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 2695 0 0 0 1991 8 0 0 25 0 1 0 864884181 9306112 2011 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2272 2011 300 300 0 1972 0
vsize: 9088
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 3876 0 0 0 2988 11 0 0 25 0 1 0 864884181 13410304 2479 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3274 2479 300 300 0 2974 0
vsize: 13096
[startup+40.0006 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 4127 0 0 0 3987 12 0 0 25 0 1 0 864884181 14086144 2726 4294967295 134512640 135726644 3221224576 3221221520 134541091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3439 2726 300 300 0 3139 0
vsize: 13756
[startup+50.0015 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 4381 0 0 0 4986 13 0 0 25 0 1 0 864884181 14761984 2975 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3604 2975 300 300 0 3304 0
vsize: 14416
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 4604 0 0 0 5985 14 0 0 25 0 1 0 864884181 15302656 3195 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3736 3195 300 300 0 3436 0
vsize: 14944
[startup+70.0021 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 4806 0 0 0 6984 15 0 0 25 0 1 0 864884181 15843328 3394 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3868 3394 300 300 0 3568 0
vsize: 15472
[startup+80.0036 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 4997 0 0 0 7984 16 0 0 25 0 1 0 864884181 16384000 3582 4294967295 134512640 135726644 3221224576 3221221472 134543511 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4000 3582 300 300 0 3700 0
vsize: 16000
[startup+90.0112 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 5176 0 0 0 8984 17 0 0 25 0 1 0 864884181 16789504 3758 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4099 3758 300 300 0 3799 0
vsize: 16396
[startup+100.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 5347 0 0 0 9983 18 0 0 25 0 1 0 864884181 17330176 3926 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4231 3926 300 300 0 3931 0
vsize: 16924
[startup+110.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 5511 0 0 0 10982 19 0 0 25 0 1 0 864884181 17735680 4087 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4330 4087 300 300 0 4030 0
vsize: 17320
[startup+120.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 7495 0 0 0 11977 24 0 0 25 0 1 0 864884181 25403392 4659 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4659 300 300 0 5902 0
vsize: 24808
[startup+130.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 7550 0 0 0 12977 24 0 0 25 0 1 0 864884181 25403392 4711 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4711 300 300 0 5902 0
vsize: 24808
[startup+140.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 7602 0 0 0 13976 25 0 0 25 0 1 0 864884181 25403392 4761 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4761 300 300 0 5902 0
vsize: 24808
[startup+150.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 7679 0 0 0 14976 26 0 0 25 0 1 0 864884181 25403392 4836 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4836 300 300 0 5902 0
vsize: 24808
[startup+160.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 7729 0 0 0 15975 26 0 0 25 0 1 0 864884181 25403392 4883 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4883 300 300 0 5902 0
vsize: 24808
[startup+170.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 7854 0 0 0 16975 27 0 0 25 0 1 0 864884181 25808896 5006 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6301 5006 300 300 0 6001 0
vsize: 25204
[startup+180.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 7985 0 0 0 17974 28 0 0 25 0 1 0 864884181 26079232 5135 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6367 5135 300 300 0 6067 0
vsize: 25468
[startup+190.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 8112 0 0 0 18973 29 0 0 25 0 1 0 864884181 26484736 5260 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6466 5260 300 300 0 6166 0
vsize: 25864
[startup+200.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 8237 0 0 0 19973 29 0 0 25 0 1 0 864884181 26755072 5383 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6532 5383 300 300 0 6232 0
vsize: 26128
[startup+210.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 8359 0 0 0 20972 30 0 0 25 0 1 0 864884181 27160576 5503 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6631 5503 300 300 0 6331 0
vsize: 26524
[startup+220.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 8477 0 0 0 21972 31 0 0 25 0 1 0 864884181 27430912 5619 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6697 5619 300 300 0 6397 0
vsize: 26788
[startup+230.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 8593 0 0 0 22972 31 0 0 25 0 1 0 864884181 27701248 5733 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6763 5733 300 300 0 6463 0
vsize: 27052
[startup+240.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 8708 0 0 0 23970 32 0 0 25 0 1 0 864884181 28106752 5846 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6862 5846 300 300 0 6562 0
vsize: 27448
[startup+250.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 8819 0 0 0 24970 33 0 0 25 0 1 0 864884181 28377088 5956 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6928 5956 300 300 0 6628 0
vsize: 27712
[startup+260.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 8928 0 0 0 25970 34 0 0 25 0 1 0 864884181 28647424 6063 4294967295 134512640 135726644 3221224576 3221221664 134556168 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6994 6063 300 300 0 6694 0
vsize: 27976
[startup+270.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 9036 0 0 0 26970 34 0 0 25 0 1 0 864884181 28917760 6169 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7060 6169 300 300 0 6760 0
vsize: 28240
[startup+280.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 9142 0 0 0 27969 35 0 0 25 0 1 0 864884181 29188096 6273 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7126 6273 300 300 0 6826 0
vsize: 28504
[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 9245 0 0 0 28969 35 0 0 25 0 1 0 864884181 29458432 6375 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7192 6375 300 300 0 6892 0
vsize: 28768
[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 9348 0 0 0 29968 36 0 0 25 0 1 0 864884181 29728768 6476 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7258 6476 300 300 0 6958 0
vsize: 29032
[startup+310.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 9447 0 0 0 30968 36 0 0 25 0 1 0 864884181 29999104 6574 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7324 6574 300 300 0 7024 0
vsize: 29296
[startup+320.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 9546 0 0 0 31968 37 0 0 25 0 1 0 864884181 30269440 6671 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7390 6671 300 300 0 7090 0
vsize: 29560
[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 9644 0 0 0 32967 37 0 0 25 0 1 0 864884181 30539776 6767 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7456 6767 300 300 0 7156 0
vsize: 29824
[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 9738 0 0 0 33966 38 0 0 25 0 1 0 864884181 30810112 6860 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7522 6860 300 300 0 7222 0
vsize: 30088
[startup+350.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 9833 0 0 0 34966 39 0 0 25 0 1 0 864884181 31080448 6953 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7588 6953 300 300 0 7288 0
vsize: 30352
[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 9926 0 0 0 35965 40 0 0 25 0 1 0 864884181 31215616 7045 4294967295 134512640 135726644 3221224576 3221221664 134556181 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7621 7045 300 300 0 7321 0
vsize: 30484
[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 10019 0 0 0 36964 41 0 0 25 0 1 0 864884181 31485952 7136 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7687 7136 300 300 0 7387 0
vsize: 30748
[startup+380.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 10109 0 0 0 37964 42 0 0 25 0 1 0 864884181 31756288 7225 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7753 7225 300 300 0 7453 0
vsize: 31012
[startup+390.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 10199 0 0 0 38963 42 0 0 25 0 1 0 864884181 32026624 7313 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7819 7313 300 300 0 7519 0
vsize: 31276
[startup+400.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 10287 0 0 0 39962 43 0 0 25 0 1 0 864884181 32161792 7400 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7852 7400 300 300 0 7552 0
vsize: 31408
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 10374 0 0 0 40962 44 0 0 25 0 1 0 864884181 32432128 7486 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7918 7486 300 300 0 7618 0
vsize: 31672
[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 10462 0 0 0 41962 44 0 0 25 0 1 0 864884181 32702464 7572 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7984 7572 300 300 0 7684 0
vsize: 31936
[startup+430.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 10547 0 0 0 42961 45 0 0 25 0 1 0 864884181 32837632 7656 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8017 7656 300 300 0 7717 0
vsize: 32068
[startup+440.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 10632 0 0 0 43961 45 0 0 25 0 1 0 864884181 33107968 7739 4294967295 134512640 135726644 3221224576 3221221464 135280655 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8083 7739 300 300 0 7783 0
vsize: 32332
[startup+450.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 10715 0 0 0 44960 46 0 0 25 0 1 0 864884181 33378304 7821 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8149 7821 300 300 0 7849 0
vsize: 32596
[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 10798 0 0 0 45960 46 0 0 25 0 1 0 864884181 33513472 7903 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8182 7903 300 300 0 7882 0
vsize: 32728
[startup+470.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 10881 0 0 0 46960 47 0 0 25 0 1 0 864884181 33783808 7984 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8248 7984 300 300 0 7948 0
vsize: 32992
[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 10961 0 0 0 47959 48 0 0 25 0 1 0 864884181 34054144 8063 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8314 8063 300 300 0 8014 0
vsize: 33256
[startup+490.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 14833 0 0 0 48952 55 0 0 25 0 1 0 864884181 49254400 9116 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9116 300 300 0 11725 0
vsize: 48100
[startup+500.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 14861 0 0 0 49952 55 0 0 25 0 1 0 864884181 49254400 9143 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9143 300 300 0 11725 0
vsize: 48100
[startup+510.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 14889 0 0 0 50952 55 0 0 25 0 1 0 864884181 49254400 9169 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9169 300 300 0 11725 0
vsize: 48100
[startup+520.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 14917 0 0 0 51952 56 0 0 25 0 1 0 864884181 49254400 9196 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9196 300 300 0 11725 0
vsize: 48100
[startup+530.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 14944 0 0 0 52951 56 0 0 25 0 1 0 864884181 49254400 9222 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9222 300 300 0 11725 0
vsize: 48100
[startup+540.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 14971 0 0 0 53951 57 0 0 25 0 1 0 864884181 49254400 9248 4294967295 134512640 135726644 3221224576 3221221664 134556192 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9248 300 300 0 11725 0
vsize: 48100
[startup+550.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 14999 0 0 0 54951 57 0 0 25 0 1 0 864884181 49254400 9274 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9274 300 300 0 11725 0
vsize: 48100
[startup+560.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 15025 0 0 0 55950 58 0 0 25 0 1 0 864884181 49254400 9299 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9299 300 300 0 11725 0
vsize: 48100
[startup+570.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 15052 0 0 0 56951 58 0 0 25 0 1 0 864884181 49254400 9325 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9325 300 300 0 11725 0
vsize: 48100
[startup+580.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 15078 0 0 0 57950 58 0 0 25 0 1 0 864884181 49254400 9350 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9350 300 300 0 11725 0
vsize: 48100
[startup+590.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 15103 0 0 0 58950 58 0 0 25 0 1 0 864884181 49254400 9374 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9374 300 300 0 11725 0
vsize: 48100
[startup+600.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 15130 0 0 0 59950 59 0 0 25 0 1 0 864884181 49254400 9399 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9399 300 300 0 11725 0
vsize: 48100
[startup+610.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 15156 0 0 0 60950 59 0 0 25 0 1 0 864884181 49254400 9424 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9424 300 300 0 11725 0
vsize: 48100
[startup+620.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 15204 0 0 0 61950 60 0 0 25 0 1 0 864884181 49254400 9471 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9471 300 300 0 11725 0
vsize: 48100
[startup+630.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 15232 0 0 0 62949 60 0 0 25 0 1 0 864884181 49254400 9498 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9498 300 300 0 11725 0
vsize: 48100
[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 15256 0 0 0 63949 61 0 0 25 0 1 0 864884181 49254400 9521 4294967295 134512640 135726644 3221224576 3221221664 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9521 300 300 0 11725 0
vsize: 48100
[startup+650.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 15282 0 0 0 64949 61 0 0 25 0 1 0 864884181 49254400 9546 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9546 300 300 0 11725 0
vsize: 48100
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 15306 0 0 0 65948 62 0 0 25 0 1 0 864884181 49254400 9569 4294967295 134512640 135726644 3221224576 3221221664 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9569 300 300 0 11725 0
vsize: 48100
[startup+670.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 15331 0 0 0 66948 62 0 0 25 0 1 0 864884181 49254400 9592 4294967295 134512640 135726644 3221224576 3221221664 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9592 300 300 0 11725 0
vsize: 48100
[startup+680.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 21364 0 0 0 67934 76 0 0 25 0 1 0 864884181 71340032 15451 4294967295 134512640 135726644 3221224576 3209408464 134766539 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 17417 15451 300 300 0 17117 0
vsize: 69668
[startup+690.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 62596 0 0 0 68837 173 0 0 25 0 1 0 864884181 214335488 45864 4294967295 134512640 135726644 3221224576 3162711600 134780435 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 52328 45864 300 300 0 52028 0
vsize: 209312
[startup+700.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 94904 0 0 0 69770 241 0 0 25 0 1 0 864884181 325054464 62640 4294967295 134512640 135726644 3221224576 3161406928 134554691 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 79359 62640 300 300 0 79059 0
vsize: 317436
[startup+710.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 124124 0 0 0 70706 305 0 0 25 0 1 0 864884181 393363456 79355 4294967295 134512640 135726644 3221224576 3166815408 135280446 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 96036 79355 300 300 0 95736 0
vsize: 384144
[startup+720.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 147893 0 0 0 71653 358 0 0 25 0 1 0 864884181 602509312 102683 4294967295 134512640 135726644 3221224576 3162042960 134771796 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 147097 102683 300 300 0 146797 0
vsize: 588388
[startup+730.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 179689 0 0 0 72590 422 0 0 25 0 1 0 864884181 570675200 115115 4294967295 134512640 135726644 3221224576 3159993260 134556948 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 139325 115115 300 300 0 139025 0
vsize: 557300
[startup+740.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 215719 0 0 0 73509 503 0 0 25 0 1 0 864884181 671338496 126367 4294967295 134512640 135726644 3221224576 3160678480 134782584 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 163901 126367 300 300 0 163601 0
vsize: 655604
[startup+750.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 234126 0 0 0 74463 549 0 0 25 0 1 0 864884181 731521024 144548 4294967295 134512640 135726644 3221224576 3162172952 134784091 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 178594 144548 300 300 0 178294 0
vsize: 714376
[startup+760.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 253951 0 0 0 75418 594 0 0 25 0 1 0 864884181 760041472 164147 4294967295 134512640 135726644 3221224576 3161521148 135287576 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 185557 164147 300 300 0 185257 0
vsize: 742228
[startup+770.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 273809 0 0 0 76373 639 0 0 25 0 1 0 864884181 788156416 183777 4294967295 134512640 135726644 3221224576 3161246080 134782642 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 192421 183778 300 300 0 192121 0
vsize: 769684
[startup+780.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 274042 0 0 0 77373 640 0 0 25 0 1 0 864884181 789340160 184008 4294967295 134512640 135726644 3221224576 3198235092 135298515 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 192710 184008 300 300 0 192410 0
vsize: 770840
[startup+789.295 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 20180
Raw data (stat): 20180 (pb2sat) R 20179 3394 3393 0 -1 0 274042 0 0 0 77373 640 0 0 25 0 1 0 864884181 789340160 184008 4294967295 134512640 135726644 3221224576 3198235092 135298515 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 192710 184008 300 300 0 192410 0
vsize: 0

Child status: 1
Real time (s): 789.294
CPU time (s): 789.377
CPU user time (s): 782.614
CPU system time (s): 6.76297
CPU usage (%): 100.01
Max. virtual memory (Kb): 770840
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####