PB'05 competition: run trace

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:
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.
SOLVER DATA
This is the output of the solver (stdout and stderr).
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.
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

Name	normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb59-26-opb/normalized-frb59-26-4.opb
MD5SUM	f6c01aa815aa7b4a79652c8bfa8bef11
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
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 numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.14
Number of variables	1534
Total number of constraints	127011
Number of constraints which are clauses	127011
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	2
Trace number 5273

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        900420 kB
Buffers:         33944 kB
Cached:          79340 kB
SwapCached:          4 kB
Active:          58528 kB
Inactive:        57640 kB
HighTotal:      131008 kB
HighFree:        47824 kB
LowTotal:       903652 kB
LowFree:        852596 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12428 kB
Committed_AS:    71672 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:30:37 (client local time) WITH STATUS 10 IN 1200.1 SECONDS
stats: 3736 7 1200.1 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 127011 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 |  127011   254022 |   42337       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 3034   maxlim: 39   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  147994   329008 |   49331       0        0     nan |  0.000 % |
c |       100 |  147976   328946 |   54264      95      847     8.9 |  0.088 % |
c |       250 |  147976   328946 |   59690     245     2174     8.9 |  0.088 % |
c |       475 |  147976   328946 |   65659     470     4451     9.5 |  0.089 % |
c |       813 |  147967   328915 |   72225     806     7277     9.0 |  0.111 % |
c |      1319 |  147967   328915 |   79448    1312    14497    11.0 |  0.110 % |
c |      2078 |  147895   328667 |   87392    2053    22805    11.1 |  0.286 % |
c |      3218 |  147877   328605 |   96132    3188    37259    11.7 |  0.330 % |
c |      4926 |  147811   328379 |  105745    4881    61573    12.6 |  0.506 % |
c |      7488 |  147664   327874 |  116319    7403    94596    12.8 |  0.880 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 40   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7525 |  147664   327885 |   49221    7437    95684    12.9 |  0.880 % |
c |      7625 |  147664   327885 |   54143    7537    96648    12.8 |  0.945 % |
c |      7775 |  147655   327854 |   59557    7685   100239    13.0 |  0.967 % |
c |      8000 |  147505   327340 |   65513    7874   103845    13.2 |  1.363 % |
c |      8337 |  147429   327076 |   72064    8188   108448    13.2 |  1.582 % |
c |      8843 |  147402   326983 |   79270    8687   117191    13.5 |  1.648 % |
c |      9602 |  147277   326554 |   87198    9417   129603    13.8 |  2.000 % |
c |     10742 |  147055   325792 |   95917   10494   147502    14.1 |  2.571 % |
c |     12450 |  146764   324797 |  105509   12126   182170    15.0 |  3.364 % |
c |     15012 |  146101   322522 |  116060   14460   240289    16.6 |  5.253 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 41   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16009 |  145765   321370 |   48588   15363   263532    17.2 |  5.253 % |
c |     16109 |  145729   321246 |   53446   15450   264661    17.1 |  6.482 % |
c |     16261 |  145703   321156 |   58791   15597   267699    17.2 |  6.570 % |
c |     16486 |  145530   320565 |   64670   15752   271388    17.2 |  7.119 % |
c |     16823 |  145360   319979 |   71137   16036   278704    17.4 |  7.735 % |
c |     17329 |  145325   319858 |   78251   16532   293485    17.8 |  7.844 % |
c |     18088 |  144904   318413 |   86076   17185   314507    18.3 |  9.383 % |
c |     19227 |  144581   317304 |   94684   18246   342083    18.7 | 10.503 % |
c |     20935 |  144152   315829 |  104152   19767   391297    19.8 | 11.977 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 42   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22445 |  143608   313942 |   47869   21107   459273    21.8 | 11.977 % |
c |     22545 |  143602   313922 |   52655   21204   462066    21.8 | 14.148 % |
c |     22698 |  143549   313739 |   57921   21336   466051    21.8 | 14.345 % |
c |     22925 |  143549   313739 |   63713   21563   476426    22.1 | 14.345 % |
c |     23263 |  143445   313377 |   70085   21853   484892    22.2 | 14.763 % |
c |     23769 |  143312   312918 |   77093   22296   500672    22.5 | 15.268 % |
c |     24528 |  143078   312108 |   84802   22950   522577    22.8 | 16.103 % |
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 43   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24641 |  143079   312114 |   47693   23063   530753    23.0 | 16.103 % |
c |     24741 |  143079   312114 |   52462   23163   532874    23.0 | 16.121 % |
c |     24892 |  143024   311925 |   57708   23298   536807    23.0 | 16.320 % |
c |     25117 |  142941   311638 |   63479   23468   543098    23.1 | 16.627 % |
c |     25455 |  142860   311359 |   69827   23763   550867    23.2 | 16.913 % |
c |     25961 |  142817   311210 |   76810   24241   563324    23.2 | 17.066 % |
c |     26721 |  142694   310785 |   84491   24918   600097    24.1 | 17.527 % |
c |     27860 |  142470   310007 |   92940   25921   640827    24.7 | 18.385 % |
c |     29569 |  142225   309166 |  102234   27499   699309    25.4 | 19.329 % |
c ==============================================================================
c [1mFound solution: -44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 44   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30493 |  142230   309190 |   47410   28423   803717    28.3 | 19.329 % |
c |     30595 |  142230   309190 |   52151   28525   807378    28.3 | 19.346 % |
c |     30747 |  142196   309076 |   57366   28671   810911    28.3 | 19.500 % |
c |     30972 |  142154   308930 |   63102   28886   816484    28.3 | 19.675 % |
c |     31310 |  141919   308111 |   69412   29150   829178    28.4 | 20.773 % |
c |     31816 |  141904   308060 |   76354   29616   910388    30.7 | 20.773 % |
c |     32575 |  141784   307638 |   83989   30287   959508    31.7 | 21.322 % |
c |     33716 |  141725   307427 |   92388   31374  1114799    35.5 | 21.586 % |
c |     35425 |  141655   307185 |  101627   32971  1191218    36.1 | 21.807 % |
c |     37987 |  141460   306508 |  111790   35378  1319442    37.3 | 22.574 % |
c |     41832 |  141296   305934 |  122969   39106  1549623    39.6 | 23.254 % |
c |     47599 |  141040   305048 |  135266   44718  2168510    48.5 | 24.308 % |
c ==============================================================================
c [1mFound solution: -45[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 45   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49444 |  140977   304837 |   46992   46442  2328396    50.1 | 24.308 % |
c |     49544 |  140955   304759 |   51691   46534  2331479    50.1 | 24.632 % |
c |     49694 |  140955   304759 |   56860   46684  2342914    50.2 | 24.634 % |
c |     49919 |  140955   304759 |   62546   46909  2355215    50.2 | 24.632 % |
c |     50257 |  140949   304739 |   68800   47243  2376749    50.3 | 24.654 % |
c |     50764 |  140914   304618 |   75681   47663  2418824    50.7 | 24.765 % |
c |     51523 |  140903   304579 |   83249   48418  2490464    51.4 | 24.808 % |
c |     52662 |  140903   304579 |   91574   49557  2628848    53.0 | 24.809 % |
c |     54370 |  140885   304517 |  100731   51205  2948502    57.6 | 24.853 % |
c |     56933 |  140844   304372 |  110804   53706  3304032    61.5 | 25.027 % |
c |     60777 |  140844   304372 |  121885   57550  4079767    70.9 | 25.027 % |
c ==============================================================================
c [1mFound solution: -46[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 46   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61878 |  140733   303998 |   46911   58516  4162562    71.1 | 25.027 % |
c |     61979 |  140733   303998 |   51602   17690  1852934   104.7 | 25.484 % |
c |     62129 |  140733   303998 |   56762   17840  1859319   104.2 | 25.484 % |
c |     62354 |  140733   303998 |   62438   18065  1867879   103.4 | 25.483 % |
c |     62691 |  140733   303998 |   68682   18402  1883038   102.3 | 25.484 % |
c |     63197 |  140678   303807 |   75550   18885  1898488   100.5 | 25.658 % |
c |     63956 |  140632   303645 |   83105   19637  1931778    98.4 | 25.879 % |
c |     65096 |  140619   303598 |   91416   20773  2021791    97.3 | 25.944 % |
c |     66804 |  140610   303567 |  100557   22466  2304384   102.6 | 25.967 % |
c |     69366 |  140526   303277 |  110613   25012  2489769    99.5 | 26.251 % |
c |     73211 |  140439   302980 |  121675   28801  3059406   106.2 | 26.538 % |
c |     78977 |  140412   302889 |  133842   34536  4098727   118.7 | 26.625 % |
c ==============================================================================
c [1mFound solution: -47[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 47   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     84042 |  140363   302719 |   46787   39579  4986501   126.0 | 26.625 % |
c |     84142 |  140363   302719 |   51465   39679  4989964   125.8 | 26.861 % |
c |     84292 |  140363   302719 |   56612   39829  5001459   125.6 | 26.861 % |
c |     84517 |  140337   302633 |   62273   40032  5015909   125.3 | 26.970 % |
c |     84854 |  140233   302269 |   68500   40314  5028729   124.7 | 27.364 % |
c |     85360 |  140233   302269 |   75350   40820  5067596   124.1 | 27.366 % |
c |     86121 |  140219   302221 |   82886   41571  5122882   123.2 | 27.430 % |
c |     87260 |  140219   302221 |   91174   42710  5247597   122.9 | 27.431 % |
c |     88968 |  140204   302170 |  100292   44411  5363258   120.8 | 27.474 % |
c |     91533 |  140204   302170 |  110321   46976  5699030   121.3 | 27.475 % |
c |     95377 |  140204   302170 |  121353   50820  6021764   118.5 | 27.474 % |
c |    101143 |  140187   302111 |  133488   56580  6669110   117.9 | 27.540 % |
c |    109792 |  140161   302021 |  146837   65208  7891848   121.0 | 27.628 % |
c |    122766 |  140161   302021 |  161521   78182 10629824   136.0 | 27.628 % |
c ==============================================================================
c [1mFound solution: -48[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 48   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    137807 |  140167   302047 |   46722   93223 13473394   144.5 | 27.628 % |
c |    137907 |  140167   302047 |   51394   16797  2507218   149.3 | 27.639 % |
c |    138057 |  140167   302047 |   56533   16947  2510122   148.1 | 27.638 % |
c |    138284 |  140167   302047 |   62186   17174  2527714   147.2 | 27.638 % |
c |    138621 |  140167   302047 |   68405   17511  2534953   144.8 | 27.638 % |
c |    139127 |  140167   302047 |   75246   18017  2559891   142.1 | 27.638 % |
c |    139888 |  140114   301866 |   82770   18763  2587108   137.9 | 27.814 % |
c |    141028 |  140102   301826 |   91047   19897  2642463   132.8 | 27.857 % |
c |    142736 |  140094   301798 |  100152   21602  2771316   128.3 | 27.901 % |
c |    145298 |  140015   301523 |  110168   24146  2916852   120.8 | 28.253 % |
c |    149142 |  139982   301410 |  121184   27952  3170633   113.4 | 28.341 % |
c |    154908 |  139897   301113 |  133303   33682  3712122   110.2 | 28.691 % |
c |    163557 |  139897   301113 |  146633   42331  5508374   130.1 | 28.692 % |
c |    176534 |  139813   300819 |  161297   55264  6910414   125.0 | 29.020 % |
c ==============================================================================
c [1mFound solution: -49[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 49   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    192954 |  139790   300744 |   46596   71633 10851641   151.5 | 29.020 % |
c |    193055 |  139790   300744 |   51255   15233  3335023   218.9 | 29.102 % |
c |    193205 |  139790   300744 |   56381   15383  3339462   217.1 | 29.101 % |
c |    193430 |  139784   300724 |   62019   15604  3343902   214.3 | 29.123 % |
c |    193767 |  139784   300724 |   68221   15941  3352894   210.3 | 29.123 % |
c |    194273 |  139784   300724 |   75043   16447  3387686   206.0 | 29.123 % |
c |    195032 |  139739   300571 |   82547   17198  3420145   198.9 | 29.256 % |
c |    196171 |  139739   300571 |   90802   18337  3474723   189.5 | 29.255 % |
c |    197880 |  139709   300465 |   99882   20027  3525154   176.0 | 29.386 % |
c |    200442 |  139703   300445 |  109870   22585  3655031   161.8 | 29.408 % |
c |    204287 |  139692   300406 |  120858   26423  3994130   151.2 | 29.453 % |
c |    210053 |  139692   300406 |  132943   32189  5128979   159.3 | 29.452 % |
c |    218704 |  139692   300406 |  146238   40840  7141599   174.9 | 29.453 % |
c |    231678 |  139594   300068 |  160862   53764  9040707   168.2 | 29.846 % |
c |    251139 |  139579   300017 |  176948   73219 12344721   168.6 | 29.890 % |
c |    280331 |  139529   299841 |  194643  102364 18561946   181.3 | 30.089 % |
c |    324121 |  139500   299738 |  214107  146147 25624511   175.3 | 30.241 % |
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 -C258#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.97 0.91 2/54 23663
Raw data (stat): 23663 (runsolver) R 23662 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421585555 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 5939 0 0 0 976 22 0 0 25 0 1 0 421585555 26357760 5917 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5917 603 41 0 6394 0
vsize: 25740
[startup+20.001 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 5939 0 0 0 1976 22 0 0 25 0 1 0 421585555 26357760 5917 4294967295 134512640 134672761 3221224560 3221223760 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5917 603 41 0 6394 0
vsize: 25740
[startup+30.0017 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 5939 0 0 0 2976 22 0 0 25 0 1 0 421585555 26357760 5917 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5917 603 41 0 6394 0
vsize: 25740
[startup+40.0014 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 5939 0 0 0 3975 23 0 0 25 0 1 0 421585555 26357760 5917 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5917 603 41 0 6394 0
vsize: 25740
[startup+50.0021 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 5939 0 0 0 4975 23 0 0 25 0 1 0 421585555 26357760 5917 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5917 603 41 0 6394 0
vsize: 25740
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 5939 0 0 0 5975 24 0 0 25 0 1 0 421585555 26357760 5917 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5917 603 41 0 6394 0
vsize: 25740
[startup+70.0025 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 5939 0 0 0 6975 24 0 0 25 0 1 0 421585555 26357760 5917 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5917 603 41 0 6394 0
vsize: 25740
[startup+80.0032 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 5939 0 0 0 7974 24 0 0 25 0 1 0 421585555 26357760 5917 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5917 603 41 0 6394 0
vsize: 25740
[startup+90.0029 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 5939 0 0 0 8974 25 0 0 25 0 1 0 421585555 26357760 5917 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5917 603 41 0 6394 0
vsize: 25740
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 5939 0 0 0 9974 25 0 0 25 0 1 0 421585555 26357760 5917 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6435 5917 603 41 0 6394 0
vsize: 25740
[startup+110.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 6685 0 0 0 10972 27 0 0 25 0 1 0 421585555 29315072 6663 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7157 6663 603 41 0 7116 0
vsize: 28628
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 7120 0 0 0 11970 29 0 0 25 0 1 0 421585555 31059968 7098 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7583 7098 603 41 0 7542 0
vsize: 30332
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 7120 0 0 0 12969 29 0 0 25 0 1 0 421585555 31059968 7098 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7583 7098 603 41 0 7542 0
vsize: 30332
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 7120 0 0 0 13969 29 0 0 25 0 1 0 421585555 31059968 7098 4294967295 134512640 134672761 3221224560 3221223664 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7583 7098 603 41 0 7542 0
vsize: 30332
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 7419 0 0 0 14968 31 0 0 25 0 1 0 421585555 32407552 7397 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7912 7397 603 41 0 7871 0
vsize: 31648
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 8054 0 0 0 15966 33 0 0 25 0 1 0 421585555 34959360 8032 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8535 8032 603 41 0 8494 0
vsize: 34140
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 8584 0 0 0 16964 35 0 0 25 0 1 0 421585555 37113856 8562 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9061 8562 603 41 0 9020 0
vsize: 36244
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 9126 0 0 0 17962 37 0 0 25 0 1 0 421585555 39403520 9104 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9620 9104 603 41 0 9579 0
vsize: 38480
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 9703 0 0 0 18960 39 0 0 25 0 1 0 421585555 41676800 9681 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10175 9681 603 41 0 10134 0
vsize: 40700
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 10320 0 0 0 19958 41 0 0 25 0 1 0 421585555 44228608 10298 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10798 10298 603 41 0 10757 0
vsize: 43192
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 10882 0 0 0 20956 43 0 0 25 0 1 0 421585555 46514176 10860 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11356 10860 603 41 0 11315 0
vsize: 45424
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 11505 0 0 0 21954 45 0 0 25 0 1 0 421585555 49307648 11483 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12038 11483 603 41 0 11997 0
vsize: 48152
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 12156 0 0 0 22952 47 0 0 25 0 1 0 421585555 51978240 12134 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12690 12134 603 41 0 12649 0
vsize: 50760
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 12889 0 0 0 23950 49 0 0 25 0 1 0 421585555 54927360 12867 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12867 603 41 0 13369 0
vsize: 53640
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 13538 0 0 0 24948 51 0 0 25 0 1 0 421585555 57622528 13516 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14068 13516 603 41 0 14027 0
vsize: 56272
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 13945 0 0 0 25946 52 0 0 25 0 1 0 421585555 59224064 13923 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14459 13923 603 41 0 14418 0
vsize: 57836
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 14576 0 0 0 26945 54 0 0 25 0 1 0 421585555 61915136 14554 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15116 14554 603 41 0 15075 0
vsize: 60464
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 15168 0 0 0 27943 56 0 0 25 0 1 0 421585555 64323584 15146 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15704 15146 603 41 0 15663 0
vsize: 62816
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 15805 0 0 0 28940 59 0 0 25 0 1 0 421585555 66871296 15783 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16326 15783 603 41 0 16285 0
vsize: 65304
[startup+300.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16412 0 0 0 29938 60 0 0 25 0 1 0 421585555 69279744 16390 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16914 16390 603 41 0 16873 0
vsize: 67656
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 30937 62 0 0 25 0 1 0 421585555 70737920 16743 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16743 603 41 0 17229 0
vsize: 69080
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 31936 62 0 0 25 0 1 0 421585555 70737920 16743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16743 603 41 0 17229 0
vsize: 69080
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 32936 62 0 0 25 0 1 0 421585555 70737920 16743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16743 603 41 0 17229 0
vsize: 69080
[startup+340.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 33936 63 0 0 25 0 1 0 421585555 70737920 16743 4294967295 134512640 134672761 3221224560 3221223728 134560745 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16743 603 41 0 17229 0
vsize: 69080
[startup+350.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 34935 63 0 0 25 0 1 0 421585555 70737920 16743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16743 603 41 0 17229 0
vsize: 69080
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 35935 63 0 0 25 0 1 0 421585555 70737920 16743 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16743 603 41 0 17229 0
vsize: 69080
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 36935 64 0 0 25 0 1 0 421585555 70737920 16743 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16743 603 41 0 17229 0
vsize: 69080
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 37934 64 0 0 25 0 1 0 421585555 70737920 16743 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16743 603 41 0 17229 0
vsize: 69080
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 38934 64 0 0 25 0 1 0 421585555 70737920 16743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16743 603 41 0 17229 0
vsize: 69080
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 39934 65 0 0 25 0 1 0 421585555 70737920 16743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16743 603 41 0 17229 0
vsize: 69080
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 40933 65 0 0 25 0 1 0 421585555 70737920 16743 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16743 603 41 0 17229 0
vsize: 69080
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 41933 66 0 0 25 0 1 0 421585555 70737920 16743 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17270 16743 603 41 0 17229 0
vsize: 69080
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 42932 66 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 43932 66 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 44932 66 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 45932 66 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 46931 67 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 47931 67 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 48931 67 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134561086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 49931 67 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 50930 68 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 51930 68 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 52929 69 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 53928 69 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 54928 70 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 55927 70 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 16765 0 0 0 56927 71 0 0 25 0 1 0 421585555 70733824 16743 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17269 16743 603 41 0 17228 0
vsize: 69076
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 17041 0 0 0 57926 72 0 0 25 0 1 0 421585555 71950336 17019 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17566 17019 603 41 0 17525 0
vsize: 70264
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 17483 0 0 0 58924 73 0 0 25 0 1 0 421585555 73703424 17461 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17994 17461 603 41 0 17953 0
vsize: 71976
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 18060 0 0 0 59922 75 0 0 25 0 1 0 421585555 76115968 18038 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18583 18038 603 41 0 18542 0
vsize: 74332
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 18655 0 0 0 60920 77 0 0 25 0 1 0 421585555 78536704 18633 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19174 18633 603 41 0 19133 0
vsize: 76696
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 19168 0 0 0 61919 79 0 0 25 0 1 0 421585555 80687104 19146 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19699 19146 603 41 0 19658 0
vsize: 78796
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 19755 0 0 0 62917 80 0 0 25 0 1 0 421585555 82964480 19733 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20255 19733 603 41 0 20214 0
vsize: 81020
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 20359 0 0 0 63915 82 0 0 25 0 1 0 421585555 85499904 20337 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20874 20337 603 41 0 20833 0
vsize: 83496
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 20966 0 0 0 64914 83 0 0 25 0 1 0 421585555 87924736 20944 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21466 20944 603 41 0 21425 0
vsize: 85864
[startup+660.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 21527 0 0 0 65912 84 0 0 25 0 1 0 421585555 90214400 21505 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22025 21505 603 41 0 21984 0
vsize: 88100
[startup+670.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 22085 0 0 0 66910 87 0 0 25 0 1 0 421585555 92491776 22063 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22581 22063 603 41 0 22540 0
vsize: 90324
[startup+680.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 22438 0 0 0 67909 87 0 0 25 0 1 0 421585555 93966336 22416 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22941 22416 603 41 0 22900 0
vsize: 91764
[startup+690.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 22860 0 0 0 68908 89 0 0 25 0 1 0 421585555 95707136 22838 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23366 22838 603 41 0 23325 0
vsize: 93464
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 23263 0 0 0 69906 90 0 0 25 0 1 0 421585555 97329152 23241 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23762 23241 603 41 0 23721 0
vsize: 95048
[startup+710.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 23683 0 0 0 70905 92 0 0 25 0 1 0 421585555 99078144 23661 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24189 23661 603 41 0 24148 0
vsize: 96756
[startup+720.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 24113 0 0 0 71904 93 0 0 25 0 1 0 421585555 100814848 24091 4294967295 134512640 134672761 3221224560 3221223724 134564515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24613 24091 603 41 0 24572 0
vsize: 98452
[startup+730.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 24467 0 0 0 72902 94 0 0 25 0 1 0 421585555 102301696 24445 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24976 24445 603 41 0 24935 0
vsize: 99904
[startup+740.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 24867 0 0 0 73901 96 0 0 25 0 1 0 421585555 103907328 24845 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25368 24845 603 41 0 25327 0
vsize: 101472
[startup+750.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 25245 0 0 0 74899 97 0 0 25 0 1 0 421585555 105385984 25223 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25729 25223 603 41 0 25688 0
vsize: 102916
[startup+760.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 25621 0 0 0 75898 98 0 0 25 0 1 0 421585555 107008000 25599 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26125 25599 603 41 0 26084 0
vsize: 104500
[startup+770.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 25888 0 0 0 76897 100 0 0 25 0 1 0 421585555 108089344 25866 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26389 25866 603 41 0 26348 0
vsize: 105556
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 26169 0 0 0 77896 100 0 0 25 0 1 0 421585555 109158400 26147 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26650 26147 603 41 0 26609 0
vsize: 106600
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 26532 0 0 0 78895 102 0 0 25 0 1 0 421585555 110641152 26510 4294967295 134512640 134672761 3221224560 3221223664 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27012 26510 603 41 0 26971 0
vsize: 108048
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 26913 0 0 0 79893 103 0 0 25 0 1 0 421585555 112246784 26891 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27404 26891 603 41 0 27363 0
vsize: 109616
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 27205 0 0 0 80892 104 0 0 25 0 1 0 421585555 113451008 27183 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27698 27183 603 41 0 27657 0
vsize: 110792
[startup+820.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 27559 0 0 0 81891 106 0 0 25 0 1 0 421585555 115322880 27537 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28155 27537 603 41 0 28114 0
vsize: 112620
[startup+830.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 27918 0 0 0 82889 107 0 0 25 0 1 0 421585555 116793344 27896 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28514 27896 603 41 0 28473 0
vsize: 114056
[startup+840.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 28143 0 0 0 83888 108 0 0 25 0 1 0 421585555 117735424 28121 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28744 28121 603 41 0 28703 0
vsize: 114976
[startup+850.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 28355 0 0 0 84887 110 0 0 25 0 1 0 421585555 118685696 28333 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28976 28333 603 41 0 28935 0
vsize: 115904
[startup+860.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 28666 0 0 0 85886 111 0 0 25 0 1 0 421585555 119885824 28644 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29269 28644 603 41 0 29228 0
vsize: 117076
[startup+870.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 28903 0 0 0 86885 111 0 0 25 0 1 0 421585555 120823808 28881 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29498 28881 603 41 0 29457 0
vsize: 117992
[startup+880.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 29211 0 0 0 87885 112 0 0 25 0 1 0 421585555 122171392 29189 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29827 29189 603 41 0 29786 0
vsize: 119308
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 29446 0 0 0 88884 112 0 0 25 0 1 0 421585555 123109376 29424 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30056 29424 603 41 0 30015 0
vsize: 120224
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 29629 0 0 0 89883 113 0 0 25 0 1 0 421585555 123785216 29607 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30221 29607 603 41 0 30180 0
vsize: 120884
[startup+910.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 29862 0 0 0 90883 114 0 0 25 0 1 0 421585555 124727296 29840 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30451 29840 603 41 0 30410 0
vsize: 121804
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 30205 0 0 0 91882 115 0 0 25 0 1 0 421585555 126205952 30183 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30812 30183 603 41 0 30771 0
vsize: 123248
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 30465 0 0 0 92882 115 0 0 25 0 1 0 421585555 127143936 30443 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31041 30443 603 41 0 31000 0
vsize: 124164
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 30663 0 0 0 93881 116 0 0 25 0 1 0 421585555 128090112 30641 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31272 30641 603 41 0 31231 0
vsize: 125088
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 30895 0 0 0 94881 117 0 0 25 0 1 0 421585555 129032192 30873 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31502 30873 603 41 0 31461 0
vsize: 126008
[startup+960.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 31185 0 0 0 95880 118 0 0 25 0 1 0 421585555 130232320 31163 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31795 31163 603 41 0 31754 0
vsize: 127180
[startup+970.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 31393 0 0 0 96880 118 0 0 25 0 1 0 421585555 131039232 31371 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31992 31371 603 41 0 31951 0
vsize: 127968
[startup+980.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 31721 0 0 0 97879 119 0 0 25 0 1 0 421585555 132378624 31699 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32319 31699 603 41 0 32278 0
vsize: 129276
[startup+990.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 31933 0 0 0 98879 120 0 0 25 0 1 0 421585555 133197824 31911 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32519 31911 603 41 0 32478 0
vsize: 130076
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 32222 0 0 0 99878 120 0 0 25 0 1 0 421585555 134406144 32200 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32814 32200 603 41 0 32773 0
vsize: 131256
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 32648 0 0 0 100877 121 0 0 25 0 1 0 421585555 136146944 32626 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33239 32626 603 41 0 33198 0
vsize: 132956
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 33003 0 0 0 101876 123 0 0 25 0 1 0 421585555 137621504 32981 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33599 32981 603 41 0 33558 0
vsize: 134396
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 33428 0 0 0 102875 124 0 0 25 0 1 0 421585555 139354112 33406 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34022 33406 603 41 0 33981 0
vsize: 136088
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 33830 0 0 0 103875 124 0 0 25 0 1 0 421585555 140972032 33808 4294967295 134512640 134672761 3221224560 3221223696 134560575 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34417 33808 603 41 0 34376 0
vsize: 137668
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 34189 0 0 0 104875 125 0 0 25 0 1 0 421585555 142434304 34167 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34774 34167 603 41 0 34733 0
vsize: 139096
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 34555 0 0 0 105873 126 0 0 25 0 1 0 421585555 143908864 34533 4294967295 134512640 134672761 3221224560 3221223664 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35134 34533 603 41 0 35093 0
vsize: 140536
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 34924 0 0 0 106872 127 0 0 25 0 1 0 421585555 145379328 34902 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35493 34902 603 41 0 35452 0
vsize: 141972
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 35292 0 0 0 107872 128 0 0 25 0 1 0 421585555 146972672 35270 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35882 35270 603 41 0 35841 0
vsize: 143528
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 35657 0 0 0 108871 129 0 0 25 0 1 0 421585555 148447232 35635 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36242 35635 603 41 0 36201 0
vsize: 144968
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 36041 0 0 0 109870 130 0 0 25 0 1 0 421585555 150052864 36019 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36634 36019 603 41 0 36593 0
vsize: 146536
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 36397 0 0 0 110869 131 0 0 25 0 1 0 421585555 151392256 36375 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36961 36375 603 41 0 36920 0
vsize: 147844
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 36747 0 0 0 111867 133 0 0 25 0 1 0 421585555 152870912 36725 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37322 36725 603 41 0 37281 0
vsize: 149288
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 37129 0 0 0 112866 134 0 0 25 0 1 0 421585555 154472448 37107 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37713 37107 603 41 0 37672 0
vsize: 150852
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 37504 0 0 0 113865 135 0 0 25 0 1 0 421585555 155951104 37482 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38074 37482 603 41 0 38033 0
vsize: 152296
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 37856 0 0 0 114864 137 0 0 25 0 1 0 421585555 157421568 37834 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38433 37834 603 41 0 38392 0
vsize: 153732
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 38238 0 0 0 115863 138 0 0 25 0 1 0 421585555 159019008 38216 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38823 38216 603 41 0 38782 0
vsize: 155292
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 38581 0 0 0 116862 139 0 0 25 0 1 0 421585555 160362496 38559 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39151 38559 603 41 0 39110 0
vsize: 156604
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 38910 0 0 0 117861 140 0 0 25 0 1 0 421585555 161742848 38888 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39488 38888 603 41 0 39447 0
vsize: 157952
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 39315 0 0 0 118861 141 0 0 25 0 1 0 421585555 163352576 39293 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39881 39293 603 41 0 39840 0
vsize: 159524
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23663
Raw data (stat): 23663 (minisat+) R 23662 20937 20936 0 -1 0 39705 0 0 0 119860 142 0 0 25 0 1 0 421585555 164962304 39683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40274 39683 603 41 0 40233 0
vsize: 161096
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 23663
Raw data (stat): 23663 (minisat+) Z 23662 20937 20936 0 -1 12 39708 0 0 0 119860 149 0 0 25 0 1 0 421585555 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.1
CPU time (s): 1200.1
CPU user time (s): 1198.61
CPU system time (s): 1.49477
CPU usage (%): 100
Max. virtual memory (Kb): 161096
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####