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/web/uclid_pb_benchmarks/normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb
MD5SUM	89f41bbcf2b70665bd7071c5b58e0ec8
Bench Category	no optimization function (SAT)
Has Objective Function	NO
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	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	129
Number of bits of the biggest number in a constraint	8
Biggest sum of numbers in a constraint	510
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	95.1845
Number of variables	49621
Total number of constraints	138346
Number of constraints which are clauses	127390
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	10956
Minimum length of a constraint	1
Maximum length of a constraint	15

Trace number 34928

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-05-28 11:15:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=24227 boxname=wulflinc7 idbench=301 idsolver=17 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  89f41bbcf2b70665bd7071c5b58e0ec8  /oldhome/oroussel/tmp/wulflinc7/normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb
REAL COMMAND:  pb2sat /oldhome/oroussel/tmp/wulflinc7/normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb
IDLAUNCH: 24227
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        751788 kB
Buffers:         35728 kB
Cached:         225496 kB
SwapCached:        644 kB
Active:          25448 kB
Inactive:       237768 kB
HighTotal:      131008 kB
HighFree:        28112 kB
LowTotal:       903652 kB
LowFree:        723676 kB
SwapTotal:     2097136 kB
SwapFree:      2095560 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            13848 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-28 11:22:36 (client local time) WITH STATUS 20 IN 455.755 SECONDS
stats: 24227 7 455.755 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c This solver internally uses Chaff 2004.11.15 Simplified
c running zchaff...

Decision: 16787/255623	Time: 22.3866/86400
Decision: 16790/255623	Time: 43.6034/86400
Decision: 16791/255623	Time: 58.0662/86400
Decision: 16791/255623	Time: 66.5499/86400
Decision: 16791/255623	Time: 73.7518/86400
Decision: 16791/255623	Time: 84.6791/86400
Decision: 16791/255623	Time: 94.7096/86400
Decision: 16791/255623	Time: 104.597/86400
Decision: 16791/255623	Time: 115.668/86400
Decision: 16791/255623	Time: 125.248/86400
Decision: 18105/255623	Time: 141.793/86400
Decision: 18105/255623	Time: 149.918/86400
Decision: 18105/255623	Time: 159.24/86400
Decision: 18105/255623	Time: 169.457/86400
Decision: 18105/255623	Time: 179.751/86400
Decision: 18105/255623	Time: 190.546/86400
Decision: 20495/255623	Time: 200.953/86400
Decision: 20498/255623	Time: 220.121/86400
Decision: 20498/255623	Time: 234.156/86400
Decision: 20498/255623	Time: 245.388/86400
Decision: 20498/255623	Time: 260.205/86400
Decision: 20501/255623	Time: 283.192/86400
Decision: 20600/255623	Time: 300.64/86400
Decision: 24158/255623	Time: 316.308/86400
Decision: 24158/255623	Time: 326.71/86400
Decision: 24158/255623	Time: 332.814/86400
Decision: 24208/255623	Time: 348.67/86400
Decision: 25382/255623	Time: 364.317/86400
Decision: 27723/255623	Time: 389.444/86400
Decision: 27742/255623	Time: 399.102/86400
Decision: 27742/255623	Time: 405.811/86400
Decision: 27806/255623	Time: 411.968/86400
Decision: 27806/255623	Time: 417.649/86400
Decision: 27806/255623	Time: 423.033/86400
Decision: 27806/255623	Time: 428.475/86400s UNSATISFIABLE
#### 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.96 0.91 2/54 7806
Raw data (stat): 7806 (runsolver) R 7805 24300 24299 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 806150347 884736 94 4294967295 134512640 135332820 3221224448 3221219628 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.0005 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 5340 0 0 0 982 15 0 0 25 0 1 0 806150347 17457152 3408 4294967295 134512640 135726644 3221224576 3221221520 134541181 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 4262 3408 300 300 0 3962 0
vsize: 17048
[startup+20.0012 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 25037 0 0 0 1934 63 0 0 25 0 1 0 806150347 78753792 13911 4294967295 134512640 135726644 3221224576 3221221728 134573143 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 19227 13911 300 300 0 18927 0
vsize: 76908
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 30252 0 0 0 2919 77 0 0 25 0 1 0 806150347 89460736 18581 4294967295 134512640 135726644 3221224576 3221223232 134731206 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 21841 18581 300 300 0 21541 0
vsize: 87364
[startup+40.0015 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 30919 0 0 0 3917 79 0 0 25 0 1 0 806150347 92954624 19248 4294967295 134512640 135726644 3221224576 3221223072 134744063 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 22694 19248 300 300 0 22394 0
vsize: 90776
[startup+50.0021 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 31639 0 0 0 4915 81 0 0 25 0 1 0 806150347 94040064 19468 4294967295 134512640 135726644 3221224576 3221223072 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 22959 19468 300 300 0 22659 0
vsize: 91836
[startup+60.0021 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 31827 0 0 0 5914 83 0 0 25 0 1 0 806150347 94826496 19656 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 23151 19656 300 300 0 22851 0
vsize: 92604
[startup+70.0024 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 32410 0 0 0 6911 86 0 0 25 0 1 0 806150347 95383552 19739 4294967295 134512640 135726644 3221224576 3221223072 134743953 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 23287 19739 300 300 0 22987 0
vsize: 93148
[startup+80.0034 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 32962 0 0 0 7909 88 0 0 25 0 1 0 806150347 95580160 19791 4294967295 134512640 135726644 3221224576 3221222992 134738149 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 23335 19791 300 300 0 23035 0
vsize: 93340
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 33619 0 0 0 8906 91 0 0 25 0 1 0 806150347 96210944 19948 4294967295 134512640 135726644 3221224576 3221223200 134744659 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 23489 19948 300 300 0 23189 0
vsize: 93956
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 34216 0 0 0 9904 93 0 0 25 0 1 0 806150347 96407552 20045 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 23537 20045 300 300 0 23237 0
vsize: 94148
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 34825 0 0 0 10903 95 0 0 25 0 1 0 806150347 96935936 20154 4294967295 134512640 135726644 3221224576 3221223232 134731175 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 23666 20154 300 300 0 23366 0
vsize: 94664
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 35421 0 0 0 11901 97 0 0 25 0 1 0 806150347 97402880 20250 4294967295 134512640 135726644 3221224576 3221223072 134744036 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 23780 20250 300 300 0 23480 0
vsize: 95120
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 35995 0 0 0 12899 99 0 0 25 0 1 0 806150347 97673216 20324 4294967295 134512640 135726644 3221224576 3221223072 134744063 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 23846 20324 300 300 0 23546 0
vsize: 95384
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 36540 0 0 0 13896 102 0 0 25 0 1 0 806150347 97673216 20369 4294967295 134512640 135726644 3221224576 3221222896 134728934 0 0 7 16384 0 0 0 17 1 0 0
Raw data (statm): 23846 20369 300 300 0 23546 0
vsize: 95384
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 37112 0 0 0 14895 103 0 0 25 0 1 0 806150347 97869824 20441 4294967295 134512640 135726644 3221224576 3221222896 134728892 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 23894 20441 300 300 0 23594 0
vsize: 95576
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 37158 0 0 0 15894 104 0 0 25 0 1 0 806150347 98066432 20487 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 23942 20487 300 300 0 23642 0
vsize: 95768
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 37723 0 0 0 16893 106 0 0 25 0 1 0 806150347 98336768 20552 4294967295 134512640 135726644 3221224576 3221223072 134743953 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24008 20552 300 300 0 23708 0
vsize: 96032
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 38229 0 0 0 17891 108 0 0 25 0 1 0 806150347 98336768 20558 4294967295 134512640 135726644 3221224576 3221223072 134744051 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24008 20558 300 300 0 23708 0
vsize: 96032
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 38740 0 0 0 18889 110 0 0 25 0 1 0 806150347 98336768 20569 4294967295 134512640 135726644 3221224576 3221223200 134744557 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24008 20569 300 300 0 23708 0
vsize: 96032
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 39255 0 0 0 19886 112 0 0 25 0 1 0 806150347 98336768 20584 4294967295 134512640 135726644 3221224576 3221223072 134744163 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24008 20584 300 300 0 23708 0
vsize: 96032
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 39806 0 0 0 20884 115 0 0 25 0 1 0 806150347 98603008 20635 4294967295 134512640 135726644 3221224576 3221223072 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24073 20635 300 300 0 23773 0
vsize: 96292
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 40324 0 0 0 21882 117 0 0 25 0 1 0 806150347 98603008 20653 4294967295 134512640 135726644 3221224576 3221223072 134743951 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24073 20653 300 300 0 23773 0
vsize: 96292
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 40851 0 0 0 22880 119 0 0 25 0 1 0 806150347 98603008 20680 4294967295 134512640 135726644 3221224576 3221222896 134728892 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24073 20680 300 300 0 23773 0
vsize: 96292
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 40886 0 0 0 23880 120 0 0 25 0 1 0 806150347 98603008 20715 4294967295 134512640 135726644 3221224576 3221223072 134743901 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24073 20715 300 300 0 23773 0
vsize: 96292
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 41467 0 0 0 24877 123 0 0 25 0 1 0 806150347 99000320 20796 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24170 20796 300 300 0 23870 0
vsize: 96680
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 42170 0 0 0 25874 126 0 0 25 0 1 0 806150347 100216832 20999 4294967295 134512640 135726644 3221224576 3221223072 134743955 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24467 20999 300 300 0 24167 0
vsize: 97868
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 42695 0 0 0 26871 129 0 0 25 0 1 0 806150347 100216832 21024 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24467 21024 300 300 0 24167 0
vsize: 97868
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 42762 0 0 0 27870 130 0 0 25 0 1 0 806150347 100487168 21091 4294967295 134512640 135726644 3221224576 3221223072 134743901 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24533 21091 300 300 0 24233 0
vsize: 98132
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 43314 0 0 0 28868 132 0 0 25 0 1 0 806150347 100757504 21143 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21143 300 300 0 24299 0
vsize: 98396
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 43329 0 0 0 29867 134 0 0 25 0 1 0 806150347 100757504 21158 4294967295 134512640 135726644 3221224576 3221223072 134743980 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21158 300 300 0 24299 0
vsize: 98396
[startup+310.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 43832 0 0 0 30865 136 0 0 25 0 1 0 806150347 100757504 21161 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21161 300 300 0 24299 0
vsize: 98396
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 43858 0 0 0 31863 137 0 0 25 0 1 0 806150347 100757504 21187 4294967295 134512640 135726644 3221224576 3221223072 134744163 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21187 300 300 0 24299 0
vsize: 98396
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 44384 0 0 0 32861 140 0 0 25 0 1 0 806150347 100757504 21213 4294967295 134512640 135726644 3221224576 3221223200 134744553 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21213 300 300 0 24299 0
vsize: 98396
[startup+340.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 44923 0 0 0 33858 143 0 0 25 0 1 0 806150347 100757504 21252 4294967295 134512640 135726644 3221224576 3221222756 135277555 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21252 300 300 0 24299 0
vsize: 98396
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 45449 0 0 0 34856 145 0 0 25 0 1 0 806150347 100757504 21278 4294967295 134512640 135726644 3221224576 3221223072 134744063 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21278 300 300 0 24299 0
vsize: 98396
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 45982 0 0 0 35854 148 0 0 25 0 1 0 806150347 100757504 21311 4294967295 134512640 135726644 3221224576 3221223232 134731248 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21311 300 300 0 24299 0
vsize: 98396
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 45987 0 0 0 36853 149 0 0 25 0 1 0 806150347 100757504 21316 4294967295 134512640 135726644 3221224576 3221222992 134737984 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21316 300 300 0 24299 0
vsize: 98396
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 46509 0 0 0 37851 151 0 0 25 0 1 0 806150347 100757504 21338 4294967295 134512640 135726644 3221224576 3221222896 134728934 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21338 300 300 0 24299 0
vsize: 98396
[startup+390.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 47031 0 0 0 38849 153 0 0 25 0 1 0 806150347 100757504 21360 4294967295 134512640 135726644 3221224576 3221223072 134744163 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21360 300 300 0 24299 0
vsize: 98396
[startup+400.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 47062 0 0 0 39847 155 0 0 25 0 1 0 806150347 100757504 21391 4294967295 134512640 135726644 3221224576 3221223196 135337969 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21391 300 300 0 24299 0
vsize: 98396
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 47096 0 0 0 40846 156 0 0 25 0 1 0 806150347 100757504 21425 4294967295 134512640 135726644 3221224576 3221223072 134744220 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21425 300 300 0 24299 0
vsize: 98396
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 47668 0 0 0 41844 159 0 0 25 0 1 0 806150347 100757504 21497 4294967295 134512640 135726644 3221224576 3221223232 134731175 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21497 300 300 0 24299 0
vsize: 98396
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 48705 0 0 0 42841 162 0 0 25 0 1 0 806150347 100757504 21534 4294967295 134512640 135726644 3221224576 3221223168 134760180 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21534 300 300 0 24299 0
vsize: 98396
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 49712 0 0 0 43837 166 0 0 25 0 1 0 806150347 100757504 21541 4294967295 134512640 135726644 3221224576 3221223232 134731175 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 24599 21541 300 300 0 24299 0
vsize: 98396
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 50789 0 0 0 44834 169 0 0 25 0 1 0 806150347 102940672 22118 4294967295 134512640 135726644 3221224576 3221222752 134765547 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 25132 22118 300 300 0 24832 0
vsize: 100528
[startup+455.719 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 7806
Raw data (stat): 7806 (pb2sat) R 7805 24300 24299 0 -1 0 50789 0 0 0 44834 169 0 0 25 0 1 0 806150347 102940672 22118 4294967295 134512640 135726644 3221224576 3221222752 134765547 0 0 7 16384 0 0 0 17 0 0 0
Raw data (statm): 25132 22118 300 300 0 24832 0
vsize: 0

Child status: 20
Real time (s): 455.719
CPU time (s): 455.755
CPU user time (s): 454.017
CPU system time (s): 1.73773
CPU usage (%): 100.008
Max. virtual memory (Kb): 100528
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####