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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/web/uclid_pb_benchmarks/normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb
MD5SUM89f41bbcf2b70665bd7071c5b58e0ec8
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(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 numbers9
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark95.1845
Number of variables49621
Total number of constraints138346
Number of constraints which are clauses127390
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints10956
Minimum length of a constraint1
Maximum length of a constraint15

Trace number 38501

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-06-02 11:19:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=26571 boxname=wulflinc6 idbench=301 idsolver=19 numberseed=0
MD5SUM SOLVER: 259c660e62244fe20bfb2a303545faea  /oldhome/oroussel/solvers/Pueblo-v2
MD5SUM BENCH:  89f41bbcf2b70665bd7071c5b58e0ec8  /oldhome/oroussel/tmp/wulflinc6/normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb
REAL COMMAND:  Pueblo-v2 /oldhome/oroussel/tmp/wulflinc6/normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb
IDLAUNCH: 26571
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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	: 2
cpu MHz		: 451.042
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:        754368 kB
Buffers:         33448 kB
Cached:         225216 kB
SwapCached:        552 kB
Active:          61292 kB
Inactive:       199536 kB
HighTotal:      131008 kB
HighFree:        25228 kB
LowTotal:       903652 kB
LowFree:        729140 kB
SwapTotal:     2097136 kB
SwapFree:      2095652 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5196 kB
Slab:            13612 kB
Committed_AS:    63736 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-02 11:28:01 (client local time) WITH STATUS 20 IN 488.281 SECONDS
stats: 26571 7 488.281 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Pueblo version 1.2 (Sept 2004)
c Developed @ University of Michigan, Ann Arbor, MI
c  by Hossein Sheini
c Solving: /oldhome/oroussel/tmp/wulflinc6/normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb
c #variables read: 49621 - #constraints read: 138345
s 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.97 0.93 1/54 16008
Raw data (stat): 16008 (runsolver) R 16007 25568 25567 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 849376210 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.0002 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 120498 0 0 0 801 198 0 0 25 0 1 0 849376210 37462016 7429 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9146 7429 566 18 0 9128 0
vsize: 36584
[startup+20.001 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 453879 0 0 0 1283 716 0 0 25 0 1 0 849376210 37462016 7414 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9146 7414 566 18 0 9128 0
vsize: 36584
[startup+30.0004 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 787095 0 0 0 1759 1241 0 0 25 0 1 0 849376210 37462016 7430 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9146 7430 566 18 0 9128 0
vsize: 36584
[startup+40.0006 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 1120510 0 0 0 2242 1758 0 0 25 0 1 0 849376210 37462016 7400 4294967295 134512640 134581267 3221224560 3221223552 134531696 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9146 7400 566 18 0 9128 0
vsize: 36584
[startup+50.0012 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 1454041 0 0 0 2719 2281 0 0 25 0 1 0 849376210 37462016 7437 4294967295 134512640 134581267 3221224560 3221223384 1075288931 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9146 7437 566 18 0 9128 0
vsize: 36584
[startup+60.0009 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 1787357 0 0 0 3207 2793 0 0 25 0 1 0 849376210 37724160 7455 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9210 7455 566 18 0 9192 0
vsize: 36840
[startup+70.0001 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 2120533 0 0 0 3690 3310 0 0 25 0 1 0 849376210 37523456 7431 4294967295 134512640 134581267 3221224560 3221223528 1075710225 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9161 7431 566 18 0 9143 0
vsize: 36644
[startup+80.001 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 2453801 0 0 0 4168 3833 0 0 25 0 1 0 849376210 37724160 7450 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9210 7450 566 18 0 9192 0
vsize: 36840
[startup+90.0003 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 2786477 0 0 0 4654 4347 0 0 25 0 1 0 849376210 37724160 7465 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9210 7465 566 18 0 9192 0
vsize: 36840
[startup+99.9995 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 3118836 0 0 0 5139 4863 0 0 25 0 1 0 849376210 37994496 7507 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9276 7507 566 18 0 9258 0
vsize: 37104
[startup+110 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 3448456 0 0 0 5622 5379 0 0 25 0 1 0 849376210 38932480 7699 4294967295 134512640 134581267 3221224560 3221223552 134531696 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9505 7699 566 18 0 9487 0
vsize: 38020
[startup+120 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 3778625 0 0 0 6089 5913 0 0 25 0 1 0 849376210 39473152 7853 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9637 7853 566 18 0 9619 0
vsize: 38548
[startup+129.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 4108533 0 0 0 6553 6449 0 0 25 0 1 0 849376210 40013824 7991 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9769 7991 566 18 0 9751 0
vsize: 39076
[startup+139.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 4441241 0 0 0 7032 6970 0 0 25 0 1 0 849376210 40689664 8136 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 9934 8136 566 18 0 9916 0
vsize: 39736
[startup+149.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 4773122 0 0 0 7503 7500 0 0 25 0 1 0 849376210 41365504 8287 4294967295 134512640 134581267 3221224560 3221223552 134531696 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10099 8287 566 18 0 10081 0
vsize: 40396
[startup+159.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 5105073 0 0 0 7973 8029 0 0 25 0 1 0 849376210 41906176 8459 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10231 8459 566 18 0 10213 0
vsize: 40924
[startup+169.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 5434492 0 0 0 8442 8561 0 0 25 0 1 0 849376210 42446848 8598 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10363 8598 566 18 0 10345 0
vsize: 41452
[startup+179.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 5764672 0 0 0 8918 9085 0 0 25 0 1 0 849376210 43122688 8763 4294967295 134512640 134581267 3221224560 3221223552 134531696 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10528 8763 566 18 0 10510 0
vsize: 42112
[startup+189.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6094320 0 0 0 9397 9607 0 0 25 0 1 0 849376210 43663360 8935 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 10660 8935 566 18 0 10642 0
vsize: 42640
[startup+199.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6422959 0 0 0 9867 10137 0 0 25 0 1 0 849376210 45555712 9372 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11122 9372 566 18 0 11104 0
vsize: 44488
[startup+209.997 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6751670 0 0 0 10353 10652 0 0 25 0 1 0 849376210 48918528 10077 4294967295 134512640 134581267 3221224560 3221223552 134531694 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 11943 10077 566 18 0 11925 0
vsize: 47772
[startup+219.997 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789332 0 0 0 11292 10713 0 0 25 0 1 0 849376210 49963008 10352 4294967295 134512640 134581267 3221224560 3221223536 134560674 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12198 10352 566 18 0 12180 0
vsize: 48792
[startup+229.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789332 0 0 0 12292 10713 0 0 25 0 1 0 849376210 49963008 10352 4294967295 134512640 134581267 3221224560 3221223552 134561045 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12198 10352 566 18 0 12180 0
vsize: 48792
[startup+239.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789332 0 0 0 13292 10713 0 0 25 0 1 0 849376210 49963008 10352 4294967295 134512640 134581267 3221224560 3221223472 134527454 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12198 10352 566 18 0 12180 0
vsize: 48792
[startup+249.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789332 0 0 0 14292 10714 0 0 25 0 1 0 849376210 49963008 10352 4294967295 134512640 134581267 3221224560 3221223488 134519803 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12198 10352 566 18 0 12180 0
vsize: 48792
[startup+259.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789332 0 0 0 15292 10714 0 0 25 0 1 0 849376210 49963008 10352 4294967295 134512640 134581267 3221224560 3221223552 134561087 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12198 10352 566 18 0 12180 0
vsize: 48792
[startup+269.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789332 0 0 0 16292 10714 0 0 25 0 1 0 849376210 49963008 10352 4294967295 134512640 134581267 3221224560 3221223552 134560771 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12198 10352 566 18 0 12180 0
vsize: 48792
[startup+279.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789332 0 0 0 17292 10714 0 0 25 0 1 0 849376210 49963008 10352 4294967295 134512640 134581267 3221224560 3221223440 134560435 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12198 10352 566 18 0 12180 0
vsize: 48792
[startup+289.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789332 0 0 0 18292 10715 0 0 25 0 1 0 849376210 49963008 10352 4294967295 134512640 134581267 3221224560 3221223536 134560674 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12198 10352 566 18 0 12180 0
vsize: 48792
[startup+299.998 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789332 0 0 0 19291 10715 0 0 25 0 1 0 849376210 49963008 10352 4294967295 134512640 134581267 3221224560 3221223488 134519829 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12198 10352 566 18 0 12180 0
vsize: 48792
[startup+309.999 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789332 0 0 0 20291 10715 0 0 25 0 1 0 849376210 49963008 10352 4294967295 134512640 134581267 3221224560 3221223552 134561045 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12198 10352 566 18 0 12180 0
vsize: 48792
[startup+320 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789332 0 0 0 21291 10716 0 0 25 0 1 0 849376210 49963008 10352 4294967295 134512640 134581267 3221224560 3221223552 134561045 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12198 10352 566 18 0 12180 0
vsize: 48792
[startup+330 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789365 0 0 0 22291 10716 0 0 25 0 1 0 849376210 50225152 10385 4294967295 134512640 134581267 3221224560 3221223504 134559268 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12262 10385 566 18 0 12244 0
vsize: 49048
[startup+340 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789367 0 0 0 23291 10717 0 0 25 0 1 0 849376210 50225152 10387 4294967295 134512640 134581267 3221224560 3221223488 134519867 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12262 10387 566 18 0 12244 0
vsize: 49048
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789369 0 0 0 24291 10717 0 0 25 0 1 0 849376210 50225152 10389 4294967295 134512640 134581267 3221224560 3221223552 134561045 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12262 10389 566 18 0 12244 0
vsize: 49048
[startup+360 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789372 0 0 0 25291 10717 0 0 25 0 1 0 849376210 50225152 10392 4294967295 134512640 134581267 3221224560 3221223488 134520024 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12262 10392 566 18 0 12244 0
vsize: 49048
[startup+370 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789376 0 0 0 26291 10717 0 0 25 0 1 0 849376210 50225152 10396 4294967295 134512640 134581267 3221224560 3221223552 134561081 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12262 10396 566 18 0 12244 0
vsize: 49048
[startup+380.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789379 0 0 0 27292 10717 0 0 25 0 1 0 849376210 50225152 10399 4294967295 134512640 134581267 3221224560 3221223552 134561045 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12262 10399 566 18 0 12244 0
vsize: 49048
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789382 0 0 0 28291 10718 0 0 25 0 1 0 849376210 50225152 10402 4294967295 134512640 134581267 3221224560 3221223488 134519896 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12262 10402 566 18 0 12244 0
vsize: 49048
[startup+400.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789384 0 0 0 29291 10718 0 0 25 0 1 0 849376210 50225152 10404 4294967295 134512640 134581267 3221224560 3221223552 134561045 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12262 10404 566 18 0 12244 0
vsize: 49048
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789388 0 0 0 30291 10718 0 0 25 0 1 0 849376210 50225152 10408 4294967295 134512640 134581267 3221224560 3221223536 134560674 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12262 10408 566 18 0 12244 0
vsize: 49048
[startup+420.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789391 0 0 0 31291 10718 0 0 25 0 1 0 849376210 50225152 10411 4294967295 134512640 134581267 3221224560 3221223552 134561045 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12262 10411 566 18 0 12244 0
vsize: 49048
[startup+430.001 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789434 0 0 0 32291 10719 0 0 25 0 1 0 849376210 50495488 10454 4294967295 134512640 134581267 3221224560 3221223504 134559175 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12328 10454 566 18 0 12310 0
vsize: 49312
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789579 0 0 0 33290 10720 0 0 25 0 1 0 849376210 51019776 10599 4294967295 134512640 134581267 3221224560 3221223552 134561040 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12456 10599 566 18 0 12438 0
vsize: 49824
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789697 0 0 0 34290 10721 0 0 25 0 1 0 849376210 51814400 10717 4294967295 134512640 134581267 3221224560 3221223504 134559268 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12650 10717 566 18 0 12632 0
vsize: 50600
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6789885 0 0 0 35290 10721 0 0 25 0 1 0 849376210 52629504 10905 4294967295 134512640 134581267 3221224560 3221223552 134561045 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12849 10905 566 18 0 12831 0
vsize: 51396
[startup+470.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6790014 0 0 0 36290 10722 0 0 25 0 1 0 849376210 53030912 11034 4294967295 134512640 134581267 3221224560 3221223536 134516745 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12947 11034 566 18 0 12929 0
vsize: 51788
[startup+480.002 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6790014 0 0 0 37290 10722 0 0 25 0 1 0 849376210 53030912 11034 4294967295 134512640 134581267 3221224560 3221223548 134561046 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12947 11034 566 18 0 12929 0
vsize: 51788
[startup+488.156 s]
Raw data (loadavg): 0.99 0.97 0.93 1/53 16008
Raw data (stat): 16008 (Pueblo-v2) R 16007 25568 25567 0 -1 0 6790014 0 0 0 37290 10722 0 0 25 0 1 0 849376210 53030912 11034 4294967295 134512640 134581267 3221224560 3221223548 134561046 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 12947 11034 566 18 0 12929 0
vsize: 0

Child status: 20
Real time (s): 488.155
CPU time (s): 488.281
CPU user time (s): 381.034
CPU system time (s): 107.247
CPU usage (%): 100.026
Max. virtual memory (Kb): 51788
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####