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/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-pilot.we.opb
MD5SUM9228fcb33929c7b5e80529359154089f
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
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 1840
Biggest coefficient in the objective function 111935488000000000
Number of bits for the biggest coefficient in the objective function 57
Sum of the numbers in the objective function 5990082122274938325
Number of bits of the sum of numbers in the objective function 63
Biggest number in a constraint 111935488000000000
Number of bits of the biggest number in a constraint 57
Biggest sum of numbers in a constraint 5990082122274938325
Number of bits of the biggest sum of numbers63
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark1.3408
Number of variables52626
Total number of constraints1016
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints1016
Minimum length of a constraint7
Maximum length of a constraint1620

Trace number 19813

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 19:44:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16103 boxname=wulflinc12 idbench=1239 idsolver=9 numberseed=0
MD5SUM SOLVER: daf345f6fbf228671abfac48013b9cac  /oldhome/oroussel/solvers/sat4jPseudo.jar
MD5SUM BENCH:  9228fcb33929c7b5e80529359154089f  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-pilot.we.opb
REAL COMMAND:  java -server -Xms650M -Xmx650M -jar /oldhome/oroussel/solvers/sat4jPseudo.jar /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-pilot.we.opb
IDLAUNCH: 16103
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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	: 2
cpu MHz		: 451.091
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:        732528 kB
Buffers:         32236 kB
Cached:         247892 kB
SwapCached:        508 kB
Active:          73892 kB
Inactive:       208308 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        732276 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            14260 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 19:57:33 (client local time) WITH STATUS 20 IN 809.342 SECONDS
stats: 16103 7 809.342 20
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c solving /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-pilot.we.opb
c reading problem 
c [nbvar=52626]
c [nbconstr=1016]
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
org.sat4j.specs.ContradictionException: non satisfiable constraint
	at org.sat4j.minisat.constraints.pb.MinWatchPb.computeWatches(MinWatchPb.java:177)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:259)
	at org.sat4j.minisat.constraints.pb.MinWatchPb.minWatchPbNew(MinWatchPb.java:221)
	at org.sat4j.minisat.constraints.PBMinDataStructure.constraintFactory(PBMinDataStructure.java:35)
	at org.sat4j.minisat.constraints.AbstractPBDataStructureFactory.createPseudoBooleanConstraint(AbstractPBDataStructureFactory.java:76)
	at org.sat4j.minisat.core.Solver.addPseudoBoolean(Solver.java:284)
	at org.sat4j.reader.OPBReader2005.endConstraint(OPBReader2005.java:146)
	at org.sat4j.reader.OPBReader2005.readConstraint(OPBReader2005.java:563)
	at org.sat4j.reader.OPBReader2005.parse(OPBReader2005.java:593)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:616)
	at org.sat4j.reader.OPBReader2005.parseInstance(OPBReader2005.java:605)
	at org.sat4j.LanceurPseudo2005.readProblem(LanceurPseudo2005.java:61)
	at org.sat4j.LanceurPseudo2005.main(LanceurPseudo2005.java:73)
c time 803.584
c #vars     52626
c #clauses  1580
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) : 803.638
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.77 0.90 0.89 2/54 2044
Raw data (stat): 2044 (runsolver) R 2043 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489470651 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.0001 s]
Raw data (loadavg): 0.80 0.91 0.89 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18007 0 1 0 854 39 0 0 25 0 10 0 489470651 859013120 20518 4294967295 134512640 134569956 3221224400 3221214464 1076461342 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 20518 13073 16 0 209704 0
vsize: 838880
[startup+20.002 s]
Raw data (loadavg): 0.83 0.91 0.89 2/63 2053
Raw data (stat): 2044 (java) S 2043 25285 25284 0 -1 0 18008 0 1 0 1745 39 0 0 25 0 10 0 489470651 859013120 21063 4294967295 134512640 134569956 3221224400 3221213768 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 21063 13073 16 0 209704 0
vsize: 838880
[startup+30.1053 s]
Raw data (loadavg): 0.86 0.91 0.90 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 2633 39 0 0 25 0 10 0 489470651 859013120 21822 4294967295 134512640 134569956 3221224400 3221214808 1131180801 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 21822 13073 16 0 209704 0
vsize: 838880
[startup+40.106 s]
Raw data (loadavg): 0.88 0.91 0.90 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 3543 39 0 0 25 0 10 0 489470651 859013120 21949 4294967295 134512640 134569956 3221224400 3221214408 1079276148 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 21949 13073 16 0 209704 0
vsize: 838880
[startup+50.1064 s]
Raw data (loadavg): 0.90 0.92 0.90 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 4462 40 0 0 25 0 10 0 489470651 859013120 22126 4294967295 134512640 134569956 3221224400 3221214808 1131237405 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 22126 13073 16 0 209704 0
vsize: 838880
[startup+60.1062 s]
Raw data (loadavg): 0.91 0.92 0.90 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 5369 40 0 0 25 0 10 0 489470651 859013120 22286 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 22286 13073 16 0 209704 0
vsize: 838880
[startup+70.1088 s]
Raw data (loadavg): 0.92 0.92 0.90 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 6273 41 0 0 24 0 10 0 489470651 859013120 22440 4294967295 134512640 134569956 3221224400 3221214804 1080204163 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 22440 13073 16 0 209704 0
vsize: 838880
[startup+80.1119 s]
Raw data (loadavg): 0.94 0.92 0.90 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 7184 41 0 0 25 0 10 0 489470651 859013120 22675 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 22675 13073 16 0 209704 0
vsize: 838880
[startup+90.1117 s]
Raw data (loadavg): 0.95 0.92 0.90 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 8094 41 0 0 25 0 10 0 489470651 859013120 22858 4294967295 134512640 134569956 3221224400 3221214248 1077558376 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 22858 13073 16 0 209704 0
vsize: 838880
[startup+100.113 s]
Raw data (loadavg): 0.95 0.93 0.90 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 8989 42 0 0 25 0 10 0 489470651 859013120 23113 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 23113 13073 16 0 209704 0
vsize: 838880
[startup+110.113 s]
Raw data (loadavg): 0.96 0.93 0.90 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 9864 43 0 0 24 0 10 0 489470651 859013120 23314 4294967295 134512640 134569956 3221224400 3221214796 1080204031 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 23314 13073 16 0 209704 0
vsize: 838880
[startup+120.141 s]
Raw data (loadavg): 0.97 0.93 0.90 2/63 2053
Raw data (stat): 2044 (java) S 2043 25285 25284 0 -1 0 18008 0 1 0 10774 43 0 0 25 0 10 0 489470651 859013120 23580 4294967295 134512640 134569956 3221224400 3221213504 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 23580 13073 16 0 209704 0
vsize: 838880
[startup+130.152 s]
Raw data (loadavg): 0.97 0.93 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 11702 44 0 0 25 0 10 0 489470651 859013120 23730 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 23730 13073 16 0 209704 0
vsize: 838880
[startup+140.27 s]
Raw data (loadavg): 0.97 0.93 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 12645 44 0 0 25 0 10 0 489470651 859013120 23787 4294967295 134512640 134569956 3221224400 3221214788 1080204031 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 23787 13073 16 0 209704 0
vsize: 838880
[startup+150.271 s]
Raw data (loadavg): 0.98 0.94 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 13571 45 0 0 25 0 10 0 489470651 859013120 23895 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 23895 13073 16 0 209704 0
vsize: 838880
[startup+160.271 s]
Raw data (loadavg): 0.98 0.94 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 14496 45 0 0 25 0 10 0 489470651 859013120 24003 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 24003 13073 16 0 209704 0
vsize: 838880
[startup+170.272 s]
Raw data (loadavg): 0.98 0.94 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 15422 46 0 0 25 0 10 0 489470651 859013120 24055 4294967295 134512640 134569956 3221224400 3221214264 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 24055 13073 16 0 209704 0
vsize: 838880
[startup+180.272 s]
Raw data (loadavg): 0.99 0.94 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 16348 46 0 0 24 0 10 0 489470651 859013120 24158 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 24158 13073 16 0 209704 0
vsize: 838880
[startup+190.276 s]
Raw data (loadavg): 0.99 0.94 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 17257 47 0 0 25 0 10 0 489470651 859013120 24204 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 24204 13073 16 0 209704 0
vsize: 838880
[startup+200.277 s]
Raw data (loadavg): 0.99 0.94 0.91 2/63 2053
Raw data (stat): 2044 (java) S 2043 25285 25284 0 -1 0 18008 0 1 0 18170 47 0 0 25 0 10 0 489470651 859013120 24462 4294967295 134512640 134569956 3221224400 3221213512 1073943035 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 24462 13073 16 0 209704 0
vsize: 838880
[startup+210.278 s]
Raw data (loadavg): 0.99 0.94 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 19093 48 0 0 24 0 10 0 489470651 859013120 24507 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 24507 13073 16 0 209704 0
vsize: 838880
[startup+220.279 s]
Raw data (loadavg): 0.99 0.95 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 20018 48 0 0 25 0 10 0 489470651 859013120 24655 4294967295 134512640 134569956 3221224400 3221214796 1080204031 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 24655 13073 16 0 209704 0
vsize: 838880
[startup+230.294 s]
Raw data (loadavg): 0.99 0.95 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 20944 49 0 0 25 0 10 0 489470651 859013120 24696 4294967295 134512640 134569956 3221224400 3221214264 1080019600 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 24696 13073 16 0 209704 0
vsize: 838880
[startup+240.294 s]
Raw data (loadavg): 0.99 0.95 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 21869 49 0 0 25 0 10 0 489470651 859013120 24844 4294967295 134512640 134569956 3221224400 3221214804 1080204163 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 24844 13073 16 0 209704 0
vsize: 838880
[startup+250.295 s]
Raw data (loadavg): 0.99 0.95 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 22753 50 0 0 24 0 10 0 489470651 859013120 25004 4294967295 134512640 134569956 3221224400 3221214264 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 25004 13073 16 0 209704 0
vsize: 838880
[startup+260.297 s]
Raw data (loadavg): 0.99 0.95 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 23617 51 0 0 25 0 10 0 489470651 859013120 25251 4294967295 134512640 134569956 3221224400 3221214264 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 25251 13073 16 0 209704 0
vsize: 838880
[startup+270.296 s]
Raw data (loadavg): 0.99 0.95 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 24510 52 0 0 25 0 10 0 489470651 859013120 25529 4294967295 134512640 134569956 3221224400 3221214248 1077558376 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 25529 13073 16 0 209704 0
vsize: 838880
[startup+280.297 s]
Raw data (loadavg): 0.99 0.95 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 25431 52 0 0 25 0 10 0 489470651 859013120 25598 4294967295 134512640 134569956 3221224400 3221214264 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 25598 13073 16 0 209704 0
vsize: 838880
[startup+290.297 s]
Raw data (loadavg): 0.99 0.95 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 26344 53 0 0 18 0 10 0 489470651 859013120 25657 4294967295 134512640 134569956 3221224400 3221214248 1077558376 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 25657 13073 16 0 209704 0
vsize: 838880
[startup+300.297 s]
Raw data (loadavg): 0.99 0.95 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 27255 53 0 0 25 0 10 0 489470651 859013120 25772 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 25772 13073 16 0 209704 0
vsize: 838880
[startup+310.297 s]
Raw data (loadavg): 0.99 0.95 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 28170 54 0 0 24 0 10 0 489470651 859013120 25828 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 25828 13073 16 0 209704 0
vsize: 838880
[startup+320.298 s]
Raw data (loadavg): 0.99 0.96 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 29059 54 0 0 25 0 10 0 489470651 859013120 25880 4294967295 134512640 134569956 3221224400 3221214296 1079300873 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 25880 13073 16 0 209704 0
vsize: 838880
[startup+330.298 s]
Raw data (loadavg): 0.99 0.96 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 29950 54 0 0 25 0 10 0 489470651 859013120 26074 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 26074 13073 16 0 209704 0
vsize: 838880
[startup+340.298 s]
Raw data (loadavg): 0.99 0.96 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 30865 55 0 0 25 0 10 0 489470651 859013120 26218 4294967295 134512640 134569956 3221224400 3221214248 1077558376 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 26218 13073 16 0 209704 0
vsize: 838880
[startup+350.299 s]
Raw data (loadavg): 0.99 0.96 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 31785 55 0 0 25 0 10 0 489470651 859013120 26274 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 26274 13073 16 0 209704 0
vsize: 838880
[startup+360.299 s]
Raw data (loadavg): 0.99 0.96 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 32705 56 0 0 25 0 10 0 489470651 859013120 26318 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 26318 13073 16 0 209704 0
vsize: 838880
[startup+370.3 s]
Raw data (loadavg): 0.99 0.96 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 33620 56 0 0 25 0 10 0 489470651 859013120 26373 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 26373 13073 16 0 209704 0
vsize: 838880
[startup+380.3 s]
Raw data (loadavg): 0.99 0.96 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 34512 57 0 0 25 0 10 0 489470651 859013120 26414 4294967295 134512640 134569956 3221224400 3221214788 1080204031 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 26414 13073 16 0 209704 0
vsize: 838880
[startup+390.311 s]
Raw data (loadavg): 0.99 0.96 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 35388 57 0 0 18 0 10 0 489470651 859013120 26564 4294967295 134512640 134569956 3221224400 3221214344 1131212641 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 26564 13073 16 0 209704 0
vsize: 838880
[startup+400.318 s]
Raw data (loadavg): 0.99 0.96 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 36280 58 0 0 21 0 10 0 489470651 859013120 26751 4294967295 134512640 134569956 3221224400 3221214532 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 26751 13073 16 0 209704 0
vsize: 838880
[startup+410.322 s]
Raw data (loadavg): 0.99 0.96 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 37176 58 0 0 19 0 10 0 489470651 859013120 26850 4294967295 134512640 134569956 3221224400 3221214264 1080019608 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 26850 13073 16 0 209704 0
vsize: 838880
[startup+420.321 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 38082 58 0 0 22 0 10 0 489470651 859013120 26955 4294967295 134512640 134569956 3221224400 3221214248 1077558376 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 26955 13073 16 0 209704 0
vsize: 838880
[startup+430.334 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 38990 58 0 0 21 0 10 0 489470651 859013120 27046 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 27046 13073 16 0 209704 0
vsize: 838880
[startup+440.334 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 39909 59 0 0 25 0 10 0 489470651 859013120 27196 4294967295 134512640 134569956 3221224400 3221214248 1077558376 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 27196 13073 16 0 209704 0
vsize: 838880
[startup+450.336 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 40841 59 0 0 25 0 10 0 489470651 859013120 27226 4294967295 134512640 134569956 3221224400 3221214264 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 27226 13073 16 0 209704 0
vsize: 838880
[startup+460.336 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 41752 59 0 0 24 0 10 0 489470651 859013120 27254 4294967295 134512640 134569956 3221224400 3221214248 1077558376 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 27254 13073 16 0 209704 0
vsize: 838880
[startup+470.337 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 42669 59 0 0 25 0 10 0 489470651 859013120 27406 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 0 0 0
Raw data (statm): 209720 27406 13073 16 0 209704 0
vsize: 838880
[startup+480.337 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 43603 60 0 0 25 0 10 0 489470651 859013120 27433 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 27433 13073 16 0 209704 0
vsize: 838880
[startup+490.338 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 44515 60 0 0 22 0 10 0 489470651 859013120 27460 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 27460 13073 16 0 209704 0
vsize: 838880
[startup+500.339 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 45423 60 0 0 25 0 10 0 489470651 859013120 27487 4294967295 134512640 134569956 3221224400 3221214804 1080204163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 27487 13073 16 0 209704 0
vsize: 838880
[startup+510.339 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 46354 60 0 0 25 0 10 0 489470651 859013120 27642 4294967295 134512640 134569956 3221224400 3221214264 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 27642 13073 16 0 209704 0
vsize: 838880
[startup+520.347 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) S 2043 25285 25284 0 -1 0 18008 0 1 0 47273 60 0 0 25 0 10 0 489470651 859013120 27667 4294967295 134512640 134569956 3221224400 3221213512 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 27667 13073 16 0 209704 0
vsize: 838880
[startup+530.347 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 48182 60 0 0 25 0 10 0 489470651 859013120 27693 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 27693 13073 16 0 209704 0
vsize: 838880
[startup+540.349 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 49106 60 0 0 25 0 10 0 489470651 859013120 27851 4294967295 134512640 134569956 3221224400 3221214248 1077558376 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 27851 13073 16 0 209704 0
vsize: 838880
[startup+550.35 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 50029 60 0 0 25 0 10 0 489470651 859013120 27876 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 27876 13073 16 0 209704 0
vsize: 838880
[startup+560.36 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) S 2043 25285 25284 0 -1 0 18008 0 1 0 50941 61 0 0 25 0 10 0 489470651 859013120 27900 4294967295 134512640 134569956 3221224400 3221213512 1073943035 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 27900 13073 16 0 209704 0
vsize: 838880
[startup+570.374 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 51854 61 0 0 25 0 10 0 489470651 859013120 28059 4294967295 134512640 134569956 3221224400 3221214264 1080019600 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28059 13073 16 0 209704 0
vsize: 838880
[startup+580.374 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 52784 61 0 0 25 0 10 0 489470651 859013120 28084 4294967295 134512640 134569956 3221224400 3221214804 1080204163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28084 13073 16 0 209704 0
vsize: 838880
[startup+590.374 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 53693 61 0 0 25 0 10 0 489470651 859013120 28108 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28108 13073 16 0 209704 0
vsize: 838880
[startup+600.375 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 54603 61 0 0 25 0 10 0 489470651 859013120 28131 4294967295 134512640 134569956 3221224400 3221214264 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28131 13073 16 0 209704 0
vsize: 838880
[startup+610.376 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 55526 61 0 0 25 0 10 0 489470651 859013120 28293 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28293 13073 16 0 209704 0
vsize: 838880
[startup+620.376 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 56450 61 0 0 25 0 10 0 489470651 859013120 28317 4294967295 134512640 134569956 3221224400 3221214804 1080204163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28317 13073 16 0 209704 0
vsize: 838880
[startup+630.377 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 57352 61 0 0 24 0 10 0 489470651 859013120 28340 4294967295 134512640 134569956 3221224400 3221214248 1077558376 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28340 13073 16 0 209704 0
vsize: 838880
[startup+640.377 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 58263 62 0 0 25 0 10 0 489470651 859013120 28502 4294967295 134512640 134569956 3221224400 3221214804 1080204163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28502 13073 16 0 209704 0
vsize: 838880
[startup+650.378 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 59190 62 0 0 25 0 10 0 489470651 859013120 28525 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28525 13073 16 0 209704 0
vsize: 838880
[startup+660.379 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 60105 62 0 0 25 0 10 0 489470651 859013120 28548 4294967295 134512640 134569956 3221224400 3221214804 1080204163 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28548 13073 16 0 209704 0
vsize: 838880
[startup+670.379 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 61011 62 0 0 25 0 10 0 489470651 859013120 28570 4294967295 134512640 134569956 3221224400 3221214264 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28570 13073 16 0 209704 0
vsize: 838880
[startup+680.38 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 61921 62 0 0 25 0 10 0 489470651 859013120 28735 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28735 13073 16 0 209704 0
vsize: 838880
[startup+690.38 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 62847 62 0 0 25 0 10 0 489470651 859013120 28759 4294967295 134512640 134569956 3221224400 3221214788 1080203551 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 28759 13073 16 0 209704 0
vsize: 838880
[startup+700.381 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 63755 62 0 0 25 0 10 0 489470651 859013120 29185 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 29185 13073 16 0 209704 0
vsize: 838880
[startup+710.382 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 64648 62 0 0 25 0 10 0 489470651 859013120 29292 4294967295 134512640 134569956 3221224400 3221214796 1080204031 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 29292 13073 16 0 209704 0
vsize: 838880
[startup+720.381 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 65536 62 0 0 25 0 10 0 489470651 859013120 29303 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 29303 13073 16 0 209704 0
vsize: 838880
[startup+730.383 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 66419 63 0 0 25 0 10 0 489470651 859013120 29392 4294967295 134512640 134569956 3221224400 3221214788 1080204031 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 29392 13073 16 0 209704 0
vsize: 838880
[startup+740.384 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 67299 63 0 0 25 0 10 0 489470651 859013120 29462 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 29462 13073 16 0 209704 0
vsize: 838880
[startup+750.386 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 68182 63 0 0 25 0 10 0 489470651 859013120 29538 4294967295 134512640 134569956 3221224400 3221214788 1080204031 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 29538 13073 16 0 209704 0
vsize: 838880
[startup+760.386 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 69070 64 0 0 25 0 10 0 489470651 859013120 30226 4294967295 134512640 134569956 3221224400 3221214692 1079677938 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 30226 13073 16 0 209704 0
vsize: 838880
[startup+770.387 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 69956 64 0 0 25 0 10 0 489470651 859013120 30394 4294967295 134512640 134569956 3221224400 3221214272 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 30394 13073 16 0 209704 0
vsize: 838880
[startup+780.389 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 70846 64 0 0 25 0 10 0 489470651 859013120 30621 4294967295 134512640 134569956 3221224400 3221214272 1080019741 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 30621 13073 16 0 209704 0
vsize: 838880
[startup+790.389 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 71733 64 0 0 25 0 10 0 489470651 859013120 30849 4294967295 134512640 134569956 3221224400 3221214264 1080019608 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 30849 13073 16 0 209704 0
vsize: 838880
[startup+800.39 s]
Raw data (loadavg): 0.99 0.97 0.91 2/63 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 72619 65 0 0 24 0 10 0 489470651 859013120 31078 4294967295 134512640 134569956 3221224400 3221214796 1080204031 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 31078 13073 16 0 209704 0
vsize: 838880
[startup+804.354 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 2053
Raw data (stat): 2044 (java) R 2043 25285 25284 0 -1 0 18008 0 1 0 72619 65 0 0 24 0 10 0 489470651 859013120 31078 4294967295 134512640 134569956 3221224400 3221214796 1080204031 0 4 3 23756 0 0 0 17 1 0 0
Raw data (statm): 209720 31078 13073 16 0 209704 0
vsize: 0

Child status: 20
Real time (s): 804.354
CPU time (s): 809.342
CPU user time (s): 808.12
CPU system time (s): 1.22181
CPU usage (%): 100.62
Max. virtual memory (Kb): 838880
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####