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.tag12.ucl.opb
MD5SUM04162d5197113d66489e9d95b6572385
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 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 numbers8
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark20.7588
Number of variables20605
Total number of constraints59851
Number of constraints which are clauses58675
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1176
Minimum length of a constraint1
Maximum length of a constraint11

Trace number 38514

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-06-02 11:39:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=26581 boxname=wulflinc3 idbench=311 idsolver=19 numberseed=0
MD5SUM SOLVER: 259c660e62244fe20bfb2a303545faea  /oldhome/oroussel/solvers/Pueblo-v2
MD5SUM BENCH:  04162d5197113d66489e9d95b6572385  /oldhome/oroussel/tmp/wulflinc3/normalized-ooo.tag12.ucl.opb
REAL COMMAND:  Pueblo-v2 /oldhome/oroussel/tmp/wulflinc3/normalized-ooo.tag12.ucl.opb
IDLAUNCH: 26581
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        702728 kB
Buffers:         34164 kB
Cached:         275348 kB
SwapCached:        228 kB
Active:          62420 kB
Inactive:       249740 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        702476 kB
SwapTotal:     2097136 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6332 kB
Slab:            14144 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-02 11:47:02 (client local time) WITH STATUS 20 IN 431.442 SECONDS
stats: 26581 7 431.442 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/wulflinc3/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
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.84 0.93 0.90 1/54 9702
Raw data (stat): 9702 (runsolver) R 9701 20224 20223 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 849488791 884736 94 4294967295 134512640 135332820 3221224464 3221219644 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 216 94 205 205 0 11 0
vsize: 864
[startup+10.0005 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 3224 0 0 0 990 8 0 0 25 0 1 0 849488791 19738624 3198 4294967295 134512640 134581267 3221224576 3221223568 134531688 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 4819 3198 566 18 0 4801 0
vsize: 19276
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 3832 0 0 0 1990 9 0 0 25 0 1 0 849488791 22298624 3806 4294967295 134512640 134581267 3221224576 3221223568 134531696 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5444 3806 566 18 0 5426 0
vsize: 21776
[startup+30.0008 s]
Raw data (loadavg): 0.90 0.93 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 4116 0 0 0 2989 10 0 0 25 0 1 0 849488791 23445504 4090 4294967295 134512640 134581267 3221224576 3221223456 134560284 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5724 4090 566 18 0 5706 0
vsize: 22896
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 4116 0 0 0 3989 10 0 0 25 0 1 0 849488791 23445504 4090 4294967295 134512640 134581267 3221224576 3221223552 134560674 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5724 4090 566 18 0 5706 0
vsize: 22896
[startup+50.0015 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 4116 0 0 0 4989 10 0 0 25 0 1 0 849488791 23445504 4090 4294967295 134512640 134581267 3221224576 3221223568 134561040 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5724 4090 566 18 0 5706 0
vsize: 22896
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 4116 0 0 0 5989 10 0 0 25 0 1 0 849488791 23445504 4090 4294967295 134512640 134581267 3221224576 3221223568 134561040 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5724 4090 566 18 0 5706 0
vsize: 22896
[startup+70.0025 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 4116 0 0 0 6990 10 0 0 25 0 1 0 849488791 23445504 4090 4294967295 134512640 134581267 3221224576 3221223504 134519829 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5724 4090 566 18 0 5706 0
vsize: 22896
[startup+80.003 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 4116 0 0 0 7990 10 0 0 25 0 1 0 849488791 23445504 4090 4294967295 134512640 134581267 3221224576 3221223552 134561057 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5724 4090 566 18 0 5706 0
vsize: 22896
[startup+90.0028 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 4116 0 0 0 8990 10 0 0 25 0 1 0 849488791 23445504 4090 4294967295 134512640 134581267 3221224576 3221223568 134561036 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5724 4090 566 18 0 5706 0
vsize: 22896
[startup+100.003 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 4116 0 0 0 9990 10 0 0 25 0 1 0 849488791 23445504 4090 4294967295 134512640 134581267 3221224576 3221223492 134519972 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5724 4090 566 18 0 5706 0
vsize: 22896
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 4265 0 0 0 10990 10 0 0 25 0 1 0 849488791 24096768 4239 4294967295 134512640 134581267 3221224576 3221223504 134519867 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 5883 4239 566 18 0 5865 0
vsize: 23532
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 4477 0 0 0 11990 11 0 0 25 0 1 0 849488791 25128960 4451 4294967295 134512640 134581267 3221224576 3221223504 134519803 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 6135 4451 566 18 0 6117 0
vsize: 24540
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 4728 0 0 0 12989 11 0 0 25 0 1 0 849488791 26185728 4702 4294967295 134512640 134581267 3221224576 3221223552 134560677 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 6393 4702 566 18 0 6375 0
vsize: 25572
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 5019 0 0 0 13989 12 0 0 25 0 1 0 849488791 27373568 4993 4294967295 134512640 134581267 3221224576 3221223504 134519829 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 6683 4993 566 18 0 6665 0
vsize: 26732
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 5362 0 0 0 14988 13 0 0 25 0 1 0 849488791 28717056 5336 4294967295 134512640 134581267 3221224576 3221223568 134561081 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 7011 5336 566 18 0 6993 0
vsize: 28044
[startup+160.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 5557 0 0 0 15987 14 0 0 25 0 1 0 849488791 29503488 5531 4294967295 134512640 134581267 3221224576 3221223504 134519928 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 7203 5531 566 18 0 7185 0
vsize: 28812
[startup+170.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 5785 0 0 0 16987 15 0 0 25 0 1 0 849488791 30433280 5759 4294967295 134512640 134581267 3221224576 3221223504 134519888 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 7430 5759 566 18 0 7412 0
vsize: 29720
[startup+180.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 6008 0 0 0 17987 15 0 0 25 0 1 0 849488791 31358976 5982 4294967295 134512640 134581267 3221224576 3221223568 134561045 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 7656 5982 566 18 0 7638 0
vsize: 30624
[startup+190.006 s]
Raw data (loadavg): 1.07 0.97 0.91 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 6236 0 0 0 18986 16 0 0 25 0 1 0 849488791 32280576 6210 4294967295 134512640 134581267 3221224576 3221223568 134561045 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 7881 6210 566 18 0 7863 0
vsize: 31524
[startup+200.006 s]
Raw data (loadavg): 1.13 0.99 0.92 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 6462 0 0 0 19985 17 0 0 25 0 1 0 849488791 33193984 6436 4294967295 134512640 134581267 3221224576 3221223568 134561045 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8104 6436 566 18 0 8086 0
vsize: 32416
[startup+210.006 s]
Raw data (loadavg): 1.11 0.99 0.92 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 6691 0 0 0 20985 17 0 0 25 0 1 0 849488791 34250752 6665 4294967295 134512640 134581267 3221224576 3221223504 134519952 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8362 6665 566 18 0 8344 0
vsize: 33448
[startup+220.007 s]
Raw data (loadavg): 1.09 0.99 0.92 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 6891 0 0 0 21985 18 0 0 25 0 1 0 849488791 35028992 6865 4294967295 134512640 134581267 3221224576 3221223568 134561040 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8552 6865 566 18 0 8534 0
vsize: 34208
[startup+230.007 s]
Raw data (loadavg): 1.08 0.99 0.92 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 7109 0 0 0 22984 18 0 0 25 0 1 0 849488791 35950592 7083 4294967295 134512640 134581267 3221224576 3221223568 134561045 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8777 7083 566 18 0 8759 0
vsize: 35108
[startup+240.006 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 7296 0 0 0 23984 19 0 0 25 0 1 0 849488791 36741120 7270 4294967295 134512640 134581267 3221224576 3221223504 134519803 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8970 7270 566 18 0 8952 0
vsize: 35880
[startup+250.007 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 7539 0 0 0 24984 19 0 0 25 0 1 0 849488791 37793792 7513 4294967295 134512640 134581267 3221224576 3221223504 134519797 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 9227 7513 566 18 0 9209 0
vsize: 36908
[startup+260.007 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 7817 0 0 0 25983 21 0 0 25 0 1 0 849488791 38838272 7791 4294967295 134512640 134581267 3221224576 3221223568 134561045 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 9482 7791 566 18 0 9464 0
vsize: 37928
[startup+270.008 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 8030 0 0 0 26982 21 0 0 25 0 1 0 849488791 39768064 8004 4294967295 134512640 134581267 3221224576 3221223504 134520027 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 9709 8004 566 18 0 9691 0
vsize: 38836
[startup+280.008 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 8268 0 0 0 27981 22 0 0 25 0 1 0 849488791 40779776 8242 4294967295 134512640 134581267 3221224576 3221223496 134519971 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 9956 8242 566 18 0 9938 0
vsize: 39824
[startup+290.008 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 8369 0 0 0 28981 23 0 0 25 0 1 0 849488791 41172992 8343 4294967295 134512640 134581267 3221224576 3221223504 134519803 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10052 8343 566 18 0 10034 0
vsize: 40208
[startup+300.007 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 8562 0 0 0 29980 24 0 0 25 0 1 0 849488791 41959424 8536 4294967295 134512640 134581267 3221224576 3221223548 134554608 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10244 8536 566 18 0 10226 0
vsize: 40976
[startup+310.008 s]
Raw data (loadavg): 1.10 1.00 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 8749 0 0 0 30980 24 0 0 25 0 1 0 849488791 42631168 8723 4294967295 134512640 134581267 3221224576 3221223568 134561045 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10408 8723 566 18 0 10390 0
vsize: 41632
[startup+320.008 s]
Raw data (loadavg): 1.16 1.02 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 8977 0 0 0 31980 25 0 0 25 0 1 0 849488791 43556864 8951 4294967295 134512640 134581267 3221224576 3221223456 134560294 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10634 8951 566 18 0 10616 0
vsize: 42536
[startup+330.009 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 9160 0 0 0 32980 25 0 0 25 0 1 0 849488791 44351488 9134 4294967295 134512640 134581267 3221224576 3221223568 134561045 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 10828 9134 566 18 0 10810 0
vsize: 43312
[startup+340.009 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 9426 0 0 0 33979 26 0 0 25 0 1 0 849488791 45416448 9400 4294967295 134512640 134581267 3221224576 3221223504 134520099 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11088 9400 566 18 0 11070 0
vsize: 44352
[startup+350.01 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 9731 0 0 0 34978 27 0 0 25 0 1 0 849488791 46723072 9705 4294967295 134512640 134581267 3221224576 3221223456 134560462 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11407 9705 566 18 0 11389 0
vsize: 45628
[startup+360.009 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 9757 0 0 0 35978 27 0 0 25 0 1 0 849488791 46723072 9731 4294967295 134512640 134581267 3221224576 3221223540 134519780 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11407 9731 566 18 0 11389 0
vsize: 45628
[startup+370.01 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 9757 0 0 0 36978 27 0 0 25 0 1 0 849488791 46723072 9731 4294967295 134512640 134581267 3221224576 3221223456 134520291 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11407 9731 566 18 0 11389 0
vsize: 45628
[startup+380.01 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 9757 0 0 0 37978 27 0 0 25 0 1 0 849488791 46723072 9731 4294967295 134512640 134581267 3221224576 3221223568 134561045 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11407 9731 566 18 0 11389 0
vsize: 45628
[startup+390.009 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 9757 0 0 0 38978 27 0 0 25 0 1 0 849488791 46723072 9731 4294967295 134512640 134581267 3221224576 3221223504 134519803 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11407 9731 566 18 0 11389 0
vsize: 45628
[startup+400.01 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 9757 0 0 0 39979 27 0 0 25 0 1 0 849488791 46723072 9731 4294967295 134512640 134581267 3221224576 3221223568 134561029 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11407 9731 566 18 0 11389 0
vsize: 45628
[startup+410.01 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 9757 0 0 0 40979 27 0 0 25 0 1 0 849488791 46723072 9731 4294967295 134512640 134581267 3221224576 3221223540 134519780 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11407 9731 566 18 0 11389 0
vsize: 45628
[startup+420.01 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 9757 0 0 0 41979 27 0 0 25 0 1 0 849488791 46723072 9731 4294967295 134512640 134581267 3221224576 3221223568 134561045 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11407 9731 566 18 0 11389 0
vsize: 45628
[startup+430.012 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 9757 0 0 0 42979 27 0 0 25 0 1 0 849488791 46723072 9731 4294967295 134512640 134581267 3221224576 3221223568 134561098 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11407 9731 566 18 0 11389 0
vsize: 45628
[startup+431.383 s]
Raw data (loadavg): 1.02 1.01 0.93 1/53 9702
Raw data (stat): 9702 (Pueblo-v2) R 9701 20224 20223 0 -1 0 9757 0 0 0 42979 27 0 0 25 0 1 0 849488791 46723072 9731 4294967295 134512640 134581267 3221224576 3221223568 134561098 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 11407 9731 566 18 0 11389 0
vsize: 0

Child status: 20
Real time (s): 431.382
CPU time (s): 431.442
CPU user time (s): 431.147
CPU system time (s): 0.294955
CPU usage (%): 100.014
Max. virtual memory (Kb): 45628
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####