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.tag12.ucl.opb
MD5SUM	04162d5197113d66489e9d95b6572385
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	41
Number of bits of the biggest number in a constraint	6
Biggest sum of numbers in a constraint	134
Number of bits of the biggest sum of numbers	8
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	20.7588
Number of variables	20605
Total number of constraints	59851
Number of constraints which are clauses	58675
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	1176
Minimum length of a constraint	1
Maximum length of a constraint	11

Trace number 24695

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-11 21:06:59 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2797 boxname=wulflinc31 idbench=311 idsolver=7 numberseed=0
MD5SUM SOLVER: d9a5994a76be78982e492b397ce73911  /oldhome/oroussel/solvers/Pueblo
MD5SUM BENCH:  04162d5197113d66489e9d95b6572385  /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.tag12.ucl.opb
REAL COMMAND:  Pueblo /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.tag12.ucl.opb
IDLAUNCH: 2797
/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:        922236 kB
Buffers:          8644 kB
Cached:          80700 kB
SwapCached:       3340 kB
Active:          50648 kB
Inactive:        43268 kB
HighTotal:      131008 kB
HighFree:        49420 kB
LowTotal:       903652 kB
LowFree:        872816 kB
SwapTotal:     2097892 kB
SwapFree:      2093816 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5352 kB
Slab:            12680 kB
Committed_AS:    63844 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-11 21:18:42 (client local time) WITH STATUS 20 IN 702.491 SECONDS
stats: 2797 7 702.491 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.tag12.ucl.opb
c #variables read: 20605 - #constraints read: 59850
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.92 0.96 0.98 2/55 2986
Raw data (stat): 2986 (runsolver) R 2985 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 720998562 1056768 100 4294967295 134512640 135381576 3221221696 3221216920 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.0006 s]
Raw data (loadavg): 0.93 0.96 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 2904 0 0 0 988 8 0 0 25 0 1 0 720998562 18440192 2881 4294967295 134512640 134581331 3221221792 3221220800 134531325 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 4502 2881 566 18 0 4484 0
vsize: 18008
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.96 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 3498 0 0 0 1986 10 0 0 25 0 1 0 720998562 20865024 3475 4294967295 134512640 134581331 3221221792 3221220784 134531726 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5094 3475 566 18 0 5076 0
vsize: 20376
[startup+30.0013 s]
Raw data (loadavg): 0.95 0.96 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 3796 0 0 0 2985 11 0 0 25 0 1 0 720998562 22147072 3773 4294967295 134512640 134581331 3221221792 3221220780 134561090 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5407 3773 566 18 0 5389 0
vsize: 21628
[startup+40.0016 s]
Raw data (loadavg): 0.96 0.96 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 3796 0 0 0 3985 11 0 0 25 0 1 0 720998562 22147072 3773 4294967295 134512640 134581331 3221221792 3221220720 134519803 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5407 3773 566 18 0 5389 0
vsize: 21628
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.96 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 3796 0 0 0 4986 11 0 0 25 0 1 0 720998562 22147072 3773 4294967295 134512640 134581331 3221221792 3221220848 134556137 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5407 3773 566 18 0 5389 0
vsize: 21628
[startup+60.0021 s]
Raw data (loadavg): 0.97 0.96 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 3796 0 0 0 5986 11 0 0 25 0 1 0 720998562 22147072 3773 4294967295 134512640 134581331 3221221792 3221220720 134519803 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5407 3773 566 18 0 5389 0
vsize: 21628
[startup+70.0024 s]
Raw data (loadavg): 0.97 0.96 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 3796 0 0 0 6986 11 0 0 25 0 1 0 720998562 22147072 3773 4294967295 134512640 134581331 3221221792 3221220720 134519803 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5407 3773 566 18 0 5389 0
vsize: 21628
[startup+80.003 s]
Raw data (loadavg): 0.98 0.96 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 3796 0 0 0 7986 11 0 0 25 0 1 0 720998562 22147072 3773 4294967295 134512640 134581331 3221221792 3221220720 134520027 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5407 3773 566 18 0 5389 0
vsize: 21628
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.96 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 3796 0 0 0 8986 11 0 0 25 0 1 0 720998562 22147072 3773 4294967295 134512640 134581331 3221221792 3221220720 134519803 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5407 3773 566 18 0 5389 0
vsize: 21628
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 3820 0 0 0 9986 11 0 0 25 0 1 0 720998562 22290432 3797 4294967295 134512640 134581331 3221221792 3221220768 134560687 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5442 3797 566 18 0 5424 0
vsize: 21768
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 3950 0 0 0 10986 11 0 0 25 0 1 0 720998562 22822912 3927 4294967295 134512640 134581331 3221221792 3221220676 134557790 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5572 3927 566 18 0 5554 0
vsize: 22288
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 4101 0 0 0 11986 12 0 0 25 0 1 0 720998562 23502848 4078 4294967295 134512640 134581331 3221221792 3221220720 134520027 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5738 4078 566 18 0 5720 0
vsize: 22952
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 4325 0 0 0 12986 12 0 0 25 0 1 0 720998562 24420352 4302 4294967295 134512640 134581331 3221221792 3221220656 134528278 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 5962 4302 566 18 0 5944 0
vsize: 23848
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 4530 0 0 0 13985 13 0 0 25 0 1 0 720998562 25272320 4507 4294967295 134512640 134581331 3221221792 3221220784 134561084 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 6170 4507 566 18 0 6152 0
vsize: 24680
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 4656 0 0 0 14985 14 0 0 25 0 1 0 720998562 25796608 4633 4294967295 134512640 134581331 3221221792 3221220720 134519867 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 6298 4633 566 18 0 6280 0
vsize: 25192
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 4888 0 0 0 15984 15 0 0 25 0 1 0 720998562 26750976 4865 4294967295 134512640 134581331 3221221792 3221220720 134519829 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 6531 4865 566 18 0 6513 0
vsize: 26124
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 5091 0 0 0 16984 15 0 0 25 0 1 0 720998562 27643904 5068 4294967295 134512640 134581331 3221221792 3221220736 134559057 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 6749 5068 566 18 0 6731 0
vsize: 26996
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 5254 0 0 0 17983 16 0 0 25 0 1 0 720998562 28295168 5231 4294967295 134512640 134581331 3221221792 3221220752 134554662 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 6908 5231 566 18 0 6890 0
vsize: 27632
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 5444 0 0 0 18983 16 0 0 25 0 1 0 720998562 29102080 5421 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 7105 5421 566 18 0 7087 0
vsize: 28420
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 5631 0 0 0 19982 17 0 0 25 0 1 0 720998562 29876224 5608 4294967295 134512640 134581331 3221221792 3221220676 134557874 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 7294 5608 566 18 0 7276 0
vsize: 29176
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 5798 0 0 0 20982 17 0 0 25 0 1 0 720998562 30539776 5775 4294967295 134512640 134581331 3221221792 3221220768 134560718 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 7456 5775 566 18 0 7438 0
vsize: 29824
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 5873 0 0 0 21982 17 0 0 25 0 1 0 720998562 30806016 5850 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 7521 5850 566 18 0 7503 0
vsize: 30084
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 6042 0 0 0 22982 18 0 0 25 0 1 0 720998562 31481856 6019 4294967295 134512640 134581331 3221221792 3221220736 134559090 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 7686 6019 566 18 0 7668 0
vsize: 30744
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 6179 0 0 0 23982 18 0 0 25 0 1 0 720998562 32010240 6156 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 7815 6156 566 18 0 7797 0
vsize: 31260
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 6321 0 0 0 24982 18 0 0 25 0 1 0 720998562 32534528 6298 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 7943 6298 566 18 0 7925 0
vsize: 31772
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 6515 0 0 0 25982 19 0 0 25 0 1 0 720998562 33452032 6492 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8167 6492 566 18 0 8149 0
vsize: 32668
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 6644 0 0 0 26981 19 0 0 25 0 1 0 720998562 34119680 6621 4294967295 134512640 134581331 3221221792 3221220720 134519867 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8330 6621 566 18 0 8312 0
vsize: 33320
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 6831 0 0 0 27981 20 0 0 25 0 1 0 720998562 34799616 6808 4294967295 134512640 134581331 3221221792 3221220720 134520043 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8496 6808 566 18 0 8478 0
vsize: 33984
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 6976 0 0 0 28981 20 0 0 25 0 1 0 720998562 35483648 6953 4294967295 134512640 134581331 3221221792 3221220756 134519780 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8663 6953 566 18 0 8645 0
vsize: 34652
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 7157 0 0 0 29980 21 0 0 25 0 1 0 720998562 36143104 7134 4294967295 134512640 134581331 3221221792 3221220672 134560363 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 8824 7134 566 18 0 8806 0
vsize: 35296
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 7391 0 0 0 30980 22 0 0 25 0 1 0 720998562 37212160 7368 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9085 7368 566 18 0 9067 0
vsize: 36340
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 7528 0 0 0 31979 22 0 0 25 0 1 0 720998562 37744640 7505 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9215 7505 566 18 0 9197 0
vsize: 36860
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 7875 0 0 0 32979 23 0 0 25 0 1 0 720998562 39202816 7852 4294967295 134512640 134581331 3221221792 3221220784 134561084 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9571 7852 566 18 0 9553 0
vsize: 38284
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 8093 0 0 0 33978 24 0 0 25 0 1 0 720998562 40001536 8070 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9766 8070 566 18 0 9748 0
vsize: 39064
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 8252 0 0 0 34978 25 0 0 25 0 1 0 720998562 40759296 8229 4294967295 134512640 134581331 3221221792 3221220720 134519803 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 9951 8229 566 18 0 9933 0
vsize: 39804
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 8461 0 0 0 35977 25 0 0 25 0 1 0 720998562 41558016 8438 4294967295 134512640 134581331 3221221792 3221220720 134519829 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10146 8438 566 18 0 10128 0
vsize: 40584
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 8646 0 0 0 36977 25 0 0 25 0 1 0 720998562 42348544 8623 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10339 8623 566 18 0 10321 0
vsize: 41356
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 8868 0 0 0 37976 26 0 0 25 0 1 0 720998562 43274240 8845 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10565 8845 566 18 0 10547 0
vsize: 42260
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 9075 0 0 0 38976 27 0 0 25 0 1 0 720998562 44191744 9052 4294967295 134512640 134581331 3221221792 3221220720 134519829 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10789 9052 566 18 0 10771 0
vsize: 43156
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 9272 0 0 0 39975 28 0 0 25 0 1 0 720998562 44990464 9249 4294967295 134512640 134581331 3221221792 3221220656 134528270 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 10984 9249 566 18 0 10966 0
vsize: 43936
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 9434 0 0 0 40975 28 0 0 25 0 1 0 720998562 45654016 9411 4294967295 134512640 134581331 3221221792 3221220760 134527292 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11146 9411 566 18 0 11128 0
vsize: 44584
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 9684 0 0 0 41974 29 0 0 25 0 1 0 720998562 46579712 9661 4294967295 134512640 134581331 3221221792 3221220768 134560718 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11372 9661 566 18 0 11354 0
vsize: 45488
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 9839 0 0 0 42974 30 0 0 25 0 1 0 720998562 47247360 9816 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11535 9816 566 18 0 11517 0
vsize: 46140
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 10029 0 0 0 43973 30 0 0 25 0 1 0 720998562 48050176 10006 4294967295 134512640 134581331 3221221792 3221220720 134519928 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11731 10006 566 18 0 11713 0
vsize: 46924
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 10234 0 0 0 44973 31 0 0 25 0 1 0 720998562 48865280 10211 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 11930 10211 566 18 0 11912 0
vsize: 47720
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 10380 0 0 0 45973 32 0 0 25 0 1 0 720998562 49565696 10357 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 12101 10357 566 18 0 12083 0
vsize: 48404
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 10589 0 0 0 46972 32 0 0 25 0 1 0 720998562 50364416 10566 4294967295 134512640 134581331 3221221792 3221220756 134519893 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 12296 10566 566 18 0 12278 0
vsize: 49184
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 10766 0 0 0 47972 33 0 0 25 0 1 0 720998562 51023872 10743 4294967295 134512640 134581331 3221221792 3221220720 134519829 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 12457 10743 566 18 0 12439 0
vsize: 49828
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 11031 0 0 0 48971 34 0 0 25 0 1 0 720998562 52092928 11008 4294967295 134512640 134581331 3221221792 3221220672 134560421 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 12718 11008 566 18 0 12700 0
vsize: 50872
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 11205 0 0 0 49971 34 0 0 25 0 1 0 720998562 52879360 11182 4294967295 134512640 134581331 3221221792 3221220768 134560718 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 12910 11182 566 18 0 12892 0
vsize: 51640
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 11425 0 0 0 50970 35 0 0 25 0 1 0 720998562 53821440 11402 4294967295 134512640 134581331 3221221792 3221220676 134557761 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13140 11402 566 18 0 13122 0
vsize: 52560
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 11707 0 0 0 51969 36 0 0 25 0 1 0 720998562 54906880 11684 4294967295 134512640 134581331 3221221792 3221220688 134517902 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13405 11684 566 18 0 13387 0
vsize: 53620
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 11822 0 0 0 52969 36 0 0 25 0 1 0 720998562 55312384 11799 4294967295 134512640 134581331 3221221792 3221220784 134561150 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13504 11799 566 18 0 13486 0
vsize: 54016
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 11922 0 0 0 53969 36 0 0 25 0 1 0 720998562 55734272 11899 4294967295 134512640 134581331 3221221792 3221220720 134520049 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13607 11899 566 18 0 13589 0
vsize: 54428
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 12040 0 0 0 54969 37 0 0 25 0 1 0 720998562 56262656 12017 4294967295 134512640 134581331 3221221792 3221220720 134520049 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13736 12017 566 18 0 13718 0
vsize: 54944
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 12202 0 0 0 55969 37 0 0 25 0 1 0 720998562 57196544 12179 4294967295 134512640 134581331 3221221792 3221220720 134519803 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 13964 12179 566 18 0 13946 0
vsize: 55856
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 12356 0 0 0 56969 37 0 0 25 0 1 0 720998562 57856000 12333 4294967295 134512640 134581331 3221221792 3221220704 134527498 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14125 12333 566 18 0 14107 0
vsize: 56500
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 12618 0 0 0 57967 39 0 0 25 0 1 0 720998562 58925056 12595 4294967295 134512640 134581331 3221221792 3221220720 134519797 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14386 12595 566 18 0 14368 0
vsize: 57544
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 12686 0 0 0 58967 39 0 0 25 0 1 0 720998562 59191296 12663 4294967295 134512640 134581331 3221221792 3221220768 134560721 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14451 12663 566 18 0 14433 0
vsize: 57804
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 12908 0 0 0 59967 40 0 0 25 0 1 0 720998562 59994112 12885 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14647 12885 566 18 0 14629 0
vsize: 58588
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 13077 0 0 0 60966 41 0 0 25 0 1 0 720998562 60792832 13054 4294967295 134512640 134581331 3221221792 3221220676 134557948 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14842 13054 566 18 0 14824 0
vsize: 59368
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 13111 0 0 0 61966 41 0 0 25 0 1 0 720998562 61054976 13088 4294967295 134512640 134581331 3221221792 3221220784 134560848 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14906 13088 566 18 0 14888 0
vsize: 59624
[startup+630.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 13111 0 0 0 62966 41 0 0 25 0 1 0 720998562 61054976 13088 4294967295 134512640 134581331 3221221792 3221220720 134519928 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14906 13088 566 18 0 14888 0
vsize: 59624
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 13111 0 0 0 63966 41 0 0 25 0 1 0 720998562 61054976 13088 4294967295 134512640 134581331 3221221792 3221220780 134561090 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14906 13088 566 18 0 14888 0
vsize: 59624
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 13111 0 0 0 64967 41 0 0 25 0 1 0 720998562 61054976 13088 4294967295 134512640 134581331 3221221792 3221220756 134519780 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14906 13088 566 18 0 14888 0
vsize: 59624
[startup+660.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 13111 0 0 0 65967 41 0 0 25 0 1 0 720998562 61054976 13088 4294967295 134512640 134581331 3221221792 3221220784 134561089 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14906 13088 566 18 0 14888 0
vsize: 59624
[startup+670.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 13111 0 0 0 66967 41 0 0 25 0 1 0 720998562 61054976 13088 4294967295 134512640 134581331 3221221792 3221220736 134559059 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14906 13088 566 18 0 14888 0
vsize: 59624
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 13111 0 0 0 67967 41 0 0 25 0 1 0 720998562 61054976 13088 4294967295 134512640 134581331 3221221792 3221220736 134559274 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14906 13088 566 18 0 14888 0
vsize: 59624
[startup+690.019 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 13111 0 0 0 68967 41 0 0 25 0 1 0 720998562 61054976 13088 4294967295 134512640 134581331 3221221792 3221220428 1075289220 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14906 13088 566 18 0 14888 0
vsize: 59624
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/55 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 13111 0 0 0 69967 41 0 0 25 0 1 0 720998562 61054976 13088 4294967295 134512640 134581331 3221221792 3221220484 1074910624 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14906 13088 566 18 0 14888 0
vsize: 59624
[startup+702.418 s]
Raw data (loadavg): 0.99 0.97 0.98 1/54 2986
Raw data (stat): 2986 (Pueblo) R 2985 7876 7672 0 -1 0 13111 0 0 0 69967 41 0 0 25 0 1 0 720998562 61054976 13088 4294967295 134512640 134581331 3221221792 3221220484 1074910624 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 14906 13088 566 18 0 14888 0
vsize: 0

Child status: 20
Real time (s): 702.417
CPU time (s): 702.491
CPU user time (s): 702.049
CPU system time (s): 0.441932
CPU usage (%): 100.011
Max. virtual memory (Kb): 59624
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####