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/uclid_pb_benchmarks/normalized-ooo.burch_dill.6.accl.ucl.opb
MD5SUM	f306f9e77db4c563a096b79aebdedeaa
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	71
Number of bits of the biggest number in a constraint	7
Biggest sum of numbers in a constraint	261
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	23621
Total number of constraints	67526
Number of constraints which are clauses	65126
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2400
Minimum length of a constraint	1
Maximum length of a constraint	13
Trace number 5982

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-14 02:40:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4435 boxname=wulflinc7 idbench=299 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f306f9e77db4c563a096b79aebdedeaa  /oldhome/oroussel/tmp/wulflinc7/normalized-ooo.burch_dill.6.accl.ucl.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc7/normalized-ooo.burch_dill.6.accl.ucl.opb /oldhome/oroussel/tmp/wulflinc7/normalized-ooo.burch_dill.6.accl.ucl.opb
IDLAUNCH: 4435
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        874860 kB
Buffers:         38036 kB
Cached:         101704 kB
SwapCached:          0 kB
Active:          75112 kB
Inactive:        67536 kB
HighTotal:      131008 kB
HighFree:        25424 kB
LowTotal:       903652 kB
LowFree:        849436 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11592 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:00:36 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 4435 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 67525 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #########################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[67505]---> BDD-cost:    1
c ---[67500]---> BDD-cost:    1
c ---[67486]---> BDD-cost:    1
c ---[67478]---> BDD-cost:    1
c ---[67434]---> BDD-cost:    1
c ---[67426]---> BDD-cost:    1
c ---[67412]---> BDD-cost:    1
c ---[67368]---> BDD-cost:    1
c ---[67354]---> BDD-cost:    1
c ---[67280]---> BDD-cost:    1
c ---[67272]---> BDD-cost:    1
c ---[67258]---> BDD-cost:    1
c ---[67217]---> BDD-cost:    1
c ---[67179]---> BDD-cost:    1
c ---[67159]---> BDD-cost:    1
c ---[67055]---> BDD-cost:    1
c ---[67047]---> BDD-cost:    1
c ---[67033]---> BDD-cost:    1
c ---[66992]---> BDD-cost:    1
c ---[66954]---> BDD-cost:    1
c ---[66916]---> BDD-cost:    1
c ---[66890]---> BDD-cost:    1
c ---[66753]---> BDD-cost:    1
c ---[66745]---> BDD-cost:    1
c ---[66731]---> BDD-cost:    1
c ---[66690]---> BDD-cost:    1
c ---[66652]---> BDD-cost:    1
c ---[66614]---> BDD-cost:    1
c ---[66576]---> BDD-cost:    1
c ---[66544]---> BDD-cost:    1
c ---[66371]---> BDD-cost:    1
c ---[66363]---> BDD-cost:    1
c ---[66349]---> BDD-cost:    1
c ---[66308]---> BDD-cost:    1
c ---[66270]---> BDD-cost:    1
c ---[66232]---> BDD-cost:    1
c ---[66194]---> BDD-cost:    1
c ---[66156]---> BDD-cost:    1
c ---[66118]---> BDD-cost:    1
c ---[65879]---> BDD-cost:    1
c ---[65856]---> BDD-cost:    1
c ---[65848]---> BDD-cost:    1
c ---[65819]---> BDD-cost:    1
c ---[65811]---> BDD-cost:    1
c ---[65797]---> BDD-cost:    1
c ---[65774]---> BDD-cost:    1
c ---[65766]---> BDD-cost:    1
c ---[65758]---> BDD-cost:    1
c ---[65738]---> BDD-cost:    1
c ---[65706]---> BDD-cost:    1
c ---[65698]---> BDD-cost:    1
c ---[65690]---> BDD-cost:    1
c ---[65682]---> BDD-cost:    1
c ---[65656]---> BDD-cost:    1
c ---[65633]---> BDD-cost:    1
c ---[65625]---> BDD-cost:    1
c ---[65617]---> BDD-cost:    1
c ---[65609]---> BDD-cost:    1
c ---[65601]---> BDD-cost:    1
c ---[65569]---> BDD-cost:    1
c ---[65537]---> BDD-cost:    1
c ---[65529]---> BDD-cost:    1
c ---[65521]---> BDD-cost:    1
c ---[65513]---> BDD-cost:    1
c ---[65505]---> BDD-cost:    1
c ---[65497]---> BDD-cost:    1
c ---[65459]---> BDD-cost:    1
c ---[65436]---> BDD-cost:    1
c ---[65428]---> BDD-cost:    1
c ---[65420]---> BDD-cost:    1
c ---[65412]---> BDD-cost:    1
c ---[65404]---> BDD-cost:    1
c ---[65396]---> BDD-cost:    1
c ---[65388]---> BDD-cost:    1
c ---[65344]---> BDD-cost:    1
c ---[65312]---> BDD-cost:    1
c ---[65304]---> BDD-cost:    1
c ---[65296]---> BDD-cost:    1
c ---[65288]---> BDD-cost:    1
c ---[65280]---> BDD-cost:    1
c ---[65272]---> BDD-cost:    1
c ---[65264]---> BDD-cost:    1
c ---[65256]---> BDD-cost:    1
c ---[65206]---> BDD-cost:    1
c ---[65183]---> BDD-cost:    1
c ---[65175]---> BDD-cost:    1
c ---[65167]---> BDD-cost:    1
c ---[65159]---> BDD-cost:    1
c ---[65151]---> BDD-cost:    1
c ---[65143]---> BDD-cost:    1
c ---[65135]---> BDD-cost:    1
c ---[65127]---> BDD-cost:    1
c ---[65119]---> BDD-cost:    1
c ---[65063]---> BDD-cost:    1
c ---[65031]---> BDD-cost:    1
c ---[65023]---> BDD-cost:    1
c ---[65015]---> BDD-cost:    1
c ---[65007]---> BDD-cost:    1
c ---[64999]---> BDD-cost:    1
c ---[64991]---> BDD-cost:    1
c ---[64983]---> BDD-cost:    1
c ---[64975]---> BDD-cost:    1
c ---[64967]---> BDD-cost:    1
c ---[64959]---> BDD-cost:    1
c ---[64897]---> BDD-cost:    1
c ---[64874]---> BDD-cost:    1
c ---[64866]---> BDD-cost:    1
c ---[64858]---> BDD-cost:    1
c ---[64850]---> BDD-cost:    1
c ---[64842]---> BDD-cost:    1
c ---[64834]---> BDD-cost:    1
c ---[64826]---> BDD-cost:    1
c ---[64818]---> BDD-cost:    1
c ---[64810]---> BDD-cost:    1
c ---[64802]---> BDD-cost:    1
c ---[64794]---> BDD-cost:    1
c ---[64726]---> BDD-cost:    1
c ---[64697]---> BDD-cost:    1
c ---[64677]---> BDD-cost:    1
c ---[64660]---> BDD-cost:    1
c ---[64643]---> BDD-cost:    1
c ---[64626]---> BDD-cost:    1
c ---[64609]---> BDD-cost:    1
c ---[64592]---> BDD-cost:    1
c ---[64242]---> BDD-cost:    1
c ---[64234]---> BDD-cost:    1
c ---[64163]---> BDD-cost:    1
c ---[64092]---> BDD-cost:    1
c ---[64021]---> BDD-cost:    1
c ---[63950]---> BDD-cost:    1
c ---[63879]---> BDD-cost:    1
c ---[63815]---> BDD-cost:    1
c ---[63807]---> BDD-cost:    1
c ---[63802]---> BDD-cost:    1
c ---[63800]---> BDD-cost:    1
c ---[63786]---> BDD-cost:    1
c ---[63781]---> BDD-cost:    1
c ---[63776]---> BDD-cost:    1
c ---[63771]---> BDD-cost:    1
c ---[63766]---> BDD-cost:    1
c ---[63761]---> BDD-cost:    1
c ---[63756]---> BDD-cost:    1
c ---[63751]---> BDD-cost:    1
c ---[63746]---> BDD-cost:    1
c ---[63741]---> BDD-cost:    1
c ---[63736]---> BDD-cost:    1
c ---[63731]---> BDD-cost:    1
c ---[63648]---> BDD-cost:    1
c ---[63637]---> BDD-cost:    1
c ---[63596]---> BDD-cost:    1
c ---[63528]---> BDD-cost:    1
c ---[63433]---> BDD-cost:    1
c ---[63311]---> BDD-cost:    1
c ---[63174]---> BDD-cost:    1
c ---[63067]---> BDD-cost:    1
c ---[63014]---> BDD-cost:    1
c ---[63000]---> BDD-cost:    1
c ---[62983]---> BDD-cost:    1
c ---[62963]---> BDD-cost:    1
c ---[62940]---> BDD-cost:    1
c ---[62914]---> BDD-cost:    1
c ---[62885]---> BDD-cost:    1
c ---[62331]---> BDD-cost:    1
c ---[62128]---> BDD-cost:    1
c ---[62120]---> BDD-cost:    1
c ---[62112]---> BDD-cost:    1
c ---[62104]---> BDD-cost:    1
c ---[62096]---> BDD-cost:    1
c ---[62088]---> BDD-cost:    1
c ---[62080]---> BDD-cost:    1
c ---[62072]---> BDD-cost:    1
c ---[62064]---> BDD-cost:    1
c ---[62056]---> BDD-cost:    1
c ---[62048]---> BDD-cost:    1
c ---[62040]---> BDD-cost:    1
c ---[61951]---> BDD-cost:    1
c ---[61928]---> BDD-cost:    1
c ---[61920]---> BDD-cost:    1
c ---[61912]---> BDD-cost:    1
c ---[61904]---> BDD-cost:    1
c ---[61896]---> BDD-cost:    1
c ---[61888]---> BDD-cost:    1
c ---[61784]---> BDD-cost:    1
c ---[61776]---> BDD-cost:    1
c ---[61768]---> BDD-cost:    1
c ---[61760]---> BDD-cost:    1
c ---[61752]---> BDD-cost:    1
c ---[61744]---> BDD-cost:    1
c ---[61736]---> BDD-cost:    1
c ---[61728]---> BDD-cost:    1
c ---[61720]---> BDD-cost:    1
c ---[61712]---> BDD-cost:    1
c ---[61704]---> BDD-cost:    1
c ---[61696]---> BDD-cost:    1
c ---[61685]---> BDD-cost:    1
c ---[61599]---> BDD-cost:    1
c ---[61576]---> BDD-cost:    1
c ---[61556]---> BDD-cost:    1
c ---[61440]---> BDD-cost:    1
c ---[61369]---> BDD-cost:    1
c ---[61298]---> BDD-cost:    1
c ---[61227]---> BDD-cost:    1
c ---[61156]---> BDD-cost:    1
c ---[61085]---> BDD-cost:    1
c ---[61014]---> BDD-cost:    1
c ---[60943]---> BDD-cost:    1
c ---[60872]---> BDD-cost:    1
c ---[60801]---> BDD-cost:    1
c ---[60730]---> BDD-cost:    1
c ---[60659]---> BDD-cost:    1
c ---[60582]---> BDD-cost:    1
c ---[60457]---> BDD-cost:    1
c ---[60401]---> BDD-cost:    1
c ---[60384]---> BDD-cost:    1
c ---[60367]---> BDD-cost:    1
c ---[60350]---> BDD-cost:    1
c ---[60333]---> BDD-cost:    1
c ---[60316]---> BDD-cost:    1
c ---[60299]---> BDD-cost:    1
c ---[60282]---> BDD-cost:    1
c ---[60265]---> BDD-cost:    1
c ---[60248]---> BDD-cost:    1
c ---[60231]---> BDD-cost:    1
c ---[60214]---> BDD-cost:    1
c ---[60197]---> BDD-cost:    1
c ---[60048]---> BDD-cost:    1
c ---[59944]---> BDD-cost:    1
c ---[59918]---> BDD-cost:    1
c ---[59913]---> BDD-cost:    1
c ---[59908]---> BDD-cost:    1
c ---[59903]---> BDD-cost:    1
c ---[59883]---> BDD-cost:    1
c ---[59869]---> BDD-cost:    1
c ---[59837]---> BDD-cost:    1
c ---[59751]---> BDD-cost:    1
c ---[59542]---> BDD-cost:    1
c ---[59483]---> BDD-cost:    1
c ---[59199]---> BDD-cost:    1
c ---[59176]---> BDD-cost:    1
c ---[59153]---> BDD-cost:    1
c ---[59130]---> BDD-cost:    1
c ---[59107]---> BDD-cost:    1
c ---[59084]---> BDD-cost:    1
c ---[59061]---> BDD-cost:    1
c ---[59038]---> BDD-cost:    1
c ---[59015]---> BDD-cost:    1
c ---[58992]---> BDD-cost:    1
c ---[58969]---> BDD-cost:    1
c ---[58946]---> BDD-cost:    1
c ---[58923]---> BDD-cost:    1
c ---[58702]---> BDD-cost:    1
c ---[58586]---> BDD-cost:    1
c ---[58554]---> BDD-cost:    1
c ---[58549]---> BDD-cost:    1
c ---[58544]---> BDD-cost:    1
c ---[58539]---> BDD-cost:    1
c ---[58534]---> BDD-cost:    1
c ---[58508]---> BDD-cost:    1
c ---[58494]---> BDD-cost:    1
c ---[58474]---> BDD-cost:    1
c ---[58430]---> BDD-cost:    1
c ---[58302]---> BDD-cost:    1
c ---[58117]---> BDD-cost:    1
c ---[57800]---> BDD-cost:    1
c ---[57732]---> BDD-cost:    1
c ---[57460]---> BDD-cost:    1
c ---[57056]---> BDD-cost:    1
c ---[57027]---> BDD-cost:    1
c ---[56998]---> BDD-cost:    1
c ---[56969]---> BDD-cost:    1
c ---[56940]---> BDD-cost:    1
c ---[56911]---> BDD-cost:    1
c ---[56882]---> BDD-cost:    1
c ---[56853]---> BDD-cost:    1
c ---[56824]---> BDD-cost:    1
c ---[56795]---> BDD-cost:    1
c ---[56766]---> BDD-cost:    1
c ---[56737]---> BDD-cost:    1
c ---[56708]---> BDD-cost:    1
c ---[56415]---> BDD-cost:    1
c ---[56287]---> BDD-cost:    1
c ---[56249]---> BDD-cost:    1
c ---[56244]---> BDD-cost:    1
c ---[56239]---> BDD-cost:    1
c ---[56234]---> BDD-cost:    1
c ---[56229]---> BDD-cost:    1
c ---[56224]---> BDD-cost:    1
c ---[56192]---> BDD-cost:    1
c ---[56178]---> BDD-cost:    1
c ---[56158]---> BDD-cost:    1
c ---[56132]---> BDD-cost:    1
c ---[56076]---> BDD-cost:    1
c ---[55891]---> BDD-cost:    1
c ---[55664]---> BDD-cost:    1
c ---[55377]---> BDD-cost:    1
c ---[54895]---> BDD-cost:    1
c ---[54815]---> BDD-cost:    1
c ---[54519]---> BDD-cost:    1
c ---[54124]---> BDD-cost:    1
c ---[53546]---> BDD-cost:    1
c ---[53511]---> BDD-cost:    1
c ---[53476]---> BDD-cost:    1
c ---[53441]---> BDD-cost:    1
c ---[53406]---> BDD-cost:    1
c ---[53371]---> BDD-cost:    1
c ---[53336]---> BDD-cost:    1
c ---[53301]---> BDD-cost:    1
c ---[53266]---> BDD-cost:    1
c ---[53231]---> BDD-cost:    1
c ---[53196]---> BDD-cost:    1
c ---[53161]---> BDD-cost:    1
c ---[53126]---> BDD-cost:    1
c ---[52761]---> BDD-cost:    1
c ---[52621]---> BDD-cost:    1
c ---[52577]---> BDD-cost:    1
c ---[52572]---> BDD-cost:    1
c ---[52567]---> BDD-cost:    1
c ---[52562]---> BDD-cost:    1
c ---[52557]---> BDD-cost:    1
c ---[52552]---> BDD-cost:    1
c ---[52547]---> BDD-cost:    1
c ---[52509]---> BDD-cost:    1
c ---[52495]---> BDD-cost:    1
c ---[52475]---> BDD-cost:    1
c ---[52449]---> BDD-cost:    1
c ---[52417]---> BDD-cost:    1
c ---[52349]---> BDD-cost:    1
c ---[52095]---> BDD-cost:    1
c ---[51826]---> BDD-cost:    1
c ---[51485]---> BDD-cost:    1
c ---[51036]---> BDD-cost:    1
c ---[50353]---> BDD-cost:    1
c ---[50261]---> BDD-cost:    1
c ---[49941]---> BDD-cost:    1
c ---[49510]---> BDD-cost:    1
c ---[48941]---> BDD-cost:    1
c ---[48165]---> BDD-cost:    1
c ---[48124]---> BDD-cost:    1
c ---[48083]---> BDD-cost:    1
c ---[48042]---> BDD-cost:    1
c ---[48001]---> BDD-cost:    1
c ---[47960]---> BDD-cost:    1
c ---[47919]---> BDD-cost:    1
c ---[47878]---> BDD-cost:    1
c ---[47837]---> BDD-cost:    1
c ---[47796]---> BDD-cost:    1
c ---[47755]---> BDD-cost:    1
c ---[47714]---> BDD-cost:    1
c ---[47673]---> BDD-cost:    1
c ---[47236]---> BDD-cost:    1
c ---[47084]---> BDD-cost:    1
c ---[46869]---> BDD-cost:    1
c ---[46822]---> BDD-cost:    1
c ---[46775]---> BDD-cost:    1
c ---[46728]---> BDD-cost:    1
c ---[46681]---> BDD-cost:    1
c ---[46634]---> BDD-cost:    1
c ---[46587]---> BDD-cost:    1
c ---[46540]---> BDD-cost:    1
c ---[46493]---> BDD-cost:    1
c ---[46446]---> BDD-cost:    1
c ---[46399]---> BDD-cost:    1
c ---[46352]---> BDD-cost:    1
c ---[46341]---> BDD-cost:    1
c ---[46333]---> BDD-cost:    1
c ---[46328]---> BDD-cost:    1
c ---[46323]---> BDD-cost:    1
c ---[46318]---> BDD-cost:    1
c ---[46313]---> BDD-cost:    1
c ---[46161]---> BDD-cost:    1
c ---[46159]---> BDD-cost:    1
c ---[46157]---> BDD-cost:    1
c ---[46155]---> BDD-cost:    1
c ---[46150]---> BDD-cost:    1
c ---[46145]---> BDD-cost:    1
c ---[46143]---> BDD-cost:    1
c ---[46120]---> BDD-cost:    1
c ---[46118]---> BDD-cost:    1
c ---[46116]---> BDD-cost:    1
c ---[46114]---> BDD-cost:    1
c ---[46109]---> BDD-cost:    1
c ---[46104]---> BDD-cost:    1
c ---[46102]---> BDD-cost:    1
c ---[46070]---> BDD-cost:    1
c ---[46050]---> BDD-cost:    1
c ---[46048]---> BDD-cost:    1
c ---[46046]---> BDD-cost:    1
c ---[46041]---> BDD-cost:    1
c ---[46036]---> BDD-cost:    1
c ---[46034]---> BDD-cost:    1
c ---[46014]---> BDD-cost:    1
c ---[46012]---> BDD-cost:    1
c ---[46010]---> BDD-cost:    1
c ---[46005]---> BDD-cost:    1
c ---[46000]---> BDD-cost:    1
c ---[45998]---> BDD-cost:    1
c ---[45969]---> BDD-cost:    1
c ---[45931]---> BDD-cost:    1
c ---[45929]---> BDD-cost:    1
c ---[45924]---> BDD-cost:    1
c ---[45919]---> BDD-cost:    1
c ---[45917]---> BDD-cost:    1
c ---[45900]---> BDD-cost:    1
c ---[45898]---> BDD-cost:    1
c ---[45893]---> BDD-cost:    1
c ---[45888]---> BDD-cost:    1
c ---[45886]---> BDD-cost:    1
c ---[45860]---> BDD-cost:    1
c ---[45801]---> BDD-cost:    1
c ---[45796]---> BDD-cost:    1
c ---[45791]---> BDD-cost:    1
c ---[45789]---> BDD-cost:    1
c ---[45775]---> BDD-cost:    1
c ---[45770]---> BDD-cost:    1
c ---[45765]---> BDD-cost:    1
c ---[45763]---> BDD-cost:    1
c ---[45740]---> BDD-cost:    1
c ---[45654]---> BDD-cost:    1
c ---[45649]---> BDD-cost:    1
c ---[45647]---> BDD-cost:    1
c ---[45633]---> BDD-cost:    1
c ---[45628]---> BDD-cost:    1
c ---[45626]---> BDD-cost:    1
c ---[45606]---> BDD-cost:    1
c ---[45571]---> BDD-cost:    1
c ---[45350]---> BDD-cost:    1
c ---[45102]---> BDD-cost:    1
c ---[44812]---> BDD-cost:    1
c ---[44444]---> BDD-cost:    1
c ---[43959]---> BDD-cost:    1
c ---[43357]---> BDD-cost:    1
c ---[42617]---> BDD-cost:    1
c ---[42615]---> BDD-cost:    1
c ---[42613]---> BDD-cost:    1
c ---[42611]---> BDD-cost:    1
c ---[42609]---> BDD-cost:    1
c ---[42604]---> BDD-cost:    1
c ---[42599]---> BDD-cost:    1
c ---[42597]---> BDD-cost:    1
c ---[42460]---> BDD-cost:    1
c ---[42362]---> BDD-cost:    1
c ---[42030]---> BDD-cost:    1
c ---[41581]---> BDD-cost:    1
c ---[40988]---> BDD-cost:    1
c ---[40251]---> BDD-cost:    1
c ---[39358]---> BDD-cost:    1
c ---[39356]---> BDD-cost:    1
c ---[39354]---> BDD-cost:    1
c ---[39352]---> BDD-cost:    1
c ---[39350]---> BDD-cost:    1
c ---[39345]---> BDD-cost:    1
c ---[39340]---> BDD-cost:    1
c ---[39338]---> BDD-cost:    1
c ---[39297]---> BDD-cost:    1
c ---[39106]---> BDD-cost:    1
c ---[39101]---> BDD-cost:    1
c ---[39096]---> BDD-cost:    1
c ---[39091]---> BDD-cost:    1
c ---[39053]---> BDD-cost:    1
c ---[38847]---> BDD-cost:    1
c ---[38842]---> BDD-cost:    1
c ---[38837]---> BDD-cost:    1
c ---[38805]---> BDD-cost:    1
c ---[38593]---> BDD-cost:    1
c ---[38588]---> BDD-cost:    1
c ---[38562]---> BDD-cost:    1
c ---[38350]---> BDD-cost:    1
c ---[38330]---> BDD-cost:    1
c ---[38073]---> BDD-cost:    1
c ---[38041]---> BDD-cost:    1
c ---[37994]---> BDD-cost:    1
c ---[37932]---> BDD-cost:    1
c ---[37861]---> BDD-cost:    1
c ---[37859]---> BDD-cost:    1
c ---[37857]---> BDD-cost:    1
c ---[37855]---> BDD-cost:    1
c ---[37853]---> BDD-cost:    1
c ---[37851]---> BDD-cost:    1
c ---[37849]---> BDD-cost:    1
c ---[37418]---> BDD-cost:    1
c ---[37383]---> BDD-cost:    1
c ---[37318]---> BDD-cost:    1
c ---[37256]---> BDD-cost:    1
c ---[37197]---> BDD-cost:    1
c ---[37141]---> BDD-cost:    1
c ---[37088]---> BDD-cost:    1
c ---[36825]---> BDD-cost:    1
c ---[36802]---> BDD-cost:    1
c ---[36788]---> BDD-cost:    1
c ---[36774]---> BDD-cost:    1
c ---[36760]---> BDD-cost:    1
c ---[36746]---> BDD-cost:    1
c ---[36732]---> BDD-cost:    1
c ---[36718]---> BDD-cost:    1
c ---[36662]---> BDD-cost:    1
c ---[36396]---> BDD-cost:    1
c ---[36310]---> BDD-cost:    1
c ---[36299]---> BDD-cost:    1
c ---[36285]---> BDD-cost:    1
c ---[36271]---> BDD-cost:    1
c ---[36257]---> BDD-cost:    1
c ---[36243]---> BDD-cost:    1
c ---[36229]---> BDD-cost:    1
c ---[36215]---> BDD-cost:    1
c ---[36201]---> BDD-cost:    1
c ---[36187]---> BDD-cost:    1
c ---[36173]---> BDD-cost:    1
c ---[36159]---> BDD-cost:    1
c ---[36142]---> BDD-cost:    1
c ---[35993]---> BDD-cost:    1
c ---[35838]---> BDD-cost:    1
c ---[35830]---> BDD-cost:    1
c ---[35825]---> BDD-cost:    1
c ---[35820]---> BDD-cost:    1
c ---[35800]---> BDD-cost:    1
c ---[35786]---> BDD-cost:    1
c ---[35766]---> BDD-cost:    1
c ---[35746]---> BDD-cost:    1
c ---[35726]---> BDD-cost:    1
c ---[35706]---> BDD-cost:    1
c ---[35686]---> BDD-cost:    1
c ---[35672]---> BDD-cost:    1
c ---[35604]---> BDD-cost:    1
c ---[35359]---> BDD-cost:    1
c ---[35036]---> BDD-cost:    1
c ---[34953]---> BDD-cost:    1
c ---[34777]---> BDD-cost:    1
c ---[34760]---> BDD-cost:    1
c ---[34740]---> BDD-cost:    1
c ---[34720]---> BDD-cost:    1
c ---[34700]---> BDD-cost:    1
c ---[34680]---> BDD-cost:    1
c ---[34660]---> BDD-cost:    1
c ---[34640]---> BDD-cost:    1
c ---[34620]---> BDD-cost:    1
c ---[34600]---> BDD-cost:    1
c ---[34580]---> BDD-cost:    1
c ---[34560]---> BDD-cost:    1
c ---[34537]---> BDD-cost:    1
c ---[34316]---> BDD-cost:    1
c ---[34149]---> BDD-cost:    1
c ---[34141]---> BDD-cost:    1
c ---[34136]---> BDD-cost:    1
c ---[34131]---> BDD-cost:    1
c ---[34126]---> BDD-cost:    1
c ---[34100]---> BDD-cost:    1
c ---[34086]---> BDD-cost:    1
c ---[34066]---> BDD-cost:    1
c ---[34040]---> BDD-cost:    1
c ---[34014]---> BDD-cost:    1
c ---[33988]---> BDD-cost:    1
c ---[33962]---> BDD-cost:    1
c ---[33948]---> BDD-cost:    1
c ---[33928]---> BDD-cost:    1
c ---[33848]---> BDD-cost:    1
c ---[33522]---> BDD-cost:    1
c ---[33277]---> BDD-cost:    1
c ---[32777]---> BDD-cost:    1
c ---[32682]---> BDD-cost:    1
c ---[32509]---> BDD-cost:    1
c ---[32219]---> BDD-cost:    1
c ---[32196]---> BDD-cost:    1
c ---[32170]---> BDD-cost:    1
c ---[32144]---> BDD-cost:    1
c ---[32118]---> BDD-cost:    1
c ---[32092]---> BDD-cost:    1
c ---[32066]---> BDD-cost:    1
c ---[32040]---> BDD-cost:    1
c ---[32014]---> BDD-cost:    1
c ---[31988]---> BDD-cost:    1
c ---[31962]---> BDD-cost:    1
c ---[31936]---> BDD-cost:    1
c ---[31907]---> BDD-cost:    1
c ---[31614]---> BDD-cost:    1
c ---[31435]---> BDD-cost:    1
c ---[31427]---> BDD-cost:    1
c ---[31422]---> BDD-cost:    1
c ---[31417]---> BDD-cost:    1
c ---[31412]---> BDD-cost:    1
c ---[31407]---> BDD-cost:    1
c ---[31375]---> BDD-cost:    1
c ---[31361]---> BDD-cost:    1
c ---[31341]---> BDD-cost:    1
c ---[31315]---> BDD-cost:    1
c ---[31283]---> BDD-cost:    1
c ---[31251]---> BDD-cost:    1
c ---[31219]---> BDD-cost:    1
c ---[31205]---> BDD-cost:    1
c ---[31185]---> BDD-cost:    1
c ---[31159]---> BDD-cost:    1
c ---[31067]---> BDD-cost:    1
c ---[30648]---> BDD-cost:    1
c ---[30367]---> BDD-cost:    1
c ---[29948]---> BDD-cost:    1
c ---[29238]---> BDD-cost:    1
c ---[29131]---> BDD-cost:    1
c ---[28934]---> BDD-cost:    1
c ---[28647]---> BDD-cost:    1
c ---[28219]---> BDD-cost:    1
c ---[28190]---> BDD-cost:    1
c ---[28158]---> BDD-cost:    1
c ---[28126]---> BDD-cost:    1
c ---[28094]---> BDD-cost:    1
c ---[28062]---> BDD-cost:    1
c ---[28030]---> BDD-cost:    1
c ---[27998]---> BDD-cost:    1
c ---[27966]---> BDD-cost:    1
c ---[27934]---> BDD-cost:    1
c ---[27902]---> BDD-cost:    1
c ---[27870]---> BDD-cost:    1
c ---[27835]---> BDD-cost:    1
c ---[27470]---> BDD-cost:    1
c ---[27279]---> BDD-cost:    1
c ---[27151]---> BDD-cost:    1
c ---[27113]---> BDD-cost:    1
c ---[27075]---> BDD-cost:    1
c ---[27037]---> BDD-cost:    1
c ---[26999]---> BDD-cost:    1
c ---[26961]---> BDD-cost:    1
c ---[26923]---> BDD-cost:    1
c ---[26885]---> BDD-cost:    1
c ---[26847]---> BDD-cost:    1
c ---[26809]---> BDD-cost:    1
c ---[26771]---> BDD-cost:    1
c ---[26733]---> BDD-cost:    1
c ---[26689]---> BDD-cost:    1
c ---[26663]---> BDD-cost:    1
c ---[26658]---> BDD-cost:    1
c ---[26653]---> BDD-cost:    1
c ---[26648]---> BDD-cost:    1
c ---[26397]---> BDD-cost:    1
c ---[26395]---> BDD-cost:    1
c ---[26393]---> BDD-cost:    1
c ---[26391]---> BDD-cost:    1
c ---[26377]---> BDD-cost:    1
c ---[26375]---> BDD-cost:    1
c ---[26373]---> BDD-cost:    1
c ---[26371]---> BDD-cost:    1
c ---[26348]---> BDD-cost:    1
c ---[26268]---> BDD-cost:    1
c ---[26266]---> BDD-cost:    1
c ---[26264]---> BDD-cost:    1
c ---[26253]---> BDD-cost:    1
c ---[26251]---> BDD-cost:    1
c ---[26249]---> BDD-cost:    1
c ---[26229]---> BDD-cost:    1
c ---[26149]---> BDD-cost:    1
c ---[26147]---> BDD-cost:    1
c ---[26139]---> BDD-cost:    1
c ---[26137]---> BDD-cost:    1
c ---[26120]---> BDD-cost:    1
c ---[26040]---> BDD-cost:    1
c ---[26035]---> BDD-cost:    1
c ---[26021]---> BDD-cost:    1
c ---[25908]---> BDD-cost:    1
c ---[25705]---> BDD-cost:    1
c ---[25229]---> BDD-cost:    1
c ---[24912]---> BDD-cost:    1
c ---[24439]---> BDD-cost:    1
c ---[23813]---> BDD-cost:    1
c ---[23016]---> BDD-cost:    1
c ---[23014]---> BDD-cost:    1
c ---[23012]---> BDD-cost:    1
c ---[23010]---> BDD-cost:    1
c ---[23008]---> BDD-cost:    1
c ---[22838]---> BDD-cost:    1
c ---[22722]---> BDD-cost:    1
c ---[22501]---> BDD-cost:    1
c ---[22178]---> BDD-cost:    1
c ---[21753]---> BDD-cost:    1
c ---[21217]---> BDD-cost:    1
c ---[21215]---> BDD-cost:    1
c ---[21213]---> BDD-cost:    1
c ---[21211]---> BDD-cost:    1
c ---[21209]---> BDD-cost:    1
c ---[21177]---> BDD-cost:    1
c ---[20827]---> BDD-cost:    1
c ---[20822]---> BDD-cost:    1
c ---[20817]---> BDD-cost:    1
c ---[20782]---> BDD-cost:    1
c ---[20420]---> BDD-cost:    1
c ---[20415]---> BDD-cost:    1
c ---[20386]---> BDD-cost:    1
c ---[20015]---> BDD-cost:    1
c ---[19992]---> BDD-cost:    1
c ---[19603]---> BDD-cost:    1
c ---[19550]---> BDD-cost:    1
c ---[19188]---> BDD-cost:    1
c ---[18913]---> BDD-cost:    1
c ---[18674]---> BDD-cost:    1
c ---[18471]---> BDD-cost:    1
c ---[18439]---> BDD-cost:    1
c ---[17906]---> BDD-cost:    1
c ---[17724]---> BDD-cost:    1
c ---[17566]---> BDD-cost:    1
c ---[17432]---> BDD-cost:    1
c ---[17322]---> BDD-cost:    1
c ---[17236]---> BDD-cost:    1
c ---[16988]---> BDD-cost:    1
c ---[16734]---> BDD-cost:    1
c ---[16531]---> BDD-cost:    1
c ---[16346]---> BDD-cost:    1
c ---[16317]---> BDD-cost:    1
c ---[15946]---> BDD-cost:    1
c ---[15743]---> BDD-cost:    1
c ---[15564]---> BDD-cost:    1
c ---[15409]---> BDD-cost:    1
c ---[15278]---> BDD-cost:    1
c ---[15171]---> BDD-cost:    1
c ---[14911]---> BDD-cost:    1
c ---[14642]---> BDD-cost:    1
c ---[14430]---> BDD-cost:    1
c ---[14404]---> BDD-cost:    1
c ---[14069]---> BDD-cost:    1
c ---[13845]---> BDD-cost:    1
c ---[13645]---> BDD-cost:    1
c ---[13469]---> BDD-cost:    1
c ---[13317]---> BDD-cost:    1
c ---[13189]---> BDD-cost:    1
c ---[12917]---> BDD-cost:    1
c ---[12633]---> BDD-cost:    1
c ---[12610]---> BDD-cost:    1
c ---[12302]---> BDD-cost:    1
c ---[12057]---> BDD-cost:    1
c ---[11836]---> BDD-cost:    1
c ---[11639]---> BDD-cost:    1
c ---[11466]---> BDD-cost:    1
c ---[11317]---> BDD-cost:    1
c ---[11033]---> BDD-cost:    1
c ---[11013]---> BDD-cost:    1
c ---[10672]---> BDD-cost:    1
c ---[10406]---> BDD-cost:    1
c ---[10164]---> BDD-cost:    1
c ---[9946]---> BDD-cost:    1
c ---[9752]---> BDD-cost:    1
c ---[9582]---> BDD-cost:    1
c ---[9289]---> BDD-cost:    1
c ---[9266]---> BDD-cost:    1
c ---[8844]---> BDD-cost:    1
c ---[8521]---> BDD-cost:    1
c ---[8222]---> BDD-cost:    1
c ---[7947]---> BDD-cost:    1
c ---[7696]---> BDD-cost:    1
c ---[7328]---> BDD-cost:    1
c ---[7320]---> BDD-cost:    1
c ---[7294]---> BDD-cost:    1
c ---[7271]---> BDD-cost:    1
c ---[7221]---> BDD-cost:    1
c ---[7168]---> BDD-cost:    1
c ---[7151]---> BDD-cost:    1
c ---[7131]---> BDD-cost:    1
c ---[7108]---> BDD-cost:    1
c ---[7082]---> BDD-cost:    1
c ---[7053]---> BDD-cost:    1
c ---[7015]---> BDD-cost:    1
c ---[6998]---> BDD-cost:    1
c ---[6978]---> BDD-cost:    1
c ---[6955]---> BDD-cost:    1
c ---[6929]---> BDD-cost:    1
c ---[4908]---> BDD-cost:    1
c ---[4783]---> BDD-cost:    1
c ---[4685]---> BDD-cost:    1
c ---[4587]---> BDD-cost:    1
c ---[4489]---> BDD-cost:    1
c ---[4391]---> BDD-cost:    1
c ---[4350]---> BDD-cost:    1
c ---[4159]---> BDD-cost:    1
c ---[4061]---> BDD-cost:    1
c ---[3963]---> BDD-cost:    1
c ---[3865]---> BDD-cost:    1
c ---[3767]---> BDD-cost:    1
c ---[3726]---> BDD-cost:    1
c ---[3550]---> BDD-cost:    1
c ---[3377]---> BDD-cost:    1
c ---[3189]---> BDD-cost:    1
c ---[2986]---> BDD-cost:    1
c ---[2768]---> BDD-cost:    1
c ---[2399]---> BDD-cost:   17
c ---[2398]---> BDD-cost:    1
c ---[2397]---> BDD-cost:    1
c ---[2396]---> BDD-cost:   17
c ---[2395]---> BDD-cost:    1
c ---[2394]---> BDD-cost:    1
c ---[2393]---> BDD-cost:   17
c ---[2392]---> BDD-cost:    1
c ---[2391]---> BDD-cost:   14
c ---[2390]---> BDD-cost:   14
c ---[2389]---> BDD-cost:    1
c ---[2388]---> BDD-cost:    1
c ---[2387]---> BDD-cost:   17
c ---[2386]---> BDD-cost:    1
c ---[2385]---> BDD-cost:   14
c ---[2384]---> BDD-cost:   14
c ---[2383]---> BDD-cost:    1
c ---[2382]---> BDD-cost:    1
c ---[2381]---> BDD-cost:   17
c ---[2380]---> BDD-cost:    1
c ---[2379]---> BDD-cost:    1
c ---[2378]---> BDD-cost:   17
c ---[2377]---> BDD-cost:    1
c ---[2376]---> BDD-cost:    1
c ---[2375]---> BDD-cost:   17
c ---[2374]---> BDD-cost:    1
c ---[2373]---> BDD-cost:   24
c ---[2372]---> BDD-cost:    1
c ---[2371]---> BDD-cost:   21
c ---[2370]---> BDD-cost:    1
c ---[2369]---> BDD-cost:    1
c ---[2368]---> BDD-cost:    1
c ---[2367]---> BDD-cost:   14
c ---[2366]---> BDD-cost:   14
c ---[2365]---> BDD-cost:    1
c ---[2364]---> BDD-cost:    1
c ---[2363]---> BDD-cost:   14
c ---[2362]---> BDD-cost:   14
c ---[2361]---> BDD-cost:    1
c ---[2360]---> BDD-cost:    1
c ---[2359]---> BDD-cost:   14
c ---[2358]---> BDD-cost:   14
c ---[2357]---> BDD-cost:    1
c ---[2356]---> BDD-cost:    1
c ---[2355]---> BDD-cost:   14
c ---[2354]---> BDD-cost:   14
c ---[2353]---> BDD-cost:    1
c ---[2352]---> BDD-cost:    1
c ---[2351]---> BDD-cost:    1
c ---[2350]---> BDD-cost:    1
c ---[2349]---> BDD-cost:   21
c ---[2348]---> BDD-cost:    1
c ---[2347]---> BDD-cost:   24
c ---[2346]---> BDD-cost:    1
c ---[2345]---> BDD-cost:    1
c ---[2344]---> BDD-cost:    1
c ---[2343]---> BDD-cost:    1
c ---[2342]---> BDD-cost:    1
c ---[2341]---> BDD-cost:    1
c ---[2340]---> BDD-cost:   17
c ---[2339]---> BDD-cost:    1
c ---[2338]---> BDD-cost:    1
c ---[2337]---> BDD-cost:   17
c ---[2336]---> BDD-cost:    1
c ---[2335]---> BDD-cost:   21
c ---[2334]---> BDD-cost:    1
c ---[2333]---> BDD-cost:   21
c ---[2332]---> BDD-cost:    1
c ---[2331]---> BDD-cost:    1
c ---[2330]---> BDD-cost:    1
c ---[2329]---> BDD-cost:   14
c ---[2328]---> BDD-cost:   14
c ---[2327]---> BDD-cost:    1
c ---[2326]---> BDD-cost:    1
c ---[2325]---> BDD-cost:   14
c ---[2324]---> BDD-cost:   14
c ---[2323]---> BDD-cost:    1
c ---[2322]---> BDD-cost:    1
c ---[2321]---> BDD-cost:   14
c ---[2320]---> BDD-cost:   14
c ---[2319]---> BDD-cost:    1
c ---[2318]---> BDD-cost:    1
c ---[2317]---> BDD-cost:   14
c ---[2316]---> BDD-cost:   14
c ---[2315]---> BDD-cost:    1
c ---[2314]---> BDD-cost:    1
c ---[2313]---> BDD-cost:    1
c ---[2312]---> BDD-cost:    1
c ---[2311]---> BDD-cost:   21
c ---[2310]---> BDD-cost:    1
c ---[2309]---> BDD-cost:   21
c ---[2308]---> BDD-cost:    1
c ---[2307]---> BDD-cost:   24
c ---[2306]---> BDD-cost:    1
c ---[2305]---> BDD-cost:    1
c ---[2304]---> BDD-cost:    1
c ---[2303]---> BDD-cost:    1
c ---[2302]---> BDD-cost:    1
c ---[2301]---> BDD-cost:    1
c ---[2300]---> BDD-cost:    1
c ---[2299]---> BDD-cost:    1
c ---[2298]---> BDD-cost:    1
c ---[2297]---> BDD-cost:    1
c ---[2296]---> BDD-cost:   24
c ---[2295]---> BDD-cost:    1
c ---[2294]---> BDD-cost:    1
c ---[2293]---> BDD-cost:   17
c ---[2292]---> BDD-cost:    1
c ---[2291]---> BDD-cost:   19
c ---[2290]---> BDD-cost:    1
c ---[2289]---> BDD-cost:   16
c ---[2288]---> BDD-cost:    1
c ---[2287]---> BDD-cost:    1
c ---[2286]---> BDD-cost:    1
c ---[2285]---> BDD-cost:   14
c ---[2284]---> BDD-cost:   14
c ---[2283]---> BDD-cost:    1
c ---[2282]---> BDD-cost:    1
c ---[2281]---> BDD-cost:   14
c ---[2280]---> BDD-cost:   14
c ---[2279]---> BDD-cost:    1
c ---[2278]---> BDD-cost:    1
c ---[2277]---> BDD-cost:   14
c ---[2276]---> BDD-cost:   14
c ---[2275]---> BDD-cost:    1
c ---[2274]---> BDD-cost:    1
c ---[2273]---> BDD-cost:   14
c ---[2272]---> BDD-cost:   14
c ---[2271]---> BDD-cost:    1
c ---[2270]---> BDD-cost:    1
c ---[2269]---> BDD-cost:   14
c ---[2268]---> BDD-cost:   14
c ---[2267]---> BDD-cost:    1
c ---[2266]---> BDD-cost:    1
c ---[2265]---> BDD-cost:    1
c ---[2264]---> BDD-cost:    1
c ---[2263]---> BDD-cost:   16
c ---[2262]---> BDD-cost:    1
c ---[2261]---> BDD-cost:   19
c ---[2260]---> BDD-cost:    1
c ---[2259]---> BDD-cost:   19
c ---[2258]---> BDD-cost:    1
c ---[2257]---> BDD-cost:   22
c ---[2256]---> BDD-cost:    1
c ---[2255]---> BDD-cost:    1
c ---[2254]---> BDD-cost:    1
c ---[2253]---> BDD-cost:    1
c ---[2252]---> BDD-cost:    1
c ---[2251]---> BDD-cost:    1
c ---[2250]---> BDD-cost:    1
c ---[2249]---> BDD-cost:    1
c ---[2248]---> BDD-cost:    1
c ---[2247]---> BDD-cost:    1
c ---[2246]---> BDD-cost:    1
c ---[2245]---> BDD-cost:    1
c ---[2244]---> BDD-cost:    1
c ---[2243]---> BDD-cost:    1
c ---[2242]---> BDD-cost:   24
c ---[2241]---> BDD-cost:    1
c ---[2240]---> BDD-cost:    1
c ---[2239]---> BDD-cost:   17
c ---[2238]---> BDD-cost:    1
c ---[2237]---> BDD-cost:   16
c ---[2236]---> BDD-cost:    1
c ---[2235]---> BDD-cost:   16
c ---[2234]---> BDD-cost:    1
c ---[2233]---> BDD-cost:    1
c ---[2232]---> BDD-cost:    1
c ---[2231]---> BDD-cost:   14
c ---[2230]---> BDD-cost:   14
c ---[2229]---> BDD-cost:    1
c ---[2228]---> BDD-cost:    1
c ---[2227]---> BDD-cost:   14
c ---[2226]---> BDD-cost:   14
c ---[2225]---> BDD-cost:    1
c ---[2224]---> BDD-cost:    1
c ---[2223]---> BDD-cost:   14
c ---[2222]---> BDD-cost:   14
c ---[2221]---> BDD-cost:    1
c ---[2220]---> BDD-cost:    1
c ---[2219]---> BDD-cost:   14
c ---[2218]---> BDD-cost:   14
c ---[2217]---> BDD-cost:    1
c ---[2216]---> BDD-cost:    1
c ---[2215]---> BDD-cost:   14
c ---[2214]---> BDD-cost:   14
c ---[2213]---> BDD-cost:    1
c ---[2212]---> BDD-cost:    1
c ---[2211]---> BDD-cost:   14
c ---[2210]---> BDD-cost:   14
c ---[2209]---> BDD-cost:    1
c ---[2208]---> BDD-cost:    1
c ---[2207]---> BDD-cost:    1
c ---[2206]---> BDD-cost:    1
c ---[2205]---> BDD-cost:   16
c ---[2204]---> BDD-cost:    1
c ---[2203]---> BDD-cost:   16
c ---[2202]---> BDD-cost:    1
c ---[2201]---> BDD-cost:   19
c ---[2200]---> BDD-cost:    1
c ---[2199]---> BDD-cost:   19
c ---[2198]---> BDD-cost:    1
c ---[2197]---> BDD-cost:   22
c ---[2196]---> BDD-cost:    1
c ---[2195]---> BDD-cost:    1
c ---[2194]---> BDD-cost:    1
c ---[2193]---> BDD-cost:    1
c ---[2192]---> BDD-cost:    1
c ---[2191]---> BDD-cost:    1
c ---[2190]---> BDD-cost:    1
c ---[2189]---> BDD-cost:    1
c ---[2188]---> BDD-cost:    1
c ---[2187]---> BDD-cost:    1
c ---[2186]---> BDD-cost:    1
c ---[2185]---> BDD-cost:    1
c ---[2184]---> BDD-cost:    1
c ---[2183]---> BDD-cost:    1
c ---[2182]---> BDD-cost:    1
c ---[2181]---> BDD-cost:    1
c ---[2180]---> BDD-cost:    1
c ---[2179]---> BDD-cost:    1
c ---[2178]---> BDD-cost:   22
c ---[2177]---> BDD-cost:    1
c ---[2176]---> BDD-cost:    1
c ---[2175]---> BDD-cost:   17
c ---[2174]---> BDD-cost:    1
c ---[2173]---> BDD-cost:   16
c ---[2172]---> BDD-cost:    1
c ---[2171]---> BDD-cost:   16
c ---[2170]---> BDD-cost:    1
c ---[2169]---> BDD-cost:    1
c ---[2168]---> BDD-cost:    1
c ---[2167]---> BDD-cost:   14
c ---[2166]---> BDD-cost:   14
c ---[2165]---> BDD-cost:    1
c ---[2164]---> BDD-cost:    1
c ---[2163]---> BDD-cost:   14
c ---[2162]---> BDD-cost:   14
c ---[2161]---> BDD-cost:    1
c ---[2160]---> BDD-cost:    1
c ---[2159]---> BDD-cost:   14
c ---[2158]---> BDD-cost:   14
c ---[2157]---> BDD-cost:    1
c ---[2156]---> BDD-cost:    1
c ---[2155]---> BDD-cost:   14
c ---[2154]---> BDD-cost:   14
c ---[2153]---> BDD-cost:    1
c ---[2152]---> BDD-cost:    1
c ---[2151]---> BDD-cost:   14
c ---[2150]---> BDD-cost:   14
c ---[2149]---> BDD-cost:    1
c ---[2148]---> BDD-cost:    1
c ---[2147]---> BDD-cost:   14
c ---[2146]---> BDD-cost:   14
c ---[2145]---> BDD-cost:    1
c ---[2144]---> BDD-cost:    1
c ---[2143]---> BDD-cost:   14
c ---[2142]---> BDD-cost:   14
c ---[2141]---> BDD-cost:    1
c ---[2140]---> BDD-cost:    1
c ---[2139]---> BDD-cost:    1
c ---[2138]---> BDD-cost:    1
c ---[2137]---> BDD-cost:   16
c ---[2136]---> BDD-cost:    1
c ---[2135]---> BDD-cost:   16
c ---[2134]---> BDD-cost:    1
c ---[2133]---> BDD-cost:   16
c ---[2132]---> BDD-cost:    1
c ---[2131]---> BDD-cost:   21
c ---[2130]---> BDD-cost:    1
c ---[2129]---> BDD-cost:   21
c ---[2128]---> BDD-cost:    1
c ---[2127]---> BDD-cost:   24
c ---[2126]---> BDD-cost:    1
c ---[2125]---> BDD-cost:    1
c ---[2124]---> BDD-cost:    1
c ---[2123]---> BDD-cost:    1
c ---[2122]---> BDD-cost:    1
c ---[2121]---> BDD-cost:    1
c ---[2120]---> BDD-cost:    1
c ---[2119]---> BDD-cost:    1
c ---[2118]---> BDD-cost:    1
c ---[2117]---> BDD-cost:    1
c ---[2116]---> BDD-cost:    1
c ---[2115]---> BDD-cost:    1
c ---[2114]---> BDD-cost:    1
c ---[2113]---> BDD-cost:    1
c ---[2112]---> BDD-cost:    1
c ---[2111]---> BDD-cost:    1
c ---[2110]---> BDD-cost:    1
c ---[2109]---> BDD-cost:    1
c ---[2108]---> BDD-cost:    1
c ---[2107]---> BDD-cost:    1
c ---[2106]---> BDD-cost:    1
c ---[2105]---> BDD-cost:    1
c ---[2104]---> BDD-cost:   22
c ---[2103]---> BDD-cost:    1
c ---[2102]---> BDD-cost:    1
c ---[2101]---> BDD-cost:   17
c ---[2100]---> BDD-cost:    1
c ---[2099]---> BDD-cost:   11
c ---[2098]---> BDD-cost:    1
c ---[2097]---> BDD-cost:    1
c ---[2096]---> BDD-cost:    1
c ---[2095]---> BDD-cost:    1
c ---[2094]---> BDD-cost:    1
c ---[2093]---> BDD-cost:    1
c ---[2092]---> BDD-cost:   16
c ---[2091]---> BDD-cost:    1
c ---[2090]---> BDD-cost:    1
c ---[2089]---> BDD-cost:   17
c ---[2088]---> BDD-cost:    1
c ---[2087]---> BDD-cost:    1
c ---[2086]---> BDD-cost:   17
c ---[2085]---> BDD-cost:    1
c ---[2084]---> BDD-cost:    1
c ---[2083]---> BDD-cost:    1
c ---[2082]---> BDD-cost:    1
c ---[2081]---> BDD-cost:   17
c ---[2080]---> BDD-cost:    1
c ---[2079]---> BDD-cost:    1
c ---[2078]---> BDD-cost:   17
c ---[2077]---> BDD-cost:    1
c ---[2076]---> BDD-cost:    1
c ---[2075]---> BDD-cost:    1
c ---[2074]---> BDD-cost:    1
c ---[2073]---> BDD-cost:   17
c ---[2072]---> BDD-cost:   17
c ---[2071]---> BDD-cost:    1
c ---[2070]---> BDD-cost:    1
c ---[2069]---> BDD-cost:   17
c ---[2068]---> BDD-cost:    1
c ---[2067]---> BDD-cost:    1
c ---[2066]---> BDD-cost:   17
c ---[2065]---> BDD-cost:    1
c ---[2064]---> BDD-cost:    1
c ---[2063]---> BDD-cost:    1
c ---[2062]---> BDD-cost:    1
c ---[2061]---> BDD-cost:   17
c ---[2060]---> BDD-cost:   17
c ---[2059]---> BDD-cost:    1
c ---[2058]---> BDD-cost:    1
c ---[2057]---> BDD-cost:   17
c ---[2056]---> BDD-cost:   17
c ---[2055]---> BDD-cost:    1
c ---[2054]---> BDD-cost:    1
c ---[2053]---> BDD-cost:   17
c ---[2052]---> BDD-cost:    1
c ---[2051]---> BDD-cost:    1
c ---[2050]---> BDD-cost:   17
c ---[2049]---> BDD-cost:    1
c ---[2048]---> BDD-cost:    1
c ---[2047]---> BDD-cost:    1
c ---[2046]---> BDD-cost:    1
c ---[2045]---> BDD-cost:   17
c ---[2044]---> BDD-cost:   17
c ---[2043]---> BDD-cost:    1
c ---[2042]---> BDD-cost:    1
c ---[2041]---> BDD-cost:   17
c ---[2040]---> BDD-cost:   17
c ---[2039]---> BDD-cost:    1
c ---[2038]---> BDD-cost:    1
c ---[2037]---> BDD-cost:   17
c ---[2036]---> BDD-cost:   17
c ---[2035]---> BDD-cost:    1
c ---[2034]---> BDD-cost:    1
c ---[2033]---> BDD-cost:   17
c ---[2032]---> BDD-cost:    1
c ---[2031]---> BDD-cost:    1
c ---[2030]---> BDD-cost:   17
c ---[2029]---> BDD-cost:    1
c ---[2028]---> BDD-cost:    1
c ---[2027]---> BDD-cost:   21
c ---[2026]---> BDD-cost:    1
c ---[2025]---> BDD-cost:   17
c ---[2024]---> BDD-cost:   17
c ---[2023]---> BDD-cost:    1
c ---[2022]---> BDD-cost:    1
c ---[2021]---> BDD-cost:   17
c ---[2020]---> BDD-cost:   17
c ---[2019]---> BDD-cost:    1
c ---[2018]---> BDD-cost:    1
c ---[2017]---> BDD-cost:   17
c ---[2016]---> BDD-cost:   17
c ---[2015]---> BDD-cost:    1
c ---[2014]---> BDD-cost:    1
c ---[2013]---> BDD-cost:   17
c ---[2012]---> BDD-cost:   17
c ---[2011]---> BDD-cost:    1
c ---[2010]---> BDD-cost:    1
c ---[2009]---> BDD-cost:   17
c ---[2008]---> BDD-cost:    1
c ---[2007]---> BDD-cost:    1
c ---[2006]---> BDD-cost:   17
c ---[2005]---> BDD-cost:    1
c ---[2004]---> BDD-cost:    1
c ---[2003]---> BDD-cost:   21
c ---[2002]---> BDD-cost:    1
c ---[2001]---> BDD-cost:   17
c ---[2000]---> BDD-cost:   17
c ---[1999]---> BDD-cost:    1
c ---[1998]---> BDD-cost:    1
c ---[1997]---> BDD-cost:   17
c ---[1996]---> BDD-cost:   17
c ---[1995]---> BDD-cost:    1
c ---[1994]---> BDD-cost:    1
c ---[1993]---> BDD-cost:   17
c ---[1992]---> BDD-cost:   17
c ---[1991]---> BDD-cost:    1
c ---[1990]---> BDD-cost:    1
c ---[1989]---> BDD-cost:   17
c ---[1988]---> BDD-cost:   17
c ---[1987]---> BDD-cost:    1
c ---[1986]---> BDD-cost:    1
c ---[1985]---> BDD-cost:   17
c ---[1984]---> BDD-cost:   17
c ---[1983]---> BDD-cost:    1
c ---[1982]---> BDD-cost:    1
c ---[1981]---> BDD-cost:   17
c ---[1980]---> BDD-cost:    1
c ---[1979]---> BDD-cost:    1
c ---[1978]---> BDD-cost:   17
c ---[1977]---> BDD-cost:    1
c ---[1976]---> BDD-cost:    1
c ---[1975]---> BDD-cost:   21
c ---[1974]---> BDD-cost:    1
c ---[1973]---> BDD-cost:   17
c ---[1972]---> BDD-cost:   17
c ---[1971]---> BDD-cost:    1
c ---[1970]---> BDD-cost:    1
c ---[1969]---> BDD-cost:   17
c ---[1968]---> BDD-cost:   17
c ---[1967]---> BDD-cost:    1
c ---[1966]---> BDD-cost:    1
c ---[1965]---> BDD-cost:   17
c ---[1964]---> BDD-cost:   17
c ---[1963]---> BDD-cost:    1
c ---[1962]---> BDD-cost:    1
c ---[1961]---> BDD-cost:   17
c ---[1960]---> BDD-cost:   17
c ---[1959]---> BDD-cost:    1
c ---[1958]---> BDD-cost:    1
c ---[1957]---> BDD-cost:   17
c ---[1956]---> BDD-cost:   17
c ---[1955]---> BDD-cost:    1
c ---[1954]---> BDD-cost:    1
c ---[1953]---> BDD-cost:   17
c ---[1952]---> BDD-cost:   17
c ---[1951]---> BDD-cost:    1
c ---[1950]---> BDD-cost:    1
c ---[1949]---> BDD-cost:   17
c ---[1948]---> BDD-cost:    1
c ---[1947]---> BDD-cost:    1
c ---[1946]---> BDD-cost:   17
c ---[1945]---> BDD-cost:    1
c ---[1944]---> BDD-cost:    1
c ---[1943]---> BDD-cost:   21
c ---[1942]---> BDD-cost:    1
c ---[1941]---> BDD-cost:   17
c ---[1940]---> BDD-cost:   17
c ---[1939]---> BDD-cost:    1
c ---[1938]---> BDD-cost:    1
c ---[1937]---> BDD-cost:   17
c ---[1936]---> BDD-cost:   17
c ---[1935]---> BDD-cost:    1
c ---[1934]---> BDD-cost:    1
c ---[1933]---> BDD-cost:   17
c ---[1932]---> BDD-cost:   17
c ---[1931]---> BDD-cost:    1
c ---[1930]---> BDD-cost:    1
c ---[1929]---> BDD-cost:   17
c ---[1928]---> BDD-cost:   17
c ---[1927]---> BDD-cost:    1
c ---[1926]---> BDD-cost:    1
c ---[1925]---> BDD-cost:   17
c ---[1924]---> BDD-cost:   17
c ---[1923]---> BDD-cost:    1
c ---[1922]---> BDD-cost:    1
c ---[1921]---> BDD-cost:   17
c ---[1920]---> BDD-cost:   17
c ---[1919]---> BDD-cost:    1
c ---[1918]---> BDD-cost:    1
c ---[1917]---> BDD-cost:   17
c ---[1916]---> BDD-cost:   17
c ---[1915]---> BDD-cost:    1
c ---[1914]---> BDD-cost:    1
c ---[1913]---> BDD-cost:   17
c ---[1912]---> BDD-cost:    1
c ---[1911]---> BDD-cost:    1
c ---[1910]---> BDD-cost:   17
c ---[1909]---> BDD-cost:    1
c ---[1908]---> BDD-cost:    1
c ---[1907]---> BDD-cost:   16
c ---[1906]---> BDD-cost:    1
c ---[1905]---> BDD-cost:   17
c ---[1904]---> BDD-cost:   17
c ---[1903]---> BDD-cost:    1
c ---[1902]---> BDD-cost:    1
c ---[1901]---> BDD-cost:   17
c ---[1900]---> BDD-cost:   17
c ---[1899]---> BDD-cost:    1
c ---[1898]---> BDD-cost:    1
c ---[1897]---> BDD-cost:   17
c ---[1896]---> BDD-cost:   17
c ---[1895]---> BDD-cost:    1
c ---[1894]---> BDD-cost:    1
c ---[1893]---> BDD-cost:   17
c ---[1892]---> BDD-cost:   17
c ---[1891]---> BDD-cost:    1
c ---[1890]---> BDD-cost:    1
c ---[1889]---> BDD-cost:   17
c ---[1888]---> BDD-cost:   17
c ---[1887]---> BDD-cost:    1
c ---[1886]---> BDD-cost:    1
c ---[1885]---> BDD-cost:   17
c ---[1884]---> BDD-cost:   17
c ---[1883]---> BDD-cost:    1
c ---[1882]---> BDD-cost:    1
c ---[1881]---> BDD-cost:   17
c ---[1880]---> BDD-cost:   17
c ---[1879]---> BDD-cost:    1
c ---[1878]---> BDD-cost:    1
c ---[1877]---> BDD-cost:   17
c ---[1876]---> BDD-cost:   17
c ---[1875]---> BDD-cost:    1
c ---[1874]---> BDD-cost:    1
c ---[1873]---> BDD-cost:   17
c ---[1872]---> BDD-cost:    1
c ---[1871]---> BDD-cost:    1
c ---[1870]---> BDD-cost:   17
c ---[1869]---> BDD-cost:    1
c ---[1868]---> BDD-cost:    1
c ---[1867]---> BDD-cost:   16
c ---[1866]---> BDD-cost:    1
c ---[1865]---> BDD-cost:   17
c ---[1864]---> BDD-cost:   17
c ---[1863]---> BDD-cost:    1
c ---[1862]---> BDD-cost:    1
c ---[1861]---> BDD-cost:   17
c ---[1860]---> BDD-cost:   17
c ---[1859]---> BDD-cost:    1
c ---[1858]---> BDD-cost:    1
c ---[1857]---> BDD-cost:   17
c ---[1856]---> BDD-cost:   17
c ---[1855]---> BDD-cost:    1
c ---[1854]---> BDD-cost:    1
c ---[1853]---> BDD-cost:   17
c ---[1852]---> BDD-cost:   17
c ---[1851]---> BDD-cost:    1
c ---[1850]---> BDD-cost:    1
c ---[1849]---> BDD-cost:   17
c ---[1848]---> BDD-cost:   17
c ---[1847]---> BDD-cost:    1
c ---[1846]---> BDD-cost:    1
c ---[1845]---> BDD-cost:   17
c ---[1844]---> BDD-cost:   17
c ---[1843]---> BDD-cost:    1
c ---[1842]---> BDD-cost:    1
c ---[1841]---> BDD-cost:   17
c ---[1840]---> BDD-cost:   17
c ---[1839]---> BDD-cost:    1
c ---[1838]---> BDD-cost:    1
c ---[1837]---> BDD-cost:   17
c ---[1836]---> BDD-cost:   17
c ---[1835]---> BDD-cost:    1
c ---[1834]---> BDD-cost:    1
c ---[1833]---> BDD-cost:   17
c ---[1832]---> BDD-cost:   17
c ---[1831]---> BDD-cost:    1
c ---[1830]---> BDD-cost:    1
c ---[1829]---> BDD-cost:   17
c ---[1828]---> BDD-cost:    1
c ---[1827]---> BDD-cost:    1
c ---[1826]---> BDD-cost:   17
c ---[1825]---> BDD-cost:    1
c ---[1824]---> BDD-cost:    1
c ---[1823]---> BDD-cost:   16
c ---[1822]---> BDD-cost:    1
c ---[1821]---> BDD-cost:   17
c ---[1820]---> BDD-cost:   17
c ---[1819]---> BDD-cost:    1
c ---[1818]---> BDD-cost:    1
c ---[1817]---> BDD-cost:   17
c ---[1816]---> BDD-cost:   17
c ---[1815]---> BDD-cost:    1
c ---[1814]---> BDD-cost:    1
c ---[1813]---> BDD-cost:   17
c ---[1812]---> BDD-cost:   17
c ---[1811]---> BDD-cost:    1
c ---[1810]---> BDD-cost:    1
c ---[1809]---> BDD-cost:   17
c ---[1808]---> BDD-cost:   17
c ---[1807]---> BDD-cost:    1
c ---[1806]---> BDD-cost:    1
c ---[1805]---> BDD-cost:   17
c ---[1804]---> BDD-cost:   17
c ---[1803]---> BDD-cost:    1
c ---[1802]---> BDD-cost:    1
c ---[1801]---> BDD-cost:   17
c ---[1800]---> BDD-cost:   17
c ---[1799]---> BDD-cost:    1
c ---[1798]---> BDD-cost:    1
c ---[1797]---> BDD-cost:   17
c ---[1796]---> BDD-cost:   17
c ---[1795]---> BDD-cost:    1
c ---[1794]---> BDD-cost:    1
c ---[1793]---> BDD-cost:   17
c ---[1792]---> BDD-cost:   17
c ---[1791]---> BDD-cost:    1
c ---[1790]---> BDD-cost:    1
c ---[1789]---> BDD-cost:   17
c ---[1788]---> BDD-cost:   17
c ---[1787]---> BDD-cost:    1
c ---[1786]---> BDD-cost:    1
c ---[1785]---> BDD-cost:   17
c ---[1784]---> BDD-cost:   17
c ---[1783]---> BDD-cost:    1
c ---[1782]---> BDD-cost:    1
c ---[1781]---> BDD-cost:   17
c ---[1780]---> BDD-cost:    1
c ---[1779]---> BDD-cost:    1
c ---[1778]---> BDD-cost:   17
c ---[1777]---> BDD-cost:    1
c ---[1776]---> BDD-cost:    1
c ---[1775]---> BDD-cost:   16
c ---[1774]---> BDD-cost:    1
c ---[1773]---> BDD-cost:   17
c ---[1772]---> BDD-cost:   17
c ---[1771]---> BDD-cost:    1
c ---[1770]---> BDD-cost:    1
c ---[1769]---> BDD-cost:   17
c ---[1768]---> BDD-cost:   17
c ---[1767]---> BDD-cost:    1
c ---[1766]---> BDD-cost:    1
c ---[1765]---> BDD-cost:   17
c ---[1764]---> BDD-cost:   17
c ---[1763]---> BDD-cost:    1
c ---[1762]---> BDD-cost:    1
c ---[1761]---> BDD-cost:   17
c ---[1760]---> BDD-cost:   17
c ---[1759]---> BDD-cost:    1
c ---[1758]---> BDD-cost:    1
c ---[1757]---> BDD-cost:   17
c ---[1756]---> BDD-cost:   17
c ---[1755]---> BDD-cost:    1
c ---[1754]---> BDD-cost:    1
c ---[1753]---> BDD-cost:   17
c ---[1752]---> BDD-cost:   17
c ---[1751]---> BDD-cost:    1
c ---[1750]---> BDD-cost:    1
c ---[1749]---> BDD-cost:   17
c ---[1748]---> BDD-cost:   17
c ---[1747]---> BDD-cost:    1
c ---[1746]---> BDD-cost:    1
c ---[1745]---> BDD-cost:   17
c ---[1744]---> BDD-cost:   17
c ---[1743]---> BDD-cost:    1
c ---[1742]---> BDD-cost:    1
c ---[1741]---> BDD-cost:   17
c ---[1740]---> BDD-cost:   17
c ---[1739]---> BDD-cost:    1
c ---[1738]---> BDD-cost:    1
c ---[1737]---> BDD-cost:   17
c ---[1736]---> BDD-cost:   17
c ---[1735]---> BDD-cost:    1
c ---[1734]---> BDD-cost:    1
c ---[1733]---> BDD-cost:   17
c ---[1732]---> BDD-cost:   17
c ---[1731]---> BDD-cost:    1
c ---[1730]---> BDD-cost:    1
c ---[1729]---> BDD-cost:   14
c ---[1728]---> BDD-cost:   14
c ---[1727]---> BDD-cost:    1
c ---[1726]---> BDD-cost:    1
c ---[1725]---> BDD-cost:   14
c ---[1724]---> BDD-cost:   14
c ---[1723]---> BDD-cost:    1
c ---[1722]---> BDD-cost:    1
c ---[1721]---> BDD-cost:   14
c ---[1720]---> BDD-cost:   14
c ---[1719]---> BDD-cost:    1
c ---[1718]---> BDD-cost:    1
c ---[1717]---> BDD-cost:   14
c ---[1716]---> BDD-cost:   14
c ---[1715]---> BDD-cost:    1
c ---[1714]---> BDD-cost:    1
c ---[1713]---> BDD-cost:   14
c ---[1712]---> BDD-cost:   14
c ---[1711]---> BDD-cost:    1
c ---[1710]---> BDD-cost:    1
c ---[1709]---> BDD-cost:   14
c ---[1708]---> BDD-cost:   14
c ---[1707]---> BDD-cost:    1
c ---[1706]---> BDD-cost:    1
c ---[1705]---> BDD-cost:   14
c ---[1704]---> BDD-cost:   14
c ---[1703]---> BDD-cost:    1
c ---[1702]---> BDD-cost:    1
c ---[1701]---> BDD-cost:   14
c ---[1700]---> BDD-cost:   14
c ---[1699]---> BDD-cost:    1
c ---[1698]---> BDD-cost:    1
c ---[1697]---> BDD-cost:    1
c ---[1696]---> BDD-cost:    1
c ---[1695]---> BDD-cost:   11
c ---[1694]---> BDD-cost:    1
c ---[1693]---> BDD-cost:   11
c ---[1692]---> BDD-cost:    1
c ---[1691]---> BDD-cost:   11
c ---[1690]---> BDD-cost:    1
c ---[1689]---> BDD-cost:   11
c ---[1688]---> BDD-cost:    1
c ---[1687]---> BDD-cost:   17
c ---[1686]---> BDD-cost:    1
c ---[1685]---> BDD-cost:    1
c ---[1684]---> BDD-cost:   11
c ---[1683]---> BDD-cost:    1
c ---[1682]---> BDD-cost:    1
c ---[1681]---> BDD-cost:    1
c ---[1680]---> BDD-cost:   11
c ---[1679]---> BDD-cost:    1
c ---[1678]---> BDD-cost:    1
c ---[1677]---> BDD-cost:    1
c ---[1676]---> BDD-cost:   11
c ---[1675]---> BDD-cost:    1
c ---[1674]---> BDD-cost:    1
c ---[1673]---> BDD-cost:    1
c ---[1672]---> BDD-cost:   11
c ---[1671]---> BDD-cost:    1
c ---[1670]---> BDD-cost:    1
c ---[1669]---> BDD-cost:    1
c ---[1668]---> BDD-cost:   14
c ---[1667]---> BDD-cost:    1
c ---[1666]---> BDD-cost:    1
c ---[1665]---> BDD-cost:    1
c ---[1664]---> BDD-cost:   17
c ---[1663]---> BDD-cost:    1
c ---[1662]---> BDD-cost:    1
c ---[1661]---> BDD-cost:   17
c ---[1660]---> BDD-cost:    1
c ---[1659]---> BDD-cost:   17
c ---[1658]---> BDD-cost:   17
c ---[1657]---> BDD-cost:    1
c ---[1656]---> BDD-cost:    1
c ---[1655]---> BDD-cost:   17
c ---[1654]---> BDD-cost:   17
c ---[1653]---> BDD-cost:    1
c ---[1652]---> BDD-cost:    1
c ---[1651]---> BDD-cost:   17
c ---[1650]---> BDD-cost:   17
c ---[1649]---> BDD-cost:    1
c ---[1648]---> BDD-cost:    1
c ---[1647]---> BDD-cost:   17
c ---[1646]---> BDD-cost:   17
c ---[1645]---> BDD-cost:    1
c ---[1644]---> BDD-cost:    1
c ---[1643]---> BDD-cost:   17
c ---[1642]---> BDD-cost:   17
c ---[1641]---> BDD-cost:    1
c ---[1640]---> BDD-cost:    1
c ---[1639]---> BDD-cost:   17
c ---[1638]---> BDD-cost:   17
c ---[1637]---> BDD-cost:    1
c ---[1636]---> BDD-cost:    1
c ---[1635]---> BDD-cost:   17
c ---[1634]---> BDD-cost:   17
c ---[1633]---> BDD-cost:    1
c ---[1632]---> BDD-cost:    1
c ---[1631]---> BDD-cost:    1
c ---[1630]---> BDD-cost:    1
c ---[1629]---> BDD-cost:    1
c ---[1628]---> BDD-cost:    1
c ---[1627]---> BDD-cost:   16
c ---[1626]---> BDD-cost:    1
c ---[1625]---> BDD-cost:    1
c ---[1624]---> BDD-cost:    1
c ---[1623]---> BDD-cost:   16
c ---[1622]---> BDD-cost:    1
c ---[1621]---> BDD-cost:    1
c ---[1620]---> BDD-cost:    1
c ---[1619]---> BDD-cost:   16
c ---[1618]---> BDD-cost:    1
c ---[1617]---> BDD-cost:    1
c ---[1616]---> BDD-cost:    1
c ---[1615]---> BDD-cost:   21
c ---[1614]---> BDD-cost:    1
c ---[1613]---> BDD-cost:    1
c ---[1612]---> BDD-cost:    1
c ---[1611]---> BDD-cost:    1
c ---[1610]---> BDD-cost:    1
c ---[1609]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1607]---> BDD-cost:   21
c ---[1606]---> BDD-cost:    1
c ---[1605]---> BDD-cost:    1
c ---[1604]---> BDD-cost:    1
c ---[1603]---> BDD-cost:   21
c ---[1602]---> BDD-cost:    1
c ---[1601]---> BDD-cost:    1
c ---[1600]---> BDD-cost:    1
c ---[1599]---> BDD-cost:   21
c ---[1598]---> BDD-cost:    1
c ---[1597]---> BDD-cost:    1
c ---[1596]---> BDD-cost:    1
c ---[1595]---> BDD-cost:    1
c ---[1594]---> BDD-cost:    1
c ---[1593]---> BDD-cost:    1
c ---[1592]---> BDD-cost:    1
c ---[1591]---> BDD-cost:   16
c ---[1590]---> BDD-cost:    1
c ---[1589]---> BDD-cost:    1
c ---[1588]---> BDD-cost:    1
c ---[1587]---> BDD-cost:   16
c ---[1586]---> BDD-cost:    1
c ---[1585]---> BDD-cost:    1
c ---[1584]---> BDD-cost:    1
c ---[1583]---> BDD-cost:    1
c ---[1582]---> BDD-cost:    1
c ---[1581]---> BDD-cost:    1
c ---[1580]---> BDD-cost:    1
c ---[1579]---> BDD-cost:   16
c ---[1578]---> BDD-cost:    1
c ---[1577]---> BDD-cost:    1
c ---[1576]---> BDD-cost:    1
c ---[1575]---> BDD-cost:   16
c ---[1574]---> BDD-cost:    1
c ---[1573]---> BDD-cost:    1
c ---[1572]---> BDD-cost:    1
c ---[1571]---> BDD-cost:   14
c ---[1570]---> BDD-cost:   14
c ---[1569]---> BDD-cost:    1
c ---[1568]---> BDD-cost:    1
c ---[1567]---> BDD-cost:    1
c ---[1566]---> BDD-cost:    1
c ---[1565]---> BDD-cost:    0
c ---[1564]---> BDD-cost:    0
c ---[1563]---> BDD-cost:    1
c ---[1562]---> BDD-cost:    1
c ---[1561]---> BDD-cost:    0
c ---[1560]---> BDD-cost:    0
c ---[1559]---> BDD-cost:    0
c ---[1558]---> BDD-cost:    0
c ---[1557]---> BDD-cost:    0
c ---[1556]---> BDD-cost:    0
c ---[1555]---> BDD-cost:    0
c ---[1554]---> BDD-cost:    0
c ---[1553]---> BDD-cost:    1
c ---[1552]---> BDD-cost:    1
c ---[1551]---> BDD-cost:    1
c ---[1550]---> BDD-cost:    1
c ---[1549]---> BDD-cost:    1
c ---[1548]---> BDD-cost:    1
c ---[1547]---> BDD-cost:    1
c ---[1546]---> BDD-cost:    1
c ---[1545]---> BDD-cost:    1
c ---[1544]---> BDD-cost:    1
c ---[1543]---> BDD-cost:    1
c ---[1542]---> BDD-cost:    1
c ---[1541]---> BDD-cost:    1
c ---[1540]---> BDD-cost:    1
c ---[1539]---> BDD-cost:    1
c ---[1538]---> BDD-cost:    1
c ---[1537]---> BDD-cost:    1
c ---[1536]---> BDD-cost:    1
c ---[1535]---> BDD-cost:    1
c ---[1534]---> BDD-cost:    1
c ---[1533]---> BDD-cost:   14
c ---[1532]---> BDD-cost:   14
c ---[1531]---> BDD-cost:    1
c ---[1530]---> BDD-cost:    1
c ---[1529]---> BDD-cost:   16
c ---[1528]---> BDD-cost:    1
c ---[1527]---> BDD-cost:    1
c ---[1526]---> BDD-cost:    1
c ---[1525]---> BDD-cost:   14
c ---[1524]---> BDD-cost:   14
c ---[1523]---> BDD-cost:    1
c ---[1522]---> BDD-cost:    1
c ---[1521]---> BDD-cost:   14
c ---[1520]---> BDD-cost:   14
c ---[1519]---> BDD-cost:    1
c ---[1518]---> BDD-cost:    1
c ---[1517]---> BDD-cost:   14
c ---[1516]---> BDD-cost:   14
c ---[1515]---> BDD-cost:    1
c ---[1514]---> BDD-cost:    1
c ---[1513]---> BDD-cost:   14
c ---[1512]---> BDD-cost:   14
c ---[1511]---> BDD-cost:    1
c ---[1510]---> BDD-cost:    1
c ---[1509]---> BDD-cost:   14
c ---[1508]---> BDD-cost:   14
c ---[1507]---> BDD-cost:    1
c ---[1506]---> BDD-cost:    1
c ---[1505]---> BDD-cost:   14
c ---[1504]---> BDD-cost:   14
c ---[1503]---> BDD-cost:    1
c ---[1502]---> BDD-cost:    1
c ---[1501]---> BDD-cost:   14
c ---[1500]---> BDD-cost:   14
c ---[1499]---> BDD-cost:    1
c ---[1498]---> BDD-cost:    1
c ---[1497]---> BDD-cost:   16
c ---[1496]---> BDD-cost:    1
c ---[1495]---> BDD-cost:    1
c ---[1494]---> BDD-cost:    1
c ---[1493]---> BDD-cost:   16
c ---[1492]---> BDD-cost:    1
c ---[1491]---> BDD-cost:    1
c ---[1490]---> BDD-cost:    1
c ---[1489]---> BDD-cost:   16
c ---[1488]---> BDD-cost:    1
c ---[1487]---> BDD-cost:    1
c ---[1486]---> BDD-cost:    1
c ---[1485]---> BDD-cost:   16
c ---[1484]---> BDD-cost:    1
c ---[1483]---> BDD-cost:    1
c ---[1482]---> BDD-cost:    1
c ---[1481]---> BDD-cost:   16
c ---[1480]---> BDD-cost:    1
c ---[1479]---> BDD-cost:    1
c ---[1478]---> BDD-cost:    1
c ---[1477]---> BDD-cost:   16
c ---[1476]---> BDD-cost:    1
c ---[1475]---> BDD-cost:    1
c ---[1474]---> BDD-cost:    1
c ---[1473]---> BDD-cost:   16
c ---[1472]---> BDD-cost:    1
c ---[1471]---> BDD-cost:    1
c ---[1470]---> BDD-cost:    1
c ---[1469]---> BDD-cost:   14
c ---[1468]---> BDD-cost:   14
c ---[1467]---> BDD-cost:    1
c ---[1466]---> BDD-cost:    1
c ---[1465]---> BDD-cost:   14
c ---[1464]---> BDD-cost:   14
c ---[1463]---> BDD-cost:    1
c ---[1462]---> BDD-cost:    1
c ---[1461]---> BDD-cost:    0
c ---[1460]---> BDD-cost:    0
c ---[1459]---> BDD-cost:   17
c ---[1458]---> BDD-cost:   17
c ---[1457]---> BDD-cost:    1
c ---[1456]---> BDD-cost:    1
c ---[1455]---> BDD-cost:   17
c ---[1454]---> BDD-cost:   17
c ---[1453]---> BDD-cost:    1
c ---[1452]---> BDD-cost:    1
c ---[1451]---> BDD-cost:   17
c ---[1450]---> BDD-cost:   17
c ---[1449]---> BDD-cost:    1
c ---[1448]---> BDD-cost:    1
c ---[1447]---> BDD-cost:   17
c ---[1446]---> BDD-cost:   17
c ---[1445]---> BDD-cost:    1
c ---[1444]---> BDD-cost:    1
c ---[1443]---> BDD-cost:   17
c ---[1442]---> BDD-cost:   17
c ---[1441]---> BDD-cost:    1
c ---[1440]---> BDD-cost:    1
c ---[1439]---> BDD-cost:   17
c ---[1438]---> BDD-cost:   17
c ---[1437]---> BDD-cost:    1
c ---[1436]---> BDD-cost:    1
c ---[1435]---> BDD-cost:   17
c ---[1434]---> BDD-cost:   17
c ---[1433]---> BDD-cost:    1
c ---[1432]---> BDD-cost:    1
c ---[1431]---> BDD-cost:   17
c ---[1430]---> BDD-cost:   17
c ---[1429]---> BDD-cost:    1
c ---[1428]---> BDD-cost:    1
c ---[1427]---> BDD-cost:   17
c ---[1426]---> BDD-cost:   17
c ---[1425]---> BDD-cost:    1
c ---[1424]---> BDD-cost:    1
c ---[1423]---> BDD-cost:   17
c ---[1422]---> BDD-cost:   17
c ---[1421]---> BDD-cost:    1
c ---[1420]---> BDD-cost:    1
c ---[1419]---> BDD-cost:   17
c ---[1418]---> BDD-cost:   17
c ---[1417]---> BDD-cost:    1
c ---[1416]---> BDD-cost:    1
c ---[1415]---> BDD-cost:   17
c ---[1414]---> BDD-cost:   17
c ---[1413]---> BDD-cost:    1
c ---[1412]---> BDD-cost:    1
c ---[1411]---> BDD-cost:   17
c ---[1410]---> BDD-cost:    1
c ---[1409]---> BDD-cost:    1
c ---[1408]---> BDD-cost:   17
c ---[1407]---> BDD-cost:    1
c ---[1406]---> BDD-cost:    1
c ---[1405]---> BDD-cost:   17
c ---[1404]---> BDD-cost:    1
c ---[1403]---> BDD-cost:    1
c ---[1402]---> BDD-cost:   21
c ---[1401]---> BDD-cost:    1
c ---[1400]---> BDD-cost:    1
c ---[1399]---> BDD-cost:    1
c ---[1398]---> BDD-cost:   21
c ---[1397]---> BDD-cost:    1
c ---[1396]---> BDD-cost:    1
c ---[1395]---> BDD-cost:    1
c ---[1394]---> BDD-cost:   16
c ---[1393]---> BDD-cost:    1
c ---[1392]---> BDD-cost:    1
c ---[1391]---> BDD-cost:    1
c ---[1390]---> BDD-cost:   16
c ---[1389]---> BDD-cost:    1
c ---[1388]---> BDD-cost:    1
c ---[1387]---> BDD-cost:    1
c ---[1386]---> BDD-cost:   16
c ---[1385]---> BDD-cost:    1
c ---[1384]---> BDD-cost:    1
c ---[1383]---> BDD-cost:   17
c ---[1382]---> BDD-cost:   17
c ---[1381]---> BDD-cost:    1
c ---[1380]---> BDD-cost:    1
c ---[1379]---> BDD-cost:   17
c ---[1378]---> BDD-cost:   17
c ---[1377]---> BDD-cost:    1
c ---[1376]---> BDD-cost:    1
c ---[1375]---> BDD-cost:   17
c ---[1374]---> BDD-cost:   17
c ---[1373]---> BDD-cost:    1
c ---[1372]---> BDD-cost:    1
c ---[1371]---> BDD-cost:   17
c ---[1370]---> BDD-cost:   17
c ---[1369]---> BDD-cost:    1
c ---[1368]---> BDD-cost:    1
c ---[1367]---> BDD-cost:   17
c ---[1366]---> BDD-cost:   17
c ---[1365]---> BDD-cost:    1
c ---[1364]---> BDD-cost:    1
c ---[1363]---> BDD-cost:   17
c ---[1362]---> BDD-cost:   17
c ---[1361]---> BDD-cost:    1
c ---[1360]---> BDD-cost:    1
c ---[1359]---> BDD-cost:   17
c ---[1358]---> BDD-cost:   17
c ---[1357]---> BDD-cost:    1
c ---[1356]---> BDD-cost:    1
c ---[1355]---> BDD-cost:   17
c ---[1354]---> BDD-cost:   17
c ---[1353]---> BDD-cost:    1
c ---[1352]---> BDD-cost:    1
c ---[1351]---> BDD-cost:   17
c ---[1350]---> BDD-cost:   17
c ---[1349]---> BDD-cost:    1
c ---[1348]---> BDD-cost:    1
c ---[1347]---> BDD-cost:   17
c ---[1346]---> BDD-cost:   17
c ---[1345]---> BDD-cost:    1
c ---[1344]---> BDD-cost:    1
c ---[1343]---> BDD-cost:   17
c ---[1342]---> BDD-cost:   17
c ---[1341]---> BDD-cost:    1
c ---[1340]---> BDD-cost:    1
c ---[1339]---> BDD-cost:   17
c ---[1338]---> BDD-cost:   17
c ---[1337]---> BDD-cost:    1
c ---[1336]---> BDD-cost:    1
c ---[1335]---> BDD-cost:   17
c ---[1334]---> BDD-cost:   17
c ---[1333]---> BDD-cost:    1
c ---[1332]---> BDD-cost:    1
c ---[1331]---> BDD-cost:   17
c ---[1330]---> BDD-cost:   17
c ---[1329]---> BDD-cost:    1
c ---[1328]---> BDD-cost:    1
c ---[1327]---> BDD-cost:   17
c ---[1326]---> BDD-cost:   17
c ---[1325]---> BDD-cost:    1
c ---[1324]---> BDD-cost:    1
c ---[1323]---> BDD-cost:   17
c ---[1322]---> BDD-cost:   17
c ---[1321]---> BDD-cost:    1
c ---[1320]---> BDD-cost:    1
c ---[1319]---> BDD-cost:   17
c ---[1318]---> BDD-cost:   17
c ---[1317]---> BDD-cost:    1
c ---[1316]---> BDD-cost:    1
c ---[1315]---> BDD-cost:   17
c ---[1314]---> BDD-cost:   17
c ---[1313]---> BDD-cost:    1
c ---[1312]---> BDD-cost:    1
c ---[1311]---> BDD-cost:   17
c ---[1310]---> BDD-cost:   17
c ---[1309]---> BDD-cost:    1
c ---[1308]---> BDD-cost:    1
c ---[1307]---> BDD-cost:   17
c ---[1306]---> BDD-cost:   17
c ---[1305]---> BDD-cost:    1
c ---[1304]---> BDD-cost:    1
c ---[1303]---> BDD-cost:   17
c ---[1302]---> BDD-cost:   17
c ---[1301]---> BDD-cost:    1
c ---[1300]---> BDD-cost:    1
c ---[1299]---> BDD-cost:   17
c ---[1298]---> BDD-cost:   17
c ---[1297]---> BDD-cost:    1
c ---[1296]---> BDD-cost:    1
c ---[1295]---> BDD-cost:   17
c ---[1294]---> BDD-cost:   17
c ---[1293]---> BDD-cost:    1
c ---[1292]---> BDD-cost:    1
c ---[1291]---> BDD-cost:   17
c ---[1290]---> BDD-cost:   17
c ---[1289]---> BDD-cost:    1
c ---[1288]---> BDD-cost:    1
c ---[1287]---> BDD-cost:   17
c ---[1286]---> BDD-cost:   17
c ---[1285]---> BDD-cost:    1
c ---[1284]---> BDD-cost:    1
c ---[1283]---> BDD-cost:   17
c ---[1282]---> BDD-cost:   17
c ---[1281]---> BDD-cost:    1
c ---[1280]---> BDD-cost:    1
c ---[1279]---> BDD-cost:   17
c ---[1278]---> BDD-cost:   17
c ---[1277]---> BDD-cost:    1
c ---[1276]---> BDD-cost:    1
c ---[1275]---> BDD-cost:   17
c ---[1274]---> BDD-cost:   17
c ---[1273]---> BDD-cost:    1
c ---[1272]---> BDD-cost:    1
c ---[1271]---> BDD-cost:   17
c ---[1270]---> BDD-cost:   17
c ---[1269]---> BDD-cost:    1
c ---[1268]---> BDD-cost:    1
c ---[1267]---> BDD-cost:   17
c ---[1266]---> BDD-cost:   17
c ---[1265]---> BDD-cost:    1
c ---[1264]---> BDD-cost:    1
c ---[1263]---> BDD-cost:   17
c ---[1262]---> BDD-cost:   17
c ---[1261]---> BDD-cost:    1
c ---[1260]---> BDD-cost:    1
c ---[1259]---> BDD-cost:   17
c ---[1258]---> BDD-cost:   17
c ---[1257]---> BDD-cost:    1
c ---[1256]---> BDD-cost:    1
c ---[1255]---> BDD-cost:   17
c ---[1254]---> BDD-cost:   17
c ---[1253]---> BDD-cost:    1
c ---[1252]---> BDD-cost:    1
c ---[1251]---> BDD-cost:   17
c ---[1250]---> BDD-cost:   17
c ---[1249]---> BDD-cost:    1
c ---[1248]---> BDD-cost:    1
c ---[1247]---> BDD-cost:   17
c ---[1246]---> BDD-cost:   17
c ---[1245]---> BDD-cost:    1
c ---[1244]---> BDD-cost:    1
c ---[1243]---> BDD-cost:   17
c ---[1242]---> BDD-cost:   17
c ---[1241]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1239]---> BDD-cost:   17
c ---[1238]---> BDD-cost:   17
c ---[1237]---> BDD-cost:    1
c ---[1236]---> BDD-cost:    1
c ---[1235]---> BDD-cost:   17
c ---[1234]---> BDD-cost:   17
c ---[1233]---> BDD-cost:    1
c ---[1232]---> BDD-cost:    1
c ---[1231]---> BDD-cost:   17
c ---[1230]---> BDD-cost:   17
c ---[1229]---> BDD-cost:    1
c ---[1228]---> BDD-cost:    1
c ---[1227]---> BDD-cost:   17
c ---[1226]---> BDD-cost:   17
c ---[1225]---> BDD-cost:    1
c ---[1224]---> BDD-cost:    1
c ---[1223]---> BDD-cost:   17
c ---[1222]---> BDD-cost:   17
c ---[1221]---> BDD-cost:    1
c ---[1220]---> BDD-cost:    1
c ---[1219]---> BDD-cost:   17
c ---[1218]---> BDD-cost:   17
c ---[1217]---> BDD-cost:    1
c ---[1216]---> BDD-cost:    1
c ---[1215]---> BDD-cost:   17
c ---[1214]---> BDD-cost:   17
c ---[1213]---> BDD-cost:    1
c ---[1212]---> BDD-cost:    1
c ---[1211]---> BDD-cost:   17
c ---[1210]---> BDD-cost:   17
c ---[1209]---> BDD-cost:    1
c ---[1208]---> BDD-cost:    1
c ---[1207]---> BDD-cost:   17
c ---[1206]---> BDD-cost:   17
c ---[1205]---> BDD-cost:    1
c ---[1204]---> BDD-cost:    1
c ---[1203]---> BDD-cost:   17
c ---[1202]---> BDD-cost:   17
c ---[1201]---> BDD-cost:    1
c ---[1200]---> BDD-cost:    1
c ---[1199]---> BDD-cost:   17
c ---[1198]---> BDD-cost:   17
c ---[1197]---> BDD-cost:    1
c ---[1196]---> BDD-cost:    1
c ---[1195]---> BDD-cost:   17
c ---[1194]---> BDD-cost:   17
c ---[1193]---> BDD-cost:    1
c ---[1192]---> BDD-cost:    1
c ---[1191]---> BDD-cost:   17
c ---[1190]---> BDD-cost:   17
c ---[1189]---> BDD-cost:    1
c ---[1188]---> BDD-cost:    1
c ---[1187]---> BDD-cost:   17
c ---[1186]---> BDD-cost:   17
c ---[1185]---> BDD-cost:    1
c ---[1184]---> BDD-cost:    1
c ---[1183]---> BDD-cost:   17
c ---[1182]---> BDD-cost:   17
c ---[1181]---> BDD-cost:    1
c ---[1180]---> BDD-cost:    1
c ---[1179]---> BDD-cost:   17
c ---[1178]---> BDD-cost:   17
c ---[1177]---> BDD-cost:    1
c ---[1176]---> BDD-cost:    1
c ---[1175]---> BDD-cost:   17
c ---[1174]---> BDD-cost:   17
c ---[1173]---> BDD-cost:    1
c ---[1172]---> BDD-cost:    1
c ---[1171]---> BDD-cost:   17
c ---[1170]---> BDD-cost:   17
c ---[1169]---> BDD-cost:    1
c ---[1168]---> BDD-cost:    1
c ---[1167]---> BDD-cost:   17
c ---[1166]---> BDD-cost:   17
c ---[1165]---> BDD-cost:    1
c ---[1164]---> BDD-cost:    1
c ---[1163]---> BDD-cost:   17
c ---[1162]---> BDD-cost:   17
c ---[1161]---> BDD-cost:    1
c ---[1160]---> BDD-cost:    1
c ---[1159]---> BDD-cost:   17
c ---[1158]---> BDD-cost:   17
c ---[1157]---> BDD-cost:    1
c ---[1156]---> BDD-cost:    1
c ---[1155]---> BDD-cost:   17
c ---[1154]---> BDD-cost:   17
c ---[1153]---> BDD-cost:    1
c ---[1152]---> BDD-cost:    1
c ---[1151]---> BDD-cost:   17
c ---[1150]---> BDD-cost:   17
c ---[1149]---> BDD-cost:    1
c ---[1148]---> BDD-cost:    1
c ---[1147]---> BDD-cost:   17
c ---[1146]---> BDD-cost:   17
c ---[1145]---> BDD-cost:    1
c ---[1144]---> BDD-cost:    1
c ---[1143]---> BDD-cost:   17
c ---[1142]---> BDD-cost:   17
c ---[1141]---> BDD-cost:    1
c ---[1140]---> BDD-cost:    1
c ---[1139]---> BDD-cost:   17
c ---[1138]---> BDD-cost:   17
c ---[1137]---> BDD-cost:    1
c ---[1136]---> BDD-cost:    1
c ---[1135]---> BDD-cost:   17
c ---[1134]---> BDD-cost:   17
c ---[1133]---> BDD-cost:    1
c ---[1132]---> BDD-cost:    1
c ---[1131]---> BDD-cost:   17
c ---[1130]---> BDD-cost:   17
c ---[1129]---> BDD-cost:    1
c ---[1128]---> BDD-cost:    1
c ---[1127]---> BDD-cost:   17
c ---[1126]---> BDD-cost:   17
c ---[1125]---> BDD-cost:    1
c ---[1124]---> BDD-cost:    1
c ---[1123]---> BDD-cost:   17
c ---[1122]---> BDD-cost:   17
c ---[1121]---> BDD-cost:    1
c ---[1120]---> BDD-cost:    1
c ---[1119]---> BDD-cost:   17
c ---[1118]---> BDD-cost:   17
c ---[1117]---> BDD-cost:    1
c ---[1116]---> BDD-cost:    1
c ---[1115]---> BDD-cost:   17
c ---[1114]---> BDD-cost:   17
c ---[1113]---> BDD-cost:    1
c ---[1112]---> BDD-cost:    1
c ---[1111]---> BDD-cost:   17
c ---[1110]---> BDD-cost:   17
c ---[1109]---> BDD-cost:    1
c ---[1108]---> BDD-cost:    1
c ---[1107]---> BDD-cost:   17
c ---[1106]---> BDD-cost:   17
c ---[1105]---> BDD-cost:    1
c ---[1104]---> BDD-cost:    1
c ---[1103]---> BDD-cost:   17
c ---[1102]---> BDD-cost:   17
c ---[1101]---> BDD-cost:    1
c ---[1100]---> BDD-cost:    1
c ---[1099]---> BDD-cost:   17
c ---[1098]---> BDD-cost:   17
c ---[1097]---> BDD-cost:    1
c ---[1096]---> BDD-cost:    1
c ---[1095]---> BDD-cost:   17
c ---[1094]---> BDD-cost:   17
c ---[1093]---> BDD-cost:    1
c ---[1092]---> BDD-cost:    1
c ---[1091]---> BDD-cost:   17
c ---[1090]---> BDD-cost:   17
c ---[1089]---> BDD-cost:    1
c ---[1088]---> BDD-cost:    1
c ---[1087]---> BDD-cost:   17
c ---[1086]---> BDD-cost:   17
c ---[1085]---> BDD-cost:    1
c ---[1084]---> BDD-cost:    1
c ---[1083]---> BDD-cost:   17
c ---[1082]---> BDD-cost:   17
c ---[1081]---> BDD-cost:    1
c ---[1080]---> BDD-cost:    1
c ---[1079]---> BDD-cost:   17
c ---[1078]---> BDD-cost:   17
c ---[1077]---> BDD-cost:    1
c ---[1076]---> BDD-cost:    1
c ---[1075]---> BDD-cost:   17
c ---[1074]---> BDD-cost:   17
c ---[1073]---> BDD-cost:    1
c ---[1072]---> BDD-cost:    1
c ---[1071]---> BDD-cost:   17
c ---[1070]---> BDD-cost:   17
c ---[1069]---> BDD-cost:    1
c ---[1068]---> BDD-cost:    1
c ---[1067]---> BDD-cost:   17
c ---[1066]---> BDD-cost:   17
c ---[1065]---> BDD-cost:    1
c ---[1064]---> BDD-cost:    1
c ---[1063]---> BDD-cost:   17
c ---[1062]---> BDD-cost:   17
c ---[1061]---> BDD-cost:    1
c ---[1060]---> BDD-cost:    1
c ---[1059]---> BDD-cost:   17
c ---[1058]---> BDD-cost:   17
c ---[1057]---> BDD-cost:    1
c ---[1056]---> BDD-cost:    1
c ---[1055]---> BDD-cost:   17
c ---[1054]---> BDD-cost:   17
c ---[1053]---> BDD-cost:    1
c ---[1052]---> BDD-cost:    1
c ---[1051]---> BDD-cost:   17
c ---[1050]---> BDD-cost:   17
c ---[1049]---> BDD-cost:    1
c ---[1048]---> BDD-cost:    1
c ---[1047]---> BDD-cost:   17
c ---[1046]---> BDD-cost:   17
c ---[1045]---> BDD-cost:    1
c ---[1044]---> BDD-cost:    1
c ---[1043]---> BDD-cost:   17
c ---[1042]---> BDD-cost:   17
c ---[1041]---> BDD-cost:    1
c ---[1040]---> BDD-cost:    1
c ---[1039]---> BDD-cost:   17
c ---[1038]---> BDD-cost:   17
c ---[1037]---> BDD-cost:    1
c ---[1036]---> BDD-cost:    1
c ---[1035]---> BDD-cost:   17
c ---[1034]---> BDD-cost:   17
c ---[1033]---> BDD-cost:    1
c ---[1032]---> BDD-cost:    1
c ---[1031]---> BDD-cost:   17
c ---[1030]---> BDD-cost:   17
c ---[1029]---> BDD-cost:    1
c ---[1028]---> BDD-cost:    1
c ---[1027]---> BDD-cost:   17
c ---[1026]---> BDD-cost:   17
c ---[1025]---> BDD-cost:    1
c ---[1024]---> BDD-cost:    1
c ---[1023]---> BDD-cost:   17
c ---[1022]---> BDD-cost:   17
c ---[1021]---> BDD-cost:    1
c ---[1020]---> BDD-cost:    1
c ---[1019]---> BDD-cost:   17
c ---[1018]---> BDD-cost:   17
c ---[1017]---> BDD-cost:    1
c ---[1016]---> BDD-cost:    1
c ---[1015]---> BDD-cost:   17
c ---[1014]---> BDD-cost:   17
c ---[1013]---> BDD-cost:    1
c ---[1012]---> BDD-cost:    1
c ---[1011]---> BDD-cost:   17
c ---[1010]---> BDD-cost:   17
c ---[1009]---> BDD-cost:    1
c ---[1008]---> BDD-cost:    1
c ---[1007]---> BDD-cost:   17
c ---[1006]---> BDD-cost:   17
c ---[1005]---> BDD-cost:    1
c ---[1004]---> BDD-cost:    1
c ---[1003]---> BDD-cost:   17
c ---[1002]---> BDD-cost:   17
c ---[1001]---> BDD-cost:    1
c ---[1000]---> BDD-cost:    1
c ---[ 999]---> BDD-cost:   17
c ---[ 998]---> BDD-cost:   17
c ---[ 997]---> BDD-cost:    1
c ---[ 996]---> BDD-cost:    1
c ---[ 995]---> BDD-cost:   17
c ---[ 994]---> BDD-cost:   17
c ---[ 993]---> BDD-cost:    1
c ---[ 992]---> BDD-cost:    1
c ---[ 991]---> BDD-cost:   17
c ---[ 990]---> BDD-cost:   17
c ---[ 989]---> BDD-cost:    1
c ---[ 988]---> BDD-cost:    1
c ---[ 987]---> BDD-cost:   17
c ---[ 986]---> BDD-cost:   17
c ---[ 985]---> BDD-cost:    1
c ---[ 984]---> BDD-cost:    1
c ---[ 983]---> BDD-cost:   17
c ---[ 982]---> BDD-cost:   17
c ---[ 981]---> BDD-cost:    1
c ---[ 980]---> BDD-cost:    1
c ---[ 979]---> BDD-cost:   17
c ---[ 978]---> BDD-cost:   17
c ---[ 977]---> BDD-cost:    1
c ---[ 976]---> BDD-cost:    1
c ---[ 975]---> BDD-cost:   17
c ---[ 974]---> BDD-cost:   17
c ---[ 973]---> BDD-cost:    1
c ---[ 972]---> BDD-cost:    1
c ---[ 971]---> BDD-cost:   17
c ---[ 970]---> BDD-cost:   17
c ---[ 969]---> BDD-cost:    1
c ---[ 968]---> BDD-cost:    1
c ---[ 967]---> BDD-cost:   21
c ---[ 966]---> BDD-cost:    1
c ---[ 965]---> BDD-cost:    1
c ---[ 964]---> BDD-cost:    1
c ---[ 963]---> BDD-cost:   21
c ---[ 962]---> BDD-cost:    1
c ---[ 961]---> BDD-cost:    1
c ---[ 960]---> BDD-cost:    1
c ---[ 959]---> BDD-cost:   21
c ---[ 958]---> BDD-cost:    1
c ---[ 957]---> BDD-cost:    1
c ---[ 956]---> BDD-cost:    1
c ---[ 955]---> BDD-cost:   21
c ---[ 954]---> BDD-cost:    1
c ---[ 953]---> BDD-cost:    1
c ---[ 952]---> BDD-cost:    1
c ---[ 951]---> BDD-cost:    1
c ---[ 950]---> BDD-cost:    1
c ---[ 949]---> BDD-cost:    1
c ---[ 948]---> BDD-cost:    1
c ---[ 947]---> BDD-cost:    1
c ---[ 946]---> BDD-cost:    1
c ---[ 945]---> BDD-cost:    1
c ---[ 944]---> BDD-cost:    1
c ---[ 943]---> BDD-cost:   21
c ---[ 942]---> BDD-cost:    1
c ---[ 941]---> BDD-cost:    1
c ---[ 940]---> BDD-cost:    1
c ---[ 939]---> BDD-cost:   21
c ---[ 938]---> BDD-cost:    1
c ---[ 937]---> BDD-cost:    1
c ---[ 936]---> BDD-cost:    1
c ---[ 935]---> BDD-cost:   21
c ---[ 934]---> BDD-cost:    1
c ---[ 933]---> BDD-cost:    1
c ---[ 932]---> BDD-cost:    1
c ---[ 931]---> BDD-cost:   21
c ---[ 930]---> BDD-cost:    1
c ---[ 929]---> BDD-cost:    1
c ---[ 928]---> BDD-cost:    1
c ---[ 927]---> BDD-cost:   21
c ---[ 926]---> BDD-cost:    1
c ---[ 925]---> BDD-cost:    1
c ---[ 924]---> BDD-cost:    1
c ---[ 923]---> BDD-cost:   21
c ---[ 922]---> BDD-cost:    1
c ---[ 921]---> BDD-cost:    1
c ---[ 920]---> BDD-cost:    1
c ---[ 919]---> BDD-cost:   17
c ---[ 918]---> BDD-cost:   17
c ---[ 917]---> BDD-cost:    1
c ---[ 916]---> BDD-cost:    1
c ---[ 915]---> BDD-cost:   17
c ---[ 914]---> BDD-cost:   17
c ---[ 913]---> BDD-cost:    1
c ---[ 912]---> BDD-cost:    1
c ---[ 911]---> BDD-cost:   24
c ---[ 910]---> BDD-cost:   17
c ---[ 909]---> BDD-cost:    1
c ---[ 908]---> BDD-cost:    1
c ---[ 907]---> BDD-cost:    1
c ---[ 906]---> BDD-cost:   14
c ---[ 905]---> BDD-cost:    1
c ---[ 904]---> BDD-cost:    1
c ---[ 903]---> BDD-cost:   24
c ---[ 902]---> BDD-cost:   17
c ---[ 901]---> BDD-cost:    1
c ---[ 900]---> BDD-cost:    1
c ---[ 899]---> BDD-cost:    1
c ---[ 898]---> BDD-cost:   14
c ---[ 897]---> BDD-cost:    1
c ---[ 896]---> BDD-cost:    1
c ---[ 895]---> BDD-cost:   17
c ---[ 894]---> BDD-cost:   17
c ---[ 893]---> BDD-cost:    1
c ---[ 892]---> BDD-cost:    1
c ---[ 891]---> BDD-cost:   17
c ---[ 890]---> BDD-cost:   17
c ---[ 889]---> BDD-cost:    1
c ---[ 888]---> BDD-cost:    1
c ---[ 887]---> BDD-cost:   24
c ---[ 886]---> BDD-cost:   17
c ---[ 885]---> BDD-cost:    1
c ---[ 884]---> BDD-cost:    1
c ---[ 883]---> BDD-cost:    1
c ---[ 882]---> BDD-cost:   14
c ---[ 881]---> BDD-cost:    1
c ---[ 880]---> BDD-cost:    1
c ---[ 879]---> BDD-cost:   24
c ---[ 878]---> BDD-cost:   17
c ---[ 877]---> BDD-cost:    1
c ---[ 876]---> BDD-cost:    1
c ---[ 875]---> BDD-cost:    1
c ---[ 874]---> BDD-cost:   14
c ---[ 873]---> BDD-cost:    1
c ---[ 872]---> BDD-cost:    1
c ---[ 871]---> BDD-cost:   21
c ---[ 870]---> BDD-cost:    1
c ---[ 869]---> BDD-cost:    1
c ---[ 868]---> BDD-cost:    1
c ---[ 867]---> BDD-cost:   21
c ---[ 866]---> BDD-cost:    1
c ---[ 865]---> BDD-cost:    1
c ---[ 864]---> BDD-cost:    1
c ---[ 863]---> BDD-cost:   21
c ---[ 862]---> BDD-cost:    1
c ---[ 861]---> BDD-cost:    1
c ---[ 860]---> BDD-cost:    1
c ---[ 859]---> BDD-cost:   21
c ---[ 858]---> BDD-cost:    1
c ---[ 857]---> BDD-cost:    1
c ---[ 856]---> BDD-cost:    1
c ---[ 855]---> BDD-cost:   21
c ---[ 854]---> BDD-cost:    1
c ---[ 853]---> BDD-cost:    1
c ---[ 852]---> BDD-cost:    1
c ---[ 851]---> BDD-cost:   21
c ---[ 850]---> BDD-cost:    1
c ---[ 849]---> BDD-cost:    1
c ---[ 848]---> BDD-cost:    1
c ---[ 847]---> BDD-cost:    1
c ---[ 846]---> BDD-cost:    1
c ---[ 845]---> BDD-cost:    1
c ---[ 844]---> BDD-cost:    1
c ---[ 843]---> BDD-cost:    1
c ---[ 842]---> BDD-cost:    1
c ---[ 841]---> BDD-cost:    1
c ---[ 840]---> BDD-cost:    1
c ---[ 839]---> BDD-cost:   21
c ---[ 838]---> BDD-cost:    1
c ---[ 837]---> BDD-cost:    1
c ---[ 836]---> BDD-cost:    1
c ---[ 835]---> BDD-cost:   21
c ---[ 834]---> BDD-cost:    1
c ---[ 833]---> BDD-cost:    1
c ---[ 832]---> BDD-cost:    1
c ---[ 831]---> BDD-cost:   21
c ---[ 830]---> BDD-cost:    1
c ---[ 829]---> BDD-cost:    1
c ---[ 828]---> BDD-cost:    1
c ---[ 827]---> BDD-cost:   21
c ---[ 826]---> BDD-cost:    1
c ---[ 825]---> BDD-cost:    1
c ---[ 824]---> BDD-cost:    1
c ---[ 823]---> BDD-cost:   17
c ---[ 822]---> BDD-cost:   17
c ---[ 821]---> BDD-cost:    1
c ---[ 820]---> BDD-cost:    1
c ---[ 819]---> BDD-cost:   24
c ---[ 818]---> BDD-cost:   17
c ---[ 817]---> BDD-cost:    1
c ---[ 816]---> BDD-cost:    1
c ---[ 815]---> BDD-cost:    1
c ---[ 814]---> BDD-cost:   14
c ---[ 813]---> BDD-cost:    1
c ---[ 812]---> BDD-cost:    1
c ---[ 811]---> BDD-cost:   21
c ---[ 810]---> BDD-cost:    1
c ---[ 809]---> BDD-cost:    1
c ---[ 808]---> BDD-cost:    1
c ---[ 807]---> BDD-cost:   21
c ---[ 806]---> BDD-cost:    1
c ---[ 805]---> BDD-cost:    1
c ---[ 804]---> BDD-cost:    1
c ---[ 803]---> BDD-cost:   21
c ---[ 802]---> BDD-cost:    1
c ---[ 801]---> BDD-cost:    1
c ---[ 800]---> BDD-cost:    1
c ---[ 799]---> BDD-cost:   17
c ---[ 798]---> BDD-cost:   17
c ---[ 797]---> BDD-cost:    1
c ---[ 796]---> BDD-cost:    1
c ---[ 795]---> BDD-cost:   24
c ---[ 794]---> BDD-cost:   17
c ---[ 793]---> BDD-cost:    1
c ---[ 792]---> BDD-cost:    1
c ---[ 791]---> BDD-cost:    1
c ---[ 790]---> BDD-cost:   14
c ---[ 789]---> BDD-cost:    1
c ---[ 788]---> BDD-cost:    1
c ---[ 787]---> BDD-cost:   21
c ---[ 786]---> BDD-cost:    1
c ---[ 785]---> BDD-cost:    1
c ---[ 784]---> BDD-cost:    1
c ---[ 783]---> BDD-cost:   21
c ---[ 782]---> BDD-cost:    1
c ---[ 781]---> BDD-cost:    1
c ---[ 780]---> BDD-cost:    1
c ---[ 779]---> BDD-cost:   21
c ---[ 778]---> BDD-cost:    1
c ---[ 777]---> BDD-cost:    1
c ---[ 776]---> BDD-cost:    1
c ---[ 775]---> BDD-cost:   16
c ---[ 774]---> BDD-cost:    1
c ---[ 773]---> BDD-cost:    1
c ---[ 772]---> BDD-cost:    1
c ---[ 771]---> BDD-cost:   16
c ---[ 770]---> BDD-cost:    1
c ---[ 769]---> BDD-cost:    1
c ---[ 768]---> BDD-cost:    1
c ---[ 767]---> BDD-cost:   16
c ---[ 766]---> BDD-cost:    1
c ---[ 765]---> BDD-cost:    1
c ---[ 764]---> BDD-cost:    1
c ---[ 763]---> BDD-cost:   16
c ---[ 762]---> BDD-cost:    1
c ---[ 761]---> BDD-cost:    1
c ---[ 760]---> BDD-cost:    1
c ---[ 759]---> BDD-cost:   16
c ---[ 758]---> BDD-cost:    1
c ---[ 757]---> BDD-cost:    1
c ---[ 756]---> BDD-cost:    1
c ---[ 755]---> BDD-cost:   16
c ---[ 754]---> BDD-cost:    1
c ---[ 753]---> BDD-cost:    1
c ---[ 752]---> BDD-cost:    1
c ---[ 751]---> BDD-cost:   16
c ---[ 750]---> BDD-cost:    1
c ---[ 749]---> BDD-cost:    1
c ---[ 748]---> BDD-cost:    1
c ---[ 747]---> BDD-cost:   16
c ---[ 746]---> BDD-cost:    1
c ---[ 745]---> BDD-cost:    1
c ---[ 744]---> BDD-cost:    1
c ---[ 743]---> BDD-cost:    1
c ---[ 742]---> BDD-cost:    1
c ---[ 741]---> BDD-cost:    1
c ---[ 740]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:    1
c ---[ 738]---> BDD-cost:    1
c ---[ 737]---> BDD-cost:    1
c ---[ 736]---> BDD-cost:    1
c ---[ 735]---> BDD-cost:   16
c ---[ 734]---> BDD-cost:    1
c ---[ 733]---> BDD-cost:    1
c ---[ 732]---> BDD-cost:    1
c ---[ 731]---> BDD-cost:   16
c ---[ 730]---> BDD-cost:    1
c ---[ 729]---> BDD-cost:    1
c ---[ 728]---> BDD-cost:    1
c ---[ 727]---> BDD-cost:   17
c ---[ 726]---> BDD-cost:   17
c ---[ 725]---> BDD-cost:    1
c ---[ 724]---> BDD-cost:    1
c ---[ 723]---> BDD-cost:   24
c ---[ 722]---> BDD-cost:   17
c ---[ 721]---> BDD-cost:    1
c ---[ 720]---> BDD-cost:    1
c ---[ 719]---> BDD-cost:    1
c ---[ 718]---> BDD-cost:   14
c ---[ 717]---> BDD-cost:    1
c ---[ 716]---> BDD-cost:    1
c ---[ 715]---> BDD-cost:   21
c ---[ 714]---> BDD-cost:    1
c ---[ 713]---> BDD-cost:    1
c ---[ 712]---> BDD-cost:    1
c ---[ 711]---> BDD-cost:   16
c ---[ 710]---> BDD-cost:    1
c ---[ 709]---> BDD-cost:    1
c ---[ 708]---> BDD-cost:    1
c ---[ 707]---> BDD-cost:   16
c ---[ 706]---> BDD-cost:    1
c ---[ 705]---> BDD-cost:    1
c ---[ 704]---> BDD-cost:    1
c ---[ 703]---> BDD-cost:   16
c ---[ 702]---> BDD-cost:    1
c ---[ 701]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 699]---> BDD-cost:   16
c ---[ 698]---> BDD-cost:    1
c ---[ 697]---> BDD-cost:    1
c ---[ 696]---> BDD-cost:    1
c ---[ 695]---> BDD-cost:   17
c ---[ 694]---> BDD-cost:   17
c ---[ 693]---> BDD-cost:    1
c ---[ 692]---> BDD-cost:    1
c ---[ 691]---> BDD-cost:   24
c ---[ 690]---> BDD-cost:   17
c ---[ 689]---> BDD-cost:    1
c ---[ 688]---> BDD-cost:    1
c ---[ 687]---> BDD-cost:    1
c ---[ 686]---> BDD-cost:   14
c ---[ 685]---> BDD-cost:    1
c ---[ 684]---> BDD-cost:    1
c ---[ 683]---> BDD-cost:   21
c ---[ 682]---> BDD-cost:    1
c ---[ 681]---> BDD-cost:    1
c ---[ 680]---> BDD-cost:    1
c ---[ 679]---> BDD-cost:   16
c ---[ 678]---> BDD-cost:    1
c ---[ 677]---> BDD-cost:    1
c ---[ 676]---> BDD-cost:    1
c ---[ 675]---> BDD-cost:   16
c ---[ 674]---> BDD-cost:    1
c ---[ 673]---> BDD-cost:    1
c ---[ 672]---> BDD-cost:    1
c ---[ 671]---> BDD-cost:   16
c ---[ 670]---> BDD-cost:    1
c ---[ 669]---> BDD-cost:    1
c ---[ 668]---> BDD-cost:    1
c ---[ 667]---> BDD-cost:   16
c ---[ 666]---> BDD-cost:    1
c ---[ 665]---> BDD-cost:    1
c ---[ 664]---> BDD-cost:    1
c ---[ 663]---> BDD-cost:   16
c ---[ 662]---> BDD-cost:    1
c ---[ 661]---> BDD-cost:    1
c ---[ 660]---> BDD-cost:    1
c ---[ 659]---> BDD-cost:   16
c ---[ 658]---> BDD-cost:    1
c ---[ 657]---> BDD-cost:    1
c ---[ 656]---> BDD-cost:    1
c ---[ 655]---> BDD-cost:   16
c ---[ 654]---> BDD-cost:    1
c ---[ 653]---> BDD-cost:    1
c ---[ 652]---> BDD-cost:    1
c ---[ 651]---> BDD-cost:   16
c ---[ 650]---> BDD-cost:    1
c ---[ 649]---> BDD-cost:    1
c ---[ 648]---> BDD-cost:    1
c ---[ 647]---> BDD-cost:   16
c ---[ 646]---> BDD-cost:    1
c ---[ 645]---> BDD-cost:    1
c ---[ 644]---> BDD-cost:    1
c ---[ 643]---> BDD-cost:   16
c ---[ 642]---> BDD-cost:    1
c ---[ 641]---> BDD-cost:    1
c ---[ 640]---> BDD-cost:    1
c ---[ 639]---> BDD-cost:   16
c ---[ 638]---> BDD-cost:    1
c ---[ 637]---> BDD-cost:    1
c ---[ 636]---> BDD-cost:    1
c ---[ 635]---> BDD-cost:   16
c ---[ 634]---> BDD-cost:    1
c ---[ 633]---> BDD-cost:    1
c ---[ 632]---> BDD-cost:    1
c ---[ 631]---> BDD-cost:   16
c ---[ 630]---> BDD-cost:    1
c ---[ 629]---> BDD-cost:    1
c ---[ 628]---> BDD-cost:    1
c ---[ 627]---> BDD-cost:   16
c ---[ 626]---> BDD-cost:    1
c ---[ 625]---> BDD-cost:    1
c ---[ 624]---> BDD-cost:    1
c ---[ 623]---> BDD-cost:    1
c ---[ 622]---> BDD-cost:    1
c ---[ 621]---> BDD-cost:    1
c ---[ 620]---> BDD-cost:    1
c ---[ 619]---> BDD-cost:    1
c ---[ 618]---> BDD-cost:    1
c ---[ 617]---> BDD-cost:    1
c ---[ 616]---> BDD-cost:    1
c ---[ 615]---> BDD-cost:   17
c ---[ 614]---> BDD-cost:   17
c ---[ 613]---> BDD-cost:    1
c ---[ 612]---> BDD-cost:    1
c ---[ 611]---> BDD-cost:   24
c ---[ 610]---> BDD-cost:   17
c ---[ 609]---> BDD-cost:    1
c ---[ 608]---> BDD-cost:    1
c ---[ 607]---> BDD-cost:    1
c ---[ 606]---> BDD-cost:   14
c ---[ 605]---> BDD-cost:    1
c ---[ 604]---> BDD-cost:    1
c ---[ 603]---> BDD-cost:   21
c ---[ 602]---> BDD-cost:    1
c ---[ 601]---> BDD-cost:    1
c ---[ 600]---> BDD-cost:    1
c ---[ 599]---> BDD-cost:   16
c ---[ 598]---> BDD-cost:    1
c ---[ 597]---> BDD-cost:    1
c ---[ 596]---> BDD-cost:    1
c ---[ 595]---> BDD-cost:   16
c ---[ 594]---> BDD-cost:    1
c ---[ 593]---> BDD-cost:    1
c ---[ 592]---> BDD-cost:    1
c ---[ 591]---> BDD-cost:   16
c ---[ 590]---> BDD-cost:    1
c ---[ 589]---> BDD-cost:    1
c ---[ 588]---> BDD-cost:    1
c ---[ 587]---> BDD-cost:   16
c ---[ 586]---> BDD-cost:    1
c ---[ 585]---> BDD-cost:    1
c ---[ 584]---> BDD-cost:    1
c ---[ 583]---> BDD-cost:   16
c ---[ 582]---> BDD-cost:    1
c ---[ 581]---> BDD-cost:    1
c ---[ 580]---> BDD-cost:    1
c ---[ 579]---> BDD-cost:   16
c ---[ 578]---> BDD-cost:    1
c ---[ 577]---> BDD-cost:    1
c ---[ 576]---> BDD-cost:    1
c ---[ 575]---> BDD-cost:   17
c ---[ 574]---> BDD-cost:   17
c ---[ 573]---> BDD-cost:    1
c ---[ 572]---> BDD-cost:    1
c ---[ 571]---> BDD-cost:   24
c ---[ 570]---> BDD-cost:   17
c ---[ 569]---> BDD-cost:    1
c ---[ 568]---> BDD-cost:    1
c ---[ 567]---> BDD-cost:    1
c ---[ 566]---> BDD-cost:   14
c ---[ 565]---> BDD-cost:    1
c ---[ 564]---> BDD-cost:    1
c ---[ 563]---> BDD-cost:   21
c ---[ 562]---> BDD-cost:    1
c ---[ 561]---> BDD-cost:    1
c ---[ 560]---> BDD-cost:    1
c ---[ 559]---> BDD-cost:   16
c ---[ 558]---> BDD-cost:    1
c ---[ 557]---> BDD-cost:    1
c ---[ 556]---> BDD-cost:    1
c ---[ 555]---> BDD-cost:   16
c ---[ 554]---> BDD-cost:    1
c ---[ 553]---> BDD-cost:    1
c ---[ 552]---> BDD-cost:    1
c ---[ 551]---> BDD-cost:   16
c ---[ 550]---> BDD-cost:    1
c ---[ 549]---> BDD-cost:    1
c ---[ 548]---> BDD-cost:    1
c ---[ 547]---> BDD-cost:   16
c ---[ 546]---> BDD-cost:    1
c ---[ 545]---> BDD-cost:    1
c ---[ 544]---> BDD-cost:    1
c ---[ 543]---> BDD-cost:   16
c ---[ 542]---> BDD-cost:    1
c ---[ 541]---> BDD-cost:    1
c ---[ 540]---> BDD-cost:    1
c ---[ 539]---> BDD-cost:   16
c ---[ 538]---> BDD-cost:    1
c ---[ 537]---> BDD-cost:    1
c ---[ 536]---> BDD-cost:    1
c ---[ 535]---> BDD-cost:   16
c ---[ 534]---> BDD-cost:    1
c ---[ 533]---> BDD-cost:    1
c ---[ 532]---> BDD-cost:    1
c ---[ 531]---> BDD-cost:   16
c ---[ 530]---> BDD-cost:    1
c ---[ 529]---> BDD-cost:    1
c ---[ 528]---> BDD-cost:    1
c ---[ 527]---> BDD-cost:   16
c ---[ 526]---> BDD-cost:    1
c ---[ 525]---> BDD-cost:    1
c ---[ 524]---> BDD-cost:    1
c ---[ 523]---> BDD-cost:   16
c ---[ 522]---> BDD-cost:    1
c ---[ 521]---> BDD-cost:    1
c ---[ 520]---> BDD-cost:    1
c ---[ 519]---> BDD-cost:   16
c ---[ 518]---> BDD-cost:    1
c ---[ 517]---> BDD-cost:    1
c ---[ 516]---> BDD-cost:    1
c ---[ 515]---> BDD-cost:   16
c ---[ 514]---> BDD-cost:    1
c ---[ 513]---> BDD-cost:    1
c ---[ 512]---> BDD-cost:    1
c ---[ 511]---> BDD-cost:   16
c ---[ 510]---> BDD-cost:    1
c ---[ 509]---> BDD-cost:    1
c ---[ 508]---> BDD-cost:    1
c ---[ 507]---> BDD-cost:   16
c ---[ 506]---> BDD-cost:    1
c ---[ 505]---> BDD-cost:    1
c ---[ 504]---> BDD-cost:    1
c ---[ 503]---> BDD-cost:   16
c ---[ 502]---> BDD-cost:    1
c ---[ 501]---> BDD-cost:    1
c ---[ 500]---> BDD-cost:    1
c ---[ 499]---> BDD-cost:   16
c ---[ 498]---> BDD-cost:    1
c ---[ 497]---> BDD-cost:    1
c ---[ 496]---> BDD-cost:    1
c ---[ 495]---> BDD-cost:   16
c ---[ 494]---> BDD-cost:    1
c ---[ 493]---> BDD-cost:    1
c ---[ 492]---> BDD-cost:    1
c ---[ 491]---> BDD-cost:   16
c ---[ 490]---> BDD-cost:    1
c ---[ 489]---> BDD-cost:    1
c ---[ 488]---> BDD-cost:    1
c ---[ 487]---> BDD-cost:    1
c ---[ 486]---> BDD-cost:   16
c ---[ 485]---> BDD-cost:    1
c ---[ 484]---> BDD-cost:    1
c ---[ 483]---> BDD-cost:   16
c ---[ 482]---> BDD-cost:    1
c ---[ 481]---> BDD-cost:    1
c ---[ 480]---> BDD-cost:    1
c ---[ 479]---> BDD-cost:   16
c ---[ 478]---> BDD-cost:    1
c ---[ 477]---> BDD-cost:    1
c ---[ 476]---> BDD-cost:    1
c ---[ 475]---> BDD-cost:   16
c ---[ 474]---> BDD-cost:    1
c ---[ 473]---> BDD-cost:    1
c ---[ 472]---> BDD-cost:    1
c ---[ 471]---> BDD-cost:   16
c ---[ 470]---> BDD-cost:    1
c ---[ 469]---> BDD-cost:    1
c ---[ 468]---> BDD-cost:    1
c ---[ 467]---> BDD-cost:   16
c ---[ 466]---> BDD-cost:    1
c ---[ 465]---> BDD-cost:    1
c ---[ 464]---> BDD-cost:    1
c ---[ 463]---> BDD-cost:   16
c ---[ 462]---> BDD-cost:    1
c ---[ 461]---> BDD-cost:    1
c ---[ 460]---> BDD-cost:    1
c ---[ 459]---> BDD-cost:   16
c ---[ 458]---> BDD-cost:    1
c ---[ 457]---> BDD-cost:    1
c ---[ 456]---> BDD-cost:    1
c ---[ 455]---> BDD-cost:   16
c ---[ 454]---> BDD-cost:    1
c ---[ 453]---> BDD-cost:    1
c ---[ 452]---> BDD-cost:    1
c ---[ 451]---> BDD-cost:   16
c ---[ 450]---> BDD-cost:    1
c ---[ 449]---> BDD-cost:    1
c ---[ 448]---> BDD-cost:    1
c ---[ 447]---> BDD-cost:   16
c ---[ 446]---> BDD-cost:    1
c ---[ 445]---> BDD-cost:    1
c ---[ 444]---> BDD-cost:    1
c ---[ 443]---> BDD-cost:   16
c ---[ 442]---> BDD-cost:    1
c ---[ 441]---> BDD-cost:    1
c ---[ 440]---> BDD-cost:    1
c ---[ 439]---> BDD-cost:   16
c ---[ 438]---> BDD-cost:    1
c ---[ 437]---> BDD-cost:    1
c ---[ 436]---> BDD-cost:    1
c ---[ 435]---> BDD-cost:   17
c ---[ 434]---> BDD-cost:   17
c ---[ 433]---> BDD-cost:    1
c ---[ 432]---> BDD-cost:    1
c ---[ 431]---> BDD-cost:   24
c ---[ 430]---> BDD-cost:   17
c ---[ 429]---> BDD-cost:    1
c ---[ 428]---> BDD-cost:    1
c ---[ 427]---> BDD-cost:    1
c ---[ 426]---> BDD-cost:   14
c ---[ 425]---> BDD-cost:    1
c ---[ 424]---> BDD-cost:    1
c ---[ 423]---> BDD-cost:   21
c ---[ 422]---> BDD-cost:    1
c ---[ 421]---> BDD-cost:    1
c ---[ 420]---> BDD-cost:    1
c ---[ 419]---> BDD-cost:   16
c ---[ 418]---> BDD-cost:    1
c ---[ 417]---> BDD-cost:    1
c ---[ 416]---> BDD-cost:    1
c ---[ 415]---> BDD-cost:   16
c ---[ 414]---> BDD-cost:    1
c ---[ 413]---> BDD-cost:    1
c ---[ 412]---> BDD-cost:    1
c ---[ 411]---> BDD-cost:   16
c ---[ 410]---> BDD-cost:    1
c ---[ 409]---> BDD-cost:    1
c ---[ 408]---> BDD-cost:    1
c ---[ 407]---> BDD-cost:   16
c ---[ 406]---> BDD-cost:    1
c ---[ 405]---> BDD-cost:    1
c ---[ 404]---> BDD-cost:    1
c ---[ 403]---> BDD-cost:   16
c ---[ 402]---> BDD-cost:    1
c ---[ 401]---> BDD-cost:    1
c ---[ 400]---> BDD-cost:    1
c ---[ 399]---> BDD-cost:   16
c ---[ 398]---> BDD-cost:    1
c ---[ 397]---> BDD-cost:    1
c ---[ 396]---> BDD-cost:    1
c ---[ 395]---> BDD-cost:   16
c ---[ 394]---> BDD-cost:    1
c ---[ 393]---> BDD-cost:    1
c ---[ 392]---> BDD-cost:    1
c ---[ 391]---> BDD-cost:   16
c ---[ 390]---> BDD-cost:    1
c ---[ 389]---> BDD-cost:    1
c ---[ 388]---> BDD-cost:    1
c ---[ 387]---> BDD-cost:   17
c ---[ 386]---> BDD-cost:   17
c ---[ 385]---> BDD-cost:    1
c ---[ 384]---> BDD-cost:    1
c ---[ 383]---> BDD-cost:   24
c ---[ 382]---> BDD-cost:   17
c ---[ 381]---> BDD-cost:    1
c ---[ 380]---> BDD-cost:    1
c ---[ 379]---> BDD-cost:    1
c ---[ 378]---> BDD-cost:   14
c ---[ 377]---> BDD-cost:    1
c ---[ 376]---> BDD-cost:    1
c ---[ 375]---> BDD-cost:   21
c ---[ 374]---> BDD-cost:    1
c ---[ 373]---> BDD-cost:    1
c ---[ 372]---> BDD-cost:    1
c ---[ 371]---> BDD-cost:   16
c ---[ 370]---> BDD-cost:    1
c ---[ 369]---> BDD-cost:    1
c ---[ 368]---> BDD-cost:    1
c ---[ 367]---> BDD-cost:   16
c ---[ 366]---> BDD-cost:    1
c ---[ 365]---> BDD-cost:    1
c ---[ 364]---> BDD-cost:    1
c ---[ 363]---> BDD-cost:   16
c ---[ 362]---> BDD-cost:    1
c ---[ 361]---> BDD-cost:    1
c ---[ 360]---> BDD-cost:    1
c ---[ 359]---> BDD-cost:   16
c ---[ 358]---> BDD-cost:    1
c ---[ 357]---> BDD-cost:    1
c ---[ 356]---> BDD-cost:    1
c ---[ 355]---> BDD-cost:   16
c ---[ 354]---> BDD-cost:    1
c ---[ 353]---> BDD-cost:    1
c ---[ 352]---> BDD-cost:    1
c ---[ 351]---> BDD-cost:   16
c ---[ 350]---> BDD-cost:    1
c ---[ 349]---> BDD-cost:    1
c ---[ 348]---> BDD-cost:    1
c ---[ 347]---> BDD-cost:   16
c ---[ 346]---> BDD-cost:    1
c ---[ 345]---> BDD-cost:    1
c ---[ 344]---> BDD-cost:    1
c ---[ 343]---> BDD-cost:   16
c ---[ 342]---> BDD-cost:    1
c ---[ 341]---> BDD-cost:    1
c ---[ 340]---> BDD-cost:    1
c ---[ 339]---> BDD-cost:   14
c ---[ 338]---> BDD-cost:   14
c ---[ 337]---> BDD-cost:    1
c ---[ 336]---> BDD-cost:    1
c ---[ 335]---> BDD-cost:   14
c ---[ 334]---> BDD-cost:   14
c ---[ 333]---> BDD-cost:    1
c ---[ 332]---> BDD-cost:    1
c ---[ 331]---> BDD-cost:   14
c ---[ 330]---> BDD-cost:   14
c ---[ 329]---> BDD-cost:    1
c ---[ 328]---> BDD-cost:    1
c ---[ 327]---> BDD-cost:   14
c ---[ 326]---> BDD-cost:   14
c ---[ 325]---> BDD-cost:    1
c ---[ 324]---> BDD-cost:    1
c ---[ 323]---> BDD-cost:   14
c ---[ 322]---> BDD-cost:   14
c ---[ 321]---> BDD-cost:    1
c ---[ 320]---> BDD-cost:    1
c ---[ 319]---> BDD-cost:   14
c ---[ 318]---> BDD-cost:   14
c ---[ 317]---> BDD-cost:    1
c ---[ 316]---> BDD-cost:    1
c ---[ 315]---> BDD-cost:   17
c ---[ 314]---> BDD-cost:   17
c ---[ 313]---> BDD-cost:    1
c ---[ 312]---> BDD-cost:    1
c ---[ 311]---> BDD-cost:   17
c ---[ 310]---> BDD-cost:   17
c ---[ 309]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 307]---> BDD-cost:   17
c ---[ 306]---> BDD-cost:   17
c ---[ 305]---> BDD-cost:    1
c ---[ 304]---> BDD-cost:    1
c ---[ 303]---> BDD-cost:   21
c ---[ 302]---> BDD-cost:    1
c ---[ 301]---> BDD-cost:    1
c ---[ 300]---> BDD-cost:    1
c ---[ 299]---> BDD-cost:   21
c ---[ 298]---> BDD-cost:    1
c ---[ 297]---> BDD-cost:    1
c ---[ 296]---> BDD-cost:    1
c ---[ 295]---> BDD-cost:   17
c ---[ 294]---> BDD-cost:   17
c ---[ 293]---> BDD-cost:    1
c ---[ 292]---> BDD-cost:    1
c ---[ 291]---> BDD-cost:   21
c ---[ 290]---> BDD-cost:    1
c ---[ 289]---> BDD-cost:    1
c ---[ 288]---> BDD-cost:    1
c ---[ 287]---> BDD-cost:   21
c ---[ 286]---> BDD-cost:    1
c ---[ 285]---> BDD-cost:    1
c ---[ 284]---> BDD-cost:    1
c ---[ 283]---> BDD-cost:   17
c ---[ 282]---> BDD-cost:   17
c ---[ 281]---> BDD-cost:    1
c ---[ 280]---> BDD-cost:    1
c ---[ 279]---> BDD-cost:   21
c ---[ 278]---> BDD-cost:    1
c ---[ 277]---> BDD-cost:    1
c ---[ 276]---> BDD-cost:    1
c ---[ 275]---> BDD-cost:   21
c ---[ 274]---> BDD-cost:    1
c ---[ 273]---> BDD-cost:    1
c ---[ 272]---> BDD-cost:    1
c ---[ 271]---> BDD-cost:   21
c ---[ 270]---> BDD-cost:    1
c ---[ 269]---> BDD-cost:    1
c ---[ 268]---> BDD-cost:    1
c ---[ 267]---> BDD-cost:   21
c ---[ 266]---> BDD-cost:    1
c ---[ 265]---> BDD-cost:    1
c ---[ 264]---> BDD-cost:    1
c ---[ 263]---> BDD-cost:   17
c ---[ 262]---> BDD-cost:   17
c ---[ 261]---> BDD-cost:    1
c ---[ 260]---> BDD-cost:    1
c ---[ 259]---> BDD-cost:   21
c ---[ 258]---> BDD-cost:    1
c ---[ 257]---> BDD-cost:    1
c ---[ 256]---> BDD-cost:    1
c ---[ 255]---> BDD-cost:   21
c ---[ 254]---> BDD-cost:    1
c ---[ 253]---> BDD-cost:    1
c ---[ 252]---> BDD-cost:    1
c ---[ 251]---> BDD-cost:   21
c ---[ 250]---> BDD-cost:    1
c ---[ 249]---> BDD-cost:    1
c ---[ 248]---> BDD-cost:    1
c ---[ 247]---> BDD-cost:   21
c ---[ 246]---> BDD-cost:    1
c ---[ 245]---> BDD-cost:    1
c ---[ 244]---> BDD-cost:    1
c ---[ 243]---> BDD-cost:   17
c ---[ 242]---> BDD-cost:   17
c ---[ 241]---> BDD-cost:    1
c ---[ 240]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:   21
c ---[ 238]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 235]---> BDD-cost:   21
c ---[ 234]---> BDD-cost:    1
c ---[ 233]---> BDD-cost:    1
c ---[ 232]---> BDD-cost:    1
c ---[ 231]---> BDD-cost:   16
c ---[ 230]---> BDD-cost:    1
c ---[ 229]---> BDD-cost:    1
c ---[ 228]---> BDD-cost:    1
c ---[ 227]---> BDD-cost:   16
c ---[ 226]---> BDD-cost:    1
c ---[ 225]---> BDD-cost:    1
c ---[ 224]---> BDD-cost:    1
c ---[ 223]---> BDD-cost:   16
c ---[ 222]---> BDD-cost:    1
c ---[ 221]---> BDD-cost:    1
c ---[ 220]---> BDD-cost:    1
c ---[ 219]---> BDD-cost:   16
c ---[ 218]---> BDD-cost:    1
c ---[ 217]---> BDD-cost:    1
c ---[ 216]---> BDD-cost:    1
c ---[ 215]---> BDD-cost:   17
c ---[ 214]---> BDD-cost:   17
c ---[ 213]---> BDD-cost:    1
c ---[ 212]---> BDD-cost:    1
c ---[ 211]---> BDD-cost:   21
c ---[ 210]---> BDD-cost:    1
c ---[ 209]---> BDD-cost:    1
c ---[ 208]---> BDD-cost:    1
c ---[ 207]---> BDD-cost:   21
c ---[ 206]---> BDD-cost:    1
c ---[ 205]---> BDD-cost:    1
c ---[ 204]---> BDD-cost:    1
c ---[ 203]---> BDD-cost:   16
c ---[ 202]---> BDD-cost:    1
c ---[ 201]---> BDD-cost:    1
c ---[ 200]---> BDD-cost:    1
c ---[ 199]---> BDD-cost:   16
c ---[ 198]---> BDD-cost:    1
c ---[ 197]---> BDD-cost:    1
c ---[ 196]---> BDD-cost:    1
c ---[ 195]---> BDD-cost:   16
c ---[ 194]---> BDD-cost:    1
c ---[ 193]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 191]---> BDD-cost:   16
c ---[ 190]---> BDD-cost:    1
c ---[ 189]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 187]---> BDD-cost:   17
c ---[ 186]---> BDD-cost:   17
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:    1
c ---[ 183]---> BDD-cost:   21
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:   21
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:   16
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:   16
c ---[ 170]---> BDD-cost:    1
c ---[ 169]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:   16
c ---[ 166]---> BDD-cost:    1
c ---[ 165]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> BDD-cost:   16
c ---[ 162]---> BDD-cost:    1
c ---[ 161]---> BDD-cost:    1
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost:   16
c ---[ 158]---> BDD-cost:    1
c ---[ 157]---> BDD-cost:    1
c ---[ 156]---> BDD-cost:    1
c ---[ 155]---> BDD-cost:   16
c ---[ 154]---> BDD-cost:    1
c ---[ 153]---> BDD-cost:    1
c ---[ 152]---> BDD-cost:    1
c ---[ 151]---> BDD-cost:   17
c ---[ 150]---> BDD-cost:   17
c ---[ 149]---> BDD-cost:    1
c ---[ 148]---> BDD-cost:    1
c ---[ 147]---> BDD-cost:   21
c ---[ 146]---> BDD-cost:    1
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:    1
c ---[ 143]---> BDD-cost:   21
c ---[ 142]---> BDD-cost:    1
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:   16
c ---[ 138]---> BDD-cost:    1
c ---[ 137]---> BDD-cost:    1
c ---[ 136]---> BDD-cost:    1
c ---[ 135]---> BDD-cost:   16
c ---[ 134]---> BDD-cost:    1
c ---[ 133]---> BDD-cost:    1
c ---[ 132]---> BDD-cost:    1
c ---[ 131]---> BDD-cost:   16
c ---[ 130]---> BDD-cost:    1
c ---[ 129]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:   16
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:   16
c ---[ 122]---> BDD-cost:    1
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:   16
c ---[ 118]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:   14
c ---[ 114]---> BDD-cost:   14
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:   14
c ---[ 110]---> BDD-cost:   14
c ---[ 109]---> BDD-cost:    1
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:   14
c ---[ 106]---> BDD-cost:   14
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[ 103]---> BDD-cost:   14
c ---[ 102]---> BDD-cost:   14
c ---[ 101]---> BDD-cost:    1
c ---[ 100]---> BDD-cost:    1
c ---[  99]---> BDD-cost:   14
c ---[  98]---> BDD-cost:   14
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  95]---> BDD-cost:   14
c ---[  94]---> BDD-cost:   14
c ---[  93]---> BDD-cost:    1
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:   14
c ---[  90]---> BDD-cost:   14
c ---[  89]---> BDD-cost:    1
c ---[  88]---> BDD-cost:    1
c ---[  87]---> BDD-cost:   14
c ---[  86]---> BDD-cost:   14
c ---[  85]---> BDD-cost:    1
c ---[  84]---> BDD-cost:    1
c ---[  83]---> BDD-cost:   14
c ---[  82]---> BDD-cost:   14
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:    1
c ---[  79]---> BDD-cost:   14
c ---[  78]---> BDD-cost:   14
c ---[  77]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  75]---> BDD-cost:   14
c ---[  74]---> BDD-cost:   14
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:   14
c ---[  70]---> BDD-cost:   14
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:   14
c ---[  66]---> BDD-cost:   14
c ---[  65]---> BDD-cost:    1
c ---[  64]---> BDD-cost:    1
c ---[  63]---> BDD-cost:   14
c ---[  62]---> BDD-cost:   14
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:   14
c ---[  58]---> BDD-cost:   14
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:   14
c ---[  54]---> BDD-cost:   14
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:   14
c ---[  50]---> BDD-cost:   14
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:   14
c ---[  46]---> BDD-cost:   14
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:   14
c ---[  42]---> BDD-cost:   14
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:   14
c ---[  38]---> BDD-cost:   14
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:   14
c ---[  34]---> BDD-cost:   14
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:   14
c ---[  30]---> BDD-cost:   14
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:   14
c ---[  26]---> BDD-cost:   14
c ---[  25]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:   14
c ---[  22]---> BDD-cost:   14
c ---[  21]---> BDD-cost:    1
c ---[  20]---> BDD-cost:    1
c ---[  19]---> BDD-cost:   14
c ---[  18]---> BDD-cost:   14
c ---[  17]---> BDD-cost:    1
c ---[  16]---> BDD-cost:    1
c ---[  15]---> BDD-cost:   14
c ---[  14]---> BDD-cost:   14
c ---[  13]---> BDD-cost:    1
c ---[  12]---> BDD-cost:    1
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:    1
c ---[   8]---> BDD-cost:    1
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   14
c ---[   5]---> BDD-cost:    1
c ---[   4]---> BDD-cost:    1
c ---[   3]---> BDD-cost:   14
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    1
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  122857   308719 |   40952       0        0     nan |  0.000 % |
c |       100 |  122857   308719 |   45047     100     1187    11.9 |  7.945 % |
c |       250 |  122846   308695 |   49551     249     2759    11.1 |  7.953 % |
c |       476 |  122846   308695 |   54507     475     9500    20.0 |  7.953 % |
c |       814 |  122846   308695 |   59957     813    14844    18.3 |  7.954 % |
c |      1320 |  122846   308695 |   65953    1319    47211    35.8 |  7.953 % |
c |      2080 |  122846   308695 |   72548    2079    60894    29.3 |  7.953 % |
c |      3220 |  122846   308695 |   79803    3219   186800    58.0 |  7.953 % |
c |      4928 |  122846   308695 |   87784    4927   310725    63.1 |  7.953 % |
c |      7490 |  122846   308695 |   96562    7489   413134    55.2 |  7.953 % |
c |     11334 |  122846   308695 |  106218   11333   890693    78.6 |  7.953 % |
c |     17102 |  119347   300689 |  116840   17096  1014501    59.3 | 10.437 % |
c |     25753 |  119347   300689 |  128524   25747  2616250   101.6 | 10.437 % |
c |     38730 |  119347   300689 |  141377   38724  4484700   115.8 | 10.437 % |
c |     58192 |  119347   300689 |  155515   58186  6020966   103.5 | 10.437 % |
c |     87384 |  119326   300643 |  171066   87374  8314322    95.2 | 10.455 % |
c |    131173 |  119326   300643 |  188173  131163 11587169    88.3 | 10.455 % |
c |    196859 |  119326   300643 |  206990  196849 16936937    86.0 | 10.455 % |
#### 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.79 0.89 0.88 2/54 28503
Raw data (stat): 28503 (runsolver) R 28502 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422848144 1052672 99 4294967295 134512640 135381576 3221224416 3221219660 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.82 0.89 0.88 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 5571 0 0 0 982 15 0 0 25 0 1 0 422848144 24961024 5343 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6094 5343 603 41 0 6053 0
vsize: 24376
[startup+20.0013 s]
Raw data (loadavg): 0.85 0.89 0.89 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 5594 0 0 0 1979 16 0 0 25 0 1 0 422848144 24961024 5366 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6094 5366 603 41 0 6053 0
vsize: 24376
[startup+30.0015 s]
Raw data (loadavg): 0.87 0.90 0.89 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 5594 0 0 0 2979 16 0 0 25 0 1 0 422848144 24961024 5366 4294967295 134512640 134672761 3221224528 3221223652 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6094 5366 603 41 0 6053 0
vsize: 24376
[startup+40.0023 s]
Raw data (loadavg): 0.89 0.90 0.89 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 6068 0 0 0 3977 18 0 0 25 0 1 0 422848144 26849280 5840 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6555 5840 603 41 0 6514 0
vsize: 26220
[startup+50.0026 s]
Raw data (loadavg): 0.91 0.90 0.89 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 6802 0 0 0 4976 19 0 0 25 0 1 0 422848144 29925376 6574 4294967295 134512640 134672761 3221224528 3221223632 134560215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7306 6574 603 41 0 7265 0
vsize: 29224
[startup+60.0022 s]
Raw data (loadavg): 0.92 0.90 0.89 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 7363 0 0 0 5974 21 0 0 25 0 1 0 422848144 32198656 7135 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7861 7135 603 41 0 7820 0
vsize: 31444
[startup+70.0031 s]
Raw data (loadavg): 0.93 0.91 0.89 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 7995 0 0 0 6973 22 0 0 25 0 1 0 422848144 34725888 7767 4294967295 134512640 134672761 3221224528 3221223664 134560634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8478 7767 603 41 0 8437 0
vsize: 33912
[startup+80.0035 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 8428 0 0 0 7972 24 0 0 25 0 1 0 422848144 36708352 8200 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8962 8200 603 41 0 8921 0
vsize: 35848
[startup+90.0041 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 8827 0 0 0 8971 25 0 0 25 0 1 0 422848144 38293504 8599 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9349 8599 603 41 0 9308 0
vsize: 37396
[startup+100.004 s]
Raw data (loadavg): 0.96 0.91 0.89 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 9339 0 0 0 9970 26 0 0 25 0 1 0 422848144 40333312 9111 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9847 9111 603 41 0 9806 0
vsize: 39388
[startup+110.003 s]
Raw data (loadavg): 0.96 0.92 0.89 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 9657 0 0 0 10969 27 0 0 25 0 1 0 422848144 41676800 9429 4294967295 134512640 134672761 3221224528 3221223664 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10175 9429 603 41 0 10134 0
vsize: 40700
[startup+120.004 s]
Raw data (loadavg): 0.97 0.92 0.89 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 9968 0 0 0 11968 28 0 0 25 0 1 0 422848144 42881024 9740 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10469 9740 603 41 0 10428 0
vsize: 41876
[startup+130.004 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 10277 0 0 0 12967 29 0 0 25 0 1 0 422848144 44208128 10049 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10793 10049 603 41 0 10752 0
vsize: 43172
[startup+140.004 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 10530 0 0 0 13967 30 0 0 25 0 1 0 422848144 45264896 10302 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11051 10302 603 41 0 11010 0
vsize: 44204
[startup+150.005 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 10790 0 0 0 14966 31 0 0 25 0 1 0 422848144 46206976 10562 4294967295 134512640 134672761 3221224528 3221223632 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11281 10562 603 41 0 11240 0
vsize: 45124
[startup+160.005 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 11065 0 0 0 15965 32 0 0 25 0 1 0 422848144 47407104 10837 4294967295 134512640 134672761 3221224528 3221223684 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11574 10837 603 41 0 11533 0
vsize: 46296
[startup+170.005 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 11263 0 0 0 16965 32 0 0 25 0 1 0 422848144 48201728 11035 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11768 11035 603 41 0 11727 0
vsize: 47072
[startup+180.005 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 11490 0 0 0 17965 33 0 0 25 0 1 0 422848144 49393664 11262 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12059 11262 603 41 0 12018 0
vsize: 48236
[startup+190.006 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 11638 0 0 0 18965 33 0 0 25 0 1 0 422848144 49926144 11410 4294967295 134512640 134672761 3221224528 3221223584 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12189 11410 603 41 0 12148 0
vsize: 48756
[startup+200.006 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 11769 0 0 0 19965 33 0 0 25 0 1 0 422848144 50454528 11541 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12318 11541 603 41 0 12277 0
vsize: 49272
[startup+210.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 11930 0 0 0 20965 33 0 0 25 0 1 0 422848144 51122176 11702 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12481 11702 603 41 0 12440 0
vsize: 49924
[startup+220.007 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 12089 0 0 0 21965 34 0 0 25 0 1 0 422848144 51802112 11861 4294967295 134512640 134672761 3221224528 3221223712 134559045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12647 11861 603 41 0 12606 0
vsize: 50588
[startup+230.006 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 12323 0 0 0 22964 34 0 0 25 0 1 0 422848144 52862976 12095 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12906 12095 603 41 0 12865 0
vsize: 51624
[startup+240.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 12658 0 0 0 23963 35 0 0 25 0 1 0 422848144 54251520 12430 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13245 12430 603 41 0 13204 0
vsize: 52980
[startup+250.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 13077 0 0 0 24963 36 0 0 25 0 1 0 422848144 55840768 12849 4294967295 134512640 134672761 3221224528 3221223696 134561027 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13633 12849 603 41 0 13592 0
vsize: 54532
[startup+260.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 13371 0 0 0 25962 37 0 0 25 0 1 0 422848144 57028608 13143 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13923 13143 603 41 0 13882 0
vsize: 55692
[startup+270.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 13569 0 0 0 26962 37 0 0 25 0 1 0 422848144 57954304 13341 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14149 13341 603 41 0 14108 0
vsize: 56596
[startup+280.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 13766 0 0 0 27962 38 0 0 25 0 1 0 422848144 58744832 13538 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14342 13538 603 41 0 14301 0
vsize: 57368
[startup+290.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 13991 0 0 0 28961 38 0 0 25 0 1 0 422848144 59678720 13763 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14570 13763 603 41 0 14529 0
vsize: 58280
[startup+300.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 14176 0 0 0 29961 39 0 0 25 0 1 0 422848144 60473344 13948 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14764 13948 603 41 0 14723 0
vsize: 59056
[startup+310.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 14334 0 0 0 30960 40 0 0 25 0 1 0 422848144 61136896 14106 4294967295 134512640 134672761 3221224528 3221223456 1075358820 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14926 14106 603 41 0 14885 0
vsize: 59704
[startup+320.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 14465 0 0 0 31960 40 0 0 25 0 1 0 422848144 61534208 14237 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15023 14237 603 41 0 14982 0
vsize: 60092
[startup+330.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 14608 0 0 0 32959 41 0 0 25 0 1 0 422848144 62197760 14380 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15185 14380 603 41 0 15144 0
vsize: 60740
[startup+340.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 14744 0 0 0 33959 41 0 0 25 0 1 0 422848144 62730240 14516 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15315 14516 603 41 0 15274 0
vsize: 61260
[startup+350.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 14911 0 0 0 34959 42 0 0 25 0 1 0 422848144 63389696 14683 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15476 14683 603 41 0 15435 0
vsize: 61904
[startup+360.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 15031 0 0 0 35959 42 0 0 25 0 1 0 422848144 63918080 14803 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15605 14803 603 41 0 15564 0
vsize: 62420
[startup+370.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 15283 0 0 0 36959 42 0 0 25 0 1 0 422848144 65110016 15055 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15896 15055 603 41 0 15855 0
vsize: 63584
[startup+380.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 15596 0 0 0 37958 43 0 0 25 0 1 0 422848144 66310144 15368 4294967295 134512640 134672761 3221224528 3221223672 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16189 15368 603 41 0 16148 0
vsize: 64756
[startup+390.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 15927 0 0 0 38957 45 0 0 25 0 1 0 422848144 67649536 15699 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16516 15699 603 41 0 16475 0
vsize: 66064
[startup+400.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 16272 0 0 0 39956 46 0 0 25 0 1 0 422848144 69111808 16044 4294967295 134512640 134672761 3221224528 3221223712 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16873 16044 603 41 0 16832 0
vsize: 67492
[startup+410.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 16492 0 0 0 40956 46 0 0 25 0 1 0 422848144 69914624 16264 4294967295 134512640 134672761 3221224528 3221223696 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17069 16264 603 41 0 17028 0
vsize: 68276
[startup+420.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 16702 0 0 0 41956 46 0 0 25 0 1 0 422848144 70844416 16474 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17296 16474 603 41 0 17255 0
vsize: 69184
[startup+430.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 16888 0 0 0 42955 47 0 0 25 0 1 0 422848144 71507968 16660 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17458 16660 603 41 0 17417 0
vsize: 69832
[startup+440.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 17053 0 0 0 43955 47 0 0 25 0 1 0 422848144 72163328 16825 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17618 16825 603 41 0 17577 0
vsize: 70472
[startup+450.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 17226 0 0 0 44954 48 0 0 25 0 1 0 422848144 73359360 16998 4294967295 134512640 134672761 3221224528 3221223712 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17910 16998 603 41 0 17869 0
vsize: 71640
[startup+460.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 17441 0 0 0 45954 49 0 0 25 0 1 0 422848144 74297344 17213 4294967295 134512640 134672761 3221224528 3221223484 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18139 17213 603 41 0 18098 0
vsize: 72556
[startup+470.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 17625 0 0 0 46953 50 0 0 25 0 1 0 422848144 74952704 17397 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18299 17397 603 41 0 18258 0
vsize: 73196
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 17775 0 0 0 47953 50 0 0 25 0 1 0 422848144 75620352 17547 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18462 17547 603 41 0 18421 0
vsize: 73848
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 17897 0 0 0 48953 50 0 0 25 0 1 0 422848144 76152832 17669 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18592 17669 603 41 0 18551 0
vsize: 74368
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 18005 0 0 0 49953 51 0 0 25 0 1 0 422848144 76546048 17777 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18688 17777 603 41 0 18647 0
vsize: 74752
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 18170 0 0 0 50953 51 0 0 25 0 1 0 422848144 77209600 17942 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18850 17942 603 41 0 18809 0
vsize: 75400
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 18352 0 0 0 51953 51 0 0 25 0 1 0 422848144 78000128 18124 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19043 18124 603 41 0 19002 0
vsize: 76172
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 18567 0 0 0 52952 52 0 0 25 0 1 0 422848144 78938112 18339 4294967295 134512640 134672761 3221224528 3221223696 134560842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19272 18339 603 41 0 19231 0
vsize: 77088
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 18723 0 0 0 53951 53 0 0 25 0 1 0 422848144 79605760 18495 4294967295 134512640 134672761 3221224528 3221223712 134558831 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19435 18495 603 41 0 19394 0
vsize: 77740
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 18924 0 0 0 54951 54 0 0 25 0 1 0 422848144 80412672 18696 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19632 18696 603 41 0 19591 0
vsize: 78528
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 19128 0 0 0 55951 54 0 0 25 0 1 0 422848144 81211392 18900 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19827 18900 603 41 0 19786 0
vsize: 79308
[startup+570.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 19315 0 0 0 56950 55 0 0 25 0 1 0 422848144 82006016 19087 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20021 19087 603 41 0 19980 0
vsize: 80084
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 19633 0 0 0 57949 56 0 0 25 0 1 0 422848144 83210240 19405 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20315 19405 603 41 0 20274 0
vsize: 81260
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 19858 0 0 0 58949 56 0 0 25 0 1 0 422848144 84135936 19630 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20541 19630 603 41 0 20500 0
vsize: 82164
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 20080 0 0 0 59949 57 0 0 25 0 1 0 422848144 85065728 19852 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20768 19852 603 41 0 20727 0
vsize: 83072
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 20313 0 0 0 60948 58 0 0 25 0 1 0 422848144 86003712 20085 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20997 20085 603 41 0 20956 0
vsize: 83988
[startup+620.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 20502 0 0 0 61948 58 0 0 25 0 1 0 422848144 86806528 20274 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21193 20274 603 41 0 21152 0
vsize: 84772
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 20651 0 0 0 62947 59 0 0 25 0 1 0 422848144 87343104 20423 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21324 20423 603 41 0 21283 0
vsize: 85296
[startup+640.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 20882 0 0 0 63947 59 0 0 25 0 1 0 422848144 88281088 20654 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21553 20654 603 41 0 21512 0
vsize: 86212
[startup+650.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 21083 0 0 0 64947 60 0 0 25 0 1 0 422848144 89075712 20855 4294967295 134512640 134672761 3221224528 3221223632 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21747 20855 603 41 0 21706 0
vsize: 86988
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 21262 0 0 0 65946 60 0 0 25 0 1 0 422848144 89866240 21034 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21940 21034 603 41 0 21899 0
vsize: 87760
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 21465 0 0 0 66946 61 0 0 25 0 1 0 422848144 90660864 21237 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22134 21237 603 41 0 22093 0
vsize: 88536
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 21661 0 0 0 67945 62 0 0 25 0 1 0 422848144 91463680 21433 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22330 21433 603 41 0 22289 0
vsize: 89320
[startup+690.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 21828 0 0 0 68945 62 0 0 25 0 1 0 422848144 92131328 21600 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22493 21600 603 41 0 22452 0
vsize: 89972
[startup+700.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 21979 0 0 0 69945 63 0 0 25 0 1 0 422848144 92663808 21751 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22623 21751 603 41 0 22582 0
vsize: 90492
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 22170 0 0 0 70945 63 0 0 25 0 1 0 422848144 93577216 21942 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22846 21942 603 41 0 22805 0
vsize: 91384
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 22351 0 0 0 71944 64 0 0 25 0 1 0 422848144 94502912 22123 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23072 22123 603 41 0 23031 0
vsize: 92288
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 22497 0 0 0 72944 64 0 0 25 0 1 0 422848144 95023104 22269 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23199 22269 603 41 0 23158 0
vsize: 92796
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 22633 0 0 0 73943 65 0 0 25 0 1 0 422848144 95682560 22405 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23360 22405 603 41 0 23319 0
vsize: 93440
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 22889 0 0 0 74942 66 0 0 25 0 1 0 422848144 96608256 22661 4294967295 134512640 134672761 3221224528 3221223664 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23586 22661 603 41 0 23545 0
vsize: 94344
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 23028 0 0 0 75942 66 0 0 25 0 1 0 422848144 97300480 22800 4294967295 134512640 134672761 3221224528 3221223632 134560184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23755 22800 603 41 0 23714 0
vsize: 95020
[startup+770.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 23165 0 0 0 76942 67 0 0 25 0 1 0 422848144 97832960 22937 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23885 22937 603 41 0 23844 0
vsize: 95540
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 23284 0 0 0 77941 68 0 0 25 0 1 0 422848144 98230272 23056 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23982 23056 603 41 0 23941 0
vsize: 95928
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 23402 0 0 0 78941 68 0 0 25 0 1 0 422848144 98627584 23174 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24079 23174 603 41 0 24038 0
vsize: 96316
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 23536 0 0 0 79941 68 0 0 25 0 1 0 422848144 99164160 23308 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24210 23308 603 41 0 24169 0
vsize: 96840
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 23677 0 0 0 80941 69 0 0 25 0 1 0 422848144 99876864 23449 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24384 23449 603 41 0 24343 0
vsize: 97536
[startup+820.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 23819 0 0 0 81940 70 0 0 25 0 1 0 422848144 100667392 23591 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24577 23591 603 41 0 24536 0
vsize: 98308
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 23904 0 0 0 82940 70 0 0 25 0 1 0 422848144 101060608 23676 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24673 23676 603 41 0 24632 0
vsize: 98692
[startup+840.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 23978 0 0 0 83940 70 0 0 25 0 1 0 422848144 101322752 23750 4294967295 134512640 134672761 3221224528 3221223728 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24737 23750 603 41 0 24696 0
vsize: 98948
[startup+850.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 24058 0 0 0 84940 71 0 0 25 0 1 0 422848144 101720064 23830 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24834 23830 603 41 0 24793 0
vsize: 99336
[startup+860.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 24209 0 0 0 85940 71 0 0 25 0 1 0 422848144 102227968 23981 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24958 23981 603 41 0 24917 0
vsize: 99832
[startup+870.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 24318 0 0 0 86939 71 0 0 25 0 1 0 422848144 102895616 24090 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25121 24090 603 41 0 25080 0
vsize: 100484
[startup+880.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 24514 0 0 0 87939 72 0 0 25 0 1 0 422848144 103682048 24286 4294967295 134512640 134672761 3221224528 3221223664 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25313 24286 603 41 0 25272 0
vsize: 101252
[startup+890.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 24721 0 0 0 88938 73 0 0 25 0 1 0 422848144 104484864 24493 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25509 24493 603 41 0 25468 0
vsize: 102036
[startup+900.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 24918 0 0 0 89938 73 0 0 25 0 1 0 422848144 105279488 24690 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25703 24690 603 41 0 25662 0
vsize: 102812
[startup+910.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25068 0 0 0 90938 73 0 0 25 0 1 0 422848144 105820160 24840 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25835 24840 603 41 0 25794 0
vsize: 103340
[startup+920.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25224 0 0 0 91937 74 0 0 25 0 1 0 422848144 106487808 24996 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25998 24996 603 41 0 25957 0
vsize: 103992
[startup+930.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25383 0 0 0 92937 74 0 0 25 0 1 0 422848144 107151360 25155 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26160 25155 603 41 0 26119 0
vsize: 104640
[startup+940.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 93937 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+950.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 94938 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223632 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+960.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 95938 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223632 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+970.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 96938 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+980.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 97938 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223632 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+990.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 98938 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 99938 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223632 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 100939 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 101939 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 102939 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 103939 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 104939 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 105939 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223664 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 106940 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 107940 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 108940 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25409 0 0 0 109940 74 0 0 25 0 1 0 422848144 107286528 25181 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25181 603 41 0 26152 0
vsize: 104772
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25410 0 0 0 110940 74 0 0 25 0 1 0 422848144 107286528 25182 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25182 603 41 0 26152 0
vsize: 104772
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25410 0 0 0 111941 74 0 0 25 0 1 0 422848144 107286528 25182 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25182 603 41 0 26152 0
vsize: 104772
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25410 0 0 0 112941 74 0 0 25 0 1 0 422848144 107286528 25182 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25182 603 41 0 26152 0
vsize: 104772
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25410 0 0 0 113941 74 0 0 25 0 1 0 422848144 107286528 25182 4294967295 134512640 134672761 3221224528 3221223664 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25182 603 41 0 26152 0
vsize: 104772
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25410 0 0 0 114941 74 0 0 25 0 1 0 422848144 107286528 25182 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25182 603 41 0 26152 0
vsize: 104772
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28503
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25410 0 0 0 115941 74 0 0 25 0 1 0 422848144 107286528 25182 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25182 603 41 0 26152 0
vsize: 104772
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 28504
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25410 0 0 0 116942 74 0 0 25 0 1 0 422848144 107286528 25182 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25182 603 41 0 26152 0
vsize: 104772
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28556
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25410 0 0 0 117942 74 0 0 25 0 1 0 422848144 107286528 25182 4294967295 134512640 134672761 3221224528 3221223632 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25182 603 41 0 26152 0
vsize: 104772
[startup+1190.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28556
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25410 0 0 0 118942 74 0 0 25 0 1 0 422848144 107286528 25182 4294967295 134512640 134672761 3221224528 3221223728 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25182 603 41 0 26152 0
vsize: 104772
[startup+1200.01 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28556
Raw data (stat): 28503 (minisat+) R 28502 22932 22931 0 -1 0 25410 0 0 0 119942 74 0 0 25 0 1 0 422848144 107286528 25182 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26193 25182 603 41 0 26152 0
vsize: 104772
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.06 0.99 0.91 1/54 28556
Raw data (stat): 28503 (minisat+) Z 28502 22932 22931 0 -1 12 25412 0 0 0 119942 79 0 0 25 0 1 0 422848144 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.22
CPU user time (s): 1199.43
CPU system time (s): 0.796878
CPU usage (%): 100.014
Max. virtual memory (Kb): 104772
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####