Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namenormalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb56-25-opb/normalized-frb56-25-5.opb
MD5SUM1694d09a3d3e6cb31138c73ed644b225
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -43
Optimality of the best value was proved NO
Number of terms in the objective function 1400
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 1400
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1400
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.12
Number of variables1400
Total number of constraints109601
Number of constraints which are clauses109601
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint2

Trace number 5266

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-13 23:06:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3732 boxname=wulflinc5 idbench=348 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1694d09a3d3e6cb31138c73ed644b225  /oldhome/oroussel/tmp/wulflinc5/normalized-frb56-25-5.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc5/normalized-frb56-25-5.opb /oldhome/oroussel/tmp/wulflinc5/normalized-frb56-25-5.opb
IDLAUNCH: 3732
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        898684 kB
Buffers:         33544 kB
Cached:          80396 kB
SwapCached:       2272 kB
Active:          55868 kB
Inactive:        63228 kB
HighTotal:      131008 kB
HighFree:        46648 kB
LowTotal:       903652 kB
LowFree:        852036 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11132 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:26:21 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 3732 7 1200.2 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 109601 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  109601   219202 |   36533       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -37
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 2772   maxlim: 37   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  128771   287708 |   42923       0        0     nan |  0.000 % |
c |       100 |  128762   287677 |   47215      96      967    10.1 |  0.096 % |
c |       250 |  128762   287677 |   51936     246     2701    11.0 |  0.097 % |
c |       475 |  128690   287429 |   57130     450     4415     9.8 |  0.289 % |
c |       812 |  128681   287398 |   62843     782     8188    10.5 |  0.314 % |
c |      1318 |  128639   287254 |   69127    1279    14370    11.2 |  0.433 % |
c |      2077 |  128594   287099 |   76040    2027    22223    11.0 |  0.555 % |
c |      3216 |  128549   286944 |   83644    3152    34765    11.0 |  0.674 % |
c ==============================================================================
c Found solution: -38
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 38   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3856 |  128443   286583 |   42814    3762    43145    11.5 |  0.674 % |
c |      3956 |  128443   286583 |   47095    3862    43800    11.3 |  1.010 % |
c |      4106 |  128443   286583 |   51804    4012    45627    11.4 |  1.010 % |
c |      4331 |  128398   286428 |   56985    4217    48426    11.5 |  1.132 % |
c |      4668 |  128380   286366 |   62683    4549    52352    11.5 |  1.180 % |
c |      5174 |  128279   286019 |   68952    5029    59031    11.7 |  1.493 % |
c |      5933 |  128228   285844 |   75847    5776    69182    12.0 |  1.636 % |
c |      7072 |  128121   285477 |   83432    6887    88169    12.8 |  1.974 % |
c |      8780 |  128019   285129 |   91775    8565   135399    15.8 |  2.287 % |
c |     11342 |  127431   283107 |  100953   10938   180723    16.5 |  4.089 % |
c ==============================================================================
c Found solution: -39
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15003 |  126213   278929 |   42071   14239   254821    17.9 |  4.089 % |
c |     15103 |  126167   278769 |   46278   14325   256446    17.9 |  8.420 % |
c |     15253 |  126158   278738 |   50905   14449   260904    18.1 |  8.443 % |
c |     15478 |  126042   278340 |   55996   14646   267230    18.2 |  8.850 % |
c |     15816 |  125991   278165 |   61596   14975   282873    18.9 |  9.067 % |
c |     16322 |  125828   277606 |   67755   15430   293150    19.0 |  9.694 % |
c |     17081 |  125706   277188 |   74531   16163   311377    19.3 | 10.173 % |
c |     18221 |  125426   276228 |   81984   17145   350944    20.5 | 11.209 % |
c |     19930 |  124712   273760 |   90182   18632   391930    21.0 | 14.069 % |
c |     22492 |  124208   272024 |   99201   20980   472092    22.5 | 16.114 % |
c ==============================================================================
c Found solution: -40
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 40   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24098 |  123935   271084 |   41311   22433   534302    23.8 | 16.114 % |
c |     24198 |  123935   271084 |   45442   22533   536902    23.8 | 17.312 % |
c |     24348 |  123904   270975 |   49986   22654   541044    23.9 | 17.432 % |
c |     24573 |  123889   270924 |   54984   22876   549120    24.0 | 17.480 % |
c |     24910 |  123889   270924 |   60483   23213   559790    24.1 | 17.480 % |
c |     25416 |  123874   270873 |   66531   23707   580097    24.5 | 17.528 % |
c |     26175 |  123786   270571 |   73184   24373   610697    25.1 | 17.913 % |
c |     27315 |  123755   270464 |   80503   25501   739278    29.0 | 18.057 % |
c ==============================================================================
c Found solution: -42
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 42   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28964 |  123416   269290 |   41138   26987   793706    29.4 | 18.057 % |
c |     29064 |  123407   269259 |   45251   27083   796677    29.4 | 19.611 % |
c |     29214 |  123407   269259 |   49776   27233   800400    29.4 | 19.611 % |
c |     29439 |  123135   268317 |   54754   27336   805064    29.5 | 20.862 % |
c |     29776 |  123050   268016 |   60230   27549   815488    29.6 | 21.246 % |
c |     30282 |  123010   267876 |   66253   27918   828595    29.7 | 21.391 % |
c |     31041 |  122886   267448 |   72878   28619   865474    30.2 | 21.918 % |
c |     32180 |  122664   266674 |   80166   29545   900576    30.5 | 22.975 % |
c |     33888 |  122491   266075 |   88182   30854   963797    31.2 | 23.528 % |
c |     36450 |  122293   265387 |   97001   33271  1179427    35.4 | 24.441 % |
c |     40295 |  122175   264981 |  106701   36898  1557629    42.2 | 24.875 % |
c |     46061 |  122044   264524 |  117371   42442  2014644    47.5 | 25.380 % |
c ==============================================================================
c Found solution: -43
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 43   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46722 |  122034   264491 |   40678   43099  2046107    47.5 | 25.380 % |
c |     46823 |  121996   264359 |   44745   17865  1016040    56.9 | 25.566 % |
c |     46973 |  121962   264241 |   49220   17964  1019366    56.7 | 25.711 % |
c |     47198 |  121905   264044 |   54142   18140  1025176    56.5 | 25.949 % |
c |     47537 |  121866   263907 |   59556   18458  1045932    56.7 | 26.117 % |
c |     48043 |  121792   263651 |   65512   18910  1070733    56.6 | 26.430 % |
c |     48802 |  121765   263556 |   72063   19664  1116671    56.8 | 26.574 % |
c |     49943 |  121692   263305 |   79269   20722  1187490    57.3 | 26.888 % |
c |     51652 |  121692   263305 |   87196   22431  1345058    60.0 | 26.886 % |
c |     54214 |  121692   263305 |   95916   24993  1624730    65.0 | 26.886 % |
c |     58058 |  121637   263112 |  105508   28827  1938817    67.3 | 27.150 % |
c |     63824 |  121540   262777 |  116059   34433  2307537    67.0 | 27.559 % |
c |     72474 |  121428   262387 |  127664   43022  3324382    77.3 | 28.137 % |
c ==============================================================================
c Found solution: -44
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 44   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75082 |  121408   262324 |   40469   45628  3555800    77.9 | 28.137 % |
c |     75184 |  121408   262324 |   44515   18321  1335926    72.9 | 28.226 % |
c |     75334 |  121408   262324 |   48967   18471  1340361    72.6 | 28.225 % |
c |     75561 |  121408   262324 |   53864   18698  1352439    72.3 | 28.226 % |
c |     75898 |  121408   262324 |   59250   19035  1371262    72.0 | 28.225 % |
c |     76404 |  121397   262285 |   65175   19519  1401337    71.8 | 28.273 % |
c |     77163 |  121397   262285 |   71693   20278  1485028    73.2 | 28.274 % |
c |     78302 |  121363   262171 |   78862   21398  1544262    72.2 | 28.441 % |
c |     80014 |  121363   262171 |   86748   23110  1745230    75.5 | 28.441 % |
c |     82577 |  121294   261932 |   95423   25624  2029685    79.2 | 28.707 % |
c |     86421 |  121294   261932 |  104966   29468  2500551    84.9 | 28.705 % |
c |     92187 |  121246   261766 |  115462   35205  2956464    84.0 | 28.921 % |
c |    100839 |  121214   261656 |  127009   43803  3928283    89.7 | 29.042 % |
c |    113815 |  121205   261625 |  139709   56761  5779851   101.8 | 29.066 % |
c |    133281 |  121205   261625 |  153680   76227 10271264   134.7 | 29.066 % |
c |    162475 |  121163   261479 |  169049  105405 14395359   136.6 | 29.258 % |
c |    206264 |  121151   261439 |  185953  149166 21915099   146.9 | 29.306 % |
c |    271949 |  121110   261300 |  204549   47391  4929221   104.0 | 29.475 % |
c ==============================================================================
c Found solution: -45
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 45   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    288421 |  121111   261307 |   40370   63863  8387467   131.3 | 29.475 % |
c |    288521 |  121078   261192 |   44407   16067  2720793   169.3 | 29.659 % |
c |    288671 |  121078   261192 |   48847   16217  2727526   168.2 | 29.659 % |
c |    288897 |  121078   261192 |   53732   16443  2734288   166.3 | 29.660 % |
c |    289234 |  121078   261192 |   59105   16780  2750654   163.9 | 29.659 % |
c |    289740 |  121036   261046 |   65016   17276  2774466   160.6 | 29.851 % |
c |    290502 |  121027   261015 |   71517   18029  2836917   157.4 | 29.875 % |
c |    291643 |  121027   261015 |   78669   19170  2920380   152.3 | 29.876 % |
c |    293352 |  121006   260944 |   86536   20864  3024195   144.9 | 29.949 % |
c |    295917 |  121006   260944 |   95190   23429  3426275   146.2 | 29.947 % |
c |    299761 |  121006   260944 |  104709   27273  3838977   140.8 | 29.947 % |
c |    305528 |  120987   260877 |  115180   33033  4362399   132.1 | 30.043 % |
c |    314178 |  120987   260877 |  126698   41683  6046378   145.1 | 30.043 % |
c |    327155 |  120987   260877 |  139368   54660  8723734   159.6 | 30.045 % |
c |    346617 |  120947   260743 |  153305   74082 11085932   149.6 | 30.237 % |
c |    375811 |  120947   260743 |  168635  103276 16147377   156.4 | 30.235 % |
c ==============================================================================
c Found solution: -46
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 46   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    384955 |  120949   260753 |   40316  112420 17772005   158.1 | 30.235 % |
c |    385055 |  120949   260753 |   44347   18207  2314227   127.1 | 30.247 % |
c |    385205 |  120949   260753 |   48782   18357  2320153   126.4 | 30.246 % |
c |    385431 |  120949   260753 |   53660   18583  2335196   125.7 | 30.245 % |
c |    385769 |  120941   260725 |   59026   18918  2350596   124.3 | 30.293 % |
c |    386275 |  120903   260591 |   64929   19417  2370774   122.1 | 30.485 % |
c |    387035 |  120903   260591 |   71422   20177  2451047   121.5 | 30.486 % |
c |    388174 |  120903   260591 |   78564   21316  2543083   119.3 | 30.486 % |
c |    389882 |  120903   260591 |   86420   23024  2643836   114.8 | 30.485 % |
c |    392444 |  120903   260591 |   95063   25586  2960963   115.7 | 30.486 % |
c |    396288 |  120903   260591 |  104569   29430  3334703   113.3 | 30.486 % |
c |    402054 |  120880   260508 |  115026   35191  3929289   111.7 | 30.629 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1400 -C1399 -C1398 -C1397 -C1396 -C1395 -C1394 -C1393 -C1392 -C1391 -C1390 -C1389 -C1388 -C1387 -C1386 -C1385 -C1384 -C1383 -C1382 -C1381 -C1380 -C1379 -C1378 -C1377 -C1376 -C1375 -C1374 -C1373 -C1372 -C1371 -C1370 -C1369 -C1368 -C1367 -C1366 -C1365 -C1364 -C1363 -C1362 -C1361 -C1360 -C1359 -C1358 -C1357 -C1356 -C1355 -C1354 -C1353 -C1352 -C1351 -C1350 -C1349 -C1348 -C1347 -C1346 -C1345 -C1344 -C1343 C1342 -C1341 -C1340 -C1339 -C1338 -C1337 -C1336 -C1335 -C1334 -C1333 -C1332 -C1331 -C1330 -C1329 -C1328 -C1327 -C1326 -C1325 -C1324 -C1323 -C1322 -C1321 -C1320 -C1319 -C1318 -C1317 -C1316 -C1315 -C1314 -C1313 -C1312 -C1311 -C1310 -C1309 -C1308 -C1307 -C1306 -C1305 -C1304 -C1303 -C1302 -C1301 -C1300 -C1299 -C1298 -C1297 -C1296 -C1295 -C1294 -C1293 -C1292 -C1291 -C1290 -C1289 -C1288 -C1287 -C1286 -C1285 -C1284 -C1283 -C1282 -C1281 -C1280 -C1279 -C1278 -C1277 -C1276 -C1275 -C1274 -C1273 -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 -C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 C1254 -C1253 -C1252 -C1251 -C1250 -C1249 -C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 -C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 -C1192 -C1191 C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 -C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 -C1121 C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 C802 -C801 -C800 -C799 -C798 C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 C243 -C242 -C241 -C240 -C239 -C238 -C237 -C236 -C235 -C234 -C233 -C232 -C231 -C230 -C229 -C228 -C227 -C226 -C225 -C224 -C223 -C222 -C221 -C220 -C219 -C218 -C217 -C216 -C215 -C214 -C213 -C212 -C211 -C210 -C209 -C208 -C207 -C206 C205 -C204 -C203 -C202 -C201 -C200 -C199 -C198 -C197 -C196 -C195 -C194 -C193 -C192 -C191 -C190 -C189 -C188 -C187 -C186 -C185 -C184 -C183 -C182 -C181 -C180 -C179 -C178 -C177 -C176 -C175 -C174 -C173 -C172 -C171 -C170 -C169 -C168 -C167 -C166 -C165 -C164 -C163 -C162 -C161 -C160 C159 -C158 -C157 -C156 -C155 -C154 -C153 -C152 -C151 -C150 -C149 -C148 -C147 -C146 -C145 -C144 -C143 -C142 -C141 -C140 -C139 -C138 C137 -C136 -C135 -C134 -C133 -C132 -C131 -C130 -C129 -C128 -C127 -C126 -C125 -C124 -C123 -C122 -C121 -C120 -C119 -C118 -C117 -C116 -C115 -C114 -C113 -C112 -C111 -C110 -C109 -C108 -C107 C106 -C105 -C104 -C103 -C102#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 27152
Raw data (stat): 27152 (runsolver) R 27151 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421558407 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99964 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 5181 0 0 0 984 14 0 0 25 0 1 0 421558407 22876160 5159 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5585 5159 603 41 0 5544 0
vsize: 22340
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 5181 0 0 0 1983 14 0 0 25 0 1 0 421558407 22876160 5159 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5585 5159 603 41 0 5544 0
vsize: 22340
[startup+30.0011 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 5181 0 0 0 2982 14 0 0 25 0 1 0 421558407 22876160 5159 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5585 5159 603 41 0 5544 0
vsize: 22340
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 5181 0 0 0 3982 14 0 0 25 0 1 0 421558407 22876160 5159 4294967295 134512640 134672761 3221224560 3221223620 1075346557 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5159 603 41 0 5544 0
vsize: 22340
[startup+50.0021 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 5181 0 0 0 4982 15 0 0 25 0 1 0 421558407 22876160 5159 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5159 603 41 0 5544 0
vsize: 22340
[startup+60.0014 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 5181 0 0 0 5982 15 0 0 25 0 1 0 421558407 22876160 5159 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5585 5159 603 41 0 5544 0
vsize: 22340
[startup+70.0019 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 5181 0 0 0 6982 15 0 0 25 0 1 0 421558407 22876160 5159 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5159 603 41 0 5544 0
vsize: 22340
[startup+80.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 5181 0 0 0 7982 15 0 0 25 0 1 0 421558407 22876160 5159 4294967295 134512640 134672761 3221224560 3221223728 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5159 603 41 0 5544 0
vsize: 22340
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 5181 0 0 0 8982 15 0 0 25 0 1 0 421558407 22876160 5159 4294967295 134512640 134672761 3221224560 3221223664 134560139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5159 603 41 0 5544 0
vsize: 22340
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 5181 0 0 0 9982 15 0 0 25 0 1 0 421558407 22876160 5159 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5585 5159 603 41 0 5544 0
vsize: 22340
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 5755 0 0 0 10980 17 0 0 25 0 1 0 421558407 25161728 5733 4294967295 134512640 134672761 3221224560 3221223664 134560134 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6143 5733 603 41 0 6102 0
vsize: 24572
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 6261 0 0 0 11979 19 0 0 25 0 1 0 421558407 27181056 6239 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 6239 603 41 0 6595 0
vsize: 26544
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 6261 0 0 0 12979 19 0 0 25 0 1 0 421558407 27181056 6239 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 6239 603 41 0 6595 0
vsize: 26544
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 6261 0 0 0 13979 19 0 0 25 0 1 0 421558407 27181056 6239 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6636 6239 603 41 0 6595 0
vsize: 26544
[startup+150.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 6315 0 0 0 14979 19 0 0 25 0 1 0 421558407 27451392 6293 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6702 6293 603 41 0 6661 0
vsize: 26808
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 7069 0 0 0 15976 22 0 0 25 0 1 0 421558407 30519296 7047 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7451 7047 603 41 0 7410 0
vsize: 29804
[startup+170.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 7761 0 0 0 16974 24 0 0 25 0 1 0 421558407 33329152 7739 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8137 7739 603 41 0 8096 0
vsize: 32548
[startup+180.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 8371 0 0 0 17972 26 0 0 25 0 1 0 421558407 35880960 8349 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8760 8349 603 41 0 8719 0
vsize: 35040
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 8921 0 0 0 18971 27 0 0 25 0 1 0 421558407 38154240 8899 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9315 8899 603 41 0 9274 0
vsize: 37260
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 9661 0 0 0 19969 30 0 0 25 0 1 0 421558407 41111552 9639 4294967295 134512640 134672761 3221224560 3221223664 134560252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10037 9639 603 41 0 9996 0
vsize: 40148
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 10413 0 0 0 20967 32 0 0 25 0 1 0 421558407 44470272 10391 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10857 10391 603 41 0 10816 0
vsize: 43428
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 11111 0 0 0 21965 34 0 0 25 0 1 0 421558407 47296512 11089 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11547 11089 603 41 0 11506 0
vsize: 46188
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 11755 0 0 0 22963 36 0 0 25 0 1 0 421558407 49987584 11733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12204 11733 603 41 0 12163 0
vsize: 48816
[startup+240.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 12435 0 0 0 23961 39 0 0 25 0 1 0 421558407 52805632 12413 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12892 12413 603 41 0 12851 0
vsize: 51568
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 13144 0 0 0 24958 41 0 0 25 0 1 0 421558407 55627776 13122 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13581 13122 603 41 0 13540 0
vsize: 54324
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 13706 0 0 0 25957 43 0 0 25 0 1 0 421558407 58032128 13684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14168 13684 603 41 0 14127 0
vsize: 56672
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 14068 0 0 0 26956 45 0 0 25 0 1 0 421558407 59383808 14046 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14498 14046 603 41 0 14457 0
vsize: 57992
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 14391 0 0 0 27955 45 0 0 25 0 1 0 421558407 60731392 14369 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14827 14369 603 41 0 14786 0
vsize: 59308
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 14783 0 0 0 28954 47 0 0 25 0 1 0 421558407 62332928 14761 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15218 14761 603 41 0 15177 0
vsize: 60872
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 15153 0 0 0 29953 48 0 0 25 0 1 0 421558407 63795200 15131 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15575 15131 603 41 0 15534 0
vsize: 62300
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 15569 0 0 0 30951 50 0 0 25 0 1 0 421558407 65540096 15547 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16001 15547 603 41 0 15960 0
vsize: 64004
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 15998 0 0 0 31950 51 0 0 25 0 1 0 421558407 67276800 15976 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16425 15976 603 41 0 16384 0
vsize: 65700
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 16465 0 0 0 32949 52 0 0 25 0 1 0 421558407 69156864 16443 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16884 16443 603 41 0 16843 0
vsize: 67536
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 16964 0 0 0 33948 54 0 0 25 0 1 0 421558407 71155712 16942 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17372 16942 603 41 0 17331 0
vsize: 69488
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 17462 0 0 0 34947 55 0 0 25 0 1 0 421558407 73297920 17440 4294967295 134512640 134672761 3221224560 3221223744 134558937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17895 17440 603 41 0 17854 0
vsize: 71580
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 17888 0 0 0 35945 56 0 0 25 0 1 0 421558407 75042816 17866 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18321 17866 603 41 0 18280 0
vsize: 73284
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 18264 0 0 0 36944 58 0 0 25 0 1 0 421558407 76529664 18242 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18684 18242 603 41 0 18643 0
vsize: 74736
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 18710 0 0 0 37943 59 0 0 25 0 1 0 421558407 78286848 18688 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18688 603 41 0 19072 0
vsize: 76452
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 19236 0 0 0 38941 60 0 0 25 0 1 0 421558407 80433152 19214 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19637 19214 603 41 0 19596 0
vsize: 78548
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 19596 0 0 0 39940 61 0 0 25 0 1 0 421558407 81903616 19574 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19996 19574 603 41 0 19955 0
vsize: 79984
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 20019 0 0 0 40939 62 0 0 25 0 1 0 421558407 83640320 19997 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20420 19997 603 41 0 20379 0
vsize: 81680
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 20428 0 0 0 41938 63 0 0 25 0 1 0 421558407 85372928 20406 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20843 20406 603 41 0 20802 0
vsize: 83372
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 20860 0 0 0 42937 65 0 0 25 0 1 0 421558407 87093248 20838 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21263 20838 603 41 0 21222 0
vsize: 85052
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 21253 0 0 0 43936 66 0 0 25 0 1 0 421558407 88694784 21231 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21654 21231 603 41 0 21613 0
vsize: 86616
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 21631 0 0 0 44935 67 0 0 25 0 1 0 421558407 90296320 21609 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22045 21609 603 41 0 22004 0
vsize: 88180
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 21962 0 0 0 45934 68 0 0 25 0 1 0 421558407 91635712 21940 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22372 21940 603 41 0 22331 0
vsize: 89488
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 22216 0 0 0 46933 69 0 0 25 0 1 0 421558407 92696576 22194 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22631 22194 603 41 0 22590 0
vsize: 90524
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 22504 0 0 0 47932 70 0 0 25 0 1 0 421558407 94294016 22482 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23021 22482 603 41 0 22980 0
vsize: 92084
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 22870 0 0 0 48930 71 0 0 25 0 1 0 421558407 95760384 22848 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23379 22848 603 41 0 23338 0
vsize: 93516
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 23167 0 0 0 49929 72 0 0 25 0 1 0 421558407 96976896 23145 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23676 23145 603 41 0 23635 0
vsize: 94704
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 23529 0 0 0 50928 73 0 0 25 0 1 0 421558407 98451456 23507 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24036 23507 603 41 0 23995 0
vsize: 96144
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 23780 0 0 0 51928 74 0 0 25 0 1 0 421558407 99524608 23758 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24298 23758 603 41 0 24257 0
vsize: 97192
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 24053 0 0 0 52927 75 0 0 25 0 1 0 421558407 100589568 24031 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24558 24031 603 41 0 24517 0
vsize: 98232
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 24390 0 0 0 53926 76 0 0 25 0 1 0 421558407 102072320 24368 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24920 24368 603 41 0 24879 0
vsize: 99680
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 24698 0 0 0 54925 77 0 0 25 0 1 0 421558407 103284736 24676 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25216 24676 603 41 0 25175 0
vsize: 100864
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 25129 0 0 0 55925 78 0 0 25 0 1 0 421558407 105017344 25107 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25639 25107 603 41 0 25598 0
vsize: 102556
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 25447 0 0 0 56924 78 0 0 25 0 1 0 421558407 106352640 25425 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25965 25425 603 41 0 25924 0
vsize: 103860
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 25683 0 0 0 57923 79 0 0 25 0 1 0 421558407 107294720 25661 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26195 25661 603 41 0 26154 0
vsize: 104780
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 25928 0 0 0 58922 80 0 0 25 0 1 0 421558407 108363776 25906 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26456 25906 603 41 0 26415 0
vsize: 105824
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 26194 0 0 0 59922 81 0 0 25 0 1 0 421558407 109436928 26172 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26718 26172 603 41 0 26677 0
vsize: 106872
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 26471 0 0 0 60921 82 0 0 25 0 1 0 421558407 110505984 26449 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26979 26449 603 41 0 26938 0
vsize: 107916
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 26717 0 0 0 61920 83 0 0 25 0 1 0 421558407 111570944 26695 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27239 26695 603 41 0 27198 0
vsize: 108956
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 26975 0 0 0 62920 83 0 0 25 0 1 0 421558407 112640000 26953 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27500 26953 603 41 0 27459 0
vsize: 110000
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 27246 0 0 0 63919 84 0 0 25 0 1 0 421558407 113700864 27224 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27759 27224 603 41 0 27718 0
vsize: 111036
[startup+650.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 27494 0 0 0 64918 85 0 0 25 0 1 0 421558407 114634752 27472 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27987 27472 603 41 0 27946 0
vsize: 111948
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 27767 0 0 0 65917 86 0 0 25 0 1 0 421558407 115834880 27745 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28280 27745 603 41 0 28239 0
vsize: 113120
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 27974 0 0 0 66917 87 0 0 25 0 1 0 421558407 116637696 27952 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28476 27952 603 41 0 28435 0
vsize: 113904
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 28221 0 0 0 67917 87 0 0 25 0 1 0 421558407 117702656 28199 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28736 28199 603 41 0 28695 0
vsize: 114944
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 28468 0 0 0 68916 88 0 0 25 0 1 0 421558407 118648832 28446 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28967 28446 603 41 0 28926 0
vsize: 115868
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 28717 0 0 0 69915 89 0 0 25 0 1 0 421558407 119713792 28695 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29227 28695 603 41 0 29186 0
vsize: 116908
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 28916 0 0 0 70915 89 0 0 25 0 1 0 421558407 120508416 28894 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29421 28894 603 41 0 29380 0
vsize: 117684
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 29127 0 0 0 71915 90 0 0 25 0 1 0 421558407 121315328 29105 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29618 29105 603 41 0 29577 0
vsize: 118472
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 29362 0 0 0 72914 91 0 0 25 0 1 0 421558407 122249216 29340 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29846 29340 603 41 0 29805 0
vsize: 119384
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 29566 0 0 0 73913 92 0 0 25 0 1 0 421558407 123183104 29544 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30074 29544 603 41 0 30033 0
vsize: 120296
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 29755 0 0 0 74913 93 0 0 25 0 1 0 421558407 123854848 29733 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30238 29733 603 41 0 30197 0
vsize: 120952
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 29948 0 0 0 75912 94 0 0 25 0 1 0 421558407 124653568 29926 4294967295 134512640 134672761 3221224560 3221223696 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30433 29926 603 41 0 30392 0
vsize: 121732
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30179 0 0 0 76911 95 0 0 25 0 1 0 421558407 125591552 30157 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30662 30157 603 41 0 30621 0
vsize: 122648
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30395 0 0 0 77910 96 0 0 25 0 1 0 421558407 126525440 30373 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30890 30373 603 41 0 30849 0
vsize: 123560
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30603 0 0 0 78910 97 0 0 25 0 1 0 421558407 127320064 30581 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31084 30581 603 41 0 31043 0
vsize: 124336
[startup+800.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 79909 97 0 0 25 0 1 0 421558407 128122880 30767 4294967295 134512640 134672761 3221224560 3221223664 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31280 30767 603 41 0 31239 0
vsize: 125120
[startup+810.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 80909 97 0 0 25 0 1 0 421558407 128122880 30767 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31280 30767 603 41 0 31239 0
vsize: 125120
[startup+820.01 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 81910 97 0 0 25 0 1 0 421558407 128122880 30767 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31280 30767 603 41 0 31239 0
vsize: 125120
[startup+830.01 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 82910 97 0 0 25 0 1 0 421558407 128122880 30767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31280 30767 603 41 0 31239 0
vsize: 125120
[startup+840.01 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 83910 97 0 0 25 0 1 0 421558407 128122880 30767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31280 30767 603 41 0 31239 0
vsize: 125120
[startup+850.012 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 84910 97 0 0 25 0 1 0 421558407 128122880 30767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31280 30767 603 41 0 31239 0
vsize: 125120
[startup+860.011 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 85910 97 0 0 25 0 1 0 421558407 128122880 30767 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31280 30767 603 41 0 31239 0
vsize: 125120
[startup+870.011 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 86909 97 0 0 25 0 1 0 421558407 128122880 30767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31280 30767 603 41 0 31239 0
vsize: 125120
[startup+880.011 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 87909 97 0 0 25 0 1 0 421558407 128122880 30767 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31280 30767 603 41 0 31239 0
vsize: 125120
[startup+890.012 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 88910 97 0 0 25 0 1 0 421558407 128122880 30767 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31280 30767 603 41 0 31239 0
vsize: 125120
[startup+900.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 89910 97 0 0 25 0 1 0 421558407 128110592 30767 4294967295 134512640 134672761 3221224560 3221223728 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30767 603 41 0 31236 0
vsize: 125108
[startup+910.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 90910 97 0 0 25 0 1 0 421558407 128110592 30767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30767 603 41 0 31236 0
vsize: 125108
[startup+920.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 91910 97 0 0 25 0 1 0 421558407 128110592 30767 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30767 603 41 0 31236 0
vsize: 125108
[startup+930.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 92910 97 0 0 25 0 1 0 421558407 128110592 30767 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30767 603 41 0 31236 0
vsize: 125108
[startup+940.011 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 93910 97 0 0 25 0 1 0 421558407 128110592 30767 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30767 603 41 0 31236 0
vsize: 125108
[startup+950.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 94911 97 0 0 25 0 1 0 421558407 128110592 30767 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30767 603 41 0 31236 0
vsize: 125108
[startup+960.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30789 0 0 0 95911 97 0 0 25 0 1 0 421558407 128110592 30767 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30767 603 41 0 31236 0
vsize: 125108
[startup+970.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 96911 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223744 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+980.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 97911 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+990.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 98911 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 99912 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 100912 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 101912 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 102912 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 103912 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 104912 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 105913 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 106913 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 107913 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 108913 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 109913 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 110914 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 111914 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 112914 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223744 134559367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 113914 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 114914 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 115914 97 0 0 25 0 1 0 421558407 128110592 30768 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31277 30768 603 41 0 31236 0
vsize: 125108
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 116915 97 0 0 25 0 1 0 421558407 128094208 30768 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31273 30768 603 41 0 31232 0
vsize: 125092
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 117915 97 0 0 25 0 1 0 421558407 128094208 30768 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31273 30768 603 41 0 31232 0
vsize: 125092
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 118915 97 0 0 25 0 1 0 421558407 128094208 30768 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31273 30768 603 41 0 31232 0
vsize: 125092
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27152
Raw data (stat): 27152 (minisat+) R 27151 24215 24214 0 -1 0 30790 0 0 0 119915 97 0 0 25 0 1 0 421558407 128094208 30768 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31273 30768 603 41 0 31232 0
vsize: 125092
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 27152
Raw data (stat): 27152 (minisat+) Z 27151 24215 24214 0 -1 12 30793 0 0 0 119916 103 0 0 25 0 1 0 421558407 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.08
CPU time (s): 1200.2
CPU user time (s): 1199.16
CPU system time (s): 1.03784
CPU usage (%): 100.01
Max. virtual memory (Kb): 125120
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####