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-1.opb
MD5SUM20fc65112f36a5d10cc9eaa82c0beb63
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -38
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.1
Number of variables1272
Total number of constraints94227
Number of constraints which are clauses94227
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 6384

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-14 04:49:03 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4851 boxname=wulflinc25 idbench=339 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  20fc65112f36a5d10cc9eaa82c0beb63  /oldhome/oroussel/tmp/wulflinc25/normalized-frb53-24-1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc25/normalized-frb53-24-1.opb /oldhome/oroussel/tmp/wulflinc25/normalized-frb53-24-1.opb
IDLAUNCH: 4851
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        856648 kB
Buffers:         35184 kB
Cached:         107580 kB
SwapCached:         36 kB
Active:          53224 kB
Inactive:        92456 kB
HighTotal:      131008 kB
HighFree:        19628 kB
LowTotal:       903652 kB
LowFree:        837020 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26528 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:09:06 (client local time) WITH STATUS 10 IN 1200.47 SECONDS
stats: 4851 7 1200.47 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 94227 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 |   94227   188454 |   31409       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -36
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 |  244947   541084 |   81649       0        0     nan |  0.000 % |
c |       100 |  244947   541084 |   89813     100     1082    10.8 |  0.014 % |
c |       251 |  244414   539871 |   98795     237     2012     8.5 |  0.372 % |
c |       476 |  240587   531087 |  108674     389     3113     8.0 |  2.599 % |
c |       813 |  235181   518674 |  119542     614     4746     7.7 |  5.835 % |
c |      1319 |  226313   498257 |  131496     916     7106     7.8 | 11.250 % |
c |      2078 |  215022   472171 |  144646    1421    11823     8.3 | 18.298 % |
c |      3217 |  199573   436478 |  159110    2233    18781     8.4 | 27.854 % |
c |      4925 |  178575   387582 |  175021    3311    27851     8.4 | 41.181 % |
c ==============================================================================
c Found solution: -38
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 |      5587 |  169033   365226 |   56344    3520    29503     8.4 | 41.181 % |
c |      5688 |  168623   364274 |   61978    3599    30725     8.5 | 47.811 % |
c |      5838 |  167224   361036 |   68176    3697    31581     8.5 | 48.691 % |
c |      6063 |  166129   358484 |   74993    3874    33139     8.6 | 49.341 % |
c |      6400 |  163008   351161 |   82493    4057    34550     8.5 | 51.463 % |
c |      6906 |  159352   342601 |   90742    4397    37323     8.5 | 53.897 % |
c |      7665 |  153177   328119 |   99816    4723    43693     9.3 | 58.073 % |
c |      8804 |  141454   300749 |  109798    5207    47906     9.2 | 65.709 % |
c |     10513 |  129713   273157 |  120778    5800    57461     9.9 | 73.591 % |
c ==============================================================================
c Found solution: -39
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 |     11112 |  125735   263896 |   41911    5940    59548    10.0 | 73.591 % |
c |     11212 |  125242   262739 |   46102    5958    59531    10.0 | 76.704 % |
c |     11362 |  124288   260476 |   50712    5956    59254     9.9 | 77.379 % |
c |     11587 |  122380   256006 |   55783    6065    60757    10.0 | 78.667 % |
c |     11924 |  121348   253577 |   61361    6219    60725     9.8 | 79.373 % |
c |     12431 |  119633   249531 |   67498    6507    66069    10.2 | 80.556 % |
c |     13191 |  118333   246466 |   74247    6956    71403    10.3 | 81.432 % |
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 |     14134 |  113554   235196 |   37851    7039    72150    10.3 | 81.432 % |
c |     14234 |  113372   234758 |   41636    7036    72002    10.2 | 84.835 % |
c |     14384 |  112513   232749 |   45799    6930    71045    10.3 | 85.421 % |
c |     14609 |  112404   232492 |   50379    7142    75264    10.5 | 85.497 % |
c |     14947 |  111609   230614 |   55417    7238    75720    10.5 | 86.063 % |
c |     15454 |  110820   228765 |   60959    7384    82571    11.2 | 86.595 % |
c |     16213 |  109537   225718 |   67055    7442    91384    12.3 | 87.514 % |
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 |     16799 |  108153   222488 |   36051    7670    94769    12.4 | 87.514 % |
c |     16902 |  107584   221146 |   39656    7595    94373    12.4 | 88.879 % |
c |     17052 |  107584   221146 |   43621    7745    97344    12.6 | 88.879 % |
c |     17279 |  107481   220901 |   47983    7935   100720    12.7 | 88.957 % |
c |     17616 |  107218   220280 |   52782    8089   103453    12.8 | 89.142 % |
c |     18122 |  107069   219925 |   58060    8520   121593    14.3 | 89.255 % |
c |     18881 |  106453   218468 |   63866    8868   148675    16.8 | 89.684 % |
c |     20020 |  106329   218172 |   70253    9856   198305    20.1 | 89.774 % |
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 |     20823 |  106076   217556 |   35358   10561   265515    25.1 | 89.774 % |
c |     20923 |  106076   217556 |   38893   10661   268738    25.2 | 89.938 % |
c |     21073 |  106076   217556 |   42783   10811   275129    25.4 | 89.938 % |
c |     21298 |  106076   217556 |   47061   11036   285202    25.8 | 89.938 % |
c |     21635 |  106076   217556 |   51767   11373   291931    25.7 | 89.938 % |
c |     22142 |  106076   217556 |   56944   11880   321705    27.1 | 89.938 % |
c |     22902 |  105776   216861 |   62638   12408   355411    28.6 | 90.131 % |
c |     24041 |  105776   216861 |   68902   13547   444666    32.8 | 90.131 % |
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 |     24522 |  105716   216733 |   35238   13715   481917    35.1 | 90.131 % |
c |     24623 |  105716   216733 |   38761   13816   486032    35.2 | 90.194 % |
c |     24774 |  105653   216586 |   42637   13945   493773    35.4 | 90.239 % |
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 |     24847 |  105568   216370 |   35189   13966   492372    35.3 | 90.239 % |
c |     24947 |  105568   216370 |   38707   14066   496882    35.3 | 90.290 % |
c |     25097 |  105568   216370 |   42578   14216   501821    35.3 | 90.290 % |
c |     25322 |  105568   216370 |   46836   14441   514536    35.6 | 90.290 % |
c |     25659 |  105504   216219 |   51520   14668   528058    36.0 | 90.334 % |
c |     26169 |  105504   216219 |   56672   15178   555755    36.6 | 90.334 % |
c |     26928 |  105504   216219 |   62339   15937   637260    40.0 | 90.334 % |
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 |     27994 |  105415   216019 |   35138   16897   717188    42.4 | 90.334 % |
c |     28094 |  105415   216019 |   38651   16997   720879    42.4 | 90.398 % |
c |     28244 |  105344   215850 |   42516   17081   729292    42.7 | 90.453 % |
c |     28470 |  105300   215745 |   46768   17241   741085    43.0 | 90.486 % |
c |     28809 |  105294   215731 |   51445   17559   769342    43.8 | 90.490 % |
c |     29315 |  105254   215636 |   56590   18051   785080    43.5 | 90.519 % |
c |     30074 |  105254   215636 |   62249   18810   834235    44.4 | 90.519 % |
c |     31213 |  105168   215439 |   68474   19854   969745    48.8 | 90.565 % |
c |     32921 |  105010   215064 |   75321   21367  1094901    51.2 | 90.684 % |
c |     35483 |  105010   215064 |   82853   23929  1454753    60.8 | 90.684 % |
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 |     36476 |  104833   214626 |   34944   24560  1529898    62.3 | 90.684 % |
c |     36576 |  104833   214626 |   38438   24660  1533499    62.2 | 90.799 % |
c |     36727 |  104833   214626 |   42282   24811  1540136    62.1 | 90.799 % |
c |     36952 |  104799   214549 |   46510   25011  1546646    61.8 | 90.819 % |
c |     37289 |  104799   214549 |   51161   25348  1561273    61.6 | 90.819 % |
c |     37795 |  104799   214549 |   56277   25854  1595462    61.7 | 90.819 % |
c |     38554 |  104773   214487 |   61905   26582  1642013    61.8 | 90.838 % |
c |     39693 |  104773   214487 |   68095   27721  1735576    62.6 | 90.838 % |
c |     41402 |  104711   214338 |   74905   29309  1872631    63.9 | 90.885 % |
c |     43964 |  104711   214338 |   82396   31871  2163660    67.9 | 90.885 % |
c |     47808 |  104711   214338 |   90635   35715  2594699    72.7 | 90.885 % |
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 |     49791 |  104753   214439 |   34917   37698  2839908    75.3 | 90.885 % |
c |     49891 |  104753   214439 |   38408   37798  2848511    75.4 | 90.881 % |
c |     50041 |  104753   214439 |   42249   37948  2859638    75.4 | 90.881 % |
c |     50266 |  104753   214439 |   46474   38173  2871725    75.2 | 90.881 % |
c |     50603 |  104753   214439 |   51121   38510  2896709    75.2 | 90.881 % |
c |     51109 |  104753   214439 |   56234   39016  2926834    75.0 | 90.881 % |
c |     51868 |  104753   214439 |   61857   39775  2981249    75.0 | 90.881 % |
c |     53007 |  104753   214439 |   68043   40914  3120209    76.3 | 90.881 % |
c |     54715 |  104753   214439 |   74847   42622  3285217    77.1 | 90.881 % |
c |     57277 |  104753   214439 |   82332   45184  3563599    78.9 | 90.881 % |
c |     61122 |  104753   214439 |   90565   49029  3960352    80.8 | 90.881 % |
c |     66888 |  104753   214439 |   99622   54795  4629161    84.5 | 90.881 % |
c |     75537 |  104691   214292 |  109584   63274  5877856    92.9 | 90.926 % |
c |     88512 |  104691   214292 |  120542   76249  7484684    98.2 | 90.926 % |
c |    107973 |  104691   214292 |  132597   95710  9561126    99.9 | 90.926 % |
c ==============================================================================
c Found solution: -48
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 |    132860 |  104615   214103 |   34871  120421 12201442   101.3 | 90.926 % |
c |    132961 |  104615   214103 |   38358   18037  1463940    81.2 | 90.975 % |
c |    133111 |  104615   214103 |   42193   18187  1468598    80.7 | 90.975 % |
c |    133337 |  104553   213957 |   46413   18409  1482285    80.5 | 91.017 % |
c |    133674 |  104553   213957 |   51054   18746  1503771    80.2 | 91.017 % |
c |    134180 |  104547   213943 |   56160   19251  1544268    80.2 | 91.021 % |
c |    134939 |  104477   213775 |   61776   19995  1579039    79.0 | 91.074 % |
c |    136079 |  104463   213741 |   67953   21132  1671797    79.1 | 91.085 % |
c |    137789 |  104463   213741 |   74749   22842  1858804    81.4 | 91.085 % |
c |    140351 |  104463   213741 |   82223   25404  2144978    84.4 | 91.085 % |
c |    144196 |  104463   213741 |   90446   29249  2519784    86.1 | 91.085 % |
c |    149962 |  104463   213741 |   99491   35015  3270196    93.4 | 91.085 % |
c |    158611 |  104451   213713 |  109440   43663  4298987    98.5 | 91.093 % |
c |    171587 |  104451   213713 |  120384   56639  6410910   113.2 | 91.093 % |
c ==============================================================================
c Found solution: -49
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 |    185156 |  104482   213787 |   34827   70208  8068756   114.9 | 91.093 % |
c |    185256 |  104482   213787 |   38309   70308  8075584   114.9 | 91.077 % |
c |    185408 |  104482   213787 |   42140   70460  8081704   114.7 | 91.077 % |
c |    185633 |  104472   213763 |   46354   70635  8097561   114.6 | 91.084 % |
c |    185970 |  104472   213763 |   50990   70972  8131396   114.6 | 91.084 % |
c |    186478 |  104472   213763 |   56089   71480  8185430   114.5 | 91.084 % |
c |    187237 |  104472   213763 |   61698   72239  8257138   114.3 | 91.084 % |
c |    188376 |  104472   213763 |   67867   73378  8347232   113.8 | 91.084 % |
c |    190086 |  104472   213763 |   74654   75088  8478132   112.9 | 91.084 % |
c |    192649 |  104472   213763 |   82120   77651  8714812   112.2 | 91.084 % |
c |    196494 |  104472   213763 |   90332   81496  9061128   111.2 | 91.084 % |
c |    202261 |  104472   213763 |   99365   87263  9594982   110.0 | 91.084 % |
c |    210910 |  104472   213763 |  109302   95912 10290527   107.3 | 91.084 % |
c |    223885 |  104468   213754 |  120232  108884 11255497   103.4 | 91.086 % |
c |    243349 |  104468   213754 |  132255  128348 12674336    98.7 | 91.086 % |
c |    272541 |  104468   213754 |  145481  157540 14398735    91.4 | 91.086 % |
c |    316330 |  104468   213754 |  160029   29601  1100197    37.2 | 91.086 % |
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 -C6#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.95 0.90 2/54 3439
Raw data (stat): 3439 (runsolver) R 3438 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481845856 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6016 0 0 0 982 16 0 0 25 0 1 0 481845856 27267072 5994 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6657 5994 603 41 0 6616 0
vsize: 26628
[startup+20.0007 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6024 0 0 0 1982 16 0 0 25 0 1 0 481845856 27267072 6002 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6657 6002 603 41 0 6616 0
vsize: 26628
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6025 0 0 0 2982 16 0 0 25 0 1 0 481845856 27267072 6003 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6657 6003 603 41 0 6616 0
vsize: 26628
[startup+40.0009 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6025 0 0 0 3981 16 0 0 25 0 1 0 481845856 27267072 6003 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6657 6003 603 41 0 6616 0
vsize: 26628
[startup+50.001 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6025 0 0 0 4982 16 0 0 25 0 1 0 481845856 27267072 6003 4294967295 134512640 134672761 3221224560 3221223728 134561272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6657 6003 603 41 0 6616 0
vsize: 26628
[startup+60.0014 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6165 0 0 0 5981 16 0 0 25 0 1 0 481845856 28311552 6143 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6912 6143 603 41 0 6871 0
vsize: 27648
[startup+70.0017 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6165 0 0 0 6981 17 0 0 25 0 1 0 481845856 28311552 6143 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6912 6143 603 41 0 6871 0
vsize: 27648
[startup+80.0013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6165 0 0 0 7981 17 0 0 25 0 1 0 481845856 28311552 6143 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6912 6143 603 41 0 6871 0
vsize: 27648
[startup+90.0012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6169 0 0 0 8982 17 0 0 25 0 1 0 481845856 28311552 6147 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6912 6147 603 41 0 6871 0
vsize: 27648
[startup+100 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6171 0 0 0 9982 17 0 0 25 0 1 0 481845856 28311552 6149 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6912 6149 603 41 0 6871 0
vsize: 27648
[startup+110.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 6477 0 0 0 10980 18 0 0 25 0 1 0 481845856 29536256 6446 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7211 6446 603 41 0 7170 0
vsize: 28844
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 7032 0 0 0 11979 19 0 0 25 0 1 0 481845856 31666176 6974 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7731 6974 603 41 0 7690 0
vsize: 30924
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 7659 0 0 0 12977 21 0 0 25 0 1 0 481845856 34160640 7592 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8340 7592 603 41 0 8299 0
vsize: 33360
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 8190 0 0 0 13976 23 0 0 25 0 1 0 481845856 36311040 8123 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8865 8123 603 41 0 8824 0
vsize: 35460
[startup+150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 8781 0 0 0 14974 25 0 0 25 0 1 0 481845856 38854656 8714 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9486 8714 603 41 0 9445 0
vsize: 37944
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 9276 0 0 0 15973 27 0 0 25 0 1 0 481845856 40898560 9201 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9985 9201 603 41 0 9944 0
vsize: 39940
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 9765 0 0 0 16971 28 0 0 25 0 1 0 481845856 42913792 9690 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10477 9690 603 41 0 10436 0
vsize: 41908
[startup+179.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 10196 0 0 0 17970 30 0 0 25 0 1 0 481845856 44642304 10121 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10899 10121 603 41 0 10858 0
vsize: 43596
[startup+189.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 10638 0 0 0 18968 31 0 0 25 0 1 0 481845856 46374912 10563 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11322 10563 603 41 0 11281 0
vsize: 45288
[startup+199.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 11050 0 0 0 19967 33 0 0 25 0 1 0 481845856 48095232 10975 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11742 10975 603 41 0 11701 0
vsize: 46968
[startup+209.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 11596 0 0 0 20966 34 0 0 25 0 1 0 481845856 50356224 11521 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12294 11521 603 41 0 12253 0
vsize: 49176
[startup+219.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 12168 0 0 0 21965 35 0 0 25 0 1 0 481845856 52617216 12093 4294967295 134512640 134672761 3221224560 3221223700 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12846 12093 603 41 0 12805 0
vsize: 51384
[startup+229.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 12601 0 0 0 22964 36 0 0 25 0 1 0 481845856 54616064 12526 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13334 12526 603 41 0 13293 0
vsize: 53336
[startup+239.999 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 13037 0 0 0 23963 38 0 0 25 0 1 0 481845856 56479744 12962 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13789 12962 603 41 0 13748 0
vsize: 55156
[startup+249.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 13418 0 0 0 24962 39 0 0 25 0 1 0 481845856 57946112 13343 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14147 13343 603 41 0 14106 0
vsize: 56588
[startup+259.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 13822 0 0 0 25961 40 0 0 25 0 1 0 481845856 59670528 13747 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14568 13747 603 41 0 14527 0
vsize: 58272
[startup+269.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 14197 0 0 0 26960 41 0 0 25 0 1 0 481845856 61145088 14122 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14928 14122 603 41 0 14887 0
vsize: 59712
[startup+279.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 14558 0 0 0 27959 42 0 0 25 0 1 0 481845856 62611456 14483 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15286 14483 603 41 0 15245 0
vsize: 61144
[startup+289.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 14884 0 0 0 28958 43 0 0 25 0 1 0 481845856 63950848 14809 4294967295 134512640 134672761 3221224560 3221223664 134560128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15613 14809 603 41 0 15572 0
vsize: 62452
[startup+299.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 15242 0 0 0 29957 44 0 0 25 0 1 0 481845856 65425408 15167 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15973 15167 603 41 0 15932 0
vsize: 63892
[startup+309.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 15556 0 0 0 30956 46 0 0 25 0 1 0 481845856 66625536 15481 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16266 15481 603 41 0 16225 0
vsize: 65064
[startup+319.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 15815 0 0 0 31955 46 0 0 25 0 1 0 481845856 67682304 15740 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16524 15740 603 41 0 16483 0
vsize: 66096
[startup+329.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 16117 0 0 0 32954 47 0 0 25 0 1 0 481845856 69013504 16042 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16849 16042 603 41 0 16808 0
vsize: 67396
[startup+339.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 16380 0 0 0 33954 48 0 0 25 0 1 0 481845856 70074368 16305 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16305 603 41 0 17067 0
vsize: 68432
[startup+349.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 16670 0 0 0 34953 49 0 0 25 0 1 0 481845856 71131136 16595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17366 16595 603 41 0 17325 0
vsize: 69464
[startup+359.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 16946 0 0 0 35953 50 0 0 25 0 1 0 481845856 72318976 16871 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17656 16871 603 41 0 17615 0
vsize: 70624
[startup+369.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 17203 0 0 0 36952 50 0 0 25 0 1 0 481845856 73379840 17128 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17915 17128 603 41 0 17874 0
vsize: 71660
[startup+379.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 17518 0 0 0 37951 51 0 0 25 0 1 0 481845856 74571776 17443 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18206 17443 603 41 0 18165 0
vsize: 72824
[startup+389.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 17840 0 0 0 38950 52 0 0 25 0 1 0 481845856 75902976 17765 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18531 17765 603 41 0 18490 0
vsize: 74124
[startup+399.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 18104 0 0 0 39949 53 0 0 25 0 1 0 481845856 76967936 18029 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18791 18029 603 41 0 18750 0
vsize: 75164
[startup+409.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 18367 0 0 0 40949 54 0 0 25 0 1 0 481845856 78028800 18292 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19050 18292 603 41 0 19009 0
vsize: 76200
[startup+419.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 18602 0 0 0 41949 55 0 0 25 0 1 0 481845856 79097856 18527 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19311 18527 603 41 0 19270 0
vsize: 77244
[startup+429.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 18852 0 0 0 42948 55 0 0 25 0 1 0 481845856 80027648 18777 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19538 18777 603 41 0 19497 0
vsize: 78152
[startup+439.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 43947 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+449.992 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 44947 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223760 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+459.992 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 45947 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+469.993 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 46947 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+479.992 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 47947 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+489.992 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 48948 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+499.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 49948 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223696 134560634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+509.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 50948 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+519.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 51948 56 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223744 134559613 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+529.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 52948 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+539.991 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 53948 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+549.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 54948 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+559.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 55949 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+569.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 56949 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+579.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 57949 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+589.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 58949 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+599.99 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 59949 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+609.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 60949 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+619.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 61950 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+629.988 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 62950 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+639.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 63950 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+649.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 64950 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+659.989 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3439
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 65950 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+670.075 s]
Raw data (loadavg): 1.15 1.00 0.92 2/57 3488
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 66959 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+680.074 s]
Raw data (loadavg): 1.12 1.00 0.92 2/54 3492
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 67959 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+690.248 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 3492
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 68977 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+700.248 s]
Raw data (loadavg): 1.09 1.00 0.92 2/54 3492
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 69977 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+710.25 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 3492
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 70977 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+720.25 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 3492
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 71977 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+730.249 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 3492
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19088 0 0 0 72977 57 0 0 25 0 1 0 481845856 80916480 19004 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19755 19004 603 41 0 19714 0
vsize: 79020
[startup+740.25 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19158 0 0 0 73978 57 0 0 25 0 1 0 481845856 81313792 19074 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19852 19074 603 41 0 19811 0
vsize: 79408
[startup+750.249 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19340 0 0 0 74977 57 0 0 25 0 1 0 481845856 81977344 19256 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20014 19256 603 41 0 19973 0
vsize: 80056
[startup+760.25 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19514 0 0 0 75977 57 0 0 25 0 1 0 481845856 82780160 19430 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20210 19430 603 41 0 20169 0
vsize: 80840
[startup+770.25 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19669 0 0 0 76977 58 0 0 25 0 1 0 481845856 83304448 19585 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20338 19585 603 41 0 20297 0
vsize: 81352
[startup+780.249 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 19844 0 0 0 77977 58 0 0 25 0 1 0 481845856 84090880 19760 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20530 19760 603 41 0 20489 0
vsize: 82120
[startup+790.249 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20029 0 0 0 78977 58 0 0 25 0 1 0 481845856 84877312 19945 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20722 19945 603 41 0 20681 0
vsize: 82888
[startup+800.249 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20217 0 0 0 79976 59 0 0 25 0 1 0 481845856 86061056 20133 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21011 20133 603 41 0 20970 0
vsize: 84044
[startup+810.249 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20392 0 0 0 80976 59 0 0 25 0 1 0 481845856 86859776 20308 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21206 20308 603 41 0 21165 0
vsize: 84824
[startup+820.249 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20556 0 0 0 81976 60 0 0 25 0 1 0 481845856 87523328 20472 4294967295 134512640 134672761 3221224560 3221223664 134560381 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21368 20472 603 41 0 21327 0
vsize: 85472
[startup+830.249 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20706 0 0 0 82976 60 0 0 25 0 1 0 481845856 88059904 20622 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21499 20622 603 41 0 21458 0
vsize: 85996
[startup+840.249 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20835 0 0 0 83975 61 0 0 25 0 1 0 481845856 88584192 20751 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21627 20751 603 41 0 21586 0
vsize: 86508
[startup+850.248 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 20968 0 0 0 84975 61 0 0 25 0 1 0 481845856 89112576 20884 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21756 20884 603 41 0 21715 0
vsize: 87024
[startup+860.248 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21092 0 0 0 85975 61 0 0 25 0 1 0 481845856 89636864 21008 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21884 21008 603 41 0 21843 0
vsize: 87536
[startup+870.248 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21207 0 0 0 86975 62 0 0 25 0 1 0 481845856 90034176 21123 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21981 21123 603 41 0 21940 0
vsize: 87924
[startup+880.247 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21325 0 0 0 87975 62 0 0 25 0 1 0 481845856 90566656 21241 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22111 21241 603 41 0 22070 0
vsize: 88444
[startup+890.247 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21444 0 0 0 88974 62 0 0 25 0 1 0 481845856 91090944 21360 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22239 21360 603 41 0 22198 0
vsize: 88956
[startup+900.246 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21561 0 0 0 89974 63 0 0 25 0 1 0 481845856 91484160 21477 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22335 21477 603 41 0 22294 0
vsize: 89340
[startup+910.247 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21677 0 0 0 90974 63 0 0 25 0 1 0 481845856 92012544 21593 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22464 21593 603 41 0 22423 0
vsize: 89856
[startup+920.247 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21781 0 0 0 91974 63 0 0 25 0 1 0 481845856 92409856 21697 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22561 21697 603 41 0 22520 0
vsize: 90244
[startup+930.246 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 21904 0 0 0 92973 64 0 0 25 0 1 0 481845856 92934144 21820 4294967295 134512640 134672761 3221224560 3221223656 1075347133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22689 21820 603 41 0 22648 0
vsize: 90756
[startup+940.246 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22015 0 0 0 93973 64 0 0 25 0 1 0 481845856 93462528 21931 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22818 21931 603 41 0 22777 0
vsize: 91272
[startup+950.246 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22129 0 0 0 94973 65 0 0 25 0 1 0 481845856 93859840 22045 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22915 22045 603 41 0 22874 0
vsize: 91660
[startup+960.246 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22250 0 0 0 95973 65 0 0 25 0 1 0 481845856 94384128 22166 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23043 22166 603 41 0 23002 0
vsize: 92172
[startup+970.246 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22361 0 0 0 96972 65 0 0 25 0 1 0 481845856 94777344 22277 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23139 22277 603 41 0 23098 0
vsize: 92556
[startup+980.246 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22460 0 0 0 97972 65 0 0 25 0 1 0 481845856 95174656 22376 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23236 22376 603 41 0 23195 0
vsize: 92944
[startup+990.246 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22576 0 0 0 98972 66 0 0 25 0 1 0 481845856 95703040 22492 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23365 22492 603 41 0 23324 0
vsize: 93460
[startup+1000.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3494
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22707 0 0 0 99972 66 0 0 25 0 1 0 481845856 96227328 22623 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23493 22623 603 41 0 23452 0
vsize: 93972
[startup+1010.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22817 0 0 0 100972 67 0 0 25 0 1 0 481845856 96620544 22733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23589 22733 603 41 0 23548 0
vsize: 94356
[startup+1020.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 22918 0 0 0 101972 67 0 0 25 0 1 0 481845856 97017856 22834 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23686 22834 603 41 0 23645 0
vsize: 94744
[startup+1030.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23010 0 0 0 102972 67 0 0 25 0 1 0 481845856 97431552 22926 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23787 22926 603 41 0 23746 0
vsize: 95148
[startup+1040.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23092 0 0 0 103972 67 0 0 25 0 1 0 481845856 97828864 23008 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23884 23008 603 41 0 23843 0
vsize: 95536
[startup+1050.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23185 0 0 0 104972 68 0 0 25 0 1 0 481845856 98230272 23101 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23982 23101 603 41 0 23941 0
vsize: 95928
[startup+1060.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23267 0 0 0 105972 68 0 0 25 0 1 0 481845856 98496512 23183 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24047 23183 603 41 0 24006 0
vsize: 96188
[startup+1070.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23340 0 0 0 106972 68 0 0 25 0 1 0 481845856 98758656 23256 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24111 23256 603 41 0 24070 0
vsize: 96444
[startup+1080.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23435 0 0 0 107972 68 0 0 25 0 1 0 481845856 99151872 23351 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24207 23351 603 41 0 24166 0
vsize: 96828
[startup+1090.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23542 0 0 0 108972 68 0 0 25 0 1 0 481845856 99549184 23458 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24304 23458 603 41 0 24263 0
vsize: 97216
[startup+1100.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23641 0 0 0 109971 69 0 0 25 0 1 0 481845856 99950592 23557 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24402 23557 603 41 0 24361 0
vsize: 97608
[startup+1110.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23723 0 0 0 110971 69 0 0 25 0 1 0 481845856 100343808 23639 4294967295 134512640 134672761 3221224560 3221223744 134559463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24498 23639 603 41 0 24457 0
vsize: 97992
[startup+1120.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23804 0 0 0 111971 69 0 0 25 0 1 0 481845856 100630528 23720 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24568 23720 603 41 0 24527 0
vsize: 98272
[startup+1130.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23908 0 0 0 112971 69 0 0 25 0 1 0 481845856 101027840 23824 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24665 23824 603 41 0 24624 0
vsize: 98660
[startup+1140.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 113972 69 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24697 23860 603 41 0 24656 0
vsize: 98788
[startup+1150.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 114972 69 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24697 23860 603 41 0 24656 0
vsize: 98788
[startup+1160.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 115971 70 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24697 23860 603 41 0 24656 0
vsize: 98788
[startup+1170.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 116971 70 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24697 23860 603 41 0 24656 0
vsize: 98788
[startup+1180.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 117971 70 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24697 23860 603 41 0 24656 0
vsize: 98788
[startup+1190.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 118972 70 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24697 23860 603 41 0 24656 0
vsize: 98788
[startup+1200.25 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 3496
Raw data (stat): 3439 (minisat+) R 3438 28099 28098 0 -1 0 23944 0 0 0 119972 70 0 0 25 0 1 0 481845856 101158912 23860 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24697 23860 603 41 0 24656 0
vsize: 98788
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.3 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 3496
Raw data (stat): 3439 (minisat+) Z 3438 28099 28098 0 -1 12 23947 0 0 0 119972 74 0 0 25 0 1 0 481845856 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.3
CPU time (s): 1200.47
CPU user time (s): 1199.72
CPU system time (s): 0.743886
CPU usage (%): 100.014
Max. virtual memory (Kb): 98788
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####