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-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-sp98ic.opb
MD5SUM	b6b40b25db69f63dc02649b5c9a3693a
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	10894
Biggest coefficient in the objective function	1079902210
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	3040671454286
Number of bits of the sum of numbers in the objective function	42
Biggest number in a constraint	1079902210
Number of bits of the biggest number in a constraint	31
Biggest sum of numbers in a constraint	3040671454286
Number of bits of the biggest sum of numbers	42
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	8.81066
Number of variables	10894
Total number of constraints	11719
Number of constraints which are clauses	20
Number of constraints which are cardinality constraints (but not clauses)	11518
Number of constraints which are nor clauses,nor cardinality constraints	181
Minimum length of a constraint	1
Maximum length of a constraint	5038

Trace number 25318

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-18 10:39:42 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20270 boxname=wulflinc31 idbench=1560 idsolver=3 numberseed=0
MD5SUM SOLVER: 03a6a792daea978e4202f78851741568  /oldhome/oroussel/solvers/bsolo_mis
MD5SUM BENCH:  b6b40b25db69f63dc02649b5c9a3693a  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-sp98ic.opb
REAL COMMAND:  bsolo_mis /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-sp98ic.opb
IDLAUNCH: 20270
/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:        737272 kB
Buffers:         19296 kB
Cached:         255240 kB
SwapCached:        932 kB
Active:          88024 kB
Inactive:       189708 kB
HighTotal:      131008 kB
HighFree:          308 kB
LowTotal:       903652 kB
LowFree:        736964 kB
SwapTotal:     2097892 kB
SwapFree:      2096072 kB
Dirty:             220 kB
Writeback:           0 kB
Mapped:           5380 kB
Slab:            14004 kB
Committed_AS:    63860 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-18 10:47:05 (client local time) WITH STATUS 20 IN 442.088 SECONDS
stats: 20270 7 442.088 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Initial problem consists of 10894 variables and 825 constraints.
c After prepocess the problem consists of 10894 variables and 797 constraints.
c preprocess terminated 441.839 s
c Initial Lower Bound: 273169839
c Lower Bound Elapsed time: 0
c Use computed LB before first solution.
s UNSATISFIABLE
c Exit Code: 20
c Total time: 441.926 s
#### 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.88 0.97 0.99 1/55 6780
Raw data (stat): 6780 (runsolver) R 6779 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 777721455 1056768 100 4294967295 134512640 135381576 3221221680 3221216900 135158418 0 2147483391 1 90112 0 0 0 17 1 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0015 s]
Raw data (loadavg): 0.90 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 28072 0 0 0 941 56 0 0 25 0 1 0 777721455 128516096 28049 4294967295 134512640 134714540 3221221776 3221220004 1077414338 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 31376 28049 1111 63 0 31313 0
vsize: 125504
[startup+20.0022 s]
Raw data (loadavg): 0.91 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 53423 0 0 0 1897 100 0 0 25 0 1 0 777721455 232308736 53400 4294967295 134512640 134714540 3221221776 3221220432 134527932 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 56716 53400 1111 63 0 56653 0
vsize: 226864
[startup+30.0023 s]
Raw data (loadavg): 0.93 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 67012 0 0 0 2875 121 0 0 25 0 1 0 777721455 288006144 66989 4294967295 134512640 134714540 3221221776 3221218320 1077364960 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 70314 66989 1111 63 0 70251 0
vsize: 281256
[startup+40.003 s]
Raw data (loadavg): 0.94 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 67619 0 0 0 3874 122 0 0 25 0 1 0 777721455 290611200 67595 4294967295 134512640 134714540 3221221776 3221220060 1077399562 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 70950 67595 1111 63 0 70887 0
vsize: 283800
[startup+50.0041 s]
Raw data (loadavg): 0.95 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 68275 0 0 0 4873 124 0 0 25 0 1 0 777721455 293347328 68251 4294967295 134512640 134714540 3221221776 3221220052 1077414413 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 71618 68251 1111 63 0 71555 0
vsize: 286472
[startup+60.0048 s]
Raw data (loadavg): 0.95 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 68872 0 0 0 5871 125 0 0 25 0 1 0 777721455 295948288 68846 4294967295 134512640 134714540 3221221776 3221220052 1077414345 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 72253 68846 1111 63 0 72190 0
vsize: 289012
[startup+70.0057 s]
Raw data (loadavg): 0.96 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 69527 0 0 0 6869 127 0 0 25 0 1 0 777721455 298684416 69501 4294967295 134512640 134714540 3221221776 3221220052 1077414408 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 72921 69501 1111 63 0 72858 0
vsize: 291684
[startup+80.0058 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 70330 0 0 0 7867 129 0 0 25 0 1 0 777721455 302080000 70302 4294967295 134512640 134714540 3221221776 3221220060 1077399562 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 73750 70302 1111 63 0 73687 0
vsize: 295000
[startup+90.0066 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 71043 0 0 0 8866 130 0 0 25 0 1 0 777721455 305082368 71011 4294967295 134512640 134714540 3221221776 3221220272 134539126 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74483 71011 1111 63 0 74420 0
vsize: 297932
[startup+100.007 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 71741 0 0 0 9865 131 0 0 25 0 1 0 777721455 308076544 71709 4294967295 134512640 134714540 3221221776 3221220052 1077414383 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 75214 71709 1111 63 0 75151 0
vsize: 300856
[startup+110.008 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 72402 0 0 0 10864 133 0 0 25 0 1 0 777721455 310788096 72368 4294967295 134512640 134714540 3221221776 3221220064 134566780 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 75876 72368 1111 63 0 75813 0
vsize: 303504
[startup+120.008 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 11862 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220220 134536766 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+130.008 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 12862 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220220 134536817 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 13862 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220220 134536817 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 14863 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220240 134543030 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 15863 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220220 134536763 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+170.012 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 16863 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220220 134536766 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+180.012 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 17863 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220220 134535952 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+190.013 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 18864 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220304 134542980 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 19864 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220240 134543097 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+210.014 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 20864 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220528 134630795 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 21864 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220220 134536766 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 22864 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220508 134672920 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 23864 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220416 134594947 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 24865 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220220 134535903 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 25865 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220220 134536766 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73283 0 0 0 26865 135 0 0 25 0 1 0 777721455 304685056 73189 4294967295 134512640 134714540 3221221776 3221220240 134543030 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73189 1111 63 0 74323 0
vsize: 297544
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73284 0 0 0 27865 135 0 0 25 0 1 0 777721455 304685056 73190 4294967295 134512640 134714540 3221221776 3221220528 134630792 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73190 1111 63 0 74323 0
vsize: 297544
[startup+290.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73284 0 0 0 28865 135 0 0 25 0 1 0 777721455 304685056 73190 4294967295 134512640 134714540 3221221776 3221220220 134536766 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73190 1111 63 0 74323 0
vsize: 297544
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73284 0 0 0 29866 135 0 0 25 0 1 0 777721455 304685056 73190 4294967295 134512640 134714540 3221221776 3221220244 134543025 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73190 1111 63 0 74323 0
vsize: 297544
[startup+310.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73285 0 0 0 30866 135 0 0 25 0 1 0 777721455 304685056 73191 4294967295 134512640 134714540 3221221776 3221220220 134536817 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73191 1111 63 0 74323 0
vsize: 297544
[startup+320.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73287 0 0 0 31865 136 0 0 25 0 1 0 777721455 304685056 73193 4294967295 134512640 134714540 3221221776 3221220240 134543030 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73193 1111 63 0 74323 0
vsize: 297544
[startup+330.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73288 0 0 0 32865 136 0 0 25 0 1 0 777721455 304685056 73194 4294967295 134512640 134714540 3221221776 3221220416 134528592 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73194 1111 63 0 74323 0
vsize: 297544
[startup+340.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73289 0 0 0 33866 136 0 0 25 0 1 0 777721455 304685056 73195 4294967295 134512640 134714540 3221221776 3221220220 134536766 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73195 1111 63 0 74323 0
vsize: 297544
[startup+350.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73294 0 0 0 34866 136 0 0 25 0 1 0 777721455 304685056 73200 4294967295 134512640 134714540 3221221776 3221220220 134536817 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73200 1111 63 0 74323 0
vsize: 297544
[startup+360.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73298 0 0 0 35866 136 0 0 25 0 1 0 777721455 304685056 73204 4294967295 134512640 134714540 3221221776 3221220220 134536766 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73204 1111 63 0 74323 0
vsize: 297544
[startup+370.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73300 0 0 0 36866 136 0 0 25 0 1 0 777721455 304685056 73206 4294967295 134512640 134714540 3221221776 3221220336 134535760 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73206 1111 63 0 74323 0
vsize: 297544
[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73303 0 0 0 37866 136 0 0 25 0 1 0 777721455 304685056 73209 4294967295 134512640 134714540 3221221776 3221220236 134535988 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73209 1111 63 0 74323 0
vsize: 297544
[startup+390.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73305 0 0 0 38866 136 0 0 25 0 1 0 777721455 304685056 73211 4294967295 134512640 134714540 3221221776 3221220528 134630795 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73211 1111 63 0 74323 0
vsize: 297544
[startup+400.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73308 0 0 0 39867 136 0 0 25 0 1 0 777721455 304685056 73214 4294967295 134512640 134714540 3221221776 3221220528 134630795 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73214 1111 63 0 74323 0
vsize: 297544
[startup+410.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73310 0 0 0 40867 136 0 0 25 0 1 0 777721455 304685056 73216 4294967295 134512640 134714540 3221221776 3221220240 134543097 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73216 1111 63 0 74323 0
vsize: 297544
[startup+420.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73317 0 0 0 41867 136 0 0 25 0 1 0 777721455 304685056 73223 4294967295 134512640 134714540 3221221776 3221220220 134535900 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73223 1111 63 0 74323 0
vsize: 297544
[startup+430.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73319 0 0 0 42867 136 0 0 25 0 1 0 777721455 304685056 73225 4294967295 134512640 134714540 3221221776 3221220220 134536817 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73225 1111 63 0 74323 0
vsize: 297544
[startup+440.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73324 0 0 0 43867 136 0 0 25 0 1 0 777721455 304685056 73230 4294967295 134512640 134714540 3221221776 3221220220 134536817 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73230 1111 63 0 74323 0
vsize: 297544
[startup+442.072 s]
Raw data (loadavg): 0.99 0.97 0.99 1/54 6780
Raw data (stat): 6780 (bsolo_mis) R 6779 7876 7672 0 -1 0 73324 0 0 0 43867 136 0 0 25 0 1 0 777721455 304685056 73230 4294967295 134512640 134714540 3221221776 3221220220 134536817 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 74386 73230 1111 63 0 74323 0
vsize: 0

Child status: 20
Real time (s): 442.071
CPU time (s): 442.088
CPU user time (s): 440.578
CPU system time (s): 1.50977
CPU usage (%): 100.004
Max. virtual memory (Kb): 303504
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####