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 40856

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-06-08 23:04:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=28911 boxname=wulflinc3 idbench=297 idsolver=21 numberseed=0
MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb  /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2
MD5SUM BENCH:  9fbb3a49a26e96e8ca349ca5e732b02f  /oldhome/oroussel/tmp/wulflinc3/normalized-ooo.burch_dill.3.accl.ucl.opb
REAL COMMAND:  bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc3/normalized-ooo.burch_dill.3.accl.ucl.opb
IDLAUNCH: 28911
/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:        908764 kB
Buffers:         18432 kB
Cached:          84728 kB
SwapCached:       3464 kB
Active:          27748 kB
Inactive:        80136 kB
HighTotal:      131008 kB
HighFree:        53732 kB
LowTotal:       903652 kB
LowFree:        855032 kB
SwapTotal:     2097136 kB
SwapFree:      2092672 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5012 kB
Slab:            12364 kB
Committed_AS:    71792 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-06-08 23:18:05 (client local time) WITH STATUS 20 IN 792.601 SECONDS
stats: 28911 7 792.601 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 101.249 s
c Not use computed LB before first solution.
s UNSATISFIABLE
c Exit Code: 20
c Total time: 792.556 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.83 0.93 0.90 2/54 1103
Raw data (stat): 1103 (runsolver) R 1102 20224 20223 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 905445957 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.0007 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 1103
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16227 0 0 0 955 42 0 0 25 0 1 0 905445957 69652480 16145 4294967295 134512640 134716908 3221224560 3221222968 134543589 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+20.0008 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 1103
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16227 0 0 0 1955 42 0 0 25 0 1 0 905445957 69652480 16145 4294967295 134512640 134716908 3221224560 3221223188 134594953 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+30.0014 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 1103
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16227 0 0 0 2955 42 0 0 25 0 1 0 905445957 69652480 16145 4294967295 134512640 134716908 3221224560 3221223184 134529222 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17005 16145 1111 63 0 16942 0
vsize: 68020
[startup+40.0012 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 1103
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16227 0 0 0 3955 42 0 0 25 0 1 0 905445957 69652480 16145 4294967295 134512640 134716908 3221224560 3221223040 134539462 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.0024 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16227 0 0 0 4955 42 0 0 25 0 1 0 905445957 69652480 16145 4294967295 134512640 134716908 3221224560 3221223288 134675274 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.0019 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16227 0 0 0 5955 42 0 0 25 0 1 0 905445957 69652480 16145 4294967295 134512640 134716908 3221224560 3221223040 134536638 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.0017 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16227 0 0 0 6956 42 0 0 25 0 1 0 905445957 69652480 16145 4294967295 134512640 134716908 3221224560 3221222924 134539237 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.0029 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16227 0 0 0 7956 42 0 0 25 0 1 0 905445957 69652480 16145 4294967295 134512640 134716908 3221224560 3221223040 134539462 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.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16227 0 0 0 8956 42 0 0 25 0 1 0 905445957 69652480 16145 4294967295 134512640 134716908 3221224560 3221223160 134543614 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.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16227 0 0 0 9956 42 0 0 25 0 1 0 905445957 69652480 16145 4294967295 134512640 134716908 3221224560 3221222944 134542352 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.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 10954 44 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223120 134542350 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+120.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 11953 45 0 0 25 0 1 0 905445957 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+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 12953 46 0 0 25 0 1 0 905445957 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+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 13952 46 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223152 134539425 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 14952 47 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223184 134543686 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+160.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 15952 47 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223152 134539462 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+170.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 16951 48 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223344 134529126 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+180.003 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 17951 49 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223296 134535745 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 18951 49 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223280 134584759 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 19951 49 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223184 134536678 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 20951 49 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223168 134549316 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 21950 50 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223288 134543834 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+230.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 22950 50 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223196 134552672 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 23949 51 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223224 134543600 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+250.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 24949 52 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223144 134542291 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+260.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 25949 52 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223068 134535956 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+270.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 26949 53 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223272 134543600 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+280.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 27948 53 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223200 134542350 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 28948 54 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223100 134539237 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 29948 54 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223152 134549527 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 30948 54 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223120 134698898 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17051 16174 1111 63 0 16988 0
vsize: 68204
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 31948 55 0 0 25 0 1 0 905445957 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 32947 55 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223240 134552650 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.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 33947 56 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223136 134542753 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 34947 56 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223328 134529281 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.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 35946 57 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223144 134543589 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 36946 57 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223232 134551963 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16256 0 0 0 37946 58 0 0 25 0 1 0 905445957 69840896 16174 4294967295 134512640 134716908 3221224560 3221223172 134523378 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.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16384 0 0 0 38945 59 0 0 25 0 1 0 905445957 70246400 16302 4294967295 134512640 134716908 3221224560 3221223264 134528677 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17150 16302 1111 63 0 17087 0
vsize: 68600
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16581 0 0 0 39944 60 0 0 25 0 1 0 905445957 71057408 16499 4294967295 134512640 134716908 3221224560 3221223216 134536736 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17348 16499 1111 63 0 17285 0
vsize: 69392
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16756 0 0 0 40943 61 0 0 25 0 1 0 905445957 71868416 16674 4294967295 134512640 134716908 3221224560 3221223264 134528410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17546 16674 1111 63 0 17483 0
vsize: 70184
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 16894 0 0 0 41942 62 0 0 25 0 1 0 905445957 72409088 16812 4294967295 134512640 134716908 3221224560 3221223144 134543600 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17678 16812 1111 63 0 17615 0
vsize: 70712
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 17038 0 0 0 42941 63 0 0 25 0 1 0 905445957 72949760 16956 4294967295 134512640 134716908 3221224560 3221223200 134542352 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17810 16956 1111 63 0 17747 0
vsize: 71240
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 17159 0 0 0 43941 64 0 0 25 0 1 0 905445957 73482240 17077 4294967295 134512640 134716908 3221224560 3221223232 134542974 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 17940 17077 1111 63 0 17877 0
vsize: 71760
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 17263 0 0 0 44940 65 0 0 25 0 1 0 905445957 73887744 17181 4294967295 134512640 134716908 3221224560 3221223128 134543614 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18039 17181 1111 63 0 17976 0
vsize: 72156
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 17475 0 0 0 45939 66 0 0 25 0 1 0 905445957 74833920 17393 4294967295 134512640 134716908 3221224560 3221222796 134613972 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18270 17393 1111 63 0 18207 0
vsize: 73080
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 17643 0 0 0 46938 67 0 0 25 0 1 0 905445957 75509760 17561 4294967295 134512640 134716908 3221224560 3221223212 134536817 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18435 17562 1111 63 0 18372 0
vsize: 73740
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 17770 0 0 0 47937 68 0 0 25 0 1 0 905445957 75915264 17688 4294967295 134512640 134716908 3221224560 3221223152 134698400 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18534 17688 1111 63 0 18471 0
vsize: 74136
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 17868 0 0 0 48937 69 0 0 25 0 1 0 905445957 76320768 17786 4294967295 134512640 134716908 3221224560 3221223324 134552548 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18633 17786 1111 63 0 18570 0
vsize: 74532
[startup+500.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 18024 0 0 0 49936 70 0 0 25 0 1 0 905445957 77000704 17942 4294967295 134512640 134716908 3221224560 3221223200 134539376 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18799 17942 1111 63 0 18736 0
vsize: 75196
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 18188 0 0 0 50936 71 0 0 25 0 1 0 905445957 77676544 18106 4294967295 134512640 134716908 3221224560 3221223116 134535967 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 18964 18106 1111 63 0 18901 0
vsize: 75856
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 18275 0 0 0 51935 72 0 0 25 0 1 0 905445957 78082048 18193 4294967295 134512640 134716908 3221224560 3221223104 134552012 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19063 18193 1111 63 0 19000 0
vsize: 76252
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 18303 0 0 0 52934 72 0 0 25 0 1 0 905445957 78217216 18221 4294967295 134512640 134716908 3221224560 3221223264 134528595 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19096 18221 1111 63 0 19033 0
vsize: 76384
[startup+540.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 18344 0 0 0 53934 73 0 0 25 0 1 0 905445957 78352384 18262 4294967295 134512640 134716908 3221224560 3221223304 134675300 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19129 18262 1111 63 0 19066 0
vsize: 76516
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 18419 0 0 0 54934 73 0 0 25 0 1 0 905445957 78622720 18337 4294967295 134512640 134716908 3221224560 3221223280 134535795 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19195 18337 1111 63 0 19132 0
vsize: 76780
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 18543 0 0 0 55933 74 0 0 25 0 1 0 905445957 79159296 18461 4294967295 134512640 134716908 3221224560 3221223284 134535756 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19326 18461 1111 63 0 19263 0
vsize: 77304
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 18654 0 0 0 56933 75 0 0 25 0 1 0 905445957 79564800 18572 4294967295 134512640 134716908 3221224560 3221223168 134549327 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19425 18572 1111 63 0 19362 0
vsize: 77700
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 18761 0 0 0 57931 76 0 0 25 0 1 0 905445957 80089088 18679 4294967295 134512640 134716908 3221224560 3221223248 134543698 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19553 18679 1111 63 0 19490 0
vsize: 78212
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 18815 0 0 0 58931 77 0 0 25 0 1 0 905445957 80224256 18733 4294967295 134512640 134716908 3221224560 3221223120 134542350 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19586 18733 1111 63 0 19523 0
vsize: 78344
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 18980 0 0 0 59930 78 0 0 25 0 1 0 905445957 80900096 18898 4294967295 134512640 134716908 3221224560 3221223200 134539362 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19751 18898 1111 63 0 19688 0
vsize: 79004
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 19126 0 0 0 60929 79 0 0 25 0 1 0 905445957 81575936 19044 4294967295 134512640 134716908 3221224560 3221223028 134699704 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19916 19044 1111 63 0 19853 0
vsize: 79664
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 19183 0 0 0 61928 80 0 0 25 0 1 0 905445957 81838080 19101 4294967295 134512640 134716908 3221224560 3221223116 134539251 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 19980 19101 1111 63 0 19917 0
vsize: 79920
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 19308 0 0 0 62928 81 0 0 25 0 1 0 905445957 82243584 19226 4294967295 134512640 134716908 3221224560 3221223288 134543804 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20079 19226 1111 63 0 20016 0
vsize: 80316
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 19470 0 0 0 63927 82 0 0 25 0 1 0 905445957 82919424 19388 4294967295 134512640 134716908 3221224560 3221223204 134536649 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20244 19388 1111 63 0 20181 0
vsize: 80976
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 19638 0 0 0 64926 83 0 0 25 0 1 0 905445957 83595264 19556 4294967295 134512640 134716908 3221224560 3221223188 134698608 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20409 19556 1111 63 0 20346 0
vsize: 81636
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 19785 0 0 0 65925 84 0 0 25 0 1 0 905445957 84267008 19703 4294967295 134512640 134716908 3221224560 3221223264 134528410 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20573 19703 1111 63 0 20510 0
vsize: 82292
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 19949 0 0 0 66925 85 0 0 25 0 1 0 905445957 84942848 19867 4294967295 134512640 134716908 3221224560 3221223280 134535762 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20738 19867 1111 63 0 20675 0
vsize: 82952
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 19994 0 0 0 67925 85 0 0 25 0 1 0 905445957 85078016 19912 4294967295 134512640 134716908 3221224560 3221223044 134699569 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20771 19912 1111 63 0 20708 0
vsize: 83084
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 20054 0 0 0 68924 86 0 0 25 0 1 0 905445957 85348352 19972 4294967295 134512640 134716908 3221224560 3221223128 134613769 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20837 19972 1111 63 0 20774 0
vsize: 83348
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 20134 0 0 0 69924 86 0 0 25 0 1 0 905445957 85618688 20052 4294967295 134512640 134716908 3221224560 3221223068 134535956 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20903 20052 1111 63 0 20840 0
vsize: 83612
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 20184 0 0 0 70923 87 0 0 25 0 1 0 905445957 85889024 20102 4294967295 134512640 134716908 3221224560 3221223152 134549689 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 20969 20102 1111 63 0 20906 0
vsize: 83876
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 20330 0 0 0 71923 88 0 0 25 0 1 0 905445957 86429696 20248 4294967295 134512640 134716908 3221224560 3221223212 134536842 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21101 20248 1111 63 0 21038 0
vsize: 84404
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 20500 0 0 0 72922 89 0 0 25 0 1 0 905445957 87105536 20418 4294967295 134512640 134716908 3221224560 3221223264 134535812 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21266 20418 1111 63 0 21203 0
vsize: 85064
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 20647 0 0 0 73921 89 0 0 25 0 1 0 905445957 87785472 20565 4294967295 134512640 134716908 3221224560 3221223116 134535649 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21432 20565 1111 63 0 21369 0
vsize: 85728
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 20803 0 0 0 74921 90 0 0 25 0 1 0 905445957 88461312 20721 4294967295 134512640 134716908 3221224560 3221223344 134529206 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21597 20721 1111 63 0 21534 0
vsize: 86388
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 20854 0 0 0 75921 90 0 0 25 0 1 0 905445957 88596480 20772 4294967295 134512640 134716908 3221224560 3221223200 134543110 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21630 20772 1111 63 0 21567 0
vsize: 86520
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 20915 0 0 0 76921 90 0 0 25 0 1 0 905445957 88854528 20833 4294967295 134512640 134716908 3221224560 3221223328 134592116 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21693 20833 1111 63 0 21630 0
vsize: 86772
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 20957 0 0 0 77920 91 0 0 25 0 1 0 905445957 88989696 20875 4294967295 134512640 134716908 3221224560 3221223068 134535952 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21726 20875 1111 63 0 21663 0
vsize: 86904
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 21017 0 0 0 78920 92 0 0 25 0 1 0 905445957 89268224 20935 4294967295 134512640 134716908 3221224560 3221223068 134535900 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21794 20935 1111 63 0 21731 0
vsize: 87176
[startup+792.507 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 1105
Raw data (stat): 1103 (bsolo_lpr_cuts-) R 1102 20224 20223 0 -1 0 21017 0 0 0 78920 92 0 0 25 0 1 0 905445957 89268224 20935 4294967295 134512640 134716908 3221224560 3221223068 134535900 0 0 7 0 0 0 0 17 0 0 0
Raw data (statm): 21794 20935 1111 63 0 21731 0
vsize: 0

Child status: 20
Real time (s): 792.507
CPU time (s): 792.601
CPU user time (s): 791.64
CPU system time (s): 0.961853
CPU usage (%): 100.012
Max. virtual memory (Kb): 87176
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####