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 29307

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-05-25 06:28:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20723 boxname=wulflinc20 idbench=313 idsolver=14 numberseed=0
MD5SUM SOLVER: d29da23ec752be69e0579424c0f0767e  /oldhome/oroussel/solvers/sat4jPseudoBis.jar
MD5SUM BENCH:  2c9d0c47cb8e4f2ef0877b0c52225df4  /oldhome/oroussel/tmp/wulflinc20/normalized-ooo.tag8.ucl.opb
REAL COMMAND:  java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudoBis.jar /oldhome/oroussel/tmp/wulflinc20/normalized-ooo.tag8.ucl.opb
IDLAUNCH: 20723
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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:        355112 kB
Buffers:         34992 kB
Cached:         614848 kB
SwapCached:        716 kB
Active:          62300 kB
Inactive:       594320 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        354860 kB
SwapTotal:     2097892 kB
SwapFree:      2096336 kB
Dirty:              44 kB
Writeback:           0 kB
Mapped:           5068 kB
Slab:            17280 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 06:38:17 (client local time) WITH STATUS 20 IN 614.232 SECONDS
stats: 20723 7 614.232 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c SAT4J: a SATisfiability library for Java (c) 2004-2005 Daniel Le Berre
c This is free software under the GNU LGPL licence. See www.sat4j.org for details.
c version Special PB05 Second trial
c --- Begin Solver configuration ---
c org.sat4j.minisat.uip.FirstUIP@1e4cbc4
c org.sat4j.minisat.constraints.PBMinDataStructure@1fdc96c
c org.sat4j.minisat.learning.MiniSATLearning@b2fd8f
c conflictBoundIncFactor=1.5 learntBoundIncFactor=1.1 initLearntBoundConstraintFactor=0.5 initConflictBound=100 
c 
c --- End Solver configuration ---
c solving /oldhome/oroussel/tmp/wulflinc20/normalized-ooo.tag8.ucl.opb
c reading problem ... done. Time 7.559 ms.
c #vars     3249
c #constraints  8983
c starts	: 9
c conflicts	: 6488
c decisions	: 11690
c propagations	: 3423146
c inspects	: 15632096
c learned literals	: 0
c learned binary clauses	: 93
c learned ternary clauses	: 104
c learned clauses	: 6487
c root simplifications	: 22
s UNSATISFIABLE
c Total CPU time (ms) : 599.76
#### 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): 1.02 1.01 1.00 2/54 1668
Raw data (stat): 1668 (runsolver) R 1667 25399 25398 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 836718834 1052672 99 4294967295 134512640 135381576 3221224400 3221219620 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.0085 s]
Raw data (loadavg): 1.17 1.04 1.01 3/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18066 0 1 0 727 37 0 0 25 0 11 0 836718834 858030080 21616 4294967295 134512640 134569956 3221224384 3221214732 1130903587 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209480 21616 13086 16 0 209464 0
vsize: 837920
[startup+20.0098 s]
Raw data (loadavg): 1.22 1.05 1.02 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18072 0 1 0 1584 37 0 0 25 0 11 0 836718834 860389376 22511 4294967295 134512640 134569956 3221224384 3221214840 1130894847 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 22511 13086 16 0 210040 0
vsize: 840224
[startup+30.0105 s]
Raw data (loadavg): 1.27 1.07 1.02 3/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18072 0 1 0 2523 38 0 0 25 0 11 0 836718834 860389376 22671 4294967295 134512640 134569956 3221224384 3221214676 1131301260 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 22671 13086 16 0 210040 0
vsize: 840224
[startup+40.0107 s]
Raw data (loadavg): 1.22 1.07 1.02 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 3455 38 0 0 25 0 11 0 836718834 860389376 22673 4294967295 134512640 134569956 3221224384 3221214816 1131343547 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 22673 13086 16 0 210040 0
vsize: 840224
[startup+50.0119 s]
Raw data (loadavg): 1.19 1.06 1.02 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 4410 38 0 0 25 0 11 0 836718834 860389376 22855 4294967295 134512640 134569956 3221224384 3221214560 1131288131 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 22855 13086 16 0 210040 0
vsize: 840224
[startup+60.0116 s]
Raw data (loadavg): 1.16 1.06 1.02 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 5355 38 0 0 25 0 11 0 836718834 860389376 22855 4294967295 134512640 134569956 3221224384 3221214768 1131338944 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 22855 13086 16 0 210040 0
vsize: 840224
[startup+70.0148 s]
Raw data (loadavg): 1.14 1.06 1.02 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 6300 39 0 0 25 0 11 0 836718834 860389376 22984 4294967295 134512640 134569956 3221224384 3221214792 1131190818 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 22984 13086 16 0 210040 0
vsize: 840224
[startup+80.0151 s]
Raw data (loadavg): 1.11 1.06 1.01 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 7244 39 0 0 24 0 11 0 836718834 860389376 23257 4294967295 134512640 134569956 3221224384 3221214832 1131416713 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 23257 13086 16 0 210040 0
vsize: 840224
[startup+90.0148 s]
Raw data (loadavg): 1.10 1.05 1.01 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 8208 39 0 0 25 0 11 0 836718834 860389376 23314 4294967295 134512640 134569956 3221224384 3221214720 1131223061 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 23314 13086 16 0 210040 0
vsize: 840224
[startup+100.016 s]
Raw data (loadavg): 1.08 1.05 1.01 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 9161 39 0 0 25 0 11 0 836718834 860389376 23418 4294967295 134512640 134569956 3221224384 3221214712 1131288713 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 23418 13086 16 0 210040 0
vsize: 840224
[startup+110.016 s]
Raw data (loadavg): 1.07 1.05 1.01 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 10122 40 0 0 25 0 11 0 836718834 860389376 23486 4294967295 134512640 134569956 3221224384 3221214664 1131531580 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 23486 13086 16 0 210040 0
vsize: 840224
[startup+120.016 s]
Raw data (loadavg): 1.06 1.05 1.01 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 11073 40 0 0 25 0 11 0 836718834 860389376 23569 4294967295 134512640 134569956 3221224384 3221214472 1131189905 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 23569 13086 16 0 210040 0
vsize: 840224
[startup+130.016 s]
Raw data (loadavg): 1.05 1.05 1.01 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 12025 40 0 0 25 0 11 0 836718834 860389376 23687 4294967295 134512640 134569956 3221224384 3221214816 1131343495 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 23687 13086 16 0 210040 0
vsize: 840224
[startup+140.015 s]
Raw data (loadavg): 1.04 1.04 1.01 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 12977 41 0 0 25 0 11 0 836718834 860389376 23768 4294967295 134512640 134569956 3221224384 3221214836 1130885186 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 23768 13086 16 0 210040 0
vsize: 840224
[startup+150.016 s]
Raw data (loadavg): 1.03 1.04 1.01 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 13929 41 0 0 25 0 11 0 836718834 860389376 23847 4294967295 134512640 134569956 3221224384 3221214560 1131287794 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 23847 13086 16 0 210040 0
vsize: 840224
[startup+160.016 s]
Raw data (loadavg): 1.03 1.04 1.01 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 14880 41 0 0 24 0 11 0 836718834 860389376 23955 4294967295 134512640 134569956 3221224384 3221214748 1130885154 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 23955 13086 16 0 210040 0
vsize: 840224
[startup+170.017 s]
Raw data (loadavg): 1.02 1.04 1.01 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 15833 42 0 0 24 0 11 0 836718834 860389376 24062 4294967295 134512640 134569956 3221224384 3221214672 1131190928 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 24062 13086 16 0 210040 0
vsize: 840224
[startup+180.016 s]
Raw data (loadavg): 1.02 1.04 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 16786 42 0 0 24 0 11 0 836718834 860389376 24172 4294967295 134512640 134569956 3221224384 3221214812 1131408684 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 24172 13086 16 0 210040 0
vsize: 840224
[startup+190.017 s]
Raw data (loadavg): 1.02 1.03 1.00 2/64 1678
Raw data (stat): 1668 (java) S 1667 25399 25398 0 -1 0 18073 0 1 0 17747 42 0 0 25 0 11 0 836718834 860389376 24252 4294967295 134512640 134569956 3221224384 3221213304 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 24252 13086 16 0 210040 0
vsize: 840224
[startup+200.017 s]
Raw data (loadavg): 1.01 1.03 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 18704 42 0 0 25 0 11 0 836718834 860389376 24334 4294967295 134512640 134569956 3221224384 3221214688 1131223096 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 24334 13086 16 0 210040 0
vsize: 840224
[startup+210.016 s]
Raw data (loadavg): 1.01 1.03 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 19647 43 0 0 25 0 11 0 836718834 860389376 24423 4294967295 134512640 134569956 3221224384 3221214560 1131287754 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 24423 13086 16 0 210040 0
vsize: 840224
[startup+220.018 s]
Raw data (loadavg): 1.01 1.03 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 20600 43 0 0 25 0 11 0 836718834 860389376 24515 4294967295 134512640 134569956 3221224384 3221214720 1131223061 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 24515 13086 16 0 210040 0
vsize: 840224
[startup+230.018 s]
Raw data (loadavg): 1.01 1.03 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 21553 43 0 0 25 0 11 0 836718834 860389376 24620 4294967295 134512640 134569956 3221224384 3221214792 1131190792 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 24620 13086 16 0 210040 0
vsize: 840224
[startup+240.018 s]
Raw data (loadavg): 1.00 1.03 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 22506 43 0 0 25 0 11 0 836718834 860389376 24700 4294967295 134512640 134569956 3221224384 3221214768 1131339000 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 24700 13086 16 0 210040 0
vsize: 840224
[startup+250.019 s]
Raw data (loadavg): 1.00 1.03 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 23458 44 0 0 25 0 11 0 836718834 860389376 24770 4294967295 134512640 134569956 3221224384 3221214560 1131288246 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 24770 13086 16 0 210040 0
vsize: 840224
[startup+260.019 s]
Raw data (loadavg): 1.00 1.02 1.00 2/64 1678
Raw data (stat): 1668 (java) S 1667 25399 25398 0 -1 0 18073 0 1 0 24405 44 0 0 25 0 11 0 836718834 860389376 24881 4294967295 134512640 134569956 3221224384 3221213304 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 24881 13086 16 0 210040 0
vsize: 840224
[startup+270.019 s]
Raw data (loadavg): 1.00 1.02 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 25364 44 0 0 25 0 11 0 836718834 860389376 24971 4294967295 134512640 134569956 3221224384 3221214688 1131222889 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 24971 13086 16 0 210040 0
vsize: 840224
[startup+280.019 s]
Raw data (loadavg): 1.00 1.02 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 26308 44 0 0 25 0 11 0 836718834 860389376 25046 4294967295 134512640 134569956 3221224384 3221214560 1131288159 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 25046 13086 16 0 210040 0
vsize: 840224
[startup+290.019 s]
Raw data (loadavg): 1.00 1.02 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 27261 44 0 0 25 0 11 0 836718834 860389376 25174 4294967295 134512640 134569956 3221224384 3221214560 1131287717 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 25174 13086 16 0 210040 0
vsize: 840224
[startup+300.02 s]
Raw data (loadavg): 1.00 1.02 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 28216 44 0 0 25 0 11 0 836718834 860389376 25260 4294967295 134512640 134569956 3221224384 3221214560 1131288713 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 25260 13086 16 0 210040 0
vsize: 840224
[startup+310.02 s]
Raw data (loadavg): 1.00 1.02 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 29172 45 0 0 25 0 11 0 836718834 860389376 25351 4294967295 134512640 134569956 3221224384 3221214752 1131192537 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 25351 13086 16 0 210040 0
vsize: 840224
[startup+320.02 s]
Raw data (loadavg): 1.00 1.02 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 30129 45 0 0 25 0 11 0 836718834 860389376 25422 4294967295 134512640 134569956 3221224384 3221214812 1131373632 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 25422 13086 16 0 210040 0
vsize: 840224
[startup+330.02 s]
Raw data (loadavg): 1.00 1.02 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 31085 45 0 0 25 0 11 0 836718834 860389376 25501 4294967295 134512640 134569956 3221224384 3221214560 1131288731 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 25501 13086 16 0 210040 0
vsize: 840224
[startup+340.02 s]
Raw data (loadavg): 1.00 1.02 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 32034 45 0 0 25 0 11 0 836718834 860389376 25594 4294967295 134512640 134569956 3221224384 3221214748 1130885186 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 25594 13086 16 0 210040 0
vsize: 840224
[startup+350.021 s]
Raw data (loadavg): 1.00 1.02 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 32991 45 0 0 25 0 11 0 836718834 860389376 25665 4294967295 134512640 134569956 3221224384 3221214664 1131531275 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 25665 13086 16 0 210040 0
vsize: 840224
[startup+360.021 s]
Raw data (loadavg): 1.00 1.01 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 33948 46 0 0 25 0 11 0 836718834 860389376 25746 4294967295 134512640 134569956 3221224384 3221214824 1131415615 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 25746 13086 16 0 210040 0
vsize: 840224
[startup+370.02 s]
Raw data (loadavg): 1.00 1.01 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 34903 46 0 0 25 0 11 0 836718834 860389376 25813 4294967295 134512640 134569956 3221224384 3221214664 1131532748 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 25813 13086 16 0 210040 0
vsize: 840224
[startup+380.021 s]
Raw data (loadavg): 1.00 1.01 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 35857 46 0 0 25 0 11 0 836718834 860389376 25888 4294967295 134512640 134569956 3221224384 3221214772 1131127964 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 25888 13086 16 0 210040 0
vsize: 840224
[startup+390.02 s]
Raw data (loadavg): 1.00 1.01 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 36810 47 0 0 25 0 11 0 836718834 860389376 25967 4294967295 134512640 134569956 3221224384 3221214776 1131283783 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 25967 13086 16 0 210040 0
vsize: 840224
[startup+400.022 s]
Raw data (loadavg): 1.00 1.01 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 37762 47 0 0 25 0 11 0 836718834 860389376 26030 4294967295 134512640 134569956 3221224384 3221214560 1131287742 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 26030 13086 16 0 210040 0
vsize: 840224
[startup+410.022 s]
Raw data (loadavg): 1.00 1.01 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 38713 47 0 0 25 0 11 0 836718834 860389376 26092 4294967295 134512640 134569956 3221224384 3221214792 1131190851 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 26092 13086 16 0 210040 0
vsize: 840224
[startup+420.022 s]
Raw data (loadavg): 1.00 1.01 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 39654 47 0 0 25 0 11 0 836718834 860389376 26198 4294967295 134512640 134569956 3221224384 3221214560 1131287782 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 26198 13086 16 0 210040 0
vsize: 840224
[startup+430.023 s]
Raw data (loadavg): 1.00 1.01 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 40606 47 0 0 25 0 11 0 836718834 860389376 26294 4294967295 134512640 134569956 3221224384 3221214624 1131189302 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 26294 13086 16 0 210040 0
vsize: 840224
[startup+440.023 s]
Raw data (loadavg): 1.00 1.01 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 41558 47 0 0 25 0 11 0 836718834 860389376 26380 4294967295 134512640 134569956 3221224384 3221214672 1131342419 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 26380 13086 16 0 210040 0
vsize: 840224
[startup+450.024 s]
Raw data (loadavg): 1.00 1.01 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 42510 48 0 0 25 0 11 0 836718834 860389376 26480 4294967295 134512640 134569956 3221224384 3221214560 1131288392 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 26480 13086 16 0 210040 0
vsize: 840224
[startup+460.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 43463 48 0 0 25 0 11 0 836718834 860389376 26562 4294967295 134512640 134569956 3221224384 3221214560 1131287933 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 26562 13086 16 0 210040 0
vsize: 840224
[startup+470.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 44415 48 0 0 25 0 11 0 836718834 860389376 26645 4294967295 134512640 134569956 3221224384 3221214688 1131223061 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 26645 13086 16 0 210040 0
vsize: 840224
[startup+480.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 45357 48 0 0 24 0 11 0 836718834 860389376 26732 4294967295 134512640 134569956 3221224384 3221214576 1131422862 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 26732 13086 16 0 210040 0
vsize: 840224
[startup+490.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 46308 48 0 0 25 0 11 0 836718834 860389376 26816 4294967295 134512640 134569956 3221224384 3221214792 1131190936 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 26816 13086 16 0 210040 0
vsize: 840224
[startup+500.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 47260 49 0 0 25 0 11 0 836718834 860389376 26905 4294967295 134512640 134569956 3221224384 3221214688 1131222728 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 26905 13086 16 0 210040 0
vsize: 840224
[startup+510.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) S 1667 25399 25398 0 -1 0 18073 0 1 0 48211 49 0 0 25 0 11 0 836718834 860389376 26994 4294967295 134512640 134569956 3221224384 3221213304 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 26994 13086 16 0 210040 0
vsize: 840224
[startup+520.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 49166 49 0 0 25 0 11 0 836718834 860389376 27076 4294967295 134512640 134569956 3221224384 3221214792 1131342456 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 27076 13086 16 0 210040 0
vsize: 840224
[startup+530.025 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 50110 50 0 0 25 0 11 0 836718834 860389376 27179 4294967295 134512640 134569956 3221224384 3221214816 1131343492 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 27179 13086 16 0 210040 0
vsize: 840224
[startup+540.025 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 51063 50 0 0 25 0 11 0 836718834 860389376 27264 4294967295 134512640 134569956 3221224384 3221214560 1131288159 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 27264 13086 16 0 210040 0
vsize: 840224
[startup+550.025 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 52017 50 0 0 25 0 11 0 836718834 860389376 27344 4294967295 134512640 134569956 3221224384 3221214640 1131461912 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 210056 27344 13086 16 0 210040 0
vsize: 840224
[startup+560.026 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 52973 50 0 0 25 0 11 0 836718834 860389376 27409 4294967295 134512640 134569956 3221224384 3221214560 1131288045 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 27409 13086 16 0 210040 0
vsize: 840224
[startup+570.025 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 53920 51 0 0 25 0 11 0 836718834 860389376 27497 4294967295 134512640 134569956 3221224384 3221214848 1131391268 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 27497 13086 16 0 210040 0
vsize: 840224
[startup+580.025 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 54878 51 0 0 25 0 11 0 836718834 860389376 27577 4294967295 134512640 134569956 3221224384 3221214496 1131330116 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 27577 13086 16 0 210040 0
vsize: 840224
[startup+590.025 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 55832 51 0 0 25 0 11 0 836718834 860389376 27673 4294967295 134512640 134569956 3221224384 3221214712 1131287779 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 27673 13086 16 0 210040 0
vsize: 840224
[startup+600.026 s]
Raw data (loadavg): 1.00 1.00 1.00 2/64 1678
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 56799 52 0 0 25 0 11 0 836718834 860389376 27727 4294967295 134512640 134569956 3221224384 3221214776 1131283504 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 27727 13086 16 0 210040 0
vsize: 840224
[startup+600.834 s]
Raw data (loadavg): 1.00 1.00 1.00 1/53 1679
Raw data (stat): 1668 (java) R 1667 25399 25398 0 -1 0 18073 0 1 0 56799 52 0 0 25 0 11 0 836718834 860389376 27727 4294967295 134512640 134569956 3221224384 3221214776 1131283504 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 210056 27727 13086 16 0 210040 0
vsize: 0

Child status: 20
Real time (s): 600.834
CPU time (s): 614.232
CPU user time (s): 613.293
CPU system time (s): 0.938857
CPU usage (%): 102.23
Max. virtual memory (Kb): 840224
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####