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-cache-ibm-q-unbounded.Ic22arity.ucl.opb
MD5SUM6bfe4c2dce1e5dbe61cc34b52b1b387f
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 130
Number of bits of the biggest number in a constraint 8
Biggest sum of numbers in a constraint 512
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark45.816
Number of variables87751
Total number of constraints254772
Number of constraints which are clauses247060
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints7712
Minimum length of a constraint1
Maximum length of a constraint15

Trace number 24540

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-10 22:09:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2518 boxname=wulflinc31 idbench=280 idsolver=7 numberseed=0
MD5SUM SOLVER: d9a5994a76be78982e492b397ce73911  /oldhome/oroussel/solvers/Pueblo
MD5SUM BENCH:  6bfe4c2dce1e5dbe61cc34b52b1b387f  /oldhome/oroussel/tmp/wulflinc31/normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb
REAL COMMAND:  Pueblo /oldhome/oroussel/tmp/wulflinc31/normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb
IDLAUNCH: 2518
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        918720 kB
Buffers:         27656 kB
Cached:          63440 kB
SwapCached:       1588 kB
Active:          52480 kB
Inactive:        41308 kB
HighTotal:      131008 kB
HighFree:        70224 kB
LowTotal:       903652 kB
LowFree:        848496 kB
SwapTotal:     2097892 kB
SwapFree:      2095268 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4812 kB
Slab:            16376 kB
Committed_AS:    63652 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-10 22:18:14 (client local time) WITH STATUS 20 IN 520.421 SECONDS
stats: 2518 7 520.421 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/wulflinc31/normalized-cache-ibm-q-unbounded.Ic22arity.ucl.opb
c #variables read: 87751 - #constraints read: 254771
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
Raw data (loadavg): 0.91 0.95 0.90 2/54 19611
Raw data (stat): 19611 (runsolver) R 19610 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 712733033 1056768 100 4294967295 134512640 135381576 3221221664 3221216888 135158418 0 2147483391 1 90112 0 0 0 17 1 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 8777 0 0 0 969 27 0 0 25 0 1 0 712733033 41623552 8755 4294967295 134512640 134581331 3221221776 3217026108 1075310600 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10162 8755 566 18 0 10144 0
vsize: 40648
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 11444 0 0 0 1962 34 0 0 25 0 1 0 712733033 55914496 11296 4294967295 134512640 134581331 3221221776 3221220768 134531728 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13651 11296 566 18 0 13633 0
vsize: 54604
[startup+30.0023 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 11444 0 0 0 2962 34 0 0 25 0 1 0 712733033 55914496 11296 4294967295 134512640 134581331 3221221776 3221220784 134531325 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13651 11296 566 18 0 13633 0
vsize: 54604
[startup+40.0022 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 240140 0 0 0 3574 422 0 0 25 0 1 0 712733033 56266752 11318 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11327 566 18 0 13719 0
vsize: 54948
[startup+50.0032 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 561036 0 0 0 4044 953 0 0 25 0 1 0 712733033 56266752 11348 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11357 566 18 0 13719 0
vsize: 54948
[startup+60.0031 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 881515 0 0 0 4499 1498 0 0 25 0 1 0 712733033 56266752 11305 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11314 566 18 0 13719 0
vsize: 54948
[startup+70.0044 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 1202028 0 0 0 4958 2039 0 0 25 0 1 0 712733033 55914496 11296 4294967295 134512640 134581331 3221221776 3221220744 1075710225 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11305 566 18 0 13719 0
vsize: 54604
[startup+80.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 1522534 0 0 0 5423 2575 0 0 25 0 1 0 712733033 56266752 11366 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11375 566 18 0 13719 0
vsize: 54948
[startup+90.0049 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 1842986 0 0 0 5880 3117 0 0 25 0 1 0 712733033 55914496 11296 4294967295 134512640 134581331 3221221776 3221220744 1075710225 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11305 566 18 0 13719 0
vsize: 54604
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 2163416 0 0 0 6341 3656 0 0 25 0 1 0 712733033 56266752 11377 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11382 566 18 0 13719 0
vsize: 54948
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 2483850 0 0 0 6798 4200 0 0 25 0 1 0 712733033 56266752 11374 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11382 566 18 0 13719 0
vsize: 54948
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 2804294 0 0 0 7253 4745 0 0 25 0 1 0 712733033 55914496 11296 4294967295 134512640 134581331 3221221776 3221220744 1075710225 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11305 566 18 0 13719 0
vsize: 54604
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 3124784 0 0 0 7709 5289 0 0 25 0 1 0 712733033 56266752 11350 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11359 566 18 0 13719 0
vsize: 54948
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 3445213 0 0 0 8170 5828 0 0 25 0 1 0 712733033 56266752 11343 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11352 566 18 0 13719 0
vsize: 54948
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 3766067 0 0 0 8627 6372 0 0 25 0 1 0 712733033 56266752 11331 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11341 566 18 0 13719 0
vsize: 54948
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4086951 0 0 0 9085 6914 0 0 25 0 1 0 712733033 56266752 11349 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13737 11358 566 18 0 13719 0
vsize: 54948
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4238584 0 0 0 9833 7167 0 0 25 0 1 0 712733033 56438784 11364 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13779 11364 566 18 0 13761 0
vsize: 55116
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4238592 0 0 0 10833 7167 0 0 25 0 1 0 712733033 56438784 11372 4294967295 134512640 134581331 3221221776 3221220784 134531324 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13779 11372 566 18 0 13761 0
vsize: 55116
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4238599 0 0 0 11833 7167 0 0 25 0 1 0 712733033 56438784 11379 4294967295 134512640 134581331 3221221776 3221220768 134531728 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13779 11379 566 18 0 13761 0
vsize: 55116
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4238606 0 0 0 12833 7167 0 0 25 0 1 0 712733033 56438784 11386 4294967295 134512640 134581331 3221221776 3221220784 134531324 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13779 11386 566 18 0 13761 0
vsize: 55116
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4238614 0 0 0 13833 7167 0 0 25 0 1 0 712733033 56438784 11394 4294967295 134512640 134581331 3221221776 3221220784 134531324 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13779 11394 566 18 0 13761 0
vsize: 55116
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4238621 0 0 0 14833 7167 0 0 25 0 1 0 712733033 56438784 11401 4294967295 134512640 134581331 3221221776 3221220784 134531324 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13779 11401 566 18 0 13761 0
vsize: 55116
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4238692 0 0 0 15833 7167 0 0 25 0 1 0 712733033 56709120 11472 4294967295 134512640 134581331 3221221776 3221220784 134531324 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 13845 11472 566 18 0 13827 0
vsize: 55380
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4238861 0 0 0 16833 7167 0 0 25 0 1 0 712733033 57384960 11641 4294967295 134512640 134581331 3221221776 3221220768 134531720 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 14010 11641 566 18 0 13992 0
vsize: 56040
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4239026 0 0 0 17833 7167 0 0 25 0 1 0 712733033 58060800 11806 4294967295 134512640 134581331 3221221776 3221220768 134531732 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 14175 11806 566 18 0 14157 0
vsize: 56700
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4239192 0 0 0 18832 7168 0 0 25 0 1 0 712733033 59260928 11972 4294967295 134512640 134581331 3221221776 3221220784 134531325 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 14468 11972 566 18 0 14450 0
vsize: 57872
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4239360 0 0 0 19832 7169 0 0 25 0 1 0 712733033 59936768 12140 4294967295 134512640 134581331 3221221776 3221220768 134531720 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 14633 12140 566 18 0 14615 0
vsize: 58532
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4239528 0 0 0 20832 7169 0 0 25 0 1 0 712733033 60612608 12308 4294967295 134512640 134581331 3221221776 3221220784 134531324 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 14798 12308 566 18 0 14780 0
vsize: 59192
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4239696 0 0 0 21832 7169 0 0 25 0 1 0 712733033 61288448 12476 4294967295 134512640 134581331 3221221776 3221220768 134531720 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 14963 12476 566 18 0 14945 0
vsize: 59852
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4239860 0 0 0 22832 7170 0 0 25 0 1 0 712733033 61829120 12640 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 15095 12640 566 18 0 15077 0
vsize: 60380
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4240026 0 0 0 23831 7170 0 0 25 0 1 0 712733033 62504960 12806 4294967295 134512640 134581331 3221221776 3221220768 134531720 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 15260 12806 566 18 0 15242 0
vsize: 61040
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4240190 0 0 0 24831 7170 0 0 25 0 1 0 712733033 63180800 12970 4294967295 134512640 134581331 3221221776 3221220768 134531720 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 15425 12970 566 18 0 15407 0
vsize: 61700
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4240357 0 0 0 25831 7171 0 0 25 0 1 0 712733033 63856640 13137 4294967295 134512640 134581331 3221221776 3221220784 134531324 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 15590 13137 566 18 0 15572 0
vsize: 62360
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4240521 0 0 0 26831 7171 0 0 25 0 1 0 712733033 64397312 13301 4294967295 134512640 134581331 3221221776 3221220768 134531720 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 15722 13301 566 18 0 15704 0
vsize: 62888
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4240688 0 0 0 27830 7172 0 0 25 0 1 0 712733033 65073152 13468 4294967295 134512640 134581331 3221221776 3221220784 134531324 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 15887 13468 566 18 0 15869 0
vsize: 63548
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4240860 0 0 0 28830 7172 0 0 25 0 1 0 712733033 65748992 13640 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 16052 13640 566 18 0 16034 0
vsize: 64208
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4241033 0 0 0 29830 7173 0 0 25 0 1 0 712733033 66424832 13813 4294967295 134512640 134581331 3221221776 3221220784 134531324 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 16217 13813 566 18 0 16199 0
vsize: 64868
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4241208 0 0 0 30829 7173 0 0 25 0 1 0 712733033 67100672 13988 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 16382 13988 566 18 0 16364 0
vsize: 65528
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4241387 0 0 0 31829 7174 0 0 25 0 1 0 712733033 67911680 14167 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 16580 14167 566 18 0 16562 0
vsize: 66320
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4241552 0 0 0 32828 7175 0 0 25 0 1 0 712733033 68452352 14332 4294967295 134512640 134581331 3221221776 3221220784 134531324 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 16712 14332 566 18 0 16694 0
vsize: 66848
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4241945 0 0 0 33828 7175 0 0 25 0 1 0 712733033 70074368 14725 4294967295 134512640 134581331 3221221776 3221220784 134531324 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17108 14725 566 18 0 17090 0
vsize: 68432
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4242855 0 0 0 34826 7178 0 0 25 0 1 0 712733033 74039296 15635 4294967295 134512640 134581331 3221221776 3221220688 134519017 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18076 15635 566 18 0 18058 0
vsize: 72304
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4242855 0 0 0 35826 7178 0 0 25 0 1 0 712733033 74039296 15635 4294967295 134512640 134581331 3221221776 3221220688 134528088 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18076 15635 566 18 0 18058 0
vsize: 72304
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4242855 0 0 0 36826 7178 0 0 25 0 1 0 712733033 74039296 15635 4294967295 134512640 134581331 3221221776 3221220752 134560721 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18076 15635 566 18 0 18058 0
vsize: 72304
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4242855 0 0 0 37826 7178 0 0 25 0 1 0 712733033 74039296 15635 4294967295 134512640 134581331 3221221776 3221220496 134523390 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18076 15635 566 18 0 18058 0
vsize: 72304
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4242855 0 0 0 38826 7178 0 0 25 0 1 0 712733033 74039296 15635 4294967295 134512640 134581331 3221221776 3221220720 134560142 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18076 15635 566 18 0 18058 0
vsize: 72304
[startup+470.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4242855 0 0 0 39826 7178 0 0 25 0 1 0 712733033 74039296 15635 4294967295 134512640 134581331 3221221776 3221220696 134519971 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18076 15635 566 18 0 18058 0
vsize: 72304
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4242855 0 0 0 40827 7178 0 0 25 0 1 0 712733033 74039296 15635 4294967295 134512640 134581331 3221221776 3221220720 134560136 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18076 15635 566 18 0 18058 0
vsize: 72304
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4242855 0 0 0 41827 7178 0 0 25 0 1 0 712733033 74039296 15635 4294967295 134512640 134581331 3221221776 3221220720 134559087 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18076 15635 566 18 0 18058 0
vsize: 72304
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4242855 0 0 0 42826 7178 0 0 25 0 1 0 712733033 74039296 15635 4294967295 134512640 134581331 3221221776 3221220720 134559377 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18076 15635 566 18 0 18058 0
vsize: 72304
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4242855 0 0 0 43826 7178 0 0 25 0 1 0 712733033 74039296 15635 4294967295 134512640 134581331 3221221776 3221220752 134560718 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18076 15635 566 18 0 18058 0
vsize: 72304
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4242855 0 0 0 44827 7178 0 0 25 0 1 0 712733033 74039296 15635 4294967295 134512640 134581331 3221221776 3221220784 134519703 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18076 15635 566 18 0 18058 0
vsize: 72304
[startup+520.377 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 19611
Raw data (stat): 19611 (Pueblo) R 19610 7876 7672 0 -1 0 4242855 0 0 0 44827 7178 0 0 25 0 1 0 712733033 74039296 15635 4294967295 134512640 134581331 3221221776 3221220784 134519703 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 18076 15635 566 18 0 18058 0
vsize: 0

Child status: 20
Real time (s): 520.376
CPU time (s): 520.421
CPU user time (s): 448.603
CPU system time (s): 71.8181
CPU usage (%): 100.009
Max. virtual memory (Kb): 72304
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####