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/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb53-24-opb/normalized-frb53-24-4.opb
MD5SUMb7f280d80b52f97899362fbc10d59421
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -40
Optimality of the best value was proved NO
Number of terms in the objective function 1272
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 1272
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1272
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.12
Number of variables1272
Total number of constraints94308
Number of constraints which are clauses94308
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint2

Trace number 5051

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-04-13 21:39:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3074 boxname=wulflinc27 idbench=342 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  b7f280d80b52f97899362fbc10d59421  /oldhome/oroussel/tmp/wulflinc27/normalized-frb53-24-4.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc27/normalized-frb53-24-4.opb
IDLAUNCH: 3074
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
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:        871596 kB
Buffers:         33424 kB
Cached:          92276 kB
SwapCached:       3160 kB
Active:          50784 kB
Inactive:        81000 kB
HighTotal:      131008 kB
HighFree:        35224 kB
LowTotal:       903652 kB
LowFree:        836372 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25748 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 21:59:55 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 3074 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 94308 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   94308   188616 |   31436       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -35
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:70300     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  169359   364682 |   56453       0        0     nan |  0.000 % |
c |       100 |  168922   363775 |   62098      77      709     9.2 |  0.462 % |
c |       250 |  168305   362472 |   68308     192     1716     8.9 |  1.133 % |
c |       475 |  166978   359599 |   75138     381     5781    15.2 |  2.646 % |
c |       812 |  165218   355749 |   82652     626     8251    13.2 |  4.692 % |
c |      1318 |  162383   349476 |   90918     969    12154    12.5 |  8.056 % |
c |      2077 |  157617   338824 |  100009    1476    17994    12.2 | 13.811 % |
c |      3216 |  151802   325721 |  110010    2318    29720    12.8 | 20.921 % |
c ==============================================================================
c Found solution: -37
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4326 |  144676   309573 |   48225    3058    38672    12.6 | 20.921 % |
c |      4426 |  144186   308463 |   53047    3120    40617    13.0 | 30.445 % |
c |      4578 |  143238   306289 |   58352    3231    41825    12.9 | 31.640 % |
c |      4803 |  142402   304387 |   64187    3414    43860    12.8 | 32.673 % |
c |      5140 |  140852   300820 |   70606    3633    46525    12.8 | 34.621 % |
c |      5646 |  137216   292423 |   77666    3913    51403    13.1 | 39.212 % |
c |      6405 |  133356   283441 |   85433    4391    54876    12.5 | 44.054 % |
c |      7544 |  127322   269284 |   93976    4922    61075    12.4 | 51.849 % |
c ==============================================================================
c Found solution: -40
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9035 |  122166   257188 |   40722    5712    68946    12.1 | 51.849 % |
c |      9135 |  121552   255722 |   44794    5751    69272    12.0 | 59.554 % |
c |      9285 |  121245   255012 |   49273    5828    69502    11.9 | 59.945 % |
c |      9510 |  121055   254568 |   54200    6029    72399    12.0 | 60.191 % |
c |      9847 |  120494   253218 |   59621    6279    75507    12.0 | 60.946 % |
c |     10353 |  118916   249506 |   65583    6555    78969    12.0 | 62.996 % |
c |     11112 |  117082   245139 |   72141    7037    85135    12.1 | 65.428 % |
c |     12251 |  114869   239846 |   79355    7741    96400    12.5 | 68.376 % |
c |     13959 |  112196   233396 |   87291    8885   110056    12.4 | 71.966 % |
c |     16523 |  108175   223723 |   96020   10065   142813    14.2 | 77.395 % |
c ==============================================================================
c Found solution: -41
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19072 |  106303   219239 |   35434   11936   210099    17.6 | 77.395 % |
c |     19172 |  106043   218597 |   38977   11913   208439    17.5 | 80.304 % |
c |     19322 |  105714   217753 |   42875   11980   209621    17.5 | 80.776 % |
c |     19547 |  105655   217612 |   47162   12193   214538    17.6 | 80.854 % |
c ==============================================================================
c Found solution: -42
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19700 |  105414   216919 |   35138   12302   216558    17.6 | 80.854 % |
c |     19802 |  105209   216406 |   38651   12305   216661    17.6 | 81.471 % |
c |     19953 |  105203   216390 |   42516   12451   220393    17.7 | 81.480 % |
c |     20178 |  105058   216037 |   46768   12580   223266    17.7 | 81.681 % |
c |     20516 |  104867   215577 |   51445   12813   230857    18.0 | 81.941 % |
c |     21023 |  104818   215452 |   56590   13308   264533    19.9 | 82.011 % |
c |     21782 |  104386   214420 |   62249   13800   279516    20.3 | 82.590 % |
c |     22921 |  104213   214009 |   68474   14850   336123    22.6 | 82.822 % |
c |     24629 |  103871   213167 |   75321   16186   396533    24.5 | 83.304 % |
c ==============================================================================
c Found solution: -43
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26527 |  103755   212908 |   34585   17822   678720    38.1 | 83.304 % |
c |     26627 |  103735   212860 |   38043   17778   677205    38.1 | 83.537 % |
c |     26777 |  103735   212860 |   41847   17928   682500    38.1 | 83.537 % |
c |     27002 |  103433   212117 |   46032   17979   684667    38.1 | 83.965 % |
c ==============================================================================
c Found solution: -44
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27134 |  103393   211992 |   34464   18086   687939    38.0 | 83.965 % |
c |     27235 |  103393   211992 |   37910   18187   690077    37.9 | 84.028 % |
c |     27385 |  103330   211845 |   41701   18330   694511    37.9 | 84.110 % |
c |     27610 |  103274   211723 |   45871   18540   704605    38.0 | 84.174 % |
c |     27947 |  103174   211495 |   50458   18784   712675    37.9 | 84.298 % |
c |     28453 |  103125   211380 |   55504   19201   738207    38.4 | 84.363 % |
c |     29213 |  103036   211162 |   61055   19929   801117    40.2 | 84.483 % |
c |     30354 |  103036   211162 |   67160   21070   872549    41.4 | 84.483 % |
c |     32062 |  102929   210905 |   73876   22689   978508    43.1 | 84.629 % |
c |     34625 |  102876   210772 |   81264   25209  1290370    51.2 | 84.705 % |
c |     38470 |  102422   209622 |   89390   28495  1592565    55.9 | 85.367 % |
c ==============================================================================
c Found solution: -45
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42150 |  102402   209586 |   34134   32167  2030327    63.1 | 85.367 % |
c |     42250 |  102360   209480 |   37547   32094  2030566    63.3 | 85.465 % |
c |     42400 |  102360   209480 |   41302   32244  2037497    63.2 | 85.465 % |
c |     42627 |  102312   209368 |   45432   32244  2042126    63.3 | 85.527 % |
c |     42964 |  102312   209368 |   49975   32581  2056632    63.1 | 85.527 % |
c |     43470 |  102291   209319 |   54973   33064  2093079    63.3 | 85.554 % |
c |     44229 |  102285   209305 |   60470   33822  2138960    63.2 | 85.562 % |
c |     45368 |  102285   209305 |   66517   34961  2228762    63.7 | 85.562 % |
c |     47079 |  102253   209229 |   73169   36649  2377893    64.9 | 85.605 % |
c |     49642 |  102161   209013 |   80486   38901  2692898    69.2 | 85.725 % |
c |     53486 |  101926   208427 |   88534   42083  3015186    71.6 | 86.065 % |
c |     59252 |  101926   208427 |   97388   47849  4019284    84.0 | 86.065 % |
c ==============================================================================
c Found solution: -46
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63656 |  101864   208243 |   33954   52055  4640150    89.1 | 86.065 % |
c |     63756 |  101864   208243 |   37349   52155  4646978    89.1 | 86.150 % |
c |     63906 |  101784   208061 |   41084   52010  4649791    89.4 | 86.249 % |
c |     64133 |  101747   207976 |   45192   52227  4665999    89.3 | 86.295 % |
c |     64471 |  101747   207976 |   49712   52565  4707636    89.6 | 86.295 % |
c |     64979 |  101698   207853 |   54683   53067  4764394    89.8 | 86.367 % |
c |     65739 |  101698   207853 |   60151   53827  4818117    89.5 | 86.367 % |
c |     66878 |  101698   207853 |   66166   54966  4969185    90.4 | 86.367 % |
c |     68586 |  101644   207713 |   72783   56584  5161376    91.2 | 86.451 % |
c |     71148 |  101596   207595 |   80061   59103  5440262    92.0 | 86.515 % |
c |     74993 |  101575   207542 |   88067   62857  5902484    93.9 | 86.546 % |
c |     80759 |  101529   207432 |   96874   68536  6548383    95.5 | 86.608 % |
c |     89409 |  101529   207432 |  106562   77186  7759810   100.5 | 86.608 % |
c |    102383 |  101499   207363 |  117218   89990  9717255   108.0 | 86.643 % |
c ==============================================================================
c Found solution: -47
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111569 |  101519   207425 |   33839   99175 10870430   109.6 | 86.643 % |
c |    111669 |  101519   207425 |   37222   21174  1649250    77.9 | 86.653 % |
c |    111819 |  101519   207425 |   40945   21324  1657282    77.7 | 86.653 % |
c |    112044 |  101519   207425 |   45039   21549  1669973    77.5 | 86.653 % |
c |    112381 |  101519   207425 |   49543   21886  1703740    77.8 | 86.653 % |
c |    112888 |  101519   207425 |   54498   22393  1760303    78.6 | 86.653 % |
c |    113648 |  101519   207425 |   59947   23153  1822629    78.7 | 86.653 % |
c |    114788 |  101519   207425 |   65942   24293  1967003    81.0 | 86.653 % |
c |    116496 |  101426   207199 |   72536   25977  2138860    82.3 | 86.779 % |
c |    119058 |  101330   206964 |   79790   28358  2417119    85.2 | 86.911 % |
c |    122902 |  101305   206907 |   87769   32146  2874288    89.4 | 86.942 % |
c |    128668 |  101287   206865 |   96546   37909  3613117    95.3 | 86.965 % |
c |    137317 |  101265   206813 |  106201   46547  4922270   105.7 | 86.994 % |
c |    150291 |  101143   206513 |  116821   59498  6548282   110.1 | 87.163 % |
c |    169752 |  101069   206331 |  128503   78930  9574296   121.3 | 87.268 % |
c |    198948 |  101014   206202 |  141353  108099 13638722   126.2 | 87.336 % |
c |    242737 |  101007   206183 |  155489  151887 17463503   115.0 | 87.347 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 -C1190 -C1189 C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 C1081 -C1080 -C1079 -C1078 -C1077 C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 C985 -C984 -C983 -C982 -C981 -C980 -C979 C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 C893 -C892 -C891 -C890 -C889 C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C63#### 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.95 0.90 2/54 21555
Raw data (stat): 21555 (runsolver) R 21554 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479258500 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0012 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 5661 0 0 0 981 18 0 0 25 0 1 0 479258500 26189824 5639 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6394 5639 603 41 0 6353 0
vsize: 25576
[startup+20.0022 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 5669 0 0 0 1980 18 0 0 25 0 1 0 479258500 26189824 5647 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6394 5647 603 41 0 6353 0
vsize: 25576
[startup+30.0026 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 5674 0 0 0 2980 18 0 0 25 0 1 0 479258500 26324992 5652 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6427 5652 603 41 0 6386 0
vsize: 25708
[startup+40.0027 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 5684 0 0 0 3980 19 0 0 25 0 1 0 479258500 26324992 5662 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6427 5662 603 41 0 6386 0
vsize: 25708
[startup+50.0035 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 5873 0 0 0 4979 19 0 0 25 0 1 0 479258500 27471872 5851 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6707 5851 603 41 0 6666 0
vsize: 26828
[startup+60.0044 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 5873 0 0 0 5979 19 0 0 25 0 1 0 479258500 27471872 5851 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6707 5851 603 41 0 6666 0
vsize: 26828
[startup+70.0053 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 5873 0 0 0 6979 20 0 0 25 0 1 0 479258500 27471872 5851 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6707 5851 603 41 0 6666 0
vsize: 26828
[startup+80.006 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 5873 0 0 0 7979 20 0 0 25 0 1 0 479258500 27471872 5851 4294967295 134512640 134672761 3221224624 3221223796 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6707 5851 603 41 0 6666 0
vsize: 26828
[startup+90.0064 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 5875 0 0 0 8978 21 0 0 25 0 1 0 479258500 27471872 5853 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6707 5853 603 41 0 6666 0
vsize: 26828
[startup+100.006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 5875 0 0 0 9978 21 0 0 25 0 1 0 479258500 27471872 5853 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6707 5853 603 41 0 6666 0
vsize: 26828
[startup+110.008 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 5875 0 0 0 10978 21 0 0 25 0 1 0 479258500 27471872 5853 4294967295 134512640 134672761 3221224624 3221223888 134562492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6707 5853 603 41 0 6666 0
vsize: 26828
[startup+120.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 6011 0 0 0 11977 22 0 0 25 0 1 0 479258500 27901952 5971 4294967295 134512640 134672761 3221224624 3221223812 1075346941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6812 5971 603 41 0 6771 0
vsize: 27248
[startup+130.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 6519 0 0 0 12975 25 0 0 25 0 1 0 479258500 29990912 6470 4294967295 134512640 134672761 3221224624 3221117296 134594592 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7322 6470 603 41 0 7281 0
vsize: 29288
[startup+140.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 6957 0 0 0 13972 27 0 0 25 0 1 0 479258500 31719424 6899 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7744 6899 603 41 0 7703 0
vsize: 30976
[startup+150.008 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 7483 0 0 0 14970 29 0 0 25 0 1 0 479258500 33873920 7425 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8270 7425 603 41 0 8229 0
vsize: 33080
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 8040 0 0 0 15969 31 0 0 25 0 1 0 479258500 36257792 7973 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8852 7973 603 41 0 8811 0
vsize: 35408
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 8451 0 0 0 16968 32 0 0 25 0 1 0 479258500 38010880 8384 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9280 8384 603 41 0 9239 0
vsize: 37120
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 8878 0 0 0 17966 33 0 0 25 0 1 0 479258500 39616512 8811 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9672 8811 603 41 0 9631 0
vsize: 38688
[startup+190.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 9499 0 0 0 18965 35 0 0 25 0 1 0 479258500 42176512 9432 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10297 9432 603 41 0 10256 0
vsize: 41188
[startup+200.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 10116 0 0 0 19964 36 0 0 25 0 1 0 479258500 44724224 10049 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10919 10049 603 41 0 10878 0
vsize: 43676
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 10621 0 0 0 20963 38 0 0 25 0 1 0 479258500 46723072 10554 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11407 10554 603 41 0 11366 0
vsize: 45628
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 10996 0 0 0 21962 39 0 0 25 0 1 0 479258500 48263168 10921 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11783 10921 603 41 0 11742 0
vsize: 47132
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 11438 0 0 0 22961 40 0 0 25 0 1 0 479258500 50003968 11363 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12208 11363 603 41 0 12167 0
vsize: 48832
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 11837 0 0 0 23960 41 0 0 25 0 1 0 479258500 51740672 11762 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12632 11762 603 41 0 12591 0
vsize: 50528
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 12245 0 0 0 24960 41 0 0 25 0 1 0 479258500 53350400 12170 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13025 12170 603 41 0 12984 0
vsize: 52100
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 12627 0 0 0 25959 42 0 0 25 0 1 0 479258500 55209984 12552 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13479 12552 603 41 0 13438 0
vsize: 53916
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 12979 0 0 0 26958 43 0 0 25 0 1 0 479258500 56545280 12904 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13805 12904 603 41 0 13764 0
vsize: 55220
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 13389 0 0 0 27956 45 0 0 25 0 1 0 479258500 58281984 13314 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14229 13314 603 41 0 14188 0
vsize: 56916
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 13846 0 0 0 28955 46 0 0 25 0 1 0 479258500 60153856 13771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14686 13771 603 41 0 14645 0
vsize: 58744
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 14247 0 0 0 29954 48 0 0 25 0 1 0 479258500 61759488 14172 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15078 14172 603 41 0 15037 0
vsize: 60312
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 14772 0 0 0 30953 49 0 0 25 0 1 0 479258500 63893504 14697 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15599 14697 603 41 0 15558 0
vsize: 62396
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 15179 0 0 0 31953 50 0 0 25 0 1 0 479258500 65503232 15104 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15992 15104 603 41 0 15951 0
vsize: 63968
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 15525 0 0 0 32952 50 0 0 25 0 1 0 479258500 66969600 15450 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16350 15450 603 41 0 16309 0
vsize: 65400
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 15858 0 0 0 33951 51 0 0 25 0 1 0 479258500 68300800 15783 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16675 15783 603 41 0 16634 0
vsize: 66700
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 16192 0 0 0 34951 52 0 0 25 0 1 0 479258500 69636096 16117 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17001 16117 603 41 0 16960 0
vsize: 68004
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 16504 0 0 0 35950 53 0 0 25 0 1 0 479258500 70979584 16429 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17329 16429 603 41 0 17288 0
vsize: 69316
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 16876 0 0 0 36950 54 0 0 25 0 1 0 479258500 72454144 16801 4294967295 134512640 134672761 3221224624 3221223816 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17689 16801 603 41 0 17648 0
vsize: 70756
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17233 0 0 0 37948 55 0 0 25 0 1 0 479258500 73912320 17158 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18045 17158 603 41 0 18004 0
vsize: 72180
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 38948 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 39948 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 40948 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 41948 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223776 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 42948 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 43948 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 44948 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 45949 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223784 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 46949 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223728 134560022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 47949 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 48949 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 49949 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 50950 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 51950 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 52950 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 53950 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 54950 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 55950 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 56951 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 57951 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+590.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17399 0 0 0 58951 56 0 0 25 0 1 0 479258500 74481664 17316 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18184 17316 603 41 0 18143 0
vsize: 72736
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 17707 0 0 0 59950 57 0 0 25 0 1 0 479258500 75825152 17624 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18512 17624 603 41 0 18471 0
vsize: 74048
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 18033 0 0 0 60950 57 0 0 25 0 1 0 479258500 77164544 17950 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18839 17950 603 41 0 18798 0
vsize: 75356
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 18314 0 0 0 61949 59 0 0 25 0 1 0 479258500 78360576 18231 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19131 18231 603 41 0 19090 0
vsize: 76524
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 18577 0 0 0 62949 59 0 0 25 0 1 0 479258500 79425536 18494 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19391 18494 603 41 0 19350 0
vsize: 77564
[startup+640.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 18862 0 0 0 63949 59 0 0 25 0 1 0 479258500 80490496 18779 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19651 18779 603 41 0 19610 0
vsize: 78604
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 19143 0 0 0 64948 60 0 0 25 0 1 0 479258500 81678336 19060 4294967295 134512640 134672761 3221224624 3221223792 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19941 19060 603 41 0 19900 0
vsize: 79764
[startup+660.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 19446 0 0 0 65947 62 0 0 25 0 1 0 479258500 82890752 19363 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20237 19363 603 41 0 20196 0
vsize: 80948
[startup+670.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 19731 0 0 0 66946 62 0 0 25 0 1 0 479258500 84090880 19648 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20530 19648 603 41 0 20489 0
vsize: 82120
[startup+680.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 20063 0 0 0 67946 63 0 0 25 0 1 0 479258500 85430272 19980 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20857 19980 603 41 0 20816 0
vsize: 83428
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 20402 0 0 0 68945 64 0 0 25 0 1 0 479258500 86777856 20319 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21186 20319 603 41 0 21145 0
vsize: 84744
[startup+700.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 20672 0 0 0 69944 65 0 0 25 0 1 0 479258500 87982080 20589 4294967295 134512640 134672761 3221224624 3221223728 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21480 20589 603 41 0 21439 0
vsize: 85920
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 20943 0 0 0 70943 66 0 0 25 0 1 0 479258500 89038848 20860 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21738 20860 603 41 0 21697 0
vsize: 86952
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 21231 0 0 0 71942 67 0 0 25 0 1 0 479258500 90230784 21148 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22029 21148 603 41 0 21988 0
vsize: 88116
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 21485 0 0 0 72941 68 0 0 25 0 1 0 479258500 91291648 21402 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22288 21402 603 41 0 22247 0
vsize: 89152
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 21797 0 0 0 73940 69 0 0 25 0 1 0 479258500 92491776 21714 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22581 21714 603 41 0 22540 0
vsize: 90324
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 22057 0 0 0 74940 69 0 0 25 0 1 0 479258500 93552640 21974 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22840 21974 603 41 0 22799 0
vsize: 91360
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 22262 0 0 0 75940 70 0 0 25 0 1 0 479258500 94347264 22179 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23034 22179 603 41 0 22993 0
vsize: 92136
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 22457 0 0 0 76939 71 0 0 25 0 1 0 479258500 95145984 22374 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23229 22374 603 41 0 23188 0
vsize: 92916
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 22643 0 0 0 77939 71 0 0 25 0 1 0 479258500 95940608 22560 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23423 22560 603 41 0 23382 0
vsize: 93692
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 22832 0 0 0 78938 72 0 0 25 0 1 0 479258500 96739328 22749 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23618 22749 603 41 0 23577 0
vsize: 94472
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 23006 0 0 0 79938 72 0 0 25 0 1 0 479258500 97398784 22923 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23779 22923 603 41 0 23738 0
vsize: 95116
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 23139 0 0 0 80938 73 0 0 25 0 1 0 479258500 98451456 23056 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24036 23056 603 41 0 23995 0
vsize: 96144
[startup+820.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 23314 0 0 0 81938 73 0 0 25 0 1 0 479258500 99262464 23231 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24234 23231 603 41 0 24193 0
vsize: 96936
[startup+830.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 23484 0 0 0 82938 73 0 0 25 0 1 0 479258500 99930112 23401 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24397 23401 603 41 0 24356 0
vsize: 97588
[startup+840.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 23624 0 0 0 83937 74 0 0 25 0 1 0 479258500 100458496 23541 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24526 23541 603 41 0 24485 0
vsize: 98104
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 23747 0 0 0 84937 75 0 0 25 0 1 0 479258500 100986880 23664 4294967295 134512640 134672761 3221224624 3221223784 134561240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24655 23664 603 41 0 24614 0
vsize: 98620
[startup+860.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 23870 0 0 0 85937 75 0 0 25 0 1 0 479258500 101523456 23787 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24786 23787 603 41 0 24745 0
vsize: 99144
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 24012 0 0 0 86937 75 0 0 25 0 1 0 479258500 102055936 23929 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24916 23929 603 41 0 24875 0
vsize: 99664
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 24153 0 0 0 87936 76 0 0 25 0 1 0 479258500 102580224 24070 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25044 24070 603 41 0 25003 0
vsize: 100176
[startup+890.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 24280 0 0 0 88936 76 0 0 25 0 1 0 479258500 103112704 24197 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25174 24197 603 41 0 25133 0
vsize: 100696
[startup+900.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 24399 0 0 0 89936 77 0 0 25 0 1 0 479258500 103641088 24316 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25303 24316 603 41 0 25262 0
vsize: 101212
[startup+910.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 24507 0 0 0 90936 77 0 0 25 0 1 0 479258500 104042496 24424 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25401 24424 603 41 0 25360 0
vsize: 101604
[startup+920.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 24615 0 0 0 91936 77 0 0 25 0 1 0 479258500 104443904 24532 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25499 24532 603 41 0 25458 0
vsize: 101996
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 24719 0 0 0 92935 77 0 0 25 0 1 0 479258500 104837120 24636 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25595 24636 603 41 0 25554 0
vsize: 102380
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 24851 0 0 0 93935 78 0 0 25 0 1 0 479258500 105365504 24768 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25724 24768 603 41 0 25683 0
vsize: 102896
[startup+950.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 24977 0 0 0 94934 79 0 0 25 0 1 0 479258500 105902080 24894 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25855 24894 603 41 0 25814 0
vsize: 103420
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 25096 0 0 0 95934 79 0 0 25 0 1 0 479258500 106426368 25013 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25983 25013 603 41 0 25942 0
vsize: 103932
[startup+970.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 25210 0 0 0 96934 79 0 0 25 0 1 0 479258500 106844160 25127 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26085 25127 603 41 0 26044 0
vsize: 104340
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 25321 0 0 0 97934 79 0 0 25 0 1 0 479258500 107380736 25238 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26216 25238 603 41 0 26175 0
vsize: 104864
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 25420 0 0 0 98934 80 0 0 25 0 1 0 479258500 107778048 25337 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26313 25337 603 41 0 26272 0
vsize: 105252
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 25523 0 0 0 99934 80 0 0 25 0 1 0 479258500 108175360 25440 4294967295 134512640 134672761 3221224624 3221223824 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26410 25440 603 41 0 26369 0
vsize: 105640
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 25632 0 0 0 100934 80 0 0 25 0 1 0 479258500 108576768 25549 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26508 25549 603 41 0 26467 0
vsize: 106032
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 25727 0 0 0 101934 80 0 0 25 0 1 0 479258500 108974080 25644 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26605 25644 603 41 0 26564 0
vsize: 106420
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 25828 0 0 0 102934 80 0 0 25 0 1 0 479258500 109371392 25745 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26702 25745 603 41 0 26661 0
vsize: 106808
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 25918 0 0 0 103934 80 0 0 25 0 1 0 479258500 109768704 25835 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26799 25835 603 41 0 26758 0
vsize: 107196
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 26012 0 0 0 104934 81 0 0 25 0 1 0 479258500 110170112 25929 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26897 25929 603 41 0 26856 0
vsize: 107588
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 26123 0 0 0 105934 81 0 0 25 0 1 0 479258500 110563328 26040 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26993 26040 603 41 0 26952 0
vsize: 107972
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 26234 0 0 0 106934 82 0 0 25 0 1 0 479258500 111091712 26151 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27122 26151 603 41 0 27081 0
vsize: 108488
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 26327 0 0 0 107933 82 0 0 25 0 1 0 479258500 111484928 26244 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27218 26244 603 41 0 27177 0
vsize: 108872
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 26420 0 0 0 108933 82 0 0 25 0 1 0 479258500 111747072 26337 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27282 26337 603 41 0 27241 0
vsize: 109128
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 26523 0 0 0 109933 83 0 0 25 0 1 0 479258500 112279552 26440 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27412 26440 603 41 0 27371 0
vsize: 109648
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 26612 0 0 0 110933 83 0 0 25 0 1 0 479258500 112541696 26529 4294967295 134512640 134672761 3221224624 3221223792 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27476 26529 603 41 0 27435 0
vsize: 109904
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 26694 0 0 0 111933 83 0 0 25 0 1 0 479258500 112955392 26611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27577 26611 603 41 0 27536 0
vsize: 110308
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 26815 0 0 0 112932 83 0 0 25 0 1 0 479258500 113483776 26732 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27706 26732 603 41 0 27665 0
vsize: 110824
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 26938 0 0 0 113932 84 0 0 25 0 1 0 479258500 113881088 26855 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27803 26855 603 41 0 27762 0
vsize: 111212
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 27031 0 0 0 114932 84 0 0 25 0 1 0 479258500 114274304 26948 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27899 26948 603 41 0 27858 0
vsize: 111596
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 27146 0 0 0 115932 84 0 0 25 0 1 0 479258500 114806784 27063 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28029 27063 603 41 0 27988 0
vsize: 112116
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 27241 0 0 0 116932 85 0 0 25 0 1 0 479258500 115212288 27158 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28128 27158 603 41 0 28087 0
vsize: 112512
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 27328 0 0 0 117932 85 0 0 25 0 1 0 479258500 115617792 27245 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28227 27245 603 41 0 28186 0
vsize: 112908
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 27420 0 0 0 118932 85 0 0 25 0 1 0 479258500 115879936 27337 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28291 27337 603 41 0 28250 0
vsize: 113164
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21555
Raw data (stat): 21555 (minisat+) R 21554 18865 18864 0 -1 0 27511 0 0 0 119932 85 0 0 25 0 1 0 479258500 116277248 27428 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28388 27428 603 41 0 28347 0
vsize: 113552
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 21555
Raw data (stat): 21555 (minisat+) Z 21554 18865 18864 0 -1 12 27514 0 0 0 119932 91 0 0 25 0 1 0 479258500 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.09
CPU time (s): 1200.23
CPU user time (s): 1199.32
CPU system time (s): 0.910861
CPU usage (%): 100.012
Max. virtual memory (Kb): 113552
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####