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/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-fit2p.opb
MD5SUM	5f5cb3c37eae37e49339d7674a999c27
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	172663
Biggest coefficient in the objective function	10485760
Number of bits for the biggest coefficient in the objective function	24
Sum of the numbers in the objective function	42533442284
Number of bits of the sum of numbers in the objective function	36
Biggest number in a constraint	30985420800
Number of bits of the biggest number in a constraint	35
Biggest sum of numbers in a constraint	101083836075
Number of bits of the biggest sum of numbers	37
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	1.9357
Number of variables	210852
Total number of constraints	10500
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	10500
Minimum length of a constraint	10
Maximum length of a constraint	413
Trace number 35561

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-05-28 13:12:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24745 boxname=wulflinc4 idbench=1217 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5f5cb3c37eae37e49339d7674a999c27  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-fit2p.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-fit2p.opb
IDLAUNCH: 24745
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
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:        695888 kB
Buffers:         33964 kB
Cached:         283568 kB
SwapCached:        640 kB
Active:          52224 kB
Inactive:       267532 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        695636 kB
SwapTotal:     2097136 kB
SwapFree:      2095656 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5304 kB
Slab:            13296 kB
Committed_AS:    71796 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 13:26:05 (client local time) WITH STATUS 0 IN 841.701 SECONDS
stats: 24745 7 841.701 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
#### 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.90 2/54 30809
Raw data (stat): 30809 (runsolver) R 30808 21152 21151 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 806835793 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+10.0008 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 2103 0 0 0 994 5 0 0 25 0 1 0 806835793 7819264 1429 4294967295 134512640 135726644 3221224592 3221221680 134556168 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 1909 1429 300 300 0 1609 0
vsize: 7636
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 2668 0 0 0 1992 7 0 0 25 0 1 0 806835793 9306112 1985 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 2272 1985 300 300 0 1972 0
vsize: 9088
[startup+30.0025 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 3849 0 0 0 2990 9 0 0 25 0 1 0 806835793 13410304 2454 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3274 2454 300 300 0 2974 0
vsize: 13096
[startup+40.0035 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 4086 0 0 0 3989 10 0 0 25 0 1 0 806835793 13950976 2686 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3406 2686 300 300 0 3106 0
vsize: 13624
[startup+50.0044 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 4343 0 0 0 4988 11 0 0 25 0 1 0 806835793 14626816 2939 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3571 2939 300 300 0 3271 0
vsize: 14284
[startup+60.0058 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 4573 0 0 0 5987 12 0 0 25 0 1 0 806835793 15302656 3165 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3736 3165 300 300 0 3436 0
vsize: 14944
[startup+70.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 4785 0 0 0 6986 13 0 0 25 0 1 0 806835793 15843328 3374 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 3868 3374 300 300 0 3568 0
vsize: 15472
[startup+80.0069 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 4982 0 0 0 7986 14 0 0 25 0 1 0 806835793 16384000 3568 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4000 3568 300 300 0 3700 0
vsize: 16000
[startup+90.0068 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 5170 0 0 0 8985 15 0 0 25 0 1 0 806835793 16789504 3753 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4099 3753 300 300 0 3799 0
vsize: 16396
[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 5347 0 0 0 9984 16 0 0 25 0 1 0 806835793 17330176 3927 4294967295 134512640 135726644 3221224592 3221221680 134556173 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.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 5515 0 0 0 10984 16 0 0 25 0 1 0 806835793 17735680 4092 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 4330 4092 300 300 0 4030 0
vsize: 17320
[startup+120.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 7497 0 0 0 11979 22 0 0 25 0 1 0 806835793 25403392 4662 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4662 300 300 0 5902 0
vsize: 24808
[startup+130.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 7553 0 0 0 12978 22 0 0 25 0 1 0 806835793 25403392 4715 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4715 300 300 0 5902 0
vsize: 24808
[startup+140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 7606 0 0 0 13978 23 0 0 25 0 1 0 806835793 25403392 4766 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4766 300 300 0 5902 0
vsize: 24808
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 7685 0 0 0 14978 23 0 0 25 0 1 0 806835793 25403392 4842 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6202 4842 300 300 0 5902 0
vsize: 24808
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 7735 0 0 0 15978 24 0 0 25 0 1 0 806835793 25538560 4890 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6235 4890 300 300 0 5935 0
vsize: 24940
[startup+170.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 7870 0 0 0 16978 24 0 0 25 0 1 0 806835793 25808896 5023 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6301 5023 300 300 0 6001 0
vsize: 25204
[startup+180.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 8001 0 0 0 17977 25 0 0 25 0 1 0 806835793 26214400 5152 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6400 5152 300 300 0 6100 0
vsize: 25600
[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 8130 0 0 0 18977 25 0 0 25 0 1 0 806835793 26484736 5279 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6466 5279 300 300 0 6166 0
vsize: 25864
[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 8254 0 0 0 19977 26 0 0 25 0 1 0 806835793 26890240 5401 4294967295 134512640 135726644 3221224592 3221221680 134556192 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6565 5401 300 300 0 6265 0
vsize: 26260
[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 8376 0 0 0 20976 27 0 0 25 0 1 0 806835793 27160576 5521 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6631 5521 300 300 0 6331 0
vsize: 26524
[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 8495 0 0 0 21976 27 0 0 25 0 1 0 806835793 27430912 5638 4294967295 134512640 135726644 3221224592 3221221680 134556168 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6697 5638 300 300 0 6397 0
vsize: 26788
[startup+230.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 8613 0 0 0 22976 28 0 0 25 0 1 0 806835793 27836416 5754 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6796 5754 300 300 0 6496 0
vsize: 27184
[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 8728 0 0 0 23976 28 0 0 25 0 1 0 806835793 28106752 5867 4294967295 134512640 135726644 3221224592 3221221680 134556187 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6862 5867 300 300 0 6562 0
vsize: 27448
[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 8840 0 0 0 24976 28 0 0 25 0 1 0 806835793 28377088 5977 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6928 5977 300 300 0 6628 0
vsize: 27712
[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 8949 0 0 0 25975 29 0 0 25 0 1 0 806835793 28647424 6085 4294967295 134512640 135726644 3221224592 3221221680 134556192 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 6994 6085 300 300 0 6694 0
vsize: 27976
[startup+270.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 9057 0 0 0 26974 30 0 0 25 0 1 0 806835793 28917760 6191 4294967295 134512640 135726644 3221224592 3221221288 135282351 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7060 6191 300 300 0 6760 0
vsize: 28240
[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 9163 0 0 0 27974 30 0 0 25 0 1 0 806835793 29188096 6295 4294967295 134512640 135726644 3221224592 3221221680 134556187 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7126 6295 300 300 0 6826 0
vsize: 28504
[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 9268 0 0 0 28974 31 0 0 25 0 1 0 806835793 29458432 6398 4294967295 134512640 135726644 3221224592 3221221680 134556192 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7192 6398 300 300 0 6892 0
vsize: 28768
[startup+300.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 9370 0 0 0 29973 32 0 0 25 0 1 0 806835793 29728768 6499 4294967295 134512640 135726644 3221224592 3221221680 134556179 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7258 6499 300 300 0 6958 0
vsize: 29032
[startup+310.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 9471 0 0 0 30973 33 0 0 25 0 1 0 806835793 29999104 6598 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7324 6598 300 300 0 7024 0
vsize: 29296
[startup+320.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 9569 0 0 0 31972 34 0 0 25 0 1 0 806835793 30269440 6695 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7390 6695 300 300 0 7090 0
vsize: 29560
[startup+330.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 9669 0 0 0 32972 34 0 0 25 0 1 0 806835793 30539776 6793 4294967295 134512640 135726644 3221224592 3221221680 134556187 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7456 6793 300 300 0 7156 0
vsize: 29824
[startup+340.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 9766 0 0 0 33982 35 0 0 25 0 1 0 806835793 30810112 6888 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7522 6888 300 300 0 7222 0
vsize: 30088
[startup+350.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 9861 0 0 0 34981 35 0 0 25 0 1 0 806835793 31080448 6982 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7588 6982 300 300 0 7288 0
vsize: 30352
[startup+360.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 9954 0 0 0 35981 36 0 0 25 0 1 0 806835793 31350784 7073 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7654 7073 300 300 0 7354 0
vsize: 30616
[startup+370.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 10047 0 0 0 36980 36 0 0 25 0 1 0 806835793 31621120 7165 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7720 7165 300 300 0 7420 0
vsize: 30880
[startup+380.152 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 10139 0 0 0 37982 37 0 0 25 0 1 0 806835793 31891456 7255 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7786 7255 300 300 0 7486 0
vsize: 31144
[startup+390.151 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 10229 0 0 0 38981 37 0 0 25 0 1 0 806835793 32026624 7344 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7819 7344 300 300 0 7519 0
vsize: 31276
[startup+400.152 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 10319 0 0 0 39981 38 0 0 25 0 1 0 806835793 32296960 7432 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7885 7432 300 300 0 7585 0
vsize: 31540
[startup+410.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 10406 0 0 0 40980 38 0 0 25 0 1 0 806835793 32567296 7518 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7951 7518 300 300 0 7651 0
vsize: 31804
[startup+420.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 10493 0 0 0 41981 39 0 0 25 0 1 0 806835793 32702464 7604 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 7984 7604 300 300 0 7684 0
vsize: 31936
[startup+430.154 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 10581 0 0 0 42980 39 0 0 25 0 1 0 806835793 32972800 7690 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8050 7690 300 300 0 7750 0
vsize: 32200
[startup+440.154 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 10664 0 0 0 43980 40 0 0 25 0 1 0 806835793 33243136 7772 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8116 7772 300 300 0 7816 0
vsize: 32464
[startup+450.153 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 10749 0 0 0 44980 40 0 0 25 0 1 0 806835793 33378304 7856 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8149 7856 300 300 0 7849 0
vsize: 32596
[startup+460.155 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 10833 0 0 0 45979 41 0 0 25 0 1 0 806835793 33648640 7938 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8215 7938 300 300 0 7915 0
vsize: 32860
[startup+470.163 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 10915 0 0 0 46979 41 0 0 25 0 1 0 806835793 33918976 8019 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 8281 8019 300 300 0 7981 0
vsize: 33124
[startup+480.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 14816 0 0 0 47972 49 0 0 25 0 1 0 806835793 49254400 9101 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9101 300 300 0 11725 0
vsize: 48100
[startup+490.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 14845 0 0 0 48972 49 0 0 25 0 1 0 806835793 49254400 9128 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9128 300 300 0 11725 0
vsize: 48100
[startup+500.164 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 14874 0 0 0 49972 49 0 0 25 0 1 0 806835793 49254400 9156 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9156 300 300 0 11725 0
vsize: 48100
[startup+510.165 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 14902 0 0 0 50972 50 0 0 25 0 1 0 806835793 49254400 9183 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9183 300 300 0 11725 0
vsize: 48100
[startup+520.165 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 14930 0 0 0 51971 50 0 0 25 0 1 0 806835793 49254400 9209 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9209 300 300 0 11725 0
vsize: 48100
[startup+530.166 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 14957 0 0 0 52971 50 0 0 25 0 1 0 806835793 49254400 9235 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9235 300 300 0 11725 0
vsize: 48100
[startup+540.166 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 14985 0 0 0 53971 51 0 0 25 0 1 0 806835793 49254400 9262 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9262 300 300 0 11725 0
vsize: 48100
[startup+550.167 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15012 0 0 0 54971 51 0 0 25 0 1 0 806835793 49254400 9288 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9288 300 300 0 11725 0
vsize: 48100
[startup+560.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15038 0 0 0 55970 52 0 0 25 0 1 0 806835793 49254400 9313 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9313 300 300 0 11725 0
vsize: 48100
[startup+570.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15065 0 0 0 56970 53 0 0 25 0 1 0 806835793 49254400 9338 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9338 300 300 0 11725 0
vsize: 48100
[startup+580.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15091 0 0 0 57970 53 0 0 25 0 1 0 806835793 49254400 9363 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9363 300 300 0 11725 0
vsize: 48100
[startup+590.168 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15118 0 0 0 58969 53 0 0 25 0 1 0 806835793 49254400 9389 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9389 300 300 0 11725 0
vsize: 48100
[startup+600.167 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15144 0 0 0 59969 53 0 0 25 0 1 0 806835793 49254400 9414 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9414 300 300 0 11725 0
vsize: 48100
[startup+610.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15181 0 0 0 60969 54 0 0 25 0 1 0 806835793 49254400 9450 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9450 300 300 0 11725 0
vsize: 48100
[startup+620.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15221 0 0 0 61969 54 0 0 25 0 1 0 806835793 49254400 9488 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9488 300 300 0 11725 0
vsize: 48100
[startup+630.169 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15247 0 0 0 62970 54 0 0 25 0 1 0 806835793 49254400 9513 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9513 300 300 0 11725 0
vsize: 48100
[startup+640.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15271 0 0 0 63969 54 0 0 25 0 1 0 806835793 49254400 9536 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9536 300 300 0 11725 0
vsize: 48100
[startup+650.17 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15297 0 0 0 64969 55 0 0 25 0 1 0 806835793 49254400 9561 4294967295 134512640 135726644 3221224592 3221221680 134556179 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9561 300 300 0 11725 0
vsize: 48100
[startup+660.171 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15321 0 0 0 65969 55 0 0 25 0 1 0 806835793 49254400 9584 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12025 9584 300 300 0 11725 0
vsize: 48100
[startup+670.171 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15357 0 0 0 66969 55 0 0 25 0 1 0 806835793 49389568 9619 4294967295 134512640 135726644 3221224592 3221221680 134556195 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12058 9619 300 300 0 11758 0
vsize: 48232
[startup+680.172 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15426 0 0 0 67969 56 0 0 25 0 1 0 806835793 49524736 9687 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12091 9687 300 300 0 11791 0
vsize: 48364
[startup+690.172 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15496 0 0 0 68969 56 0 0 25 0 1 0 806835793 49795072 9755 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12157 9755 300 300 0 11857 0
vsize: 48628
[startup+700.173 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15563 0 0 0 69968 56 0 0 25 0 1 0 806835793 49930240 9821 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12190 9821 300 300 0 11890 0
vsize: 48760
[startup+710.173 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15630 0 0 0 70968 57 0 0 25 0 1 0 806835793 50065408 9887 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12223 9887 300 300 0 11923 0
vsize: 48892
[startup+720.173 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15698 0 0 0 71968 57 0 0 25 0 1 0 806835793 50200576 9954 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12256 9954 300 300 0 11956 0
vsize: 49024
[startup+730.174 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15763 0 0 0 72967 58 0 0 25 0 1 0 806835793 50470912 10018 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12322 10018 300 300 0 12022 0
vsize: 49288
[startup+740.175 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15830 0 0 0 73967 58 0 0 25 0 1 0 806835793 50606080 10084 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12355 10084 300 300 0 12055 0
vsize: 49420
[startup+750.175 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15895 0 0 0 74967 59 0 0 25 0 1 0 806835793 50741248 10148 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12388 10148 300 300 0 12088 0
vsize: 49552
[startup+760.176 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 15961 0 0 0 75966 60 0 0 25 0 1 0 806835793 51011584 10213 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12454 10213 300 300 0 12154 0
vsize: 49816
[startup+770.176 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 16025 0 0 0 76965 60 0 0 25 0 1 0 806835793 51146752 10276 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12487 10276 300 300 0 12187 0
vsize: 49948
[startup+780.176 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 16090 0 0 0 77965 61 0 0 25 0 1 0 806835793 51281920 10340 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12520 10340 300 300 0 12220 0
vsize: 50080
[startup+790.183 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 16153 0 0 0 78965 61 0 0 25 0 1 0 806835793 51417088 10402 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12553 10402 300 300 0 12253 0
vsize: 50212
[startup+800.183 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 16217 0 0 0 79965 62 0 0 25 0 1 0 806835793 51687424 10465 4294967295 134512640 135726644 3221224592 3221221680 134556171 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12619 10465 300 300 0 12319 0
vsize: 50476
[startup+810.189 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 16280 0 0 0 80965 63 0 0 25 0 1 0 806835793 51822592 10527 4294967295 134512640 135726644 3221224592 3221221680 134556173 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12652 10527 300 300 0 12352 0
vsize: 50608
[startup+820.195 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 16343 0 0 0 81964 64 0 0 25 0 1 0 806835793 51957760 10589 4294967295 134512640 135726644 3221224592 3221221680 134556168 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12685 10589 300 300 0 12385 0
vsize: 50740
[startup+830.196 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 16406 0 0 0 82964 64 0 0 25 0 1 0 806835793 52092928 10651 4294967295 134512640 135726644 3221224592 3221221680 134556160 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 12718 10651 300 300 0 12418 0
vsize: 50872
[startup+840.197 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 42161 0 0 0 83907 122 0 0 25 0 1 0 806835793 146407424 30962 4294967295 134512640 135726644 3221224592 3175981056 134558066 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 35745 30963 300 300 0 35445 0
vsize: 142976
[startup+841.602 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 30809
Raw data (stat): 30809 (pb2sat) R 30808 21152 21151 0 -1 0 42161 0 0 0 83907 122 0 0 25 0 1 0 806835793 146407424 30962 4294967295 134512640 135726644 3221224592 3175981056 134558066 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 35745 30963 300 300 0 35445 0
vsize: 0

Child ended because it received signal 11 (SIGSEGV)
Real time (s): 841.602
CPU time (s): 841.701
CPU user time (s): 840.206
CPU system time (s): 1.49477
CPU usage (%): 100.012
Max. virtual memory (Kb): 142976
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####