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/frb56-25-opb/normalized-frb56-25-5.opb
MD5SUM1694d09a3d3e6cb31138c73ed644b225
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -43
Optimality of the best value was proved NO
Number of terms in the objective function 1400
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 1400
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 1400
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.12
Number of variables1400
Total number of constraints109601
Number of constraints which are clauses109601
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 6399

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-14 04:53:49 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4860 boxname=wulflinc9 idbench=348 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1694d09a3d3e6cb31138c73ed644b225  /oldhome/oroussel/tmp/wulflinc9/normalized-frb56-25-5.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc9/normalized-frb56-25-5.opb /oldhome/oroussel/tmp/wulflinc9/normalized-frb56-25-5.opb
IDLAUNCH: 4860
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        883604 kB
Buffers:         36616 kB
Cached:          93720 kB
SwapCached:        564 kB
Active:          57288 kB
Inactive:        76496 kB
HighTotal:      131008 kB
HighFree:        33404 kB
LowTotal:       903652 kB
LowFree:        850200 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            11696 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:13:52 (client local time) WITH STATUS 10 IN 1200.37 SECONDS
stats: 4860 7 1200.37 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 109601 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 |  109601   219202 |   36533       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -37
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:78076     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  277379   611709 |   92459       0        0     nan |  0.000 % |
c |       100 |  277379   611709 |  101704     100      790     7.9 |  0.002 % |
c |       250 |  276410   609500 |  111875     228     1400     6.1 |  0.498 % |
c |       475 |  275498   607416 |  123062     435     2989     6.9 |  0.973 % |
c |       813 |  271362   597927 |  135369     706     5052     7.2 |  3.182 % |
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 |      1001 |  269276   593147 |   89758     857     6124     7.1 |  3.182 % |
c |      1103 |  269276   593147 |   98733     959     6877     7.2 |  4.289 % |
c |      1254 |  268390   591137 |  108607    1092     7391     6.8 |  4.729 % |
c |      1479 |  266541   586932 |  119467    1271     8465     6.7 |  5.660 % |
c |      1816 |  262999   578773 |  131414    1540    14005     9.1 |  7.596 % |
c |      2322 |  253975   558057 |  144556    1869    16126     8.6 | 12.493 % |
c |      3081 |  246373   540370 |  159011    2404    24756    10.3 | 16.731 % |
c |      4220 |  234734   513487 |  174912    3188    32267    10.1 | 23.219 % |
c |      5928 |  213360   463951 |  192404    4308    41255     9.6 | 35.354 % |
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 |      7394 |  201009   435356 |   67003    5179    48684     9.4 | 35.354 % |
c |      7494 |  200732   434704 |   73703    5259    49255     9.4 | 42.848 % |
c |      7644 |  199247   431245 |   81073    5363    49921     9.3 | 43.673 % |
c |      7869 |  197963   428248 |   89180    5559    52100     9.4 | 44.381 % |
c |      8206 |  195420   422319 |   98099    5769    53920     9.3 | 45.861 % |
c |      8712 |  189120   407496 |  107909    5911    56919     9.6 | 49.544 % |
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 |      8819 |  187884   404659 |   62628    5960    57305     9.6 | 49.544 % |
c |      8919 |  187445   403635 |   68890    6033    58448     9.7 | 50.606 % |
c |      9069 |  185899   400018 |   75779    6133    59045     9.6 | 51.550 % |
c |      9294 |  183127   393494 |   83357    6188    60491     9.8 | 53.242 % |
c |      9631 |  181354   389341 |   91693    6418    65693    10.2 | 54.283 % |
c |     10137 |  177432   380140 |  100863    6742    69787    10.4 | 56.627 % |
c |     10896 |  173851   371804 |  110949    7290    75101    10.3 | 58.708 % |
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 |     11703 |  169258   360957 |   56419    7750    82967    10.7 | 58.708 % |
c |     11803 |  169108   360605 |   62060    7841    83677    10.7 | 61.536 % |
c |     11953 |  166829   355291 |   68266    7816    84255    10.8 | 62.886 % |
c |     12178 |  166234   353906 |   75093    8015    86788    10.8 | 63.233 % |
c |     12517 |  162280   344688 |   82603    8104    88177    10.9 | 65.569 % |
c |     13023 |  159253   337559 |   90863    8324    90280    10.8 | 67.339 % |
c |     13782 |  156769   331689 |   99949    8856    97513    11.0 | 68.817 % |
c |     14922 |  152768   322259 |  109944    9591   107627    11.2 | 71.270 % |
c |     16630 |  148615   312469 |  120939   10707   129164    12.1 | 73.844 % |
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 |     17182 |  146957   308648 |   48985   10865   132483    12.2 | 73.844 % |
c |     17282 |  146957   308648 |   53883   10965   133370    12.2 | 74.959 % |
c |     17433 |  146078   306594 |   59271   10976   133108    12.1 | 75.493 % |
c |     17659 |  145602   305480 |   65199   11154   137717    12.3 | 75.787 % |
c |     17998 |  144527   302967 |   71718   11367   142310    12.5 | 76.442 % |
c |     18504 |  142895   299122 |   78890   11523   143341    12.4 | 77.453 % |
c |     19263 |  141210   295160 |   86779   11811   149886    12.7 | 78.473 % |
c |     20403 |  139012   289999 |   95457   12523   162438    13.0 | 79.828 % |
c |     22111 |  136363   283731 |  105003   13464   180354    13.4 | 81.457 % |
c |     24673 |  133024   275867 |  115504   15116   207395    13.7 | 83.507 % |
c |     28517 |  130718   270431 |  127054   18029   264818    14.7 | 84.951 % |
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 |     32459 |  129364   267202 |   43121   20849   344914    16.5 | 84.951 % |
c |     32559 |  129292   267031 |   47433   20810   340159    16.3 | 85.848 % |
c |     32709 |  129214   266849 |   52176   20903   340608    16.3 | 85.896 % |
c |     32934 |  129176   266761 |   57394   21049   343307    16.3 | 85.917 % |
c |     33271 |  128748   265757 |   63133   21004   346278    16.5 | 86.179 % |
c |     33777 |  128578   265357 |   69446   21433   353872    16.5 | 86.286 % |
c |     34536 |  128202   264480 |   76391   21792   361038    16.6 | 86.514 % |
c |     35675 |  128134   264321 |   84030   22856   389135    17.0 | 86.556 % |
c |     37383 |  127761   263442 |   92433   24180   414632    17.1 | 86.794 % |
c |     39945 |  127405   262588 |  101677   26059   521694    20.0 | 87.028 % |
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 |     42503 |  126901   261399 |   42300   27712   620187    22.4 | 87.028 % |
c |     42603 |  126891   261376 |   46530   27801   621343    22.3 | 87.359 % |
c |     42754 |  126891   261376 |   51183   27952   623833    22.3 | 87.359 % |
c |     42979 |  126891   261376 |   56301   28177   638233    22.7 | 87.359 % |
c |     43316 |  126517   260492 |   61931   27389   613090    22.4 | 87.601 % |
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 |     43718 |  126476   260352 |   42158   27643   636763    23.0 | 87.601 % |
c |     43819 |  126412   260201 |   46373   27673   637144    23.0 | 87.657 % |
c |     43970 |  126253   259830 |   51011   27639   638261    23.1 | 87.752 % |
c |     44195 |  126243   259806 |   56112   27815   655208    23.6 | 87.759 % |
c |     44532 |  126243   259806 |   61723   28152   661920    23.5 | 87.759 % |
c |     45039 |  126243   259806 |   67895   28659   687192    24.0 | 87.759 % |
c |     45799 |  126243   259806 |   74685   29419   744415    25.3 | 87.759 % |
c |     46938 |  126243   259806 |   82154   30558   860781    28.2 | 87.759 % |
c |     48646 |  126243   259806 |   90369   32266  1138278    35.3 | 87.759 % |
c |     51209 |  126157   259603 |   99406   34737  1333948    38.4 | 87.811 % |
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 |     53803 |  126237   259806 |   42079   37331  1649243    44.2 | 87.811 % |
c |     53903 |  126237   259806 |   46286   37431  1653748    44.2 | 87.799 % |
c |     54054 |  126237   259806 |   50915   37582  1656549    44.1 | 87.799 % |
c |     54279 |  125822   258832 |   56007   37156  1649077    44.4 | 88.056 % |
c |     54617 |  125822   258832 |   61607   37494  1669870    44.5 | 88.056 % |
c |     55123 |  125560   258209 |   67768   37630  1698515    45.1 | 88.232 % |
c |     55883 |  125542   258166 |   74545   38349  1760168    45.9 | 88.244 % |
c |     57022 |  125538   258157 |   82000   39423  1863092    47.3 | 88.246 % |
c |     58732 |  125538   258157 |   90200   41133  1949443    47.4 | 88.246 % |
c |     61294 |  125347   257711 |   99220   43464  2176804    50.1 | 88.363 % |
c |     65138 |  125347   257711 |  109142   47308  2826950    59.8 | 88.363 % |
c |     70904 |  125347   257711 |  120056   53074  3420870    64.5 | 88.363 % |
c |     79553 |  125299   257599 |  132061   61710  5224483    84.7 | 88.391 % |
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 |     85170 |  125268   257508 |   41756   67096  5994876    89.3 | 88.391 % |
c |     85270 |  125254   257475 |   45931   67188  6000023    89.3 | 88.416 % |
c |     85420 |  125254   257475 |   50524   67338  6004772    89.2 | 88.416 % |
c |     85645 |  125254   257475 |   55577   67563  6024215    89.2 | 88.416 % |
c |     85982 |  125254   257475 |   61134   67900  6051811    89.1 | 88.416 % |
c |     86488 |  125236   257432 |   67248   68288  6103604    89.4 | 88.428 % |
c |     87247 |  125236   257432 |   73973   69047  6158400    89.2 | 88.428 % |
c |     88386 |  125236   257432 |   81370   70186  6324842    90.1 | 88.428 % |
c |     90094 |  125186   257315 |   89507   71707  6516529    90.9 | 88.458 % |
c |     92656 |  124955   256758 |   98458   73419  6724659    91.6 | 88.610 % |
c |     96500 |  124955   256758 |  108304   77263  7197208    93.2 | 88.610 % |
c |    102266 |  124917   256667 |  119134   82540  8090392    98.0 | 88.636 % |
c |    110917 |  124901   256630 |  131048   91183  9503175   104.2 | 88.644 % |
c |    123891 |  124901   256630 |  144153  104157 11683510   112.2 | 88.645 % |
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 |    129439 |  124896   256627 |   41632  109682 12555743   114.5 | 88.645 % |
c |    129539 |  124896   256627 |   45795   24056  2364415    98.3 | 88.659 % |
c |    129690 |  124896   256627 |   50374   24207  2371749    98.0 | 88.659 % |
c |    129915 |  124896   256627 |   55412   24432  2380830    97.4 | 88.659 % |
c |    130252 |  124896   256627 |   60953   24769  2401431    97.0 | 88.659 % |
c |    130758 |  124896   256627 |   67048   25275  2475945    98.0 | 88.659 % |
c |    131517 |  124876   256580 |   73753   26033  2522890    96.9 | 88.672 % |
c |    132657 |  124876   256580 |   81128   27173  2595914    95.5 | 88.672 % |
c |    134367 |  124876   256580 |   89241   28883  2779029    96.2 | 88.672 % |
c |    136929 |  124799   256397 |   98166   31414  3087690    98.3 | 88.724 % |
c |    140773 |  124712   256193 |  107982   35231  3649707   103.6 | 88.778 % |
c |    146539 |  124712   256193 |  118780   40997  4544129   110.8 | 88.778 % |
c |    155189 |  124712   256193 |  130659   49647  6315209   127.2 | 88.778 % |
c |    168164 |  124706   256179 |  143724   62620  8256980   131.9 | 88.781 % |
c |    187626 |  124702   256170 |  158097   82028 12405205   151.2 | 88.783 % |
c |    216818 |  124702   256170 |  173907  111220 18142121   163.1 | 88.783 % |
c |    260608 |  124684   256128 |  191297  155008 27040135   174.4 | 88.794 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1400 -C1399 -C1398 -C1397 -C1396 -C1395 -C1394 -C1393 -C1392 -C1391 -C1390 -C1389 -C1388 -C1387 C1386 -C1385 -C1384 -C1383 -C1382 -C1381 -C1380 -C1379 -C1378 -C1377 -C1376 -C1375 -C1374 -C1373 -C1372 -C1371 -C1370 -C1369 C1368 -C1367 -C1366 -C1365 -C1364 -C1363 -C1362 -C1361 -C1360 -C1359 -C1358 -C1357 -C1356 -C1355 -C1354 -C1353 -C1352 -C1351 -C1350 -C1349 -C1348 -C1347 -C1346 -C1345 -C1344 -C1343 -C1342 -C1341 -C1340 -C1339 -C1338 -C1337 -C1336 -C1335 C1334 -C1333 -C1332 -C1331 -C1330 -C1329 -C1328 -C1327 -C1326 -C1325 -C1324 -C1323 -C1322 -C1321 -C1320 -C1319 -C1318 -C1317 -C1316 -C1315 -C1314 -C1313 -C1312 -C1311 -C1310 -C1309 -C1308 -C1307 -C1306 -C1305 -C1304 -C1303 -C1302 -C1301 -C1300 -C1299 -C1298 -C1297 -C1296 -C1295 -C1294 -C1293 -C1292 -C1291 C1290 -C1289 -C1288 -C1287 -C1286 -C1285 -C1284 -C1283 -C1282 -C1281 -C1280 -C1279 -C1278 -C1277 -C1276 -C1275 -C1274 -C1273 -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 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 -C601 -C600 -C599 C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240 -C239 -C238 -C237 C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 C212 -C211 -C210 -C209 -C208 -C207 -C206 -C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 C160 -C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 -C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 -C106 -C105 -C104 -C103 -C102 -C#### 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.84 0.94 0.90 2/54 4396
Raw data (stat): 4396 (runsolver) R 4395 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423643525 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.0013 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6643 0 0 0 978 21 0 0 25 0 1 0 423643525 30318592 6621 4294967295 134512640 134672761 3221224560 3221223776 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7402 6621 603 41 0 7361 0
vsize: 29608
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6838 0 0 0 1977 21 0 0 25 0 1 0 423643525 31432704 6816 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7674 6816 603 41 0 7633 0
vsize: 30696
[startup+30.0021 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6839 0 0 0 2977 21 0 0 25 0 1 0 423643525 31432704 6817 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6817 603 41 0 7633 0
vsize: 30696
[startup+40.0021 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6839 0 0 0 3976 22 0 0 25 0 1 0 423643525 31432704 6817 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6817 603 41 0 7633 0
vsize: 30696
[startup+50.0015 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6839 0 0 0 4977 22 0 0 25 0 1 0 423643525 31432704 6817 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6817 603 41 0 7633 0
vsize: 30696
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6839 0 0 0 5977 22 0 0 25 0 1 0 423643525 31432704 6817 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6817 603 41 0 7633 0
vsize: 30696
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6839 0 0 0 6977 22 0 0 25 0 1 0 423643525 31432704 6817 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6817 603 41 0 7633 0
vsize: 30696
[startup+80.0018 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6840 0 0 0 7977 22 0 0 25 0 1 0 423643525 31432704 6818 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6818 603 41 0 7633 0
vsize: 30696
[startup+90.0016 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6840 0 0 0 8977 22 0 0 25 0 1 0 423643525 31432704 6818 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6818 603 41 0 7633 0
vsize: 30696
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6840 0 0 0 9976 22 0 0 25 0 1 0 423643525 31432704 6818 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7674 6818 603 41 0 7633 0
vsize: 30696
[startup+110.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6840 0 0 0 10976 22 0 0 25 0 1 0 423643525 31432704 6818 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6818 603 41 0 7633 0
vsize: 30696
[startup+120.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6840 0 0 0 11976 22 0 0 25 0 1 0 423643525 31432704 6818 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6818 603 41 0 7633 0
vsize: 30696
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6841 0 0 0 12976 22 0 0 25 0 1 0 423643525 31432704 6819 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6819 603 41 0 7633 0
vsize: 30696
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6841 0 0 0 13976 22 0 0 25 0 1 0 423643525 31432704 6819 4294967295 134512640 134672761 3221224560 3221223732 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7674 6819 603 41 0 7633 0
vsize: 30696
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 6865 0 0 0 14977 22 0 0 25 0 1 0 423643525 31690752 6843 4294967295 134512640 134672761 3221224560 3221223776 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7737 6843 603 41 0 7696 0
vsize: 30948
[startup+160.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 7026 0 0 0 15976 23 0 0 25 0 1 0 423643525 32092160 6973 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7835 6973 603 41 0 7794 0
vsize: 31340
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 7363 0 0 0 16976 23 0 0 25 0 1 0 423643525 33320960 7278 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8135 7278 603 41 0 8094 0
vsize: 32540
[startup+180.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 7983 0 0 0 17974 25 0 0 25 0 1 0 423643525 35913728 7866 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8768 7866 603 41 0 8727 0
vsize: 35072
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 8536 0 0 0 18972 28 0 0 25 0 1 0 423643525 37953536 8387 4294967295 134512640 134672761 3221224560 3221223728 134561234 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9266 8387 603 41 0 9225 0
vsize: 37064
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 8936 0 0 0 19970 29 0 0 25 0 1 0 423643525 39571456 8787 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9661 8787 603 41 0 9620 0
vsize: 38644
[startup+210.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 9568 0 0 0 20968 32 0 0 25 0 1 0 423643525 42254336 9419 4294967295 134512640 134672761 3221224560 3221223664 134560231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10316 9419 603 41 0 10275 0
vsize: 41264
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 10076 0 0 0 21966 34 0 0 25 0 1 0 423643525 44240896 9927 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10801 9927 603 41 0 10760 0
vsize: 43204
[startup+230.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 10748 0 0 0 22965 36 0 0 25 0 1 0 423643525 47063040 10599 4294967295 134512640 134672761 3221224560 3221223744 134558658 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11490 10599 603 41 0 11449 0
vsize: 45960
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 11594 0 0 0 23963 38 0 0 25 0 1 0 423643525 50409472 11445 4294967295 134512640 134672761 3221224560 3221223664 134555126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12307 11445 603 41 0 12266 0
vsize: 49228
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 12241 0 0 0 24961 40 0 0 25 0 1 0 423643525 53100544 12092 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12964 12092 603 41 0 12923 0
vsize: 51856
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 12718 0 0 0 25960 41 0 0 25 0 1 0 423643525 54984704 12569 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13424 12569 603 41 0 13383 0
vsize: 53696
[startup+270.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 13203 0 0 0 26959 42 0 0 25 0 1 0 423643525 57184256 13022 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13961 13022 603 41 0 13920 0
vsize: 55844
[startup+280.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 13558 0 0 0 27958 43 0 0 25 0 1 0 423643525 58527744 13377 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14289 13377 603 41 0 14248 0
vsize: 57156
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 13915 0 0 0 28957 44 0 0 25 0 1 0 423643525 59998208 13734 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14648 13734 603 41 0 14607 0
vsize: 58592
[startup+300.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 14333 0 0 0 29956 46 0 0 25 0 1 0 423643525 61743104 14152 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15074 14152 603 41 0 15033 0
vsize: 60296
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 14771 0 0 0 30955 47 0 0 25 0 1 0 423643525 63492096 14590 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15501 14590 603 41 0 15460 0
vsize: 62004
[startup+320.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 15292 0 0 0 31954 48 0 0 25 0 1 0 423643525 65634304 15111 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16024 15111 603 41 0 15983 0
vsize: 64096
[startup+330.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 15704 0 0 0 32953 49 0 0 25 0 1 0 423643525 67366912 15523 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16447 15523 603 41 0 16406 0
vsize: 65788
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 16101 0 0 0 33952 50 0 0 25 0 1 0 423643525 68968448 15920 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16838 15920 603 41 0 16797 0
vsize: 67352
[startup+350.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 16599 0 0 0 34950 52 0 0 25 0 1 0 423643525 70979584 16418 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17329 16418 603 41 0 17288 0
vsize: 69316
[startup+360.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 17039 0 0 0 35949 54 0 0 25 0 1 0 423643525 72728576 16858 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17756 16858 603 41 0 17715 0
vsize: 71024
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4396
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 17405 0 0 0 36949 54 0 0 25 0 1 0 423643525 74199040 17224 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18115 17224 603 41 0 18074 0
vsize: 72460
[startup+380.124 s]
Raw data (loadavg): 1.07 0.99 0.91 3/57 4434
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 17948 0 0 0 37953 62 0 0 25 0 1 0 423643525 76472320 17767 4294967295 134512640 134672761 3221224560 3221223664 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18670 17767 603 41 0 18629 0
vsize: 74680
[startup+390.124 s]
Raw data (loadavg): 1.14 1.00 0.92 3/56 4443
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 18434 0 0 0 38952 63 0 0 25 0 1 0 423643525 78491648 18253 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19163 18253 603 41 0 19122 0
vsize: 76652
[startup+400.124 s]
Raw data (loadavg): 1.19 1.02 0.93 2/54 4449
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 18871 0 0 0 39951 64 0 0 25 0 1 0 423643525 80236544 18690 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19589 18690 603 41 0 19548 0
vsize: 78356
[startup+410.124 s]
Raw data (loadavg): 1.16 1.02 0.93 2/54 4449
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 19294 0 0 0 40950 66 0 0 25 0 1 0 423643525 81981440 19113 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20015 19113 603 41 0 19974 0
vsize: 80060
[startup+420.124 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 4449
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 19723 0 0 0 41949 67 0 0 25 0 1 0 423643525 83722240 19542 4294967295 134512640 134672761 3221224560 3221223664 134560059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20440 19542 603 41 0 20399 0
vsize: 81760
[startup+430.125 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 4449
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20080 0 0 0 42949 67 0 0 25 0 1 0 423643525 85204992 19899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20802 19899 603 41 0 20761 0
vsize: 83208
[startup+440.124 s]
Raw data (loadavg): 1.10 1.02 0.93 2/54 4449
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 43948 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+450.124 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 4449
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 44948 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+460.124 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 4449
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 45949 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+470.124 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 46949 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+480.123 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 47949 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+490.123 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 48949 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+500.123 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 49949 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+510.123 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 50949 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223664 134560399 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+520.122 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 51949 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+530.122 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 52950 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+540.122 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 53950 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+550.122 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 54950 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+560.122 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 55950 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223696 134560634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+570.122 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 56950 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+580.122 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 57950 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+590.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 58950 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+600.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 59951 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+610.123 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20199 0 0 0 60951 68 0 0 25 0 1 0 423643525 85434368 19987 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20858 19987 603 41 0 20817 0
vsize: 83432
[startup+620.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20371 0 0 0 61950 68 0 0 25 0 1 0 423643525 86233088 20159 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21053 20159 603 41 0 21012 0
vsize: 84212
[startup+630.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 20718 0 0 0 62950 69 0 0 25 0 1 0 423643525 87695360 20506 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21410 20506 603 41 0 21369 0
vsize: 85640
[startup+640.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 21094 0 0 0 63949 70 0 0 25 0 1 0 423643525 89169920 20882 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21770 20882 603 41 0 21729 0
vsize: 87080
[startup+650.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 21485 0 0 0 64948 71 0 0 25 0 1 0 423643525 90787840 21273 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22165 21273 603 41 0 22124 0
vsize: 88660
[startup+660.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 21973 0 0 0 65947 73 0 0 25 0 1 0 423643525 92794880 21761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22655 21761 603 41 0 22614 0
vsize: 90620
[startup+670.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 22482 0 0 0 66946 74 0 0 25 0 1 0 423643525 94801920 22270 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23145 22270 603 41 0 23104 0
vsize: 92580
[startup+680.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 23036 0 0 0 67945 75 0 0 25 0 1 0 423643525 97075200 22824 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23700 22824 603 41 0 23659 0
vsize: 94800
[startup+690.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4451
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 23556 0 0 0 68944 76 0 0 25 0 1 0 423643525 99221504 23344 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23344 603 41 0 24183 0
vsize: 96896
[startup+700.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 24038 0 0 0 69943 77 0 0 25 0 1 0 423643525 101232640 23826 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24715 23826 603 41 0 24674 0
vsize: 98860
[startup+710.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 24542 0 0 0 70942 78 0 0 25 0 1 0 423643525 103239680 24330 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25205 24330 603 41 0 25164 0
vsize: 100820
[startup+720.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 24936 0 0 0 71941 79 0 0 25 0 1 0 423643525 104853504 24724 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25599 24724 603 41 0 25558 0
vsize: 102396
[startup+730.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 25377 0 0 0 72940 80 0 0 25 0 1 0 423643525 106729472 25165 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26057 25165 603 41 0 26016 0
vsize: 104228
[startup+740.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 25713 0 0 0 73940 81 0 0 25 0 1 0 423643525 108077056 25501 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26386 25501 603 41 0 26345 0
vsize: 105544
[startup+750.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 26069 0 0 0 74939 82 0 0 25 0 1 0 423643525 109547520 25857 4294967295 134512640 134672761 3221224560 3221223708 1074754709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26745 25857 603 41 0 26704 0
vsize: 106980
[startup+760.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 26328 0 0 0 75938 83 0 0 25 0 1 0 423643525 110624768 26116 4294967295 134512640 134672761 3221224560 3221223696 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27008 26116 603 41 0 26967 0
vsize: 108032
[startup+770.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 26643 0 0 0 76937 85 0 0 25 0 1 0 423643525 111947776 26431 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27331 26431 603 41 0 27290 0
vsize: 109324
[startup+780.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 26889 0 0 0 77936 85 0 0 25 0 1 0 423643525 112877568 26677 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27558 26677 603 41 0 27517 0
vsize: 110232
[startup+790.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 27252 0 0 0 78936 86 0 0 25 0 1 0 423643525 114343936 27040 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27916 27040 603 41 0 27875 0
vsize: 111664
[startup+800.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 27685 0 0 0 79935 86 0 0 25 0 1 0 423643525 116084736 27473 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28341 27473 603 41 0 28300 0
vsize: 113364
[startup+810.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 28113 0 0 0 80935 87 0 0 25 0 1 0 423643525 117813248 27901 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28763 27901 603 41 0 28722 0
vsize: 115052
[startup+820.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 28498 0 0 0 81934 88 0 0 25 0 1 0 423643525 119427072 28286 4294967295 134512640 134672761 3221224560 3221223696 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29157 28286 603 41 0 29116 0
vsize: 116628
[startup+830.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 28824 0 0 0 82933 89 0 0 25 0 1 0 423643525 120754176 28612 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29481 28612 603 41 0 29440 0
vsize: 117924
[startup+840.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 29127 0 0 0 83933 89 0 0 25 0 1 0 423643525 121950208 28915 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29773 28915 603 41 0 29732 0
vsize: 119092
[startup+850.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 29372 0 0 0 84932 90 0 0 25 0 1 0 423643525 123019264 29160 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30034 29160 603 41 0 29993 0
vsize: 120136
[startup+860.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 29731 0 0 0 85932 91 0 0 25 0 1 0 423643525 125014016 29519 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30521 29519 603 41 0 30480 0
vsize: 122084
[startup+870.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 30189 0 0 0 86931 92 0 0 25 0 1 0 423643525 126881792 29977 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30977 29977 603 41 0 30936 0
vsize: 123908
[startup+880.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 30631 0 0 0 87930 93 0 0 25 0 1 0 423643525 128626688 30419 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31403 30419 603 41 0 31362 0
vsize: 125612
[startup+890.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 31041 0 0 0 88929 94 0 0 25 0 1 0 423643525 130363392 30829 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31827 30829 603 41 0 31786 0
vsize: 127308
[startup+900.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 31487 0 0 0 89928 95 0 0 25 0 1 0 423643525 132214784 31275 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32279 31275 603 41 0 32238 0
vsize: 129116
[startup+910.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 31951 0 0 0 90928 96 0 0 25 0 1 0 423643525 134090752 31739 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32737 31740 603 41 0 32696 0
vsize: 130948
[startup+920.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 32412 0 0 0 91927 97 0 0 25 0 1 0 423643525 135958528 32200 4294967295 134512640 134672761 3221224560 3221223744 134558885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33193 32200 603 41 0 33152 0
vsize: 132772
[startup+930.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 32838 0 0 0 92925 98 0 0 25 0 1 0 423643525 137691136 32626 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33616 32626 603 41 0 33575 0
vsize: 134464
[startup+940.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 33284 0 0 0 93924 100 0 0 25 0 1 0 423643525 139563008 33072 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34073 33072 603 41 0 34032 0
vsize: 136292
[startup+950.121 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 33623 0 0 0 94924 100 0 0 25 0 1 0 423643525 140902400 33411 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34400 33411 603 41 0 34359 0
vsize: 137600
[startup+960.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 33976 0 0 0 95923 101 0 0 25 0 1 0 423643525 142385152 33764 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34762 33764 603 41 0 34721 0
vsize: 139048
[startup+970.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 34302 0 0 0 96923 101 0 0 25 0 1 0 423643525 143589376 34090 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35056 34090 603 41 0 35015 0
vsize: 140224
[startup+980.122 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 34652 0 0 0 97923 102 0 0 25 0 1 0 423643525 145072128 34440 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35418 34440 603 41 0 35377 0
vsize: 141672
[startup+990.123 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 35000 0 0 0 98922 103 0 0 25 0 1 0 423643525 146530304 34788 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35774 34788 603 41 0 35733 0
vsize: 143096
[startup+1000.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 35338 0 0 0 99921 104 0 0 25 0 1 0 423643525 147877888 35126 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36103 35126 603 41 0 36062 0
vsize: 144412
[startup+1010.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 35668 0 0 0 100920 105 0 0 25 0 1 0 423643525 149229568 35456 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36433 35456 603 41 0 36392 0
vsize: 145732
[startup+1020.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 36025 0 0 0 101919 106 0 0 25 0 1 0 423643525 150700032 35813 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36792 35813 603 41 0 36751 0
vsize: 147168
[startup+1030.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 36370 0 0 0 102918 107 0 0 25 0 1 0 423643525 152039424 36158 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37119 36158 603 41 0 37078 0
vsize: 148476
[startup+1040.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 36642 0 0 0 103918 108 0 0 25 0 1 0 423643525 153235456 36430 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37411 36430 603 41 0 37370 0
vsize: 149644
[startup+1050.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 36852 0 0 0 104917 108 0 0 25 0 1 0 423643525 154042368 36640 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37608 36640 603 41 0 37567 0
vsize: 150432
[startup+1060.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 37150 0 0 0 105916 109 0 0 25 0 1 0 423643525 155246592 36938 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37902 36938 603 41 0 37861 0
vsize: 151608
[startup+1070.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 37449 0 0 0 106916 110 0 0 25 0 1 0 423643525 156450816 37237 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38196 37237 603 41 0 38155 0
vsize: 152784
[startup+1080.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 37759 0 0 0 107915 111 0 0 25 0 1 0 423643525 157777920 37547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38520 37547 603 41 0 38479 0
vsize: 154080
[startup+1090.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 38017 0 0 0 108914 112 0 0 25 0 1 0 423643525 158842880 37805 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38780 37805 603 41 0 38739 0
vsize: 155120
[startup+1100.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 38220 0 0 0 109914 112 0 0 25 0 1 0 423643525 159662080 38008 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38980 38008 603 41 0 38939 0
vsize: 155920
[startup+1110.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 38479 0 0 0 110914 113 0 0 25 0 1 0 423643525 160735232 38267 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39242 38267 603 41 0 39201 0
vsize: 156968
[startup+1120.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 38807 0 0 0 111913 114 0 0 25 0 1 0 423643525 162074624 38595 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39569 38595 603 41 0 39528 0
vsize: 158276
[startup+1130.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 39098 0 0 0 112913 115 0 0 25 0 1 0 423643525 163278848 38886 4294967295 134512640 134672761 3221224560 3221223664 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39863 38886 603 41 0 39822 0
vsize: 159452
[startup+1140.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 39468 0 0 0 113911 116 0 0 25 0 1 0 423643525 164757504 39256 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40224 39256 603 41 0 40183 0
vsize: 160896
[startup+1150.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 39780 0 0 0 114911 117 0 0 25 0 1 0 423643525 165965824 39568 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40519 39568 603 41 0 40478 0
vsize: 162076
[startup+1160.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 40039 0 0 0 115910 117 0 0 25 0 1 0 423643525 167055360 39827 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40785 39827 603 41 0 40744 0
vsize: 163140
[startup+1170.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 40325 0 0 0 116910 118 0 0 25 0 1 0 423643525 168267776 40113 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41081 40113 603 41 0 41040 0
vsize: 164324
[startup+1180.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 40591 0 0 0 117910 118 0 0 25 0 1 0 423643525 169332736 40379 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41341 40379 603 41 0 41300 0
vsize: 165364
[startup+1190.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 40892 0 0 0 118909 119 0 0 25 0 1 0 423643525 170532864 40680 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41634 40680 603 41 0 41593 0
vsize: 166536
[startup+1200.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4453
Raw data (stat): 4396 (minisat+) R 4395 30854 30853 0 -1 0 41185 0 0 0 119908 120 0 0 25 0 1 0 423643525 171724800 40973 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41925 40973 603 41 0 41884 0
vsize: 167700
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.21 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 4453
Raw data (stat): 4396 (minisat+) Z 4395 30854 30853 0 -1 12 41188 0 0 0 119908 128 0 0 25 0 1 0 423643525 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.21
CPU time (s): 1200.37
CPU user time (s): 1199.09
CPU system time (s): 1.2828
CPU usage (%): 100.014
Max. virtual memory (Kb): 167700
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####