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/web/uclid_pb_benchmarks/normalized-ooo.burch_dill.3.accl.ucl.opb
MD5SUM	9fbb3a49a26e96e8ca349ca5e732b02f
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(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 numbers	8
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	9.8365
Number of variables	4622
Total number of constraints	12569
Number of constraints which are clauses	11753
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	816
Minimum length of a constraint	1
Maximum length of a constraint	11
Trace number 24623

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-05-11 07:35:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2666 boxname=wulflinc31 idbench=297 idsolver=2 numberseed=0
MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7  /oldhome/oroussel/solvers/bsolo_lpr_cuts
MD5SUM BENCH:  9fbb3a49a26e96e8ca349ca5e732b02f  /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.burch_dill.3.accl.ucl.opb
REAL COMMAND:  bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc31/normalized-ooo.burch_dill.3.accl.ucl.opb
IDLAUNCH: 2666
/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:        921396 kB
Buffers:         12744 kB
Cached:          77792 kB
SwapCached:       1672 kB
Active:          54104 kB
Inactive:        39240 kB
HighTotal:      131008 kB
HighFree:        51464 kB
LowTotal:       903652 kB
LowFree:        869932 kB
SwapTotal:     2097892 kB
SwapFree:      2094976 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4700 kB
Slab:            14216 kB
Committed_AS:    63652 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-11 07:49:26 (client local time) WITH STATUS 20 IN 819.947 SECONDS
stats: 2666 7 819.947 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 105.213 s
c Not use computed LB before first solution.
s UNSATISFIABLE
c Exit Code: 20
c Total time: 819.886 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.92 0.95 0.90 2/54 27502
Raw data (stat): 27502 (runsolver) R 27501 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 716130700 1056768 100 4294967295 134512640 135381576 3221221664 3221216880 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0
Raw data (statm): 258 100 215 215 0 43 0
vsize: 1032
[startup+10.0014 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16226 0 0 0 950 45 0 0 25 0 1 0 716130700 69656576 16147 4294967295 134512640 134714508 3221221760 3221220360 134543614 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17006 16147 1111 63 0 16943 0
vsize: 68024
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16226 0 0 0 1951 45 0 0 25 0 1 0 716130700 69656576 16147 4294967295 134512640 134714508 3221221760 3221220448 134606709 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17006 16147 1111 63 0 16943 0
vsize: 68024
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16226 0 0 0 2951 45 0 0 25 0 1 0 716130700 69656576 16147 4294967295 134512640 134714508 3221221760 3221220124 134539296 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17006 16147 1111 63 0 16943 0
vsize: 68024
[startup+40.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16226 0 0 0 3951 45 0 0 25 0 1 0 716130700 69656576 16147 4294967295 134512640 134714508 3221221760 3221220268 134543615 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17006 16147 1111 63 0 16943 0
vsize: 68024
[startup+50.0024 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16226 0 0 0 4951 45 0 0 25 0 1 0 716130700 69656576 16147 4294967295 134512640 134714508 3221221760 3221220368 134529381 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17006 16147 1111 63 0 16943 0
vsize: 68024
[startup+60.0033 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16226 0 0 0 5951 45 0 0 25 0 1 0 716130700 69656576 16147 4294967295 134512640 134714508 3221221760 3221220124 134539237 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17006 16147 1111 63 0 16943 0
vsize: 68024
[startup+70.0038 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16226 0 0 0 6952 45 0 0 25 0 1 0 716130700 69656576 16147 4294967295 134512640 134714508 3221221760 3221220264 134543600 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17006 16147 1111 63 0 16943 0
vsize: 68024
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16226 0 0 0 7952 45 0 0 25 0 1 0 716130700 69656576 16147 4294967295 134512640 134714508 3221221760 3221220240 134542365 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17006 16147 1111 63 0 16943 0
vsize: 68024
[startup+90.0031 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16226 0 0 0 8952 45 0 0 25 0 1 0 716130700 69656576 16147 4294967295 134512640 134714508 3221221760 3221220376 134536921 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17006 16147 1111 63 0 16943 0
vsize: 68024
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16226 0 0 0 9952 45 0 0 25 0 1 0 716130700 69656576 16147 4294967295 134512640 134714508 3221221760 3221220124 134539223 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17006 16147 1111 63 0 16943 0
vsize: 68024
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 10951 46 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220368 134548843 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 11949 48 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220352 134539511 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 12948 50 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220424 134543600 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 13947 51 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220400 134539471 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 14947 52 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220000 134697328 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 15945 53 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220416 134524067 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 16944 54 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220320 134542352 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 17943 55 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220472 134543665 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 18943 56 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220416 134536638 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 19942 57 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220328 134543614 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 20941 57 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220352 134549689 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 21941 58 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220316 134539208 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 22939 60 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220432 134551963 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 23938 61 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220416 134536638 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 24938 61 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220472 134552681 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 25937 62 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220268 134535900 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 26937 62 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220400 134696273 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 27937 63 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220236 134613956 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 28936 63 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220400 134539362 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 29936 64 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220352 134549745 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 30935 65 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220432 134543712 0 0 1 0 0 0 0 17 1 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 31935 65 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220464 134528543 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+330.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 32935 66 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220348 134539329 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 33934 66 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220344 134543600 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 34934 67 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220320 134542347 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 35934 67 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220308 134696712 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 36933 68 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220416 134536638 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+380.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 37933 69 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220504 134543133 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16256 0 0 0 38931 70 0 0 25 0 1 0 716130700 69844992 16177 4294967295 134512640 134714508 3221221760 3221220412 134536817 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17052 16177 1111 63 0 16989 0
vsize: 68208
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16314 0 0 0 39930 72 0 0 25 0 1 0 716130700 69980160 16235 4294967295 134512640 134714508 3221221760 3221220464 134528665 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17085 16235 1111 63 0 17022 0
vsize: 68340
[startup+410.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16535 0 0 0 40929 73 0 0 25 0 1 0 716130700 70926336 16456 4294967295 134512640 134714508 3221221760 3221220340 134549630 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17316 16456 1111 63 0 17253 0
vsize: 69264
[startup+420.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16693 0 0 0 41928 74 0 0 25 0 1 0 716130700 71602176 16614 4294967295 134512640 134714508 3221221760 3221220376 134542657 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17481 16614 1111 63 0 17418 0
vsize: 69924
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16869 0 0 0 42927 76 0 0 25 0 1 0 716130700 72278016 16790 4294967295 134512640 134714508 3221221760 3221220384 134542936 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17646 16790 1111 63 0 17583 0
vsize: 70584
[startup+440.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 16978 0 0 0 43926 77 0 0 25 0 1 0 716130700 72683520 16899 4294967295 134512640 134714508 3221221760 3221220352 134696069 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17745 16899 1111 63 0 17682 0
vsize: 70980
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 17109 0 0 0 44925 77 0 0 25 0 1 0 716130700 73224192 17030 4294967295 134512640 134714508 3221221760 3221220464 134528617 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 17877 17030 1111 63 0 17814 0
vsize: 71508
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 17224 0 0 0 45924 79 0 0 25 0 1 0 716130700 73756672 17145 4294967295 134512640 134714508 3221221760 3221220364 134536766 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18007 17145 1111 63 0 17944 0
vsize: 72028
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 17401 0 0 0 46923 80 0 0 25 0 1 0 716130700 74432512 17322 4294967295 134512640 134714508 3221221760 3221220408 134543638 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18172 17322 1111 63 0 18109 0
vsize: 72688
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 17569 0 0 0 47922 81 0 0 25 0 1 0 716130700 75108352 17490 4294967295 134512640 134714508 3221221760 3221220476 134552579 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18337 17490 1111 63 0 18274 0
vsize: 73348
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 17705 0 0 0 48921 82 0 0 25 0 1 0 716130700 75649024 17626 4294967295 134512640 134714508 3221221760 3221220268 134535882 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18469 17626 1111 63 0 18406 0
vsize: 73876
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 17809 0 0 0 49921 83 0 0 25 0 1 0 716130700 76189696 17730 4294967295 134512640 134714508 3221221760 3221220344 134543600 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18601 17730 1111 63 0 18538 0
vsize: 74404
[startup+510.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 17900 0 0 0 50919 84 0 0 25 0 1 0 716130700 76460032 17821 4294967295 134512640 134714508 3221221760 3221220320 134542701 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18667 17821 1111 63 0 18604 0
vsize: 74668
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 18088 0 0 0 51919 85 0 0 25 0 1 0 716130700 77275136 18009 4294967295 134512640 134714508 3221221760 3221220412 134542288 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18866 18009 1111 63 0 18803 0
vsize: 75464
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 18213 0 0 0 52918 87 0 0 25 0 1 0 716130700 77815808 18134 4294967295 134512640 134714508 3221221760 3221220300 134539282 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 18998 18134 1111 63 0 18935 0
vsize: 75992
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 18298 0 0 0 53917 87 0 0 25 0 1 0 716130700 78086144 18219 4294967295 134512640 134714508 3221221760 3221220360 134543614 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19064 18219 1111 63 0 19001 0
vsize: 76256
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 18322 0 0 0 54917 88 0 0 25 0 1 0 716130700 78221312 18243 4294967295 134512640 134714508 3221221760 3221220496 134535745 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19097 18243 1111 63 0 19034 0
vsize: 76388
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 18351 0 0 0 55917 88 0 0 25 0 1 0 716130700 78356480 18272 4294967295 134512640 134714508 3221221760 3221220352 134549609 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19130 18272 1111 63 0 19067 0
vsize: 76520
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 18444 0 0 0 56916 88 0 0 25 0 1 0 716130700 78761984 18365 4294967295 134512640 134714508 3221221760 3221220432 134551968 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19229 18365 1111 63 0 19166 0
vsize: 76916
[startup+580.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 18568 0 0 0 57916 89 0 0 25 0 1 0 716130700 79298560 18489 4294967295 134512640 134714508 3221221760 3221220352 134539374 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19360 18489 1111 63 0 19297 0
vsize: 77440
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 18655 0 0 0 58916 90 0 0 25 0 1 0 716130700 79568896 18576 4294967295 134512640 134714508 3221221760 3221220400 134696078 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19426 18576 1111 63 0 19363 0
vsize: 77704
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 18775 0 0 0 59915 91 0 0 25 0 1 0 716130700 80093184 18696 4294967295 134512640 134714508 3221221760 3221220464 134528691 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19554 18696 1111 63 0 19491 0
vsize: 78216
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 18816 0 0 0 60915 91 0 0 25 0 1 0 716130700 80228352 18737 4294967295 134512640 134714508 3221221760 3221220320 134542347 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19587 18737 1111 63 0 19524 0
vsize: 78348
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 18977 0 0 0 61914 92 0 0 25 0 1 0 716130700 80904192 18898 4294967295 134512640 134714508 3221221760 3221220380 134536748 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19752 18898 1111 63 0 19689 0
vsize: 79008
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 19127 0 0 0 62913 93 0 0 25 0 1 0 716130700 81580032 19048 4294967295 134512640 134714508 3221221760 3221220316 134535967 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19917 19048 1111 63 0 19854 0
vsize: 79668
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 19179 0 0 0 63912 95 0 0 25 0 1 0 716130700 81707008 19100 4294967295 134512640 134714508 3221221760 3221220400 134542347 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 19948 19100 1111 63 0 19885 0
vsize: 79792
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 19286 0 0 0 64911 95 0 0 25 0 1 0 716130700 82247680 19207 4294967295 134512640 134714508 3221221760 3221220516 134652883 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20080 19207 1111 63 0 20017 0
vsize: 80320
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 19447 0 0 0 65911 96 0 0 25 0 1 0 716130700 82923520 19368 4294967295 134512640 134714508 3221221760 3221220340 134696240 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20245 19368 1111 63 0 20182 0
vsize: 80980
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 19593 0 0 0 66910 96 0 0 25 0 1 0 716130700 83464192 19514 4294967295 134512640 134714508 3221221760 3221220400 134539382 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20377 19514 1111 63 0 20314 0
vsize: 81508
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 19738 0 0 0 67909 98 0 0 25 0 1 0 716130700 84000768 19659 4294967295 134512640 134714508 3221221760 3221220544 134529174 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20508 19659 1111 63 0 20445 0
vsize: 82032
[startup+690.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 19902 0 0 0 68908 98 0 0 25 0 1 0 716130700 84676608 19823 4294967295 134512640 134714508 3221221760 3221220452 134528601 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20673 19823 1111 63 0 20610 0
vsize: 82692
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 19983 0 0 0 69908 99 0 0 25 0 1 0 716130700 85082112 19904 4294967295 134512640 134714508 3221221760 3221220432 134536700 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20772 19904 1111 63 0 20709 0
vsize: 83088
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 20022 0 0 0 70908 99 0 0 25 0 1 0 716130700 85217280 19943 4294967295 134512640 134714508 3221221760 3221220496 134535745 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20805 19943 1111 63 0 20742 0
vsize: 83220
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 20116 0 0 0 71908 100 0 0 25 0 1 0 716130700 85622784 20037 4294967295 134512640 134714508 3221221760 3221220684 1077781665 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20904 20037 1111 63 0 20841 0
vsize: 83616
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 20153 0 0 0 72908 100 0 0 25 0 1 0 716130700 85757952 20074 4294967295 134512640 134714508 3221221760 3221220404 134536694 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 20937 20074 1111 63 0 20874 0
vsize: 83748
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 20232 0 0 0 73907 100 0 0 25 0 1 0 716130700 86028288 20153 4294967295 134512640 134714508 3221221760 3221220300 134539284 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 21003 20153 1111 63 0 20940 0
vsize: 84012
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 20410 0 0 0 74907 101 0 0 25 0 1 0 716130700 86839296 20331 4294967295 134512640 134714508 3221221760 3221220316 134539243 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 21201 20331 1111 63 0 21138 0
vsize: 84804
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 20559 0 0 0 75907 102 0 0 25 0 1 0 716130700 87379968 20480 4294967295 134512640 134714508 3221221760 3221220384 134543097 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 21333 20480 1111 63 0 21270 0
vsize: 85332
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 20731 0 0 0 76906 103 0 0 25 0 1 0 716130700 88186880 20652 4294967295 134512640 134714508 3221221760 3221220300 134613956 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 21530 20652 1111 63 0 21467 0
vsize: 86120
[startup+780.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 20829 0 0 0 77905 103 0 0 25 0 1 0 716130700 88457216 20750 4294967295 134512640 134714508 3221221760 3221220352 134549689 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 21596 20750 1111 63 0 21533 0
vsize: 86384
[startup+790.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 20875 0 0 0 78905 104 0 0 25 0 1 0 716130700 88727552 20796 4294967295 134512640 134714508 3221221760 3221220084 134697183 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 21662 20796 1111 63 0 21599 0
vsize: 86648
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 20916 0 0 0 79904 104 0 0 25 0 1 0 716130700 88862720 20837 4294967295 134512640 134714508 3221221760 3221220344 134543647 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 21695 20837 1111 63 0 21632 0
vsize: 86780
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 20971 0 0 0 80904 105 0 0 25 0 1 0 716130700 89137152 20892 4294967295 134512640 134714508 3221221760 3221220420 134543680 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 21762 20892 1111 63 0 21699 0
vsize: 87048
[startup+819.873 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 27502
Raw data (stat): 27502 (bsolo_lpr_cuts) R 27501 7876 7672 0 -1 0 20971 0 0 0 80904 105 0 0 25 0 1 0 716130700 89137152 20892 4294967295 134512640 134714508 3221221760 3221220420 134543680 0 0 1 0 0 0 0 17 0 0 0
Raw data (statm): 21762 20892 1111 63 0 21699 0
vsize: 0

Child status: 20
Real time (s): 819.872
CPU time (s): 819.947
CPU user time (s): 818.846
CPU system time (s): 1.10083
CPU usage (%): 100.009
Max. virtual memory (Kb): 87048
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####