Some explanations

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

General information on the benchmark

Namenormalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb59-26-opb/normalized-frb59-26-1.opb
MD5SUM42c2d619b73aa24781f1b54bddde28cc
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -44
Optimality of the best value was proved NO
Number of terms in the objective function 1534
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 1534
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 1534
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1175.13
Number of variables1534
Total number of constraints126555
Number of constraints which are clauses126555
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 6402

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-14 04:55:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4861 boxname=wulflinc7 idbench=349 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  42c2d619b73aa24781f1b54bddde28cc  /oldhome/oroussel/tmp/wulflinc7/normalized-frb59-26-1.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc7/normalized-frb59-26-1.opb /oldhome/oroussel/tmp/wulflinc7/normalized-frb59-26-1.opb
IDLAUNCH: 4861
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        848088 kB
Buffers:         38192 kB
Cached:         128204 kB
SwapCached:          0 kB
Active:          76172 kB
Inactive:        93076 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        847836 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11736 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:15:26 (client local time) WITH STATUS 10 IN 1201.14 SECONDS
stats: 4861 7 1201.14 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 126555 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 |  126555   253110 |   42185       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -38
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:85954     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  308361   678450 |  102787       0        0     nan |  0.000 % |
c |       100 |  307823   677227 |  113065      72      389     5.4 |  0.302 % |
c |       250 |  306406   673990 |  124372     197      923     4.7 |  0.941 % |
c |       476 |  302120   664187 |  136809     331     1910     5.8 |  3.020 % |
c ==============================================================================
c Found solution: -39
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       677 |  300134   659883 |  100044     473     2739     5.8 |  3.020 % |
c ==============================================================================
c Found solution: -41
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       716 |  299798   659210 |   99932     501     2848     5.7 |  3.020 % |
c |       817 |  298505   656235 |  109925     546     3424     6.3 |  5.146 % |
c |       967 |  297399   653689 |  120917     666     3920     5.9 |  5.702 % |
c |      1192 |  293639   645037 |  133009     818     5201     6.4 |  7.589 % |
c |      1529 |  286529   628662 |  146310    1030     6724     6.5 | 11.176 % |
c |      2035 |  280755   615345 |  160941    1417    11859     8.4 | 14.088 % |
c |      2794 |  270934   592632 |  177035    1935    16101     8.3 | 19.163 % |
c |      3933 |  257357   561213 |  194739    2703    22392     8.3 | 26.170 % |
c |      5641 |  237145   514293 |  214213    3825    32607     8.5 | 36.743 % |
c |      8203 |  208257   446741 |  235634    5328    49888     9.4 | 52.193 % |
c |     12049 |  177354   374358 |  259197    6963    69165     9.9 | 69.275 % |
c ==============================================================================
c Found solution: -42
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14333 |  166301   348205 |   55433    8054    78658     9.8 | 69.275 % |
c |     14435 |  165989   347471 |   60976    8105    78923     9.7 | 75.714 % |
c |     14586 |  165551   346447 |   67073    8131    79560     9.8 | 75.790 % |
c |     14811 |  164983   345119 |   73781    8236    80448     9.8 | 76.102 % |
c |     15149 |  163652   341986 |   81159    8369    82399     9.8 | 76.866 % |
c |     15656 |  162547   339380 |   89275    8717    86042     9.9 | 77.505 % |
c |     16415 |  159470   332159 |   98202    8907    89860    10.1 | 79.236 % |
c |     17555 |  157488   327526 |  108023    9679   106242    11.0 | 80.345 % |
c |     19264 |  154342   320119 |  118825   10812   138879    12.8 | 82.110 % |
c |     21826 |  149425   308520 |  130708   12088   155493    12.9 | 84.915 % |
c ==============================================================================
c Found solution: -43
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22705 |  148907   307332 |   49635   12741   166681    13.1 | 84.915 % |
c |     22805 |  148707   306863 |   54598   12746   166420    13.1 | 85.368 % |
c |     22955 |  148707   306863 |   60058   12896   168016    13.0 | 85.368 % |
c |     23180 |  148609   306631 |   66064   13092   170111    13.0 | 85.425 % |
c |     23517 |  148512   306404 |   72670   13395   173876    13.0 | 85.478 % |
c |     24023 |  148490   306353 |   79937   13872   179385    12.9 | 85.489 % |
c ==============================================================================
c Found solution: -44
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24636 |  148444   306221 |   49481   14433   187691    13.0 | 85.489 % |
c |     24736 |  148303   305894 |   54429   14432   187242    13.0 | 85.582 % |
c |     24886 |  148303   305894 |   59872   14582   190569    13.1 | 85.582 % |
c |     25111 |  148303   305894 |   65859   14807   193183    13.0 | 85.582 % |
c |     25448 |  147819   304750 |   72445   14813   193828    13.1 | 85.874 % |
c |     25954 |  147441   303854 |   79689   15180   202355    13.3 | 86.098 % |
c ==============================================================================
c Found solution: -45
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26399 |  147342   303637 |   49114   15530   209932    13.5 | 86.098 % |
c |     26499 |  147280   303491 |   54025   15592   211647    13.6 | 86.215 % |
c |     26649 |  146788   302331 |   59427   15476   210188    13.6 | 86.494 % |
c |     26874 |  146542   301752 |   65370   15541   211094    13.6 | 86.635 % |
c |     27211 |  146536   301738 |   71907   15864   214050    13.5 | 86.638 % |
c |     27718 |  146416   301456 |   79098   16286   223202    13.7 | 86.704 % |
c |     28477 |  146294   301166 |   87008   16861   239294    14.2 | 86.778 % |
c |     29618 |  144942   297973 |   95709   17015   241579    14.2 | 87.553 % |
c ==============================================================================
c Found solution: -46
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29694 |  144898   297818 |   48299   17080   243117    14.2 | 87.553 % |
c |     29795 |  144714   297379 |   53128   16921   240413    14.2 | 87.683 % |
c |     29945 |  144478   296833 |   58441   16965   241120    14.2 | 87.807 % |
c |     30170 |  144472   296819 |   64285   17185   253247    14.7 | 87.810 % |
c |     30507 |  144315   296447 |   70714   17452   267278    15.3 | 87.907 % |
c |     31013 |  144315   296447 |   77786   17958   282298    15.7 | 87.907 % |
c |     31774 |  143410   294320 |   85564   18081   300096    16.6 | 88.423 % |
c |     32913 |  143158   293724 |   94121   18963   326176    17.2 | 88.565 % |
c |     34621 |  143158   293724 |  103533   20671   454293    22.0 | 88.565 % |
c ==============================================================================
c Found solution: -47
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34985 |  143204   293842 |   47734   20927   464462    22.2 | 88.565 % |
c |     35085 |  143204   293842 |   52507   21027   465690    22.1 | 88.576 % |
c |     35235 |  143204   293842 |   57758   21177   472907    22.3 | 88.576 % |
c |     35460 |  143198   293828 |   63533   21394   479270    22.4 | 88.579 % |
c |     35798 |  143194   293819 |   69887   21727   492200    22.7 | 88.581 % |
c |     36304 |  143194   293819 |   76876   22233   519713    23.4 | 88.581 % |
c |     37063 |  143180   293787 |   84563   22975   546622    23.8 | 88.587 % |
c |     38204 |  143078   293545 |   93020   23925   641127    26.8 | 88.647 % |
c |     39912 |  143060   293503 |  102322   25616   701678    27.4 | 88.657 % |
c ==============================================================================
c Found solution: -48
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42144 |  142818   292922 |   47606   27291   914328    33.5 | 88.657 % |
c |     42244 |  142818   292922 |   52366   27391   915916    33.4 | 88.787 % |
c |     42394 |  142818   292922 |   57603   27541   922169    33.5 | 88.787 % |
c |     42619 |  142810   292903 |   63363   27735   931773    33.6 | 88.792 % |
c |     42956 |  142810   292903 |   69699   28072   970626    34.6 | 88.792 % |
c |     43462 |  142810   292903 |   76669   28578  1009811    35.3 | 88.792 % |
c |     44221 |  142810   292903 |   84336   29337  1054976    36.0 | 88.792 % |
c |     45360 |  142684   292608 |   92770   30386  1141900    37.6 | 88.863 % |
c |     47068 |  142684   292608 |  102047   32094  1430025    44.6 | 88.863 % |
c |     49630 |  142610   292435 |  112252   34549  1704756    49.3 | 88.905 % |
c |     53476 |  142610   292435 |  123477   38395  2109918    55.0 | 88.905 % |
c ==============================================================================
c Found solution: -49
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     55243 |  142540   292271 |   47513   39777  2271037    57.1 | 88.905 % |
c |     55343 |  142540   292271 |   52264   39877  2273581    57.0 | 88.965 % |
c |     55493 |  142540   292271 |   57490   40027  2284604    57.1 | 88.965 % |
c |     55718 |  142540   292271 |   63239   40252  2299502    57.1 | 88.965 % |
c |     56055 |  142540   292271 |   69563   40589  2322225    57.2 | 88.965 % |
c |     56562 |  142540   292271 |   76520   41096  2343502    57.0 | 88.965 % |
c ==============================================================================
c Found solution: -50
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57114 |  142503   292158 |   47501   41043  2276977    55.5 | 88.965 % |
c |     57214 |  142177   291399 |   52251   40643  2272059    55.9 | 89.158 % |
c |     57368 |  142177   291399 |   57476   40797  2289223    56.1 | 89.158 % |
c |     57593 |  142177   291399 |   63223   41022  2297812    56.0 | 89.158 % |
c |     57930 |  142109   291239 |   69546   41153  2311283    56.2 | 89.197 % |
c |     58436 |  142109   291239 |   76500   41659  2344088    56.3 | 89.197 % |
c |     59195 |  141987   290947 |   84150   42165  2401792    57.0 | 89.274 % |
c |     60334 |  141987   290947 |   92566   43304  2531793    58.5 | 89.274 % |
c |     62042 |  141969   290905 |  101822   44965  2723582    60.6 | 89.284 % |
c |     64604 |  141875   290685 |  112004   47265  3067950    64.9 | 89.339 % |
c |     68448 |  141875   290685 |  123205   51109  3575262    70.0 | 89.339 % |
c |     74214 |  141857   290642 |  135525   56871  4293119    75.5 | 89.350 % |
c |     82865 |  141849   290623 |  149078   65506  5697489    87.0 | 89.355 % |
c ==============================================================================
c Found solution: -51
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87560 |  141904   290760 |   47301   70201  6316773    90.0 | 89.355 % |
c |     87660 |  141904   290760 |   52031   70301  6317839    89.9 | 89.350 % |
c |     87810 |  141904   290760 |   57234   70451  6334844    89.9 | 89.350 % |
c |     88035 |  141898   290746 |   62957   70657  6341207    89.7 | 89.353 % |
c |     88373 |  141898   290746 |   69253   70995  6350366    89.4 | 89.353 % |
c |     88879 |  141892   290732 |   76178   71500  6384920    89.3 | 89.357 % |
c |     89638 |  141886   290718 |   83796   72255  6427153    89.0 | 89.360 % |
c |     90777 |  141886   290718 |   92176   73394  6585203    89.7 | 89.360 % |
c |     92485 |  141872   290685 |  101393   75099  6759705    90.0 | 89.368 % |
c |     95047 |  141848   290628 |  111533   77649  6990980    90.0 | 89.382 % |
c |     98891 |  141848   290628 |  122686   81493  7513784    92.2 | 89.382 % |
c |    104657 |  141848   290628 |  134955   87259  8507306    97.5 | 89.382 % |
c |    113306 |  141797   290507 |  148450   95742  9759364   101.9 | 89.414 % |
c |    126280 |  141791   290493 |  163295  108673 12226802   112.5 | 89.418 % |
c ==============================================================================
c Found solution: -52
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    136164 |  141761   290408 |   47253  117906 14184514   120.3 | 89.418 % |
c |    136264 |  141705   290276 |   51978   21039  2724699   129.5 | 89.464 % |
c |    136414 |  141705   290276 |   57176   21189  2735472   129.1 | 89.464 % |
c |    136639 |  141705   290276 |   62893   21414  2751246   128.5 | 89.464 % |
c |    136976 |  141699   290262 |   69183   21715  2759451   127.1 | 89.468 % |
c |    137483 |  141556   289923 |   76101   22161  2777762   125.3 | 89.554 % |
c |    138242 |  141499   289789 |   83711   22908  2817991   123.0 | 89.585 % |
c |    139381 |  141495   289780 |   92082   24002  2863396   119.3 | 89.587 % |
c |    141089 |  141495   289780 |  101291   25710  3042874   118.4 | 89.587 % |
c |    143651 |  141495   289780 |  111420   28272  3321773   117.5 | 89.587 % |
c |    147495 |  141477   289738 |  122562   32109  3885758   121.0 | 89.596 % |
c |    153261 |  141280   289269 |  134818   37765  4619601   122.3 | 89.715 % |
c |    161910 |  141270   289245 |  148300   46412  6220016   134.0 | 89.721 % |
c |    174884 |  141270   289245 |  163130   59386  8463468   142.5 | 89.721 % |
c |    194345 |  141248   289194 |  179443   78837 11570118   146.8 | 89.733 % |
c |    223538 |  141248   289194 |  197387  108030 17385900   160.9 | 89.733 % |
c |    267327 |  141134   288925 |  217126  151706 24409291   160.9 | 89.798 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1534 -C1533 -C1532 -C1531 -C1530 -C1529 -C1528 -C1527 -C1526 -C1525 -C1524 -C1523 -C1522 -C1521 -C1520 -C1519 -C1518 -C1517 -C1516 -C1515 -C1514 -C1513 -C1512 -C1511 -C1510 -C1509 -C1508 -C1507 -C1506 -C1505 -C1504 -C1503 -C1502 -C1501 -C1500 -C1499 -C1498 -C1497 -C1496 -C1495 -C1494 C1493 -C1492 -C1491 -C1490 -C1489 -C1488 -C1487 -C1486 -C1485 -C1484 -C1483 -C1482 -C1481 -C1480 -C1479 -C1478 -C1477 C1476 -C1475 -C1474 -C1473 -C1472 -C1471 -C1470 -C1469 -C1468 -C1467 -C1466 -C1465 -C1464 -C1463 -C1462 -C1461 -C1460 -C1459 -C1458 -C1457 -C1456 -C1455 -C1454 -C1453 -C1452 C1451 -C1450 -C1449 -C1448 -C1447 -C1446 -C1445 -C1444 -C1443 -C1442 -C1441 -C1440 -C1439 -C1438 -C1437 -C1436 -C1435 -C1434 -C1433 -C1432 -C1431 -C1430 -C1429 -C1428 -C1427 -C1426 -C1425 C1424 -C1423 -C1422 -C1421 -C1420 -C1419 -C1418 -C1417 -C1416 -C1415 -C1414 -C1413 -C1412 -C1411 -C1410 -C1409 -C1408 -C1407 -C1406 -C1405 -C1404 -C1403 -C1402 -C1401 -C1400 -C1399 -C1398 -C1397 -C1396 -C1395 -C1394 -C1393 -C1392 -C1391 -C1390 -C1389 -C1388 -C1387 -C1386 C1385 -C1384 -C1383 -C1382 -C1381 -C1380 -C1379 -C1378 -C1377 -C1376 -C1375 -C1374 -C1373 -C1372 -C1371 -C1370 -C1369 -C1368 -C1367 -C1366 -C1365 -C1364 -C1363 -C1362 C1361 -C1360 -C1359 -C1358 -C1357 -C1356 -C1355 -C1354 -C1353 -C1352 -C1351 -C1350 -C1349 -C1348 -C1347 -C1346 -C1345 -C1344 -C1343 -C1342 -C1341 -C1340 -C1339 -C1338 -C1337 -C1336 -C1335 -C1334 -C1333 -C1332 -C1331 -C1330 -C1329 C1328 -C1327 C1326 -C1325 -C1324 -C1323 -C1322 -C1321 -C1320 -C1319 -C1318 -C1317 -C1316 -C1315 -C1314 -C1313 -C1312 -C1311 -C1310 -C1309 -C1308 -C1307 -C1306 -C1305 -C1304 -C1303 -C1302 -C1301 -C1300 -C1299 -C1298 -C1297 -C1296 -C1295 -C1294 -C1293 -C1292 -C1291 -C1290 -C1289 -C1288 -C1287 -C1286 -C1285 -C1284 -C1283 -C1282 -C1281 -C1280 -C1279 C1278 -C1277 -C1276 -C1275 -C1274 -C1273 -C1272 -C1271 -C1270 -C1269 -C1268 -C1267 C1266 -C1265 -C1264 -C1263 -C1262 -C1261 -C1260 -C1259 -C1258 -C1257 -C1256 -C1255 -C1254 -C1253 -C1252 -C1251 -C1250 -C1249 C1248 -C1247 -C1246 -C1245 -C1244 -C1243 -C1242 -C1241 -C1240 -C1239 -C1238 -C1237 -C1236 -C1235 -C1234 -C1233 -C1232 -C1231 -C1230 -C1229 -C1228 -C1227 -C1226 -C1225 -C1224 -C1223 -C1222 -C1221 -C1220 -C1219 -C1218 -C1217 -C1216 -C1215 -C1214 -C1213 -C1212 -C1211 -C1210 -C1209 -C1208 C1207 -C1206 -C1205 -C1204 -C1203 -C1202 -C1201 -C1200 -C1199 -C1198 -C1197 -C1196 -C1195 -C1194 -C1193 C1192 -C1191 -C1190 -C1189 -C1188 -C1187 -C1186 -C1185 -C1184 -C1183 -C1182 -C1181 -C1180 -C1179 -C1178 -C1177 -C1176 -C1175 -C1174 -C1173 -C1172 -C1171 -C1170 -C1169 -C1168 -C1167 -C1166 -C1165 -C1164 -C1163 -C1162 -C1161 -C1160 C1159 -C1158 -C1157 -C1156 -C1155 -C1154 -C1153 -C1152 -C1151 -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 -C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 -C1122 C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 -C1087 -C1086 C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 -C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 -C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 -C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 -C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 C989 C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 -C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 C955 -C954 -C953 -C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 C833 -C832 -C831 -C830 C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 C712 -C711 -C710 -C709 -C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 -C604 -C603 -C602 C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C25#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.94 0.97 0.91 2/54 29612
Raw data (stat): 29612 (runsolver) R 29611 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423657140 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99972 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7374 0 0 0 977 21 0 0 25 0 1 0 423657140 32636928 7352 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7968 7352 603 41 0 7927 0
vsize: 31872
[startup+20.0008 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7609 0 0 0 1977 22 0 0 25 0 1 0 423657140 34099200 7587 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7587 603 41 0 8284 0
vsize: 33300
[startup+30.0011 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 2976 22 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+40.0016 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 3975 23 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+50.0027 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 4975 23 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+60.0019 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 5974 24 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223776 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+70.0025 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 6974 24 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223756 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+80.0037 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 7974 24 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+90.0038 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 8974 24 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+100.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 9974 25 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 10973 25 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 11973 25 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 12973 25 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223760 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+140.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 13973 25 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223696 134560579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7611 0 0 0 14973 26 0 0 25 0 1 0 423657140 34099200 7589 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7589 603 41 0 8284 0
vsize: 33300
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7640 0 0 0 15971 27 0 0 25 0 1 0 423657140 34099200 7600 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8325 7600 603 41 0 8284 0
vsize: 33300
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 7753 0 0 0 16971 27 0 0 25 0 1 0 423657140 34459648 7649 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8413 7649 603 41 0 8372 0
vsize: 33652
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 8162 0 0 0 17970 28 0 0 25 0 1 0 423657140 35934208 8025 4294967295 134512640 134672761 3221224560 3221223728 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8773 8025 603 41 0 8732 0
vsize: 35092
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 8641 0 0 0 18968 30 0 0 25 0 1 0 423657140 37793792 8471 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9227 8471 603 41 0 9186 0
vsize: 36908
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 9362 0 0 0 19967 32 0 0 25 0 1 0 423657140 40742912 9192 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9947 9192 603 41 0 9906 0
vsize: 39788
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 9894 0 0 0 20964 34 0 0 25 0 1 0 423657140 43020288 9724 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10503 9724 603 41 0 10462 0
vsize: 42012
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 10189 0 0 0 21963 35 0 0 25 0 1 0 423657140 43872256 9955 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10711 9955 603 41 0 10670 0
vsize: 42844
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 10762 0 0 0 22961 37 0 0 25 0 1 0 423657140 46292992 10528 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11302 10528 603 41 0 11261 0
vsize: 45208
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 11357 0 0 0 23960 38 0 0 25 0 1 0 423657140 48582656 11123 4294967295 134512640 134672761 3221224560 3221223712 134564785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11861 11123 603 41 0 11820 0
vsize: 47444
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 11872 0 0 0 24958 40 0 0 25 0 1 0 423657140 50737152 11638 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12387 11638 603 41 0 12346 0
vsize: 49548
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 12355 0 0 0 25956 42 0 0 25 0 1 0 423657140 52740096 12121 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12876 12121 603 41 0 12835 0
vsize: 51504
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 12944 0 0 0 26954 44 0 0 25 0 1 0 423657140 55148544 12710 4294967295 134512640 134672761 3221224560 3221223664 134559838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13464 12710 603 41 0 13423 0
vsize: 53856
[startup+280.195 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29612
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 13516 0 0 0 27971 46 0 0 25 0 1 0 423657140 57413632 13282 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14017 13282 603 41 0 13976 0
vsize: 56068
[startup+290.668 s]
Raw data (loadavg): 1.15 1.01 0.93 3/57 29653
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 13976 0 0 0 29015 49 0 0 25 0 1 0 423657140 59555840 13742 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14540 13742 603 41 0 14499 0
vsize: 58160
[startup+300.668 s]
Raw data (loadavg): 1.12 1.01 0.93 2/54 29665
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 14415 0 0 0 30014 50 0 0 25 0 1 0 423657140 61190144 14149 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14939 14149 603 41 0 14898 0
vsize: 59756
[startup+310.912 s]
Raw data (loadavg): 1.10 1.00 0.93 2/54 29665
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 14789 0 0 0 31037 51 0 0 25 0 1 0 423657140 62795776 14523 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15331 14523 603 41 0 15290 0
vsize: 61324
[startup+320.912 s]
Raw data (loadavg): 1.09 1.00 0.93 2/54 29665
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 15146 0 0 0 32037 52 0 0 25 0 1 0 423657140 64143360 14880 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15660 14880 603 41 0 15619 0
vsize: 62640
[startup+330.913 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 29665
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 15590 0 0 0 33036 53 0 0 25 0 1 0 423657140 66011136 15324 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16116 15324 603 41 0 16075 0
vsize: 64464
[startup+340.913 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 29665
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 16052 0 0 0 34035 54 0 0 25 0 1 0 423657140 67895296 15786 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16576 15786 603 41 0 16535 0
vsize: 66304
[startup+350.913 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 29665
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 16547 0 0 0 35034 55 0 0 25 0 1 0 423657140 69885952 16281 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17062 16281 603 41 0 17021 0
vsize: 68248
[startup+360.914 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 29665
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 16893 0 0 0 36033 56 0 0 25 0 1 0 423657140 71360512 16627 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17422 16627 603 41 0 17381 0
vsize: 69688
[startup+370.915 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 17345 0 0 0 37032 57 0 0 25 0 1 0 423657140 73093120 17079 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17845 17079 603 41 0 17804 0
vsize: 71380
[startup+380.914 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 17803 0 0 0 38031 59 0 0 25 0 1 0 423657140 74964992 17537 4294967295 134512640 134672761 3221224560 3221223696 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17537 603 41 0 18261 0
vsize: 73208
[startup+390.915 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 18114 0 0 0 39030 60 0 0 25 0 1 0 423657140 76304384 17848 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18629 17848 603 41 0 18588 0
vsize: 74516
[startup+400.915 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 18546 0 0 0 40030 61 0 0 25 0 1 0 423657140 78036992 18280 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19052 18280 603 41 0 19011 0
vsize: 76208
[startup+410.915 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 18994 0 0 0 41028 63 0 0 25 0 1 0 423657140 79900672 18728 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19507 18728 603 41 0 19466 0
vsize: 78028
[startup+420.916 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 19409 0 0 0 42027 64 0 0 25 0 1 0 423657140 81494016 19143 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19896 19143 603 41 0 19855 0
vsize: 79584
[startup+430.916 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 19770 0 0 0 43026 65 0 0 25 0 1 0 423657140 82960384 19504 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20254 19504 603 41 0 20213 0
vsize: 81016
[startup+440.917 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 20220 0 0 0 44026 66 0 0 25 0 1 0 423657140 84824064 19954 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20709 19954 603 41 0 20668 0
vsize: 82836
[startup+450.918 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 20639 0 0 0 45025 67 0 0 25 0 1 0 423657140 86544384 20373 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21129 20373 603 41 0 21088 0
vsize: 84516
[startup+460.917 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 21043 0 0 0 46025 67 0 0 25 0 1 0 423657140 88150016 20777 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21521 20777 603 41 0 21480 0
vsize: 86084
[startup+470.918 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 21472 0 0 0 47023 69 0 0 25 0 1 0 423657140 89890816 21206 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21946 21206 603 41 0 21905 0
vsize: 87784
[startup+480.917 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 21888 0 0 0 48023 69 0 0 25 0 1 0 423657140 91623424 21622 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22369 21622 603 41 0 22328 0
vsize: 89476
[startup+490.918 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22313 0 0 0 49021 71 0 0 25 0 1 0 423657140 93356032 22047 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22792 22047 603 41 0 22751 0
vsize: 91168
[startup+500.919 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 50020 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223664 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+510.918 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 51020 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+520.919 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 52020 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+530.919 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 53020 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+540.919 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 54021 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223732 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+550.92 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 55021 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+560.92 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 56021 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223664 134555076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+570.92 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 57021 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+580.919 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 58021 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+590.92 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 59022 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+600.921 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 60022 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+610.922 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 61022 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+620.922 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 62022 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+630.922 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 63022 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+640.922 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 64023 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+650.922 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 65023 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+660.922 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 66023 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+670.923 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29667
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 67023 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+680.923 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 68023 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+690.924 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 69024 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+700.924 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 70024 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+710.924 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 71024 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+720.925 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 72024 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+730.924 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 22705 0 0 0 73024 73 0 0 25 0 1 0 423657140 94785536 22406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22406 603 41 0 23100 0
vsize: 92564
[startup+740.925 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 23024 0 0 0 74023 74 0 0 25 0 1 0 423657140 96108544 22725 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23464 22725 603 41 0 23423 0
vsize: 93856
[startup+750.926 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 23411 0 0 0 75022 75 0 0 25 0 1 0 423657140 97697792 23112 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23852 23112 603 41 0 23811 0
vsize: 95408
[startup+760.925 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 23808 0 0 0 76021 77 0 0 25 0 1 0 423657140 99422208 23509 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24273 23509 603 41 0 24232 0
vsize: 97092
[startup+770.925 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 24200 0 0 0 77020 78 0 0 25 0 1 0 423657140 101007360 23901 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24660 23901 603 41 0 24619 0
vsize: 98640
[startup+780.926 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 24522 0 0 0 78020 79 0 0 25 0 1 0 423657140 102330368 24223 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24983 24223 603 41 0 24942 0
vsize: 99932
[startup+790.926 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 24826 0 0 0 79019 79 0 0 25 0 1 0 423657140 103538688 24527 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25278 24527 603 41 0 25237 0
vsize: 101112
[startup+800.927 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 25145 0 0 0 80018 81 0 0 25 0 1 0 423657140 104865792 24846 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25602 24846 603 41 0 25561 0
vsize: 102408
[startup+810.927 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 25507 0 0 0 81017 82 0 0 25 0 1 0 423657140 106328064 25208 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25959 25208 603 41 0 25918 0
vsize: 103836
[startup+820.927 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 25858 0 0 0 82016 83 0 0 25 0 1 0 423657140 107782144 25559 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26314 25559 603 41 0 26273 0
vsize: 105256
[startup+830.927 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 26205 0 0 0 83015 84 0 0 25 0 1 0 423657140 109244416 25906 4294967295 134512640 134672761 3221224560 3221223696 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26671 25906 603 41 0 26630 0
vsize: 106684
[startup+840.927 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 26514 0 0 0 84015 85 0 0 25 0 1 0 423657140 110456832 26215 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26967 26215 603 41 0 26926 0
vsize: 107868
[startup+850.928 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 26732 0 0 0 85014 85 0 0 25 0 1 0 423657140 111394816 26433 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27196 26433 603 41 0 27155 0
vsize: 108784
[startup+860.928 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 26978 0 0 0 86014 86 0 0 25 0 1 0 423657140 112463872 26679 4294967295 134512640 134672761 3221224560 3221223664 134555211 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27457 26679 603 41 0 27416 0
vsize: 109828
[startup+870.928 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 27358 0 0 0 87013 87 0 0 25 0 1 0 423657140 113917952 27059 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27812 27059 603 41 0 27771 0
vsize: 111248
[startup+880.928 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 27786 0 0 0 88012 88 0 0 25 0 1 0 423657140 115658752 27487 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28237 27487 603 41 0 28196 0
vsize: 112948
[startup+890.928 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 28226 0 0 0 89011 89 0 0 25 0 1 0 423657140 117530624 27927 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28694 27927 603 41 0 28653 0
vsize: 114776
[startup+900.929 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 28651 0 0 0 90010 90 0 0 25 0 1 0 423657140 119255040 28352 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29115 28352 603 41 0 29074 0
vsize: 116460
[startup+910.929 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 29041 0 0 0 91009 92 0 0 25 0 1 0 423657140 120852480 28742 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29505 28742 603 41 0 29464 0
vsize: 118020
[startup+920.929 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 29394 0 0 0 92008 93 0 0 25 0 1 0 423657140 122310656 29095 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29861 29095 603 41 0 29820 0
vsize: 119444
[startup+930.929 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 29739 0 0 0 93008 93 0 0 25 0 1 0 423657140 123645952 29440 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30187 29440 603 41 0 30146 0
vsize: 120748
[startup+940.928 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 30097 0 0 0 94007 95 0 0 25 0 1 0 423657140 125104128 29798 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30543 29798 603 41 0 30502 0
vsize: 122172
[startup+950.928 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 30493 0 0 0 95006 95 0 0 25 0 1 0 423657140 126705664 30194 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30934 30194 603 41 0 30893 0
vsize: 123736
[startup+960.929 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 30834 0 0 0 96005 96 0 0 25 0 1 0 423657140 128700416 30535 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31421 30535 603 41 0 31380 0
vsize: 125684
[startup+970.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 31077 0 0 0 97005 97 0 0 25 0 1 0 423657140 129630208 30778 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31648 30778 603 41 0 31607 0
vsize: 126592
[startup+980.929 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 31349 0 0 0 98004 98 0 0 25 0 1 0 423657140 130719744 31050 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31914 31050 603 41 0 31873 0
vsize: 127656
[startup+990.929 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 31616 0 0 0 99004 98 0 0 25 0 1 0 423657140 131792896 31317 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32176 31317 603 41 0 32135 0
vsize: 128704
[startup+1000.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 31841 0 0 0 100003 99 0 0 25 0 1 0 423657140 132718592 31542 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32402 31542 603 41 0 32361 0
vsize: 129608
[startup+1010.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 32051 0 0 0 101003 100 0 0 25 0 1 0 423657140 133652480 31752 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32630 31752 603 41 0 32589 0
vsize: 130520
[startup+1020.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 32230 0 0 0 102002 101 0 0 25 0 1 0 423657140 134316032 31931 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32792 31931 603 41 0 32751 0
vsize: 131168
[startup+1030.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 32503 0 0 0 103002 101 0 0 25 0 1 0 423657140 135516160 32204 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33085 32204 603 41 0 33044 0
vsize: 132340
[startup+1040.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 32827 0 0 0 104001 102 0 0 25 0 1 0 423657140 136843264 32528 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33409 32528 603 41 0 33368 0
vsize: 133636
[startup+1050.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 33133 0 0 0 105000 103 0 0 25 0 1 0 423657140 138047488 32834 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33703 32834 603 41 0 33662 0
vsize: 134812
[startup+1060.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 33426 0 0 0 105999 104 0 0 25 0 1 0 423657140 139251712 33127 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33997 33127 603 41 0 33956 0
vsize: 135988
[startup+1070.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 33665 0 0 0 106999 104 0 0 25 0 1 0 423657140 140181504 33366 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34224 33366 603 41 0 34183 0
vsize: 136896
[startup+1080.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 33917 0 0 0 107999 105 0 0 25 0 1 0 423657140 141254656 33618 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34486 33618 603 41 0 34445 0
vsize: 137944
[startup+1090.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 34180 0 0 0 108998 106 0 0 25 0 1 0 423657140 142315520 33881 4294967295 134512640 134672761 3221224560 3221223712 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34745 33881 603 41 0 34704 0
vsize: 138980
[startup+1100.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 34444 0 0 0 109998 106 0 0 25 0 1 0 423657140 143384576 34145 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35006 34145 603 41 0 34965 0
vsize: 140024
[startup+1110.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 34712 0 0 0 110997 107 0 0 25 0 1 0 423657140 144437248 34413 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35263 34413 603 41 0 35222 0
vsize: 141052
[startup+1120.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 35013 0 0 0 111997 108 0 0 25 0 1 0 423657140 145637376 34714 4294967295 134512640 134672761 3221224560 3221223664 134560355 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35556 34714 603 41 0 35515 0
vsize: 142224
[startup+1130.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 35313 0 0 0 112996 108 0 0 25 0 1 0 423657140 146841600 35014 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35850 35014 603 41 0 35809 0
vsize: 143400
[startup+1140.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 35624 0 0 0 113995 109 0 0 25 0 1 0 423657140 148168704 35325 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36174 35325 603 41 0 36133 0
vsize: 144696
[startup+1150.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 35886 0 0 0 114995 110 0 0 25 0 1 0 423657140 149229568 35587 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36433 35587 603 41 0 36392 0
vsize: 145732
[startup+1160.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 36173 0 0 0 115994 110 0 0 25 0 1 0 423657140 150421504 35874 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36724 35874 603 41 0 36683 0
vsize: 146896
[startup+1170.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 36468 0 0 0 116994 111 0 0 25 0 1 0 423657140 151605248 36169 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37013 36169 603 41 0 36972 0
vsize: 148052
[startup+1180.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 36762 0 0 0 117993 112 0 0 25 0 1 0 423657140 152801280 36463 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37305 36463 603 41 0 37264 0
vsize: 149220
[startup+1190.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 37032 0 0 0 118993 113 0 0 25 0 1 0 423657140 153853952 36733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37562 36733 603 41 0 37521 0
vsize: 150248
[startup+1200.93 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 29669
Raw data (stat): 29612 (minisat+) R 29611 22932 22931 0 -1 0 37296 0 0 0 119992 114 0 0 25 0 1 0 423657140 154923008 36997 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37823 36997 603 41 0 37782 0
vsize: 151292
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1201.01 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 29669
Raw data (stat): 29612 (minisat+) Z 29611 22932 22931 0 -1 12 37299 0 0 0 119992 120 0 0 25 0 1 0 423657140 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1201.01
CPU time (s): 1201.14
CPU user time (s): 1199.93
CPU system time (s): 1.20982
CPU usage (%): 100.011
Max. virtual memory (Kb): 151292
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####