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 24645

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-11 12:28:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2707 boxname=wulflinc31 idbench=301 idsolver=7 numberseed=0
MD5SUM SOLVER: d9a5994a76be78982e492b397ce73911  /oldhome/oroussel/solvers/Pueblo
MD5SUM BENCH:  89f41bbcf2b70665bd7071c5b58e0ec8  /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb
REAL COMMAND:  Pueblo /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.ex.br.mem.RobRegValid_bar.ucl.opb
IDLAUNCH: 2707
/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:        920960 kB
Buffers:          8916 kB
Cached:          79128 kB
SwapCached:       4232 kB
Active:          51656 kB
Inactive:        41856 kB
HighTotal:      131008 kB
HighFree:        51632 kB
LowTotal:       903652 kB
LowFree:        869328 kB
SwapTotal:     2097892 kB
SwapFree:      2093028 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5308 kB
Slab:            14356 kB
Committed_AS:    63632 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-11 12:36:26 (client local time) WITH STATUS 20 IN 453.675 SECONDS
stats: 2707 7 453.675 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-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
Raw data (loadavg): 0.91 0.97 0.98 2/54 29838
Raw data (stat): 29838 (runsolver) R 29837 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 717889484 1056768 100 4294967295 134512640 135381576 3221221664 3221216888 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0008 s]
Raw data (loadavg): 0.92 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 115756 0 0 0 792 205 0 0 25 0 1 0 717889484 34430976 6659 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 8406 6668 566 18 0 8388 0
vsize: 33624
[startup+20.0007 s]
Raw data (loadavg): 0.93 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 441653 0 0 0 1254 743 0 0 25 0 1 0 717889484 34430976 6657 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 8406 6666 566 18 0 8388 0
vsize: 33624
[startup+30.0018 s]
Raw data (loadavg): 0.94 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 764943 0 0 0 1722 1275 0 0 25 0 1 0 717889484 34430976 6695 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8406 6695 566 18 0 8388 0
vsize: 33624
[startup+40.0017 s]
Raw data (loadavg): 0.95 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 1087161 0 0 0 2185 1812 0 0 25 0 1 0 717889484 34430976 6688 4294967295 134512640 134581331 3221221776 3221220768 134531728 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8406 6688 566 18 0 8388 0
vsize: 33624
[startup+50.0017 s]
Raw data (loadavg): 0.96 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 1410863 0 0 0 2643 2353 0 0 25 0 1 0 717889484 34230272 6647 4294967295 134512640 134581331 3221221776 3221220744 1075710225 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8357 6647 566 18 0 8339 0
vsize: 33428
[startup+60.0016 s]
Raw data (loadavg): 0.96 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 1731456 0 0 0 3107 2890 0 0 25 0 1 0 717889484 34693120 6731 4294967295 134512640 134581331 3221221776 3221220784 134531324 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8470 6731 566 18 0 8452 0
vsize: 33880
[startup+70.0015 s]
Raw data (loadavg): 0.97 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 2053196 0 0 0 3555 3442 0 0 25 0 1 0 717889484 34693120 6737 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8421 6688 566 18 0 8403 0
vsize: 33880
[startup+80.0023 s]
Raw data (loadavg): 0.97 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 2374771 0 0 0 4021 3976 0 0 25 0 1 0 717889484 34693120 6725 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8470 6734 566 18 0 8452 0
vsize: 33880
[startup+90.0022 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 2695802 0 0 0 4487 4510 0 0 25 0 1 0 717889484 34693120 6708 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8470 6717 566 18 0 8452 0
vsize: 33880
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 3017051 0 0 0 4951 5046 0 0 25 0 1 0 717889484 34828288 6762 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8454 6713 566 18 0 8436 0
vsize: 34012
[startup+110.003 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 3338448 0 0 0 5412 5586 0 0 25 0 1 0 717889484 35631104 6915 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8699 6868 566 18 0 8681 0
vsize: 34796
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 3659610 0 0 0 5863 6135 0 0 25 0 1 0 717889484 36171776 7030 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8831 7038 566 18 0 8813 0
vsize: 35324
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 3979880 0 0 0 6327 6671 0 0 25 0 1 0 717889484 36847616 7182 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8996 7191 566 18 0 8978 0
vsize: 35984
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 4301216 0 0 0 6799 7199 0 0 25 0 1 0 717889484 37388288 7323 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9128 7332 566 18 0 9110 0
vsize: 36512
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 4622640 0 0 0 7272 7727 0 0 25 0 1 0 717889484 37928960 7503 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9260 7512 566 18 0 9242 0
vsize: 37040
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 4941358 0 0 0 7742 8257 0 0 25 0 1 0 717889484 38604800 7623 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9425 7632 566 18 0 9407 0
vsize: 37700
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 5258851 0 0 0 8206 8793 0 0 25 0 1 0 717889484 39145472 7792 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9557 7800 566 18 0 9539 0
vsize: 38228
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 5577916 0 0 0 8665 9334 0 0 25 0 1 0 717889484 39686144 7916 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9689 7925 566 18 0 9671 0
vsize: 38756
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 5897640 0 0 0 9126 9874 0 0 25 0 1 0 717889484 40361984 8062 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9854 8071 566 18 0 9836 0
vsize: 39416
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6218152 0 0 0 9583 10416 0 0 25 0 1 0 717889484 40701952 8212 4294967295 134512640 134581331 3221221776 3221220544 1075710051 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9986 8222 566 18 0 9968 0
vsize: 39748
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6538954 0 0 0 10056 10943 0 0 25 0 1 0 717889484 44130304 8897 4294967295 134512640 134581331 3221221776 3221220768 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10774 8905 566 18 0 10756 0
vsize: 43096
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788590 0 0 0 10644 11356 0 0 25 0 1 0 717889484 46931968 9613 4294967295 134512640 134581331 3221221776 3221220768 134561084 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9613 566 18 0 11440 0
vsize: 45832
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 11644 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220752 134560718 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 12644 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220704 134519880 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 13645 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220672 134560197 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 14645 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220608 134528569 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 15645 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220740 134519780 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 16645 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220720 134559093 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 17645 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220688 134519017 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 18645 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220704 134519820 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 19646 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220768 134561084 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 20646 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220688 134527454 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 21646 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220548 1075289714 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 22646 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220656 134520246 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 23646 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220768 134560963 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788591 0 0 0 24647 11356 0 0 25 0 1 0 717889484 46931968 9614 4294967295 134512640 134581331 3221221776 3221220752 134561101 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11458 9614 566 18 0 11440 0
vsize: 45832
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788626 0 0 0 25647 11356 0 0 25 0 1 0 717889484 47194112 9649 4294967295 134512640 134581331 3221221776 3221220488 1075291634 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11522 9649 566 18 0 11504 0
vsize: 46088
[startup+380.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788628 0 0 0 26647 11356 0 0 25 0 1 0 717889484 47194112 9651 4294967295 134512640 134581331 3221221776 3221220768 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11522 9651 566 18 0 11504 0
vsize: 46088
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788630 0 0 0 27647 11356 0 0 25 0 1 0 717889484 47194112 9653 4294967295 134512640 134581331 3221221776 3221220704 134519928 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11522 9653 566 18 0 11504 0
vsize: 46088
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788631 0 0 0 28647 11356 0 0 25 0 1 0 717889484 47194112 9654 4294967295 134512640 134581331 3221221776 3221220688 134527454 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11522 9654 566 18 0 11504 0
vsize: 46088
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788634 0 0 0 29647 11356 0 0 25 0 1 0 717889484 47194112 9657 4294967295 134512640 134581331 3221221776 3221220688 134527407 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11522 9657 566 18 0 11504 0
vsize: 46088
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788635 0 0 0 30647 11356 0 0 25 0 1 0 717889484 47194112 9658 4294967295 134512640 134581331 3221221776 3221220704 134519829 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11522 9658 566 18 0 11504 0
vsize: 46088
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788638 0 0 0 31648 11356 0 0 25 0 1 0 717889484 47194112 9661 4294967295 134512640 134581331 3221221776 3221220704 134519803 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11522 9661 566 18 0 11504 0
vsize: 46088
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788640 0 0 0 32648 11356 0 0 25 0 1 0 717889484 47194112 9663 4294967295 134512640 134581331 3221221776 3221220688 134527534 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11522 9663 566 18 0 11504 0
vsize: 46088
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/54 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788689 0 0 0 33648 11356 0 0 25 0 1 0 717889484 47460352 9712 4294967295 134512640 134581331 3221221776 3221220784 134519703 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11587 9712 566 18 0 11569 0
vsize: 46348
[startup+453.638 s]
Raw data (loadavg): 0.99 0.97 0.98 1/53 29838
Raw data (stat): 29838 (Pueblo) R 29837 7876 7672 0 -1 0 6788689 0 0 0 33648 11356 0 0 25 0 1 0 717889484 47460352 9712 4294967295 134512640 134581331 3221221776 3221220784 134519703 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11587 9712 566 18 0 11569 0
vsize: 0

Child status: 20
Real time (s): 453.637
CPU time (s): 453.675
CPU user time (s): 340.091
CPU system time (s): 113.584
CPU usage (%): 100.008
Max. virtual memory (Kb): 46348
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####