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/frb59-26-opb/normalized-frb59-26-2.opb
MD5SUM5b8ef604a7452dcb7c7d749b75aed566
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -45
Optimality of the best value was proved NO
Number of terms in the objective function 1534
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 1534
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 1534
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.15
Number of variables1534
Total number of constraints126163
Number of constraints which are clauses126163
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 6025

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-14 03:06:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4486 boxname=wulflinc12 idbench=350 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  5b8ef604a7452dcb7c7d749b75aed566  /oldhome/oroussel/tmp/wulflinc12/normalized-frb59-26-2.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc12/normalized-frb59-26-2.opb /oldhome/oroussel/tmp/wulflinc12/normalized-frb59-26-2.opb
IDLAUNCH: 4486
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        898428 kB
Buffers:         35856 kB
Cached:          80544 kB
SwapCached:         16 kB
Active:          64548 kB
Inactive:        54704 kB
HighTotal:      131008 kB
HighFree:        46564 kB
LowTotal:       903652 kB
LowFree:        851864 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11448 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:26:12 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 4486 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 126163 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 |  126163   252326 |   42054       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -42
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:85954     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  216902   465187 |   72300       0        0     nan |  0.000 % |
c |       100 |  216378   464089 |   79530      71     1045    14.7 |  0.476 % |
c |       250 |  215666   462590 |   87483     197     2307    11.7 |  1.110 % |
c |       475 |  214693   460491 |   96231     382     4569    12.0 |  2.022 % |
c |       812 |  212890   456566 |  105854     654     7279    11.1 |  3.734 % |
c |      1318 |  210422   451160 |  116439    1060    10851    10.2 |  6.157 % |
c |      2077 |  206393   442217 |  128083    1635    16954    10.4 | 10.063 % |
c |      3216 |  198975   425552 |  140892    2422    25813    10.7 | 17.559 % |
c |      4924 |  190640   406622 |  154981    3664    40208    11.0 | 26.087 % |
c |      7486 |  179470   381025 |  170479    5477    62777    11.5 | 37.698 % |
c |     11330 |  166692   351158 |  187527    8259    96088    11.6 | 51.142 % |
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 |     14201 |  159762   334804 |   53254   10383   124904    12.0 | 51.142 % |
c |     14301 |  159518   334234 |   58579   10463   126556    12.1 | 59.111 % |
c |     14451 |  159171   333401 |   64437   10595   128502    12.1 | 59.497 % |
c |     14676 |  158480   331759 |   70881   10678   129458    12.1 | 60.258 % |
c |     15013 |  158174   331032 |   77969   10915   133832    12.3 | 60.595 % |
c |     15520 |  157341   329073 |   85766   11321   139331    12.3 | 61.505 % |
c |     16280 |  155349   324351 |   94342   11703   145801    12.5 | 63.687 % |
c |     17419 |  153760   320544 |  103776   12549   161675    12.9 | 65.453 % |
c |     19127 |  152453   317467 |  114154   13881   182702    13.2 | 66.863 % |
c |     21689 |  148743   308640 |  125570   15567   217965    14.0 | 70.881 % |
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 |     24382 |  145456   300817 |   48485   17375   249367    14.4 | 70.881 % |
c |     24483 |  145363   300588 |   53333   17440   251246    14.4 | 74.648 % |
c |     24633 |  145288   300407 |   58666   17551   251739    14.3 | 74.732 % |
c |     24858 |  144991   299696 |   64533   17581   253807    14.4 | 75.065 % |
c |     25195 |  144671   298897 |   70986   17767   260713    14.7 | 75.446 % |
c |     25702 |  144071   297413 |   78085   18002   268321    14.9 | 76.147 % |
c |     26461 |  143083   295047 |   85894   18367   278416    15.2 | 77.238 % |
c |     27600 |  142217   292945 |   94483   19129   300433    15.7 | 78.224 % |
c |     29308 |  141140   290360 |  103931   20436   345754    16.9 | 79.432 % |
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 |     30862 |  140267   288181 |   46755   21633   397822    18.4 | 79.432 % |
c |     30963 |  140267   288181 |   51430   21734   399242    18.4 | 80.416 % |
c |     31114 |  140168   287935 |   56573   21806   400090    18.3 | 80.529 % |
c |     31339 |  140168   287935 |   62230   22031   412550    18.7 | 80.529 % |
c |     31676 |  140023   287590 |   68453   22256   418337    18.8 | 80.689 % |
c |     32183 |  140023   287590 |   75299   22763   438437    19.3 | 80.689 % |
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 |     32937 |  140085   287791 |   46695   23512   471006    20.0 | 80.689 % |
c |     33037 |  140085   287791 |   51364   23612   474023    20.1 | 80.668 % |
c |     33188 |  139985   287565 |   56500   23703   476332    20.1 | 80.768 % |
c |     33413 |  139925   287414 |   62151   23901   482389    20.2 | 80.840 % |
c |     33750 |  139819   287160 |   68366   24223   491372    20.3 | 80.958 % |
c |     34257 |  139501   286378 |   75202   24523   504115    20.6 | 81.320 % |
c |     35016 |  139221   285698 |   82723   25080   519407    20.7 | 81.634 % |
c |     36155 |  138949   285015 |   90995   26080   578152    22.2 | 81.958 % |
c |     37863 |  138937   284987 |  100094   27753   670991    24.2 | 81.971 % |
c |     40425 |  138358   283576 |  110104   29587   808674    27.3 | 82.622 % |
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 |     41630 |  138147   283085 |   46049   30685   883161    28.8 | 82.622 % |
c |     41730 |  138092   282958 |   50653   30763   884351    28.7 | 82.933 % |
c |     41880 |  137941   282583 |   55719   30835   887360    28.8 | 83.109 % |
c |     42105 |  137901   282493 |   61291   31052   893326    28.8 | 83.149 % |
c |     42442 |  137895   282479 |   67420   31375   909461    29.0 | 83.155 % |
c |     42948 |  137873   282425 |   74162   31874   947781    29.7 | 83.181 % |
c |     43707 |  137873   282425 |   81578   32633   990787    30.4 | 83.181 % |
c |     44846 |  137866   282408 |   89736   33764  1042346    30.9 | 83.189 % |
c |     46554 |  137539   281618 |   98710   35123  1108640    31.6 | 83.556 % |
c |     49116 |  137311   281072 |  108581   37144  1292520    34.8 | 83.810 % |
c |     52960 |  137157   280708 |  119439   40856  1598714    39.1 | 83.978 % |
c |     58727 |  136513   279109 |  131383   45613  1978665    43.4 | 84.730 % |
c ==============================================================================
c Found solution: -50
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 |     64383 |  136428   278853 |   45476   50690  2426715    47.9 | 84.730 % |
c |     64483 |  136372   278721 |   50023   50704  2426821    47.9 | 84.888 % |
c |     64633 |  136372   278721 |   55025   50854  2434364    47.9 | 84.888 % |
c |     64858 |  136372   278721 |   60528   51079  2451936    48.0 | 84.888 % |
c |     65195 |  136354   278679 |   66581   51330  2465308    48.0 | 84.907 % |
c |     65701 |  136354   278679 |   73239   51836  2497084    48.2 | 84.907 % |
c |     66460 |  136315   278575 |   80563   52539  2537278    48.3 | 84.952 % |
c |     67599 |  136315   278575 |   88619   53678  2687895    50.1 | 84.952 % |
c |     69307 |  136315   278575 |   97481   55386  2882870    52.1 | 84.952 % |
c |     71869 |  136315   278575 |  107230   57948  3297295    56.9 | 84.952 % |
c ==============================================================================
c Found solution: -51
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 |     74103 |  136106   278085 |   45368   59809  3485256    58.3 | 84.952 % |
c |     74203 |  136106   278085 |   49904   59909  3491775    58.3 | 85.223 % |
c |     74353 |  136063   277970 |   54895   59670  3485850    58.4 | 85.278 % |
c |     74578 |  136063   277970 |   60384   59895  3498842    58.4 | 85.278 % |
c |     74916 |  136058   277957 |   66423   60226  3530651    58.6 | 85.284 % |
c |     75422 |  135994   277802 |   73065   60597  3563296    58.8 | 85.355 % |
c |     76181 |  135950   277698 |   80372   61179  3620235    59.2 | 85.403 % |
c |     77320 |  135945   277687 |   88409   62293  3702636    59.4 | 85.408 % |
c |     79028 |  135928   277644 |   97250   63981  3892624    60.8 | 85.429 % |
c |     81590 |  135691   277063 |  106975   65768  4131868    62.8 | 85.702 % |
c |     85436 |  135590   276824 |  117672   69157  4565212    66.0 | 85.813 % |
c |     91202 |  135583   276807 |  129440   74866  5415516    72.3 | 85.821 % |
c |     99851 |  135540   276704 |  142384   83045  6414369    77.2 | 85.869 % |
c |    112826 |  135455   276509 |  156622   95875  8314958    86.7 | 85.957 % |
c ==============================================================================
c Found solution: -52
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 |    127962 |  135394   276336 |   45131  109446 11574582   105.8 | 85.957 % |
c |    128062 |  135394   276336 |   49644   22310  3255192   145.9 | 86.028 % |
c |    128212 |  135295   276100 |   54608   22395  3259721   145.6 | 86.136 % |
c |    128437 |  135290   276089 |   60069   22610  3275212   144.9 | 86.141 % |
c |    128775 |  135238   275955 |   66076   22938  3289266   143.4 | 86.207 % |
c |    129281 |  135204   275877 |   72683   23429  3310280   141.3 | 86.242 % |
c |    130040 |  135194   275853 |   79952   24166  3344207   138.4 | 86.253 % |
c |    131179 |  135186   275835 |   87947   25295  3433065   135.7 | 86.261 % |
c |    132888 |  135178   275815 |   96742   26972  3689589   136.8 | 86.271 % |
c |    135450 |  135123   275675 |  106416   29433  4012571   136.3 | 86.338 % |
c |    139294 |  135123   275675 |  117058   33277  4564286   137.2 | 86.338 % |
c |    145060 |  134993   275371 |  128764   38714  5165896   133.4 | 86.475 % |
c |    153709 |  134993   275371 |  141640   47363  7432043   156.9 | 86.475 % |
c |    166684 |  134984   275352 |  155804   60336  9779793   162.1 | 86.483 % |
c |    186146 |  134984   275352 |  171384   79798 13225885   165.7 | 86.483 % |
c |    215338 |  134936   275238 |  188523  108912 18650008   171.2 | 86.536 % |
c |    259127 |  134911   275179 |  207375  152675 26672713   174.7 | 86.563 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1534 -C1533 -C1532 -C1531 -C1530 -C1529 -C1528 -C1527 -C1526 C1525 -C1524 -C1523 -C1522 -C1521 -C1520 -C1519 -C1518 -C1517 -C1516 -C1515 -C1514 -C1513 -C1512 -C1511 -C1510 -C1509 -C1508 -C1507 -C1506 -C1505 -C1504 -C1503 -C1502 -C1501 -C1500 -C1499 -C1498 -C1497 -C1496 -C1495 -C1494 -C1493 -C1492 -C1491 -C1490 C1489 -C1488 -C1487 -C1486 -C1485 -C1484 -C1483 -C1482 -C1481 -C1480 -C1479 -C1478 -C1477 -C1476 -C1475 -C1474 -C1473 -C1472 -C1471 -C1470 -C1469 -C1468 -C1467 -C1466 -C1465 -C1464 -C1463 -C1462 -C1461 -C1460 -C1459 -C1458 -C1457 -C1456 -C1455 -C1454 -C1453 -C1452 -C1451 -C1450 -C1449 C1448 -C1447 -C1446 -C1445 -C1444 -C1443 -C1442 -C1441 -C1440 -C1439 -C1438 -C1437 -C1436 -C1435 -C1434 -C1433 -C1432 -C1431 -C1430 -C1429 -C1428 -C1427 -C1426 -C1425 -C1424 -C1423 -C1422 C1421 -C1420 -C1419 -C1418 -C1417 -C1416 -C1415 -C1414 -C1413 -C1412 -C1411 -C1410 -C1409 -C1408 -C1407 -C1406 -C1405 -C1404 -C1403 -C1402 -C1401 -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 -C25#### 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.93 0.98 0.94 1/54 30857
Raw data (stat): 30857 (runsolver) D 30856 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 422994332 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 3225161850 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.94 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 6901 0 0 0 976 19 0 0 25 0 1 0 422994332 30392320 6879 4294967295 134512640 134672761 3221224560 3221223760 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7420 6879 603 41 0 7379 0
vsize: 29680
[startup+20.0013 s]
Raw data (loadavg): 0.95 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 6907 0 0 0 1975 19 0 0 25 0 1 0 422994332 30392320 6885 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7420 6885 603 41 0 7379 0
vsize: 29680
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 6913 0 0 0 2976 19 0 0 25 0 1 0 422994332 30392320 6891 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7420 6891 603 41 0 7379 0
vsize: 29680
[startup+40.0026 s]
Raw data (loadavg): 0.96 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 6919 0 0 0 3975 19 0 0 25 0 1 0 422994332 30392320 6897 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7420 6897 603 41 0 7379 0
vsize: 29680
[startup+50.0029 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 6924 0 0 0 4975 19 0 0 25 0 1 0 422994332 30392320 6902 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7420 6902 603 41 0 7379 0
vsize: 29680
[startup+60.0027 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 6929 0 0 0 5975 19 0 0 25 0 1 0 422994332 30392320 6907 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7420 6907 603 41 0 7379 0
vsize: 29680
[startup+70.0031 s]
Raw data (loadavg): 0.97 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 6934 0 0 0 6975 19 0 0 25 0 1 0 422994332 30527488 6912 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7453 6912 603 41 0 7412 0
vsize: 29812
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 6945 0 0 0 7975 19 0 0 25 0 1 0 422994332 30527488 6923 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7453 6923 603 41 0 7412 0
vsize: 29812
[startup+90.0041 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 6952 0 0 0 8975 19 0 0 25 0 1 0 422994332 30527488 6930 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7453 6930 603 41 0 7412 0
vsize: 29812
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 6956 0 0 0 9975 19 0 0 25 0 1 0 422994332 30527488 6934 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7453 6934 603 41 0 7412 0
vsize: 29812
[startup+110.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 6967 0 0 0 10976 19 0 0 25 0 1 0 422994332 30662656 6945 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7486 6945 603 41 0 7445 0
vsize: 29944
[startup+120.005 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 6982 0 0 0 11976 19 0 0 25 0 1 0 422994332 30662656 6960 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7486 6960 603 41 0 7445 0
vsize: 29944
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 7163 0 0 0 12976 20 0 0 25 0 1 0 422994332 31870976 7141 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7781 7141 603 41 0 7740 0
vsize: 31124
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 7165 0 0 0 13976 20 0 0 25 0 1 0 422994332 31870976 7143 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7781 7143 603 41 0 7740 0
vsize: 31124
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 7166 0 0 0 14975 20 0 0 25 0 1 0 422994332 31870976 7144 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7781 7144 603 41 0 7740 0
vsize: 31124
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 7169 0 0 0 15975 20 0 0 25 0 1 0 422994332 31870976 7147 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7781 7147 603 41 0 7740 0
vsize: 31124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 7221 0 0 0 16974 20 0 0 25 0 1 0 422994332 32133120 7199 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7845 7199 603 41 0 7804 0
vsize: 31380
[startup+180.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 7281 0 0 0 17974 21 0 0 25 0 1 0 422994332 32403456 7259 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7911 7259 603 41 0 7870 0
vsize: 31644
[startup+190.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 7480 0 0 0 18974 22 0 0 25 0 1 0 422994332 33169408 7458 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8098 7458 603 41 0 8057 0
vsize: 32392
[startup+200.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 7709 0 0 0 19973 22 0 0 25 0 1 0 422994332 34099200 7687 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8325 7687 603 41 0 8284 0
vsize: 33300
[startup+210.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 8035 0 0 0 20972 24 0 0 25 0 1 0 422994332 35467264 8013 4294967295 134512640 134672761 3221224560 3221223696 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8659 8013 603 41 0 8618 0
vsize: 34636
[startup+220.007 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 8308 0 0 0 21971 25 0 0 25 0 1 0 422994332 36675584 8286 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8954 8286 603 41 0 8913 0
vsize: 35816
[startup+230.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 8734 0 0 0 22969 27 0 0 25 0 1 0 422994332 38428672 8712 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9382 8712 603 41 0 9341 0
vsize: 37528
[startup+240.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 9102 0 0 0 23968 28 0 0 25 0 1 0 422994332 39907328 9080 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9743 9080 603 41 0 9702 0
vsize: 38972
[startup+250.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 9507 0 0 0 24967 29 0 0 25 0 1 0 422994332 41517056 9485 4294967295 134512640 134672761 3221224560 3221223744 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10136 9485 603 41 0 10095 0
vsize: 40544
[startup+260.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 9787 0 0 0 25967 30 0 0 25 0 1 0 422994332 42708992 9765 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10427 9765 603 41 0 10386 0
vsize: 41708
[startup+270.008 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 10331 0 0 0 26965 31 0 0 25 0 1 0 422994332 44867584 10309 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10954 10309 603 41 0 10913 0
vsize: 43816
[startup+280.009 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 10693 0 0 0 27964 33 0 0 25 0 1 0 422994332 46350336 10671 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11316 10671 603 41 0 11275 0
vsize: 45264
[startup+290.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 10963 0 0 0 28964 34 0 0 25 0 1 0 422994332 47415296 10941 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11576 10941 603 41 0 11535 0
vsize: 46304
[startup+300.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 11281 0 0 0 29962 35 0 0 25 0 1 0 422994332 48762880 11259 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11905 11259 603 41 0 11864 0
vsize: 47620
[startup+310.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 11599 0 0 0 30961 36 0 0 25 0 1 0 422994332 50364416 11577 4294967295 134512640 134672761 3221224560 3221223712 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12296 11577 603 41 0 12255 0
vsize: 49184
[startup+320.01 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 12003 0 0 0 31960 38 0 0 25 0 1 0 422994332 51982336 11981 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12691 11981 603 41 0 12650 0
vsize: 50764
[startup+330.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 12438 0 0 0 32959 39 0 0 25 0 1 0 422994332 53710848 12416 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13113 12416 603 41 0 13072 0
vsize: 52452
[startup+340.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 12952 0 0 0 33957 41 0 0 25 0 1 0 422994332 55865344 12930 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13639 12930 603 41 0 13598 0
vsize: 54556
[startup+350.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 13351 0 0 0 34955 43 0 0 25 0 1 0 422994332 57487360 13329 4294967295 134512640 134672761 3221224560 3221223616 134565096 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14035 13329 603 41 0 13994 0
vsize: 56140
[startup+360.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 13657 0 0 0 35954 44 0 0 25 0 1 0 422994332 58695680 13635 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14330 13635 603 41 0 14289 0
vsize: 57320
[startup+370.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 14047 0 0 0 36953 46 0 0 25 0 1 0 422994332 60305408 14025 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14723 14025 603 41 0 14682 0
vsize: 58892
[startup+380.011 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 14518 0 0 0 37951 48 0 0 25 0 1 0 422994332 62177280 14496 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15180 14496 603 41 0 15139 0
vsize: 60720
[startup+390.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 14793 0 0 0 38950 49 0 0 25 0 1 0 422994332 63254528 14771 4294967295 134512640 134672761 3221224560 3221223760 134557919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15443 14771 603 41 0 15402 0
vsize: 61772
[startup+400.012 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 15183 0 0 0 39949 50 0 0 25 0 1 0 422994332 64860160 15161 4294967295 134512640 134672761 3221224560 3221223664 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15835 15161 603 41 0 15794 0
vsize: 63340
[startup+410.013 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 15665 0 0 0 40948 51 0 0 25 0 1 0 422994332 66867200 15643 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16325 15643 603 41 0 16284 0
vsize: 65300
[startup+420.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 16029 0 0 0 41948 52 0 0 25 0 1 0 422994332 68329472 16007 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16682 16007 603 41 0 16641 0
vsize: 66728
[startup+430.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 16434 0 0 0 42947 53 0 0 25 0 1 0 422994332 69939200 16412 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17075 16412 603 41 0 17034 0
vsize: 68300
[startup+440.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 16888 0 0 0 43946 54 0 0 25 0 1 0 422994332 71819264 16866 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17534 16866 603 41 0 17493 0
vsize: 70136
[startup+450.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 17432 0 0 0 44945 55 0 0 25 0 1 0 422994332 74084352 17410 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18087 17410 603 41 0 18046 0
vsize: 72348
[startup+460.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 17939 0 0 0 45943 57 0 0 25 0 1 0 422994332 76099584 17917 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18579 17917 603 41 0 18538 0
vsize: 74316
[startup+470.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 18455 0 0 0 46942 58 0 0 25 0 1 0 422994332 78221312 18433 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19097 18433 603 41 0 19056 0
vsize: 76388
[startup+480.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19024 0 0 0 47941 60 0 0 25 0 1 0 422994332 80625664 19002 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19684 19002 603 41 0 19643 0
vsize: 78736
[startup+490.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19501 0 0 0 48940 61 0 0 25 0 1 0 422994332 82485248 19479 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20138 19479 603 41 0 20097 0
vsize: 80552
[startup+500.014 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 49939 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223748 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+510.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 50939 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+520.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 51940 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+530.015 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 52940 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+540.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 53940 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+550.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 54940 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+560.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 55940 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223744 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+570.016 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 56941 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+580.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 57941 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+590.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 58941 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+600.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 59941 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+610.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 60941 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+620.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 61941 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+630.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 62941 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+640.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 63942 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+650.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 64942 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+660.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 19717 0 0 0 65942 62 0 0 25 0 1 0 422994332 83341312 19695 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20347 19695 603 41 0 20306 0
vsize: 81388
[startup+670.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 20101 0 0 0 66941 63 0 0 25 0 1 0 422994332 84955136 20079 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20741 20079 603 41 0 20700 0
vsize: 82964
[startup+680.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 20510 0 0 0 67940 64 0 0 25 0 1 0 422994332 86704128 20488 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21168 20488 603 41 0 21127 0
vsize: 84672
[startup+690.017 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 21012 0 0 0 68938 66 0 0 25 0 1 0 422994332 88715264 20990 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21659 20990 603 41 0 21618 0
vsize: 86636
[startup+700.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 21422 0 0 0 69937 68 0 0 25 0 1 0 422994332 90324992 21400 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22052 21400 603 41 0 22011 0
vsize: 88208
[startup+710.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 21821 0 0 0 70936 69 0 0 25 0 1 0 422994332 92053504 21799 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22474 21799 603 41 0 22433 0
vsize: 89896
[startup+720.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 22229 0 0 0 71935 70 0 0 25 0 1 0 422994332 93655040 22207 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22865 22207 603 41 0 22824 0
vsize: 91460
[startup+730.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 22682 0 0 0 72934 71 0 0 25 0 1 0 422994332 95531008 22660 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23323 22660 603 41 0 23282 0
vsize: 93292
[startup+740.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 23140 0 0 0 73933 72 0 0 25 0 1 0 422994332 97411072 23118 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23782 23118 603 41 0 23741 0
vsize: 95128
[startup+750.018 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 23490 0 0 0 74933 73 0 0 25 0 1 0 422994332 98885632 23468 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24142 23468 603 41 0 24101 0
vsize: 96568
[startup+760.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 23835 0 0 0 75931 74 0 0 25 0 1 0 422994332 100216832 23813 4294967295 134512640 134672761 3221224560 3221223664 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24467 23813 603 41 0 24426 0
vsize: 97868
[startup+770.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 24159 0 0 0 76931 75 0 0 25 0 1 0 422994332 101564416 24137 4294967295 134512640 134672761 3221224560 3221223728 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24796 24137 603 41 0 24755 0
vsize: 99184
[startup+780.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 24568 0 0 0 77929 77 0 0 25 0 1 0 422994332 103305216 24546 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25221 24546 603 41 0 25180 0
vsize: 100884
[startup+790.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 25063 0 0 0 78927 79 0 0 25 0 1 0 422994332 105312256 25041 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25711 25041 603 41 0 25670 0
vsize: 102844
[startup+800.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 25436 0 0 0 79926 80 0 0 25 0 1 0 422994332 106778624 25414 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26069 25414 603 41 0 26028 0
vsize: 104276
[startup+810.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 25797 0 0 0 80925 81 0 0 25 0 1 0 422994332 108253184 25775 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26429 25775 603 41 0 26388 0
vsize: 105716
[startup+820.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 26106 0 0 0 81925 82 0 0 25 0 1 0 422994332 109596672 26084 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26757 26084 603 41 0 26716 0
vsize: 107028
[startup+830.019 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 26514 0 0 0 82924 83 0 0 25 0 1 0 422994332 111214592 26492 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27152 26492 603 41 0 27111 0
vsize: 108608
[startup+840.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 26820 0 0 0 83923 84 0 0 25 0 1 0 422994332 112545792 26798 4294967295 134512640 134672761 3221224560 3221223684 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27477 26798 603 41 0 27436 0
vsize: 109908
[startup+850.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 27120 0 0 0 84922 84 0 0 25 0 1 0 422994332 113741824 27098 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27769 27098 603 41 0 27728 0
vsize: 111076
[startup+860.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 27443 0 0 0 85922 85 0 0 25 0 1 0 422994332 115073024 27421 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28094 27421 603 41 0 28053 0
vsize: 112376
[startup+870.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 27717 0 0 0 86921 86 0 0 25 0 1 0 422994332 116142080 27695 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28355 27695 603 41 0 28314 0
vsize: 113420
[startup+880.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 28086 0 0 0 87920 87 0 0 25 0 1 0 422994332 117616640 28064 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28715 28064 603 41 0 28674 0
vsize: 114860
[startup+890.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 28408 0 0 0 88920 88 0 0 25 0 1 0 422994332 118956032 28386 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29042 28386 603 41 0 29001 0
vsize: 116168
[startup+900.021 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 28649 0 0 0 89919 89 0 0 25 0 1 0 422994332 119894016 28627 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29271 28627 603 41 0 29230 0
vsize: 117084
[startup+910.022 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 29021 0 0 0 90917 91 0 0 25 0 1 0 422994332 121495552 28999 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29662 28999 603 41 0 29621 0
vsize: 118648
[startup+920.023 s]
Raw data (loadavg): 0.99 0.98 0.94 3/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 29376 0 0 0 91917 92 0 0 25 0 1 0 422994332 122957824 29354 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30019 29354 603 41 0 29978 0
vsize: 120076
[startup+930.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 29748 0 0 0 92916 93 0 0 25 0 1 0 422994332 124432384 29726 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30379 29726 603 41 0 30338 0
vsize: 121516
[startup+940.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 30010 0 0 0 93915 93 0 0 25 0 1 0 422994332 125501440 29988 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30640 29988 603 41 0 30599 0
vsize: 122560
[startup+950.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 30327 0 0 0 94915 94 0 0 25 0 1 0 422994332 126844928 30305 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30968 30305 603 41 0 30927 0
vsize: 123872
[startup+960.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 30612 0 0 0 95914 95 0 0 25 0 1 0 422994332 127918080 30590 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31230 30590 603 41 0 31189 0
vsize: 124920
[startup+970.023 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 30953 0 0 0 96913 96 0 0 25 0 1 0 422994332 129916928 30931 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31718 30931 603 41 0 31677 0
vsize: 126872
[startup+980.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 31265 0 0 0 97912 98 0 0 25 0 1 0 422994332 131137536 31243 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32016 31243 603 41 0 31975 0
vsize: 128064
[startup+990.024 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 31554 0 0 0 98910 100 0 0 25 0 1 0 422994332 132345856 31532 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32311 31532 603 41 0 32270 0
vsize: 129244
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 31795 0 0 0 99910 100 0 0 25 0 1 0 422994332 133283840 31773 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32540 31773 603 41 0 32499 0
vsize: 130160
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 32042 0 0 0 100909 100 0 0 25 0 1 0 422994332 134361088 32020 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32803 32020 603 41 0 32762 0
vsize: 131212
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 32313 0 0 0 101909 101 0 0 25 0 1 0 422994332 135434240 32291 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33065 32291 603 41 0 33024 0
vsize: 132260
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 32609 0 0 0 102908 102 0 0 25 0 1 0 422994332 136626176 32587 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33356 32587 603 41 0 33315 0
vsize: 133424
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 32900 0 0 0 103908 102 0 0 25 0 1 0 422994332 137834496 32878 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33651 32878 603 41 0 33610 0
vsize: 134604
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 33184 0 0 0 104907 103 0 0 25 0 1 0 422994332 138899456 33162 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33911 33162 603 41 0 33870 0
vsize: 135644
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 33522 0 0 0 105906 104 0 0 25 0 1 0 422994332 140365824 33500 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34269 33500 603 41 0 34228 0
vsize: 137076
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 33836 0 0 0 106905 106 0 0 25 0 1 0 422994332 141553664 33814 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34559 33814 603 41 0 34518 0
vsize: 138236
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 34160 0 0 0 107904 106 0 0 25 0 1 0 422994332 142880768 34138 4294967295 134512640 134672761 3221224560 3221223728 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34883 34138 603 41 0 34842 0
vsize: 139532
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 34437 0 0 0 108904 107 0 0 25 0 1 0 422994332 144097280 34415 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35180 34415 603 41 0 35139 0
vsize: 140720
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 34753 0 0 0 109904 108 0 0 25 0 1 0 422994332 145301504 34731 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35474 34731 603 41 0 35433 0
vsize: 141896
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 35060 0 0 0 110903 109 0 0 25 0 1 0 422994332 146628608 35038 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35798 35038 603 41 0 35757 0
vsize: 143192
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 35358 0 0 0 111901 110 0 0 25 0 1 0 422994332 147828736 35336 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36091 35336 603 41 0 36050 0
vsize: 144364
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 35648 0 0 0 112900 111 0 0 25 0 1 0 422994332 149032960 35626 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36385 35626 603 41 0 36344 0
vsize: 145540
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 35906 0 0 0 113900 112 0 0 25 0 1 0 422994332 150097920 35884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36645 35884 603 41 0 36604 0
vsize: 146580
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 36115 0 0 0 114899 112 0 0 25 0 1 0 422994332 150904832 36093 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36842 36093 603 41 0 36801 0
vsize: 147368
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 36328 0 0 0 115899 113 0 0 25 0 1 0 422994332 151842816 36306 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37071 36306 603 41 0 37030 0
vsize: 148284
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 36584 0 0 0 116899 114 0 0 25 0 1 0 422994332 152784896 36562 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37301 36562 603 41 0 37260 0
vsize: 149204
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 36818 0 0 0 117898 114 0 0 25 0 1 0 422994332 153849856 36796 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37561 36796 603 41 0 37520 0
vsize: 150244
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 37060 0 0 0 118898 115 0 0 25 0 1 0 422994332 154783744 37038 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37789 37038 603 41 0 37748 0
vsize: 151156
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.98 0.94 2/54 30857
Raw data (stat): 30857 (minisat+) R 30856 25285 25284 0 -1 0 37327 0 0 0 119897 115 0 0 25 0 1 0 422994332 155860992 37305 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38052 37305 603 41 0 38011 0
vsize: 152208
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.98 0.94 1/54 30857
Raw data (stat): 30857 (minisat+) Z 30856 25285 25284 0 -1 12 37330 0 0 0 119898 122 0 0 25 0 1 0 422994332 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.1
CPU time (s): 1200.21
CPU user time (s): 1198.98
CPU system time (s): 1.22981
CPU usage (%): 100.009
Max. virtual memory (Kb): 152208
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####