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.tag8.ucl.opb
MD5SUM2c9d0c47cb8e4f2ef0877b0c52225df4
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 33
Number of bits of the biggest number in a constraint 6
Biggest sum of numbers in a constraint 126
Number of bits of the biggest sum of numbers7
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark1.40878
Number of variables3249
Total number of constraints8983
Number of constraints which are clauses8599
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints384
Minimum length of a constraint1
Maximum length of a constraint11

Trace number 4466

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-13 17:39:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2817 boxname=wulflinc18 idbench=313 idsolver=9 numberseed=0
MD5SUM SOLVER: daf345f6fbf228671abfac48013b9cac  /oldhome/oroussel/solvers/sat4jPseudo.jar
MD5SUM BENCH:  2c9d0c47cb8e4f2ef0877b0c52225df4  /oldhome/oroussel/tmp/wulflinc18/normalized-ooo.tag8.ucl.opb
REAL COMMAND:  java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudo.jar /oldhome/oroussel/tmp/wulflinc18/normalized-ooo.tag8.ucl.opb
IDLAUNCH: 2817
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        924368 kB
Buffers:         33540 kB
Cached:          40872 kB
SwapCached:        320 kB
Active:          44672 kB
Inactive:        32912 kB
HighTotal:      131008 kB
HighFree:        86128 kB
LowTotal:       903652 kB
LowFree:        838240 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27148 kB
Committed_AS:    63700 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 17:51:48 (client local time) WITH STATUS 20 IN  SECONDS
stats: 2817 7  20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc18/normalized-ooo.tag8.ucl.opb
c reading problem 
c [nbvar=3249]
c [nbconstr=8983]
c time 8.052
c #vars     3249
c #clauses  8983
c starts	: 0
c conflicts	: 0
c decisions	: 0
c propagations	: 0
c inspects	: 0
c learned literals	: 0
c learned binary clauses	: 0
c learned ternary clauses	: 0
c learned clauses	: 0
c root simplifications	: 0
c Total CPU time (ms) : 762.837
s UNSATISFIABLE
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.96 2/55 21265
Raw data (stat): 21265 (runsolver) R 21264 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 477808146 1052672 99 4294967295 134512640 135381576 3221224432 3221219680 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.97 0.96 4/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18068 0 1 0 783 45 0 0 25 0 11 0 477808146 860717056 21596 4294967295 134512640 134569956 3221224416 3221214512 1080022368 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210136 21596 13073 16 0 210120 0
vsize: 840544
[startup+20.0019 s]
Raw data (loadavg): 1.12 1.02 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18076 0 1 0 1652 45 0 0 25 0 11 0 477808146 869277696 24360 4294967295 134512640 134569956 3221224416 3221214848 1131326694 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 212226 24360 13073 16 0 212210 0
vsize: 848904
[startup+30.0015 s]
Raw data (loadavg): 1.10 1.02 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18076 0 1 0 2630 45 0 0 25 0 11 0 477808146 865456128 23327 4294967295 134512640 134569956 3221224416 3221214848 1131326967 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 23327 13073 16 0 211277 0
vsize: 845172
[startup+40.0018 s]
Raw data (loadavg): 1.08 1.02 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18076 0 1 0 3617 46 0 0 25 0 11 0 477808146 865456128 23328 4294967295 134512640 134569956 3221224416 3221214848 1131326984 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 23328 13073 16 0 211277 0
vsize: 845172
[startup+50.0027 s]
Raw data (loadavg): 1.07 1.01 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 4592 46 0 0 25 0 11 0 477808146 865456128 23406 4294967295 134512640 134569956 3221224416 3221214856 1131326984 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 23406 13073 16 0 211277 0
vsize: 845172
[startup+60.0032 s]
Raw data (loadavg): 1.06 1.01 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 5580 46 0 0 25 0 11 0 477808146 865456128 23540 4294967295 134512640 134569956 3221224416 3221214856 1131326496 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 23540 13073 16 0 211277 0
vsize: 845172
[startup+70.0046 s]
Raw data (loadavg): 1.05 1.01 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 6555 46 0 0 25 0 11 0 477808146 865456128 23662 4294967295 134512640 134569956 3221224416 3221214856 1131326796 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 23662 13073 16 0 211277 0
vsize: 845172
[startup+80.0052 s]
Raw data (loadavg): 1.04 1.01 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 7541 46 0 0 25 0 11 0 477808146 865456128 23662 4294967295 134512640 134569956 3221224416 3221214960 1131313407 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 23662 13073 16 0 211277 0
vsize: 845172
[startup+90.006 s]
Raw data (loadavg): 1.03 1.01 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 8519 46 0 0 25 0 11 0 477808146 865456128 23811 4294967295 134512640 134569956 3221224416 3221214892 1080204237 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 23811 13073 16 0 211277 0
vsize: 845172
[startup+100.006 s]
Raw data (loadavg): 1.03 1.01 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 9499 47 0 0 25 0 11 0 477808146 865456128 23883 4294967295 134512640 134569956 3221224416 3221214856 1131326496 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 23883 13073 16 0 211277 0
vsize: 845172
[startup+110.007 s]
Raw data (loadavg): 1.02 1.01 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 10489 47 0 0 25 0 11 0 477808146 865456128 24047 4294967295 134512640 134569956 3221224416 3221214856 1131326721 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 24047 13073 16 0 211277 0
vsize: 845172
[startup+120.008 s]
Raw data (loadavg): 1.02 1.01 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 11472 48 0 0 25 0 11 0 477808146 865456128 24047 4294967295 134512640 134569956 3221224416 3221214688 1131239445 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 24047 13073 16 0 211277 0
vsize: 845172
[startup+130.008 s]
Raw data (loadavg): 1.02 1.01 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 12454 48 0 0 25 0 11 0 477808146 865456128 24086 4294967295 134512640 134569956 3221224416 3221214856 1131326967 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 24086 13073 16 0 211277 0
vsize: 845172
[startup+140.009 s]
Raw data (loadavg): 1.01 1.01 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 13436 48 0 0 25 0 11 0 477808146 865456128 24175 4294967295 134512640 134569956 3221224416 3221214856 1131326715 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 24175 13073 16 0 211277 0
vsize: 845172
[startup+150.009 s]
Raw data (loadavg): 1.01 1.00 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 14427 49 0 0 25 0 11 0 477808146 865456128 24231 4294967295 134512640 134569956 3221224416 3221214856 1131326535 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 24231 13073 16 0 211277 0
vsize: 845172
[startup+160.011 s]
Raw data (loadavg): 1.01 1.00 0.98 2/65 21275
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 15410 49 0 0 25 0 11 0 477808146 865456128 24352 4294967295 134512640 134569956 3221224416 3221214856 1131326808 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 24352 13073 16 0 211277 0
vsize: 845172
[startup+170.012 s]
Raw data (loadavg): 1.01 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 16394 50 0 0 25 0 11 0 477808146 865456128 24452 4294967295 134512640 134569956 3221224416 3221214856 1131326816 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 24452 13073 16 0 211277 0
vsize: 845172
[startup+180.011 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 17377 50 0 0 25 0 11 0 477808146 865456128 24588 4294967295 134512640 134569956 3221224416 3221214904 1131588674 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 24588 13073 16 0 211277 0
vsize: 845172
[startup+190.012 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 18360 50 0 0 25 0 11 0 477808146 865456128 24756 4294967295 134512640 134569956 3221224416 3221214856 1131326800 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 24756 13073 16 0 211277 0
vsize: 845172
[startup+200.012 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 19351 51 0 0 25 0 11 0 477808146 865456128 24871 4294967295 134512640 134569956 3221224416 3221214856 1131326804 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 24871 13073 16 0 211277 0
vsize: 845172
[startup+210.013 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 20327 51 0 0 25 0 11 0 477808146 865456128 25109 4294967295 134512640 134569956 3221224416 3221214704 1131565043 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 25109 13073 16 0 211277 0
vsize: 845172
[startup+220.014 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 21311 51 0 0 25 0 11 0 477808146 865456128 25241 4294967295 134512640 134569956 3221224416 3221214856 1131326992 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 25241 13073 16 0 211277 0
vsize: 845172
[startup+230.014 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 22295 51 0 0 25 0 11 0 477808146 865456128 25396 4294967295 134512640 134569956 3221224416 3221214856 1131326992 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 25396 13073 16 0 211277 0
vsize: 845172
[startup+240.015 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 23279 52 0 0 25 0 11 0 477808146 865456128 25479 4294967295 134512640 134569956 3221224416 3221214856 1131326984 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 25479 13073 16 0 211277 0
vsize: 845172
[startup+250.015 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 24263 52 0 0 25 0 11 0 477808146 865456128 25564 4294967295 134512640 134569956 3221224416 3221214856 1131326967 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 25564 13073 16 0 211277 0
vsize: 845172
[startup+260.016 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 25245 53 0 0 25 0 11 0 477808146 865456128 25737 4294967295 134512640 134569956 3221224416 3221214672 1131498681 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 25737 13073 16 0 211277 0
vsize: 845172
[startup+270.016 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 26229 53 0 0 25 0 11 0 477808146 865456128 25904 4294967295 134512640 134569956 3221224416 3221214856 1131326804 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 25904 13073 16 0 211277 0
vsize: 845172
[startup+280.017 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 27213 54 0 0 25 0 11 0 477808146 865456128 25965 4294967295 134512640 134569956 3221224416 3221214712 1131395892 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 25965 13073 16 0 211277 0
vsize: 845172
[startup+290.018 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 28191 54 0 0 25 0 11 0 477808146 865456128 26054 4294967295 134512640 134569956 3221224416 3221214856 1131326500 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 26054 13073 16 0 211277 0
vsize: 845172
[startup+300.017 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 29176 55 0 0 25 0 11 0 477808146 865456128 26173 4294967295 134512640 134569956 3221224416 3221214856 1131326516 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 26173 13073 16 0 211277 0
vsize: 845172
[startup+310.018 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 30161 55 0 0 25 0 11 0 477808146 865456128 26249 4294967295 134512640 134569956 3221224416 3221214656 1131389972 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 26249 13073 16 0 211277 0
vsize: 845172
[startup+320.019 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 31146 55 0 0 25 0 11 0 477808146 865456128 26362 4294967295 134512640 134569956 3221224416 3221214856 1131326800 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 26362 13073 16 0 211277 0
vsize: 845172
[startup+330.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 32131 56 0 0 25 0 11 0 477808146 865456128 26436 4294967295 134512640 134569956 3221224416 3221214856 1131326694 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 26436 13073 16 0 211277 0
vsize: 845172
[startup+340.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 33115 56 0 0 25 0 11 0 477808146 865456128 26570 4294967295 134512640 134569956 3221224416 3221214784 1131365491 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 26570 13073 16 0 211277 0
vsize: 845172
[startup+350.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 34098 56 0 0 25 0 11 0 477808146 865456128 26734 4294967295 134512640 134569956 3221224416 3221214856 1131326492 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 26734 13073 16 0 211277 0
vsize: 845172
[startup+360.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 35081 57 0 0 25 0 11 0 477808146 865456128 26913 4294967295 134512640 134569956 3221224416 3221214856 1131326796 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 26913 13073 16 0 211277 0
vsize: 845172
[startup+370.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 36064 57 0 0 25 0 11 0 477808146 865456128 27055 4294967295 134512640 134569956 3221224416 3221214688 1131204705 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 27055 13073 16 0 211277 0
vsize: 845172
[startup+380.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 37056 58 0 0 25 0 11 0 477808146 865456128 27147 4294967295 134512640 134569956 3221224416 3221214704 1131651856 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 27147 13073 16 0 211277 0
vsize: 845172
[startup+390.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 38039 58 0 0 25 0 11 0 477808146 865456128 27302 4294967295 134512640 134569956 3221224416 3221214856 1131326715 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 27302 13073 16 0 211277 0
vsize: 845172
[startup+400.025 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 39023 58 0 0 25 0 11 0 477808146 865456128 27465 4294967295 134512640 134569956 3221224416 3221214856 1131326984 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 27465 13073 16 0 211277 0
vsize: 845172
[startup+410.025 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 40006 58 0 0 25 0 11 0 477808146 865456128 27633 4294967295 134512640 134569956 3221224416 3221214760 1131205871 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27633 13073 16 0 211277 0
vsize: 845172
[startup+420.025 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 40991 58 0 0 25 0 11 0 477808146 865456128 27704 4294967295 134512640 134569956 3221224416 3221214856 1131326516 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27704 13073 16 0 211277 0
vsize: 845172
[startup+430.025 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 41976 58 0 0 25 0 11 0 477808146 865456128 27854 4294967295 134512640 134569956 3221224416 3221214688 1131205137 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27854 13073 16 0 211277 0
vsize: 845172
[startup+440.026 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 42961 59 0 0 25 0 11 0 477808146 865456128 27939 4294967295 134512640 134569956 3221224416 3221214744 1131336854 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 27939 13073 16 0 211277 0
vsize: 845172
[startup+450.026 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 43937 59 0 0 25 0 11 0 477808146 865456128 28228 4294967295 134512640 134569956 3221224416 3221214744 1131336880 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28228 13073 16 0 211277 0
vsize: 845172
[startup+460.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21277
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 44922 59 0 0 25 0 11 0 477808146 865456128 28376 4294967295 134512640 134569956 3221224416 3221214856 1131326516 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 28376 13073 16 0 211277 0
vsize: 845172
[startup+470.028 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 45907 59 0 0 25 0 11 0 477808146 865456128 28433 4294967295 134512640 134569956 3221224416 3221214704 1131651860 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28433 13073 16 0 211277 0
vsize: 845172
[startup+480.028 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 46885 59 0 0 25 0 11 0 477808146 865456128 28603 4294967295 134512640 134569956 3221224416 3221214856 1131326721 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28603 13073 16 0 211277 0
vsize: 845172
[startup+490.029 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 47870 59 0 0 25 0 11 0 477808146 865456128 28671 4294967295 134512640 134569956 3221224416 3221214856 1131326804 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28671 13073 16 0 211277 0
vsize: 845172
[startup+500.029 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 48854 59 0 0 25 0 11 0 477808146 865456128 28806 4294967295 134512640 134569956 3221224416 3221214904 1131595810 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28806 13073 16 0 211277 0
vsize: 845172
[startup+510.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 49840 59 0 0 25 0 11 0 477808146 865456128 28885 4294967295 134512640 134569956 3221224416 3221214744 1131239272 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28885 13073 16 0 211277 0
vsize: 845172
[startup+520.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 50825 59 0 0 25 0 11 0 477808146 865456128 28962 4294967295 134512640 134569956 3221224416 3221214856 1131326721 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 28962 13073 16 0 211277 0
vsize: 845172
[startup+530.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 51810 59 0 0 25 0 11 0 477808146 865456128 29032 4294967295 134512640 134569956 3221224416 3221214856 1131326992 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29032 13073 16 0 211277 0
vsize: 845172
[startup+540.031 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 52788 59 0 0 25 0 11 0 477808146 865456128 29204 4294967295 134512640 134569956 3221224416 3221214856 1131326503 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29204 13073 16 0 211277 0
vsize: 845172
[startup+550.031 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 53773 59 0 0 25 0 11 0 477808146 865456128 29259 4294967295 134512640 134569956 3221224416 3221214856 1131326800 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29259 13073 16 0 211277 0
vsize: 845172
[startup+560.032 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 54758 59 0 0 25 0 11 0 477808146 865456128 29355 4294967295 134512640 134569956 3221224416 3221214856 1131326800 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29355 13073 16 0 211277 0
vsize: 845172
[startup+570.033 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 55743 59 0 0 25 0 11 0 477808146 865456128 29399 4294967295 134512640 134569956 3221224416 3221214804 1131391763 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29399 13073 16 0 211277 0
vsize: 845172
[startup+580.033 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 56721 59 0 0 25 0 11 0 477808146 865456128 29514 4294967295 134512640 134569956 3221224416 3221214856 1131326784 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29514 13073 16 0 211277 0
vsize: 845172
[startup+590.033 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 57706 59 0 0 25 0 11 0 477808146 865456128 29605 4294967295 134512640 134569956 3221224416 3221214744 1131333541 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29605 13073 16 0 211277 0
vsize: 845172
[startup+600.033 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 58691 59 0 0 25 0 11 0 477808146 865456128 29689 4294967295 134512640 134569956 3221224416 3221214856 1131326984 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29689 13073 16 0 211277 0
vsize: 845172
[startup+610.034 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 59669 59 0 0 25 0 11 0 477808146 865456128 29793 4294967295 134512640 134569956 3221224416 3221214856 1131326980 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29793 13073 16 0 211277 0
vsize: 845172
[startup+620.034 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 60653 59 0 0 25 0 11 0 477808146 865456128 29876 4294967295 134512640 134569956 3221224416 3221214704 1131651856 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29876 13073 16 0 211277 0
vsize: 845172
[startup+630.034 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 61638 59 0 0 25 0 11 0 477808146 865456128 29965 4294967295 134512640 134569956 3221224416 3221214888 1131427457 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 29965 13073 16 0 211277 0
vsize: 845172
[startup+640.035 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 62616 59 0 0 25 0 11 0 477808146 865456128 30074 4294967295 134512640 134569956 3221224416 3221214688 1131204677 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30074 13073 16 0 211277 0
vsize: 845172
[startup+650.036 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 63601 59 0 0 25 0 11 0 477808146 865456128 30149 4294967295 134512640 134569956 3221224416 3221214856 1131326721 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30149 13073 16 0 211277 0
vsize: 845172
[startup+660.037 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 64586 59 0 0 25 0 11 0 477808146 865456128 30253 4294967295 134512640 134569956 3221224416 3221214760 1131204863 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30253 13073 16 0 211277 0
vsize: 845172
[startup+670.038 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 65564 59 0 0 25 0 11 0 477808146 865456128 30384 4294967295 134512640 134569956 3221224416 3221214760 1131239407 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30384 13073 16 0 211277 0
vsize: 845172
[startup+680.038 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 66549 59 0 0 25 0 11 0 477808146 865456128 30485 4294967295 134512640 134569956 3221224416 3221214904 1131593414 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30485 13073 16 0 211277 0
vsize: 845172
[startup+690.038 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 67534 59 0 0 25 0 11 0 477808146 865456128 30598 4294967295 134512640 134569956 3221224416 3221214856 1131326510 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30598 13073 16 0 211277 0
vsize: 845172
[startup+700.039 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 68513 60 0 0 25 0 11 0 477808146 865456128 30731 4294967295 134512640 134569956 3221224416 3221214840 1131355897 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 30731 13073 16 0 211277 0
vsize: 845172
[startup+710.041 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 69498 60 0 0 25 0 11 0 477808146 865456128 30855 4294967295 134512640 134569956 3221224416 3221214856 1131326982 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 30855 13073 16 0 211277 0
vsize: 845172
[startup+720.041 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 70483 60 0 0 25 0 11 0 477808146 865456128 30921 4294967295 134512640 134569956 3221224416 3221214856 1131326707 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 30921 13073 16 0 211277 0
vsize: 845172
[startup+730.042 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 71462 60 0 0 25 0 11 0 477808146 865456128 31097 4294967295 134512640 134569956 3221224416 3221214808 1131436510 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 31097 13073 16 0 211277 0
vsize: 845172
[startup+740.043 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 72447 60 0 0 25 0 11 0 477808146 865456128 31198 4294967295 134512640 134569956 3221224416 3221214808 1131442562 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 31198 13073 16 0 211277 0
vsize: 845172
[startup+750.043 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 73432 61 0 0 25 0 11 0 477808146 865456128 31314 4294967295 134512640 134569956 3221224416 3221214856 1131326492 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 211293 31314 13073 16 0 211277 0
vsize: 845172
[startup+760.044 s]
Raw data (loadavg): 1.00 1.00 0.98 2/65 21279
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 74412 61 0 0 25 0 11 0 477808146 865456128 31431 4294967295 134512640 134569956 3221224416 3221214760 1131205147 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 31431 13073 16 0 211277 0
vsize: 845172
[startup+763.593 s]
Raw data (loadavg): 1.00 1.00 0.98 1/54 21280
Raw data (stat): 21265 (java) R 21264 20024 20023 0 -1 0 18077 0 1 0 74412 61 0 0 25 0 11 0 477808146 865456128 31431 4294967295 134512640 134569956 3221224416 3221214760 1131205147 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 211293 31431 13073 16 0 211277 0
vsize: 0

Child status: 20
Real time (s): 763.593
CPU time (s): 775.515
CPU user time (s): 774.384
CPU system time (s): 1.13083
CPU usage (%): 101.561
Max. virtual memory (Kb): 848904
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####