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.burch_dill.3.accl.ucl.opb
MD5SUM9fbb3a49a26e96e8ca349ca5e732b02f
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 36
Number of bits of the biggest number in a constraint 6
Biggest sum of numbers in a constraint 130
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 benchmark9.8365
Number of variables4622
Total number of constraints12569
Number of constraints which are clauses11753
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints816
Minimum length of a constraint1
Maximum length of a constraint11

Trace number 39684

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-06-07 16:03:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=27739 boxname=wulflinc4 idbench=297 idsolver=20 numberseed=0
MD5SUM SOLVER: f6aa7fb267fa9710116626be7e6d3048  /oldhome/oroussel/solvers/bsolo_lpr-v2
MD5SUM BENCH:  9fbb3a49a26e96e8ca349ca5e732b02f  /oldhome/oroussel/tmp/wulflinc4/normalized-ooo.burch_dill.3.accl.ucl.opb
REAL COMMAND:  bsolo_lpr-v2 /oldhome/oroussel/tmp/wulflinc4/normalized-ooo.burch_dill.3.accl.ucl.opb
IDLAUNCH: 27739
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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.169
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:        922832 kB
Buffers:         33820 kB
Cached:          55132 kB
SwapCached:        944 kB
Active:          19008 kB
Inactive:        72080 kB
HighTotal:      131008 kB
HighFree:       104776 kB
LowTotal:       903652 kB
LowFree:        818056 kB
SwapTotal:     2097136 kB
SwapFree:      2095204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4800 kB
Slab:            15088 kB
Committed_AS:    71788 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-07 16:17:11 (client local time) WITH STATUS 20 IN 804.235 SECONDS
stats: 27739 7 804.235 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c INFO: OSL Context initialized.
c INFO: No cost function. Find solution and finish.
c Initial problem consists of 4622 variables and 12569 constraints.
c After prepocess the problem consists of 3453 variables and 9923 constraints.
c preprocess terminated 102.426 s
c Not use computed LB before first solution.
s UNSATISFIABLE
c Exit Code: 20
c Total time: 804.189 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
Enforcing Stack size limit: 67108864 bytes
Current StackSize limit: 67108864 bytes
Raw data (loadavg): 0.91 0.95 0.91 1/54 18126
Raw data (stat): 18126 (runsolver) R 18125 21152 21151 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 894277056 884736 94 4294967295 134512640 135332820 3221224448 3221219628 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.0011 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 18126
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 954 42 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223200 134594947 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+20.0024 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 18126
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 1954 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223360 134617258 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+30.0033 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 18126
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 2954 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223040 134539376 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+40.0034 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 18126
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 3954 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223184 134594959 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+50.0039 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 18126
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 4954 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223200 134606484 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+60.0037 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 18126
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 5955 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223288 134543552 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+70.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18126
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 6955 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223312 134630808 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+80.0054 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18126
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 7955 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223200 134594947 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+90.0053 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18126
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 8955 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221222924 134539296 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18126
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16227 0 0 0 9955 43 0 0 25 0 1 0 894277056 69652480 16145 4294967295 134512640 134716908 3221224560 3221223176 134543796 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18126
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 10954 45 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223124 134699247 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+120.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18126
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 11952 46 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223144 134543600 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+130.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 12952 47 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223320 134588009 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+140.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 13951 48 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223152 134543740 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+150.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 14950 49 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223120 134542300 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 15949 50 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223152 134539460 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 16948 51 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223072 134535032 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 17948 52 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223152 134549700 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 18947 53 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223304 134558492 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 19946 54 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223288 134535787 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 20946 54 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223264 134528481 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+220.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 21945 55 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223216 134536638 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 22944 56 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223152 134543686 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+240.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 23944 57 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223116 134539243 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 24944 57 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223164 134536788 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 25943 58 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223328 134529276 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 26943 58 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223264 134528595 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 27942 59 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221222956 134613768 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 28941 60 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223116 134539324 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 29941 60 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223284 134655251 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 30940 61 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223212 134536763 0 0 7 0 0 0 0 17 1 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 31939 62 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223484 1077781665 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 32939 63 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223284 134535756 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+340.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 33949 63 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223200 134698487 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+350.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 34948 64 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223484 1077781665 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+360.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 35948 65 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223264 134535812 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+370.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 36947 65 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223484 1077781665 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+380.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16256 0 0 0 37947 66 0 0 25 0 1 0 894277056 69840896 16174 4294967295 134512640 134716908 3221224560 3221223116 134535903 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+390.122 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16295 0 0 0 38946 67 0 0 25 0 1 0 894277056 69976064 16213 4294967295 134512640 134716908 3221224560 3221223056 134699780 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17084 16213 1111 63 0 17021 0
vsize: 68336
[startup+400.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16522 0 0 0 39945 69 0 0 25 0 1 0 894277056 70922240 16440 4294967295 134512640 134716908 3221224560 3221223192 134543090 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17315 16440 1111 63 0 17252 0
vsize: 69260
[startup+410.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16682 0 0 0 40943 70 0 0 25 0 1 0 894277056 71462912 16600 4294967295 134512640 134716908 3221224560 3221223216 134536643 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17447 16600 1111 63 0 17384 0
vsize: 69788
[startup+420.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16868 0 0 0 41942 72 0 0 25 0 1 0 894277056 72273920 16786 4294967295 134512640 134716908 3221224560 3221223312 134594947 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17645 16786 1111 63 0 17582 0
vsize: 70580
[startup+430.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 16978 0 0 0 42942 72 0 0 25 0 1 0 894277056 72679424 16896 4294967295 134512640 134716908 3221224560 3221223212 134543588 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17744 16896 1111 63 0 17681 0
vsize: 70976
[startup+440.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17109 0 0 0 43941 73 0 0 25 0 1 0 894277056 73220096 17027 4294967295 134512640 134716908 3221224560 3221223204 134536649 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17876 17027 1111 63 0 17813 0
vsize: 71504
[startup+450.123 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17224 0 0 0 44940 75 0 0 25 0 1 0 894277056 73752576 17142 4294967295 134512640 134716908 3221224560 3221223228 134551979 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18006 17142 1111 63 0 17943 0
vsize: 72024
[startup+460.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17409 0 0 0 45939 76 0 0 25 0 1 0 894277056 74563584 17327 4294967295 134512640 134716908 3221224560 3221223224 134543600 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18204 17327 1111 63 0 18141 0
vsize: 72816
[startup+470.124 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17575 0 0 0 46938 76 0 0 25 0 1 0 894277056 75239424 17493 4294967295 134512640 134716908 3221224560 3221223216 134613601 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18369 17493 1111 63 0 18306 0
vsize: 73476
[startup+480.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17706 0 0 0 47937 78 0 0 25 0 1 0 894277056 75780096 17624 4294967295 134512640 134716908 3221224560 3221223200 134539376 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18501 17624 1111 63 0 18438 0
vsize: 74004
[startup+490.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17809 0 0 0 48936 79 0 0 25 0 1 0 894277056 76185600 17727 4294967295 134512640 134716908 3221224560 3221223248 134542836 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18600 17727 1111 63 0 18537 0
vsize: 74400
[startup+500.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 17902 0 0 0 49936 80 0 0 25 0 1 0 894277056 76595200 17820 4294967295 134512640 134716908 3221224560 3221223196 134543664 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18700 17820 1111 63 0 18637 0
vsize: 74800
[startup+510.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18107 0 0 0 50934 81 0 0 25 0 1 0 894277056 77406208 18025 4294967295 134512640 134716908 3221224560 3221223296 134528677 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18898 18025 1111 63 0 18835 0
vsize: 75592
[startup+520.125 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18227 0 0 0 51934 82 0 0 25 0 1 0 894277056 77811712 18145 4294967295 134512640 134716908 3221224560 3221223164 134536817 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18997 18145 1111 63 0 18934 0
vsize: 75988
[startup+530.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18297 0 0 0 52933 83 0 0 25 0 1 0 894277056 78082048 18215 4294967295 134512640 134716908 3221224560 3221223200 134543070 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19063 18215 1111 63 0 19000 0
vsize: 76252
[startup+540.126 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18321 0 0 0 53933 83 0 0 25 0 1 0 894277056 78217216 18239 4294967295 134512640 134716908 3221224560 3221223192 134543665 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19096 18239 1111 63 0 19033 0
vsize: 76384
[startup+550.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18363 0 0 0 54933 83 0 0 25 0 1 0 894277056 78352384 18281 4294967295 134512640 134716908 3221224560 3221223196 134699250 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19129 18281 1111 63 0 19066 0
vsize: 76516
[startup+560.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18452 0 0 0 55932 84 0 0 25 0 1 0 894277056 78757888 18370 4294967295 134512640 134716908 3221224560 3221223200 134542352 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19228 18370 1111 63 0 19165 0
vsize: 76912
[startup+570.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18608 0 0 0 56931 85 0 0 25 0 1 0 894277056 79429632 18526 4294967295 134512640 134716908 3221224560 3221223232 134542936 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19392 18526 1111 63 0 19329 0
vsize: 77568
[startup+580.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18659 0 0 0 57931 86 0 0 25 0 1 0 894277056 79564800 18577 4294967295 134512640 134716908 3221224560 3221223284 134535756 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19425 18577 1111 63 0 19362 0
vsize: 77700
[startup+590.127 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18780 0 0 0 58930 87 0 0 25 0 1 0 894277056 80089088 18698 4294967295 134512640 134716908 3221224560 3221223320 134592149 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19553 18698 1111 63 0 19490 0
vsize: 78212
[startup+600.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 18840 0 0 0 59929 88 0 0 25 0 1 0 894277056 80359424 18758 4294967295 134512640 134716908 3221224560 3221223344 134529091 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19619 18758 1111 63 0 19556 0
vsize: 78476
[startup+610.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19024 0 0 0 60929 89 0 0 25 0 1 0 894277056 81170432 18942 4294967295 134512640 134716908 3221224560 3221223304 134558485 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19817 18942 1111 63 0 19754 0
vsize: 79268
[startup+620.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19149 0 0 0 61928 89 0 0 25 0 1 0 894277056 81575936 19067 4294967295 134512640 134716908 3221224560 3221223296 134524376 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19916 19067 1111 63 0 19853 0
vsize: 79664
[startup+630.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19218 0 0 0 62928 90 0 0 25 0 1 0 894277056 81973248 19136 4294967295 134512640 134716908 3221224560 3221223140 134549630 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20013 19136 1111 63 0 19950 0
vsize: 80052
[startup+640.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19351 0 0 0 63927 91 0 0 25 0 1 0 894277056 82513920 19269 4294967295 134512640 134716908 3221224560 3221223236 134551958 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20145 19269 1111 63 0 20082 0
vsize: 80580
[startup+650.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19495 0 0 0 64927 91 0 0 25 0 1 0 894277056 83054592 19413 4294967295 134512640 134716908 3221224560 3221223484 1077781665 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20277 19413 1111 63 0 20214 0
vsize: 81108
[startup+660.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19668 0 0 0 65926 92 0 0 25 0 1 0 894277056 83726336 19586 4294967295 134512640 134716908 3221224560 3221223140 134549630 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20441 19586 1111 63 0 20378 0
vsize: 81764
[startup+670.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19802 0 0 0 66926 93 0 0 25 0 1 0 894277056 84267008 19720 4294967295 134512640 134716908 3221224560 3221223264 134528617 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20573 19720 1111 63 0 20510 0
vsize: 82292
[startup+680.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 19955 0 0 0 67925 94 0 0 25 0 1 0 894277056 84942848 19873 4294967295 134512640 134716908 3221224560 3221223164 134536848 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20738 19873 1111 63 0 20675 0
vsize: 82952
[startup+690.128 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20000 0 0 0 68925 94 0 0 25 0 1 0 894277056 85078016 19918 4294967295 134512640 134716908 3221224560 3221223204 134536649 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20771 19918 1111 63 0 20708 0
vsize: 83084
[startup+700.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20070 0 0 0 69924 94 0 0 25 0 1 0 894277056 85348352 19988 4294967295 134512640 134716908 3221224560 3221223200 134539374 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20837 19988 1111 63 0 20774 0
vsize: 83348
[startup+710.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20137 0 0 0 70924 95 0 0 25 0 1 0 894277056 85618688 20055 4294967295 134512640 134716908 3221224560 3221223120 134542347 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20903 20055 1111 63 0 20840 0
vsize: 83612
[startup+720.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20187 0 0 0 71924 95 0 0 25 0 1 0 894277056 85889024 20105 4294967295 134512640 134716908 3221224560 3221223116 134535956 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20969 20105 1111 63 0 20906 0
vsize: 83876
[startup+730.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20330 0 0 0 72923 96 0 0 25 0 1 0 894277056 86429696 20248 4294967295 134512640 134716908 3221224560 3221223188 134698632 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21101 20248 1111 63 0 21038 0
vsize: 84404
[startup+740.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20500 0 0 0 73923 97 0 0 25 0 1 0 894277056 87105536 20418 4294967295 134512640 134716908 3221224560 3221223192 134552673 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21266 20418 1111 63 0 21203 0
vsize: 85064
[startup+750.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20647 0 0 0 74922 98 0 0 25 0 1 0 894277056 87785472 20565 4294967295 134512640 134716908 3221224560 3221223216 134536638 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21432 20565 1111 63 0 21369 0
vsize: 85728
[startup+760.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20791 0 0 0 75921 98 0 0 25 0 1 0 894277056 88326144 20709 4294967295 134512640 134716908 3221224560 3221223344 134529368 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21564 20709 1111 63 0 21501 0
vsize: 86256
[startup+770.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20852 0 0 0 76921 99 0 0 25 0 1 0 894277056 88596480 20770 4294967295 134512640 134716908 3221224560 3221223216 134524067 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21630 20770 1111 63 0 21567 0
vsize: 86520
[startup+780.13 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20910 0 0 0 77921 99 0 0 25 0 1 0 894277056 88854528 20828 4294967295 134512640 134716908 3221224560 3221223152 134549773 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21693 20828 1111 63 0 21630 0
vsize: 86772
[startup+790.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 20950 0 0 0 78920 100 0 0 25 0 1 0 894277056 88989696 20868 4294967295 134512640 134716908 3221224560 3221223140 134698632 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21726 20868 1111 63 0 21663 0
vsize: 86904
[startup+800.129 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 21004 0 0 0 79919 101 0 0 25 0 1 0 894277056 89268224 20922 4294967295 134512640 134716908 3221224560 3221223280 134529381 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21794 20922 1111 63 0 21731 0
vsize: 87176
[startup+804.152 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 18128
Raw data (stat): 18126 (bsolo_lpr-v2) R 18125 21152 21151 0 -1 0 21004 0 0 0 79919 101 0 0 25 0 1 0 894277056 89268224 20922 4294967295 134512640 134716908 3221224560 3221223280 134529381 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21794 20922 1111 63 0 21731 0
vsize: 0

Child status: 20
Real time (s): 804.152
CPU time (s): 804.235
CPU user time (s): 803.174
CPU system time (s): 1.06084
CPU usage (%): 100.01
Max. virtual memory (Kb): 87176
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####