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/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-markshare1.opb
MD5SUM	10386fd19d9976c249ce2be861b38a70
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63488
Optimality of the best value was proved	NO
Number of terms in the objective function	180
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	6442450938
Number of bits of the sum of numbers in the objective function	33
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	6442450938
Number of bits of the biggest sum of numbers	33
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.12
Number of variables	230
Total number of constraints	56
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	50
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	1
Maximum length of a constraint	80
Trace number 26541

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-05-24 16:10:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12643 boxname=wulflinc3 idbench=973 idsolver=7 numberseed=0
MD5SUM SOLVER: d9a5994a76be78982e492b397ce73911  /oldhome/oroussel/solvers/Pueblo
MD5SUM BENCH:  10386fd19d9976c249ce2be861b38a70  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-markshare1.opb
REAL COMMAND:  Pueblo /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-markshare1.opb
IDLAUNCH: 12643
/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:        928316 kB
Buffers:         34328 kB
Cached:          49680 kB
SwapCached:        108 kB
Active:          53124 kB
Inactive:        33828 kB
HighTotal:      131008 kB
HighFree:        77028 kB
LowTotal:       903652 kB
LowFree:        851288 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:            1484 kB
Writeback:           0 kB
Mapped:           6904 kB
Slab:            13736 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-24 16:23:51 (client local time) WITH STATUS 0 IN 804.684 SECONDS
stats: 12643 7 804.684 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
Pueblo: Global.h:70: T* xrealloc(T*, unsigned int) [with T = pbWatchTerm]: Assertion `size == 0 || tmp != __null' failed.
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-mps-v2-20-10-markshare1.opb
c #variables read: 230 - #constraints read: 63
#### 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.85 0.97 0.99 2/54 21545
Raw data (stat): 21545 (runsolver) R 21544 20224 20223 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 773342846 1052672 99 4294967295 134512640 135381576 3221224496 3221219716 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99988 s]
Raw data (loadavg): 0.87 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 3200 0 0 0 938 60 0 0 25 0 1 0 773342846 20422656 3178 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 4986 3178 566 18 0 4968 0
vsize: 19944
[startup+20.0004 s]
Raw data (loadavg): 0.89 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 6077 0 0 0 1881 117 0 0 25 0 1 0 773342846 34242560 6055 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 8360 6055 566 18 0 8342 0
vsize: 33440
[startup+30.0005 s]
Raw data (loadavg): 0.91 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 10356 0 0 0 2824 174 0 0 25 0 1 0 773342846 57573376 10334 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 14056 10334 566 18 0 14038 0
vsize: 56224
[startup+40.0014 s]
Raw data (loadavg): 0.92 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 11842 0 0 0 3764 234 0 0 25 0 1 0 773342846 61767680 11820 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 15080 11820 566 18 0 15062 0
vsize: 60320
[startup+50.0019 s]
Raw data (loadavg): 0.93 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 13238 0 0 0 4712 287 0 0 25 0 1 0 773342846 61767680 13216 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 15080 13216 566 18 0 15062 0
vsize: 60320
[startup+60.002 s]
Raw data (loadavg): 0.94 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 18169 0 0 0 5654 345 0 0 25 0 1 0 773342846 108441600 18086 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 26475 18086 566 18 0 26457 0
vsize: 105900
[startup+70.0029 s]
Raw data (loadavg): 0.95 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 20226 0 0 0 6599 400 0 0 25 0 1 0 773342846 116830208 20143 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 28523 20143 566 18 0 28505 0
vsize: 114092
[startup+80.0034 s]
Raw data (loadavg): 0.96 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 22283 0 0 0 7549 450 0 0 25 0 1 0 773342846 116830208 22200 4294967295 134512640 134581331 3221224592 3221223600 134529981 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 28523 22200 566 18 0 28505 0
vsize: 114092
[startup+90.0035 s]
Raw data (loadavg): 0.96 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 24340 0 0 0 8493 507 0 0 25 0 1 0 773342846 116830208 24257 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 28523 24257 566 18 0 28505 0
vsize: 114092
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 26578 0 0 0 9434 565 0 0 25 0 1 0 773342846 130461696 26495 4294967295 134512640 134581331 3221224592 3221223384 1075291632 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 31851 26502 566 18 0 31833 0
vsize: 127404
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 31557 0 0 0 10376 624 0 0 25 0 1 0 773342846 210030592 31188 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 51277 31188 566 18 0 51259 0
vsize: 205108
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 33912 0 0 0 11317 683 0 0 25 0 1 0 773342846 210030592 33543 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 51277 33543 566 18 0 51259 0
vsize: 205108
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 36267 0 0 0 12265 735 0 0 25 0 1 0 773342846 210030592 35898 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 51277 35898 566 18 0 51259 0
vsize: 205108
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 38622 0 0 0 13205 795 0 0 25 0 1 0 773342846 226807808 38253 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 55373 38253 566 18 0 55355 0
vsize: 221492
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 40821 0 0 0 14152 848 0 0 25 0 1 0 773342846 226807808 40452 4294967295 134512640 134581331 3221224592 3221223600 134530843 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 55373 40452 566 18 0 55355 0
vsize: 221492
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 43176 0 0 0 15101 900 0 0 25 0 1 0 773342846 226807808 42807 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 55373 42807 566 18 0 55355 0
vsize: 221492
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 45531 0 0 0 16040 961 0 0 25 0 1 0 773342846 226807808 45162 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 55373 45162 566 18 0 55355 0
vsize: 221492
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 47886 0 0 0 16984 1017 0 0 25 0 1 0 773342846 226807808 47517 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 55373 47517 566 18 0 55355 0
vsize: 221492
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 50242 0 0 0 17923 1078 0 0 25 0 1 0 773342846 226807808 49873 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 55373 49873 566 18 0 55355 0
vsize: 221492
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 53002 0 0 0 18870 1131 0 0 25 0 1 0 773342846 276090880 52633 4294967295 134512640 134581331 3221224592 3221223384 1075291632 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 67405 52639 566 18 0 67387 0
vsize: 269620
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 57747 0 0 0 19806 1195 0 0 25 0 1 0 773342846 411484160 56641 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 100460 56641 566 18 0 100442 0
vsize: 401840
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 60244 0 0 0 20752 1249 0 0 25 0 1 0 773342846 411484160 59138 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 100460 59138 566 18 0 100442 0
vsize: 401840
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 62742 0 0 0 21698 1304 0 0 25 0 1 0 773342846 411484160 61636 4294967295 134512640 134581331 3221224592 3221223600 134530828 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 100460 61636 566 18 0 100442 0
vsize: 401840
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 65071 0 0 0 22639 1363 0 0 25 0 1 0 773342846 411484160 63965 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 100460 63965 566 18 0 100442 0
vsize: 401840
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 67568 0 0 0 23582 1420 0 0 25 0 1 0 773342846 411484160 66462 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 100460 66462 566 18 0 100442 0
vsize: 401840
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 70065 0 0 0 24526 1476 0 0 25 0 1 0 773342846 411484160 68959 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 100460 68959 566 18 0 100442 0
vsize: 401840
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 72562 0 0 0 25471 1531 0 0 25 0 1 0 773342846 445038592 71456 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 71456 566 18 0 108634 0
vsize: 434608
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 75059 0 0 0 26417 1585 0 0 25 0 1 0 773342846 445038592 73953 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 73953 566 18 0 108634 0
vsize: 434608
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 77388 0 0 0 27360 1642 0 0 25 0 1 0 773342846 445038592 76282 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 76282 566 18 0 108634 0
vsize: 434608
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 79885 0 0 0 28302 1701 0 0 25 0 1 0 773342846 445038592 78779 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 78779 566 18 0 108634 0
vsize: 434608
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 82382 0 0 0 29248 1755 0 0 25 0 1 0 773342846 445038592 81276 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 81276 566 18 0 108634 0
vsize: 434608
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 84879 0 0 0 30192 1812 0 0 25 0 1 0 773342846 445038592 83773 4294967295 134512640 134581331 3221224592 3221223520 134529176 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 83773 566 18 0 108634 0
vsize: 434608
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 87208 0 0 0 31136 1867 0 0 25 0 1 0 773342846 445038592 86102 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 86102 566 18 0 108634 0
vsize: 434608
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 89705 0 0 0 32079 1925 0 0 25 0 1 0 773342846 445038592 88599 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 88599 566 18 0 108634 0
vsize: 434608
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 92202 0 0 0 33022 1982 0 0 25 0 1 0 773342846 445038592 91096 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 91096 566 18 0 108634 0
vsize: 434608
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 94699 0 0 0 33965 2039 0 0 25 0 1 0 773342846 445038592 93593 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 93593 566 18 0 108634 0
vsize: 434608
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 97135 0 0 0 34908 2097 0 0 25 0 1 0 773342846 445038592 96029 4294967295 134512640 134581331 3221224592 3221223552 134526969 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 96039 566 18 0 108634 0
vsize: 434608
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 99525 0 0 0 35851 2153 0 0 25 0 1 0 773342846 445038592 98419 4294967295 134512640 134581331 3221224592 3221223600 134529988 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 98419 566 18 0 108634 0
vsize: 434608
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 102022 0 0 0 36790 2214 0 0 25 0 1 0 773342846 445038592 100916 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 100916 566 18 0 108634 0
vsize: 434608
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 104518 0 0 0 37735 2270 0 0 25 0 1 0 773342846 445038592 103412 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 108652 103412 566 18 0 108634 0
vsize: 434608
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 109460 0 0 0 38665 2340 0 0 25 0 1 0 773342846 812298240 106881 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198315 106881 566 18 0 198297 0
vsize: 793260
[startup+420.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 112020 0 0 0 39608 2398 0 0 25 0 1 0 773342846 812298240 109441 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198315 109441 566 18 0 198297 0
vsize: 793260
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 114579 0 0 0 40555 2451 0 0 25 0 1 0 773342846 812298240 112000 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198315 112000 566 18 0 198297 0
vsize: 793260
[startup+440.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 116966 0 0 0 41498 2509 0 0 25 0 1 0 773342846 812298240 114387 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198315 114387 566 18 0 198297 0
vsize: 793260
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 119526 0 0 0 42447 2560 0 0 25 0 1 0 773342846 812298240 116947 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198315 116947 566 18 0 198297 0
vsize: 793260
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 122086 0 0 0 43388 2619 0 0 25 0 1 0 773342846 812298240 119507 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198315 119507 566 18 0 198297 0
vsize: 793260
[startup+470.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 124473 0 0 0 44329 2678 0 0 25 0 1 0 773342846 812298240 121894 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198315 121894 566 18 0 198297 0
vsize: 793260
[startup+480.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 127033 0 0 0 45276 2731 0 0 25 0 1 0 773342846 812298240 124454 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198315 124454 566 18 0 198297 0
vsize: 793260
[startup+490.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 129592 0 0 0 46221 2786 0 0 25 0 1 0 773342846 812298240 127013 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198315 127013 566 18 0 198297 0
vsize: 793260
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 131979 0 0 0 47170 2838 0 0 25 0 1 0 773342846 812298240 129400 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198315 129400 566 18 0 198297 0
vsize: 793260
[startup+510.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 134539 0 0 0 48117 2891 0 0 25 0 1 0 773342846 812298240 131960 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198315 131960 566 18 0 198297 0
vsize: 793260
[startup+520.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 137099 0 0 0 49062 2947 0 0 25 0 1 0 773342846 812298240 134520 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 198315 134520 566 18 0 198297 0
vsize: 793260
[startup+530.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 139659 0 0 0 50008 3000 0 0 25 0 1 0 773342846 879407104 137080 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 137080 566 18 0 214681 0
vsize: 858796
[startup+540.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 142046 0 0 0 50950 3059 0 0 25 0 1 0 773342846 879407104 139467 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 139467 566 18 0 214681 0
vsize: 858796
[startup+550.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 144606 0 0 0 51891 3118 0 0 25 0 1 0 773342846 879407104 142027 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 142027 566 18 0 214681 0
vsize: 858796
[startup+560.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 147166 0 0 0 52833 3176 0 0 25 0 1 0 773342846 879407104 144587 4294967295 134512640 134581331 3221224592 3221223600 134530828 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 144587 566 18 0 214681 0
vsize: 858796
[startup+570.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 149553 0 0 0 53773 3236 0 0 25 0 1 0 773342846 879407104 146974 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 146974 566 18 0 214681 0
vsize: 858796
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 152113 0 0 0 54720 3289 0 0 25 0 1 0 773342846 879407104 149534 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 149534 566 18 0 214681 0
vsize: 858796
[startup+590.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 154673 0 0 0 55663 3347 0 0 25 0 1 0 773342846 879407104 152094 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 152094 566 18 0 214681 0
vsize: 858796
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 157060 0 0 0 56610 3399 0 0 25 0 1 0 773342846 879407104 154481 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 154481 566 18 0 214681 0
vsize: 858796
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 159620 0 0 0 57558 3452 0 0 25 0 1 0 773342846 879407104 157041 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 157041 566 18 0 214681 0
vsize: 858796
[startup+620.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 162180 0 0 0 58505 3505 0 0 25 0 1 0 773342846 879407104 159601 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 159601 566 18 0 214681 0
vsize: 858796
[startup+630.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 164567 0 0 0 59450 3561 0 0 25 0 1 0 773342846 879407104 161988 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 161988 566 18 0 214681 0
vsize: 858796
[startup+640.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 167127 0 0 0 60390 3621 0 0 25 0 1 0 773342846 879407104 164548 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 164548 566 18 0 214681 0
vsize: 858796
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 169687 0 0 0 61334 3676 0 0 25 0 1 0 773342846 879407104 167108 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 167108 566 18 0 214681 0
vsize: 858796
[startup+660.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 172247 0 0 0 62280 3730 0 0 25 0 1 0 773342846 879407104 169668 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 169668 566 18 0 214681 0
vsize: 858796
[startup+670.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 174634 0 0 0 63223 3788 0 0 25 0 1 0 773342846 879407104 172055 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 172055 566 18 0 214681 0
vsize: 858796
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 177194 0 0 0 64167 3845 0 0 25 0 1 0 773342846 879407104 174615 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 174615 566 18 0 214681 0
vsize: 858796
[startup+690.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 179754 0 0 0 65109 3903 0 0 25 0 1 0 773342846 879407104 177175 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 177175 566 18 0 214681 0
vsize: 858796
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 182141 0 0 0 66055 3957 0 0 25 0 1 0 773342846 879407104 179562 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 179562 566 18 0 214681 0
vsize: 858796
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 184701 0 0 0 66997 4015 0 0 25 0 1 0 773342846 879407104 182122 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 182122 566 18 0 214681 0
vsize: 858796
[startup+720.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 187261 0 0 0 67942 4070 0 0 25 0 1 0 773342846 879407104 184682 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 184682 566 18 0 214681 0
vsize: 858796
[startup+730.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 189648 0 0 0 68889 4123 0 0 25 0 1 0 773342846 879407104 187069 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 187069 566 18 0 214681 0
vsize: 858796
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 192208 0 0 0 69831 4182 0 0 25 0 1 0 773342846 879407104 189629 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 189629 566 18 0 214681 0
vsize: 858796
[startup+750.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 194768 0 0 0 70775 4238 0 0 25 0 1 0 773342846 879407104 192189 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 192189 566 18 0 214681 0
vsize: 858796
[startup+760.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 197155 0 0 0 71721 4291 0 0 25 0 1 0 773342846 879407104 194576 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 194576 566 18 0 214681 0
vsize: 858796
[startup+770.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 199715 0 0 0 72664 4349 0 0 25 0 1 0 773342846 879407104 197136 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 197136 566 18 0 214681 0
vsize: 858796
[startup+780.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 202275 0 0 0 73609 4404 0 0 25 0 1 0 773342846 879407104 199696 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 199696 566 18 0 214681 0
vsize: 858796
[startup+790.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 204835 0 0 0 74553 4461 0 0 25 0 1 0 773342846 879407104 202256 4294967295 134512640 134581331 3221224592 3221223784 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 202256 566 18 0 214681 0
vsize: 858796
[startup+800.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/54 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 207222 0 0 0 75501 4513 0 0 25 0 1 0 773342846 879407104 204643 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 204643 566 18 0 214681 0
vsize: 858796
[startup+804.571 s]
Raw data (loadavg): 0.99 0.97 0.99 1/53 21545
Raw data (stat): 21545 (Pueblo) R 21544 20224 20223 0 -1 0 207222 0 0 0 75501 4513 0 0 25 0 1 0 773342846 879407104 204643 4294967295 134512640 134581331 3221224592 3221223656 1075514893 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 214699 204643 566 18 0 214681 0
vsize: 0

Child ended because it received signal 6 (SIGABRT)
Real time (s): 804.57
CPU time (s): 804.684
CPU user time (s): 758.891
CPU system time (s): 45.793
CPU usage (%): 100.014
Max. virtual memory (Kb): 858796
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####