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.8.accl.ucl.opb
MD5SUM	0e5bfa52e1e730089f4eefb216f69dfd
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	73
Number of bits of the biggest number in a constraint	7
Biggest sum of numbers in a constraint	262
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	21380
Total number of constraints	60984
Number of constraints which are clauses	58828
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2156
Minimum length of a constraint	1
Maximum length of a constraint	13
Trace number 5605

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-14 00:47:13 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4060 boxname=wulflinc24 idbench=300 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0e5bfa52e1e730089f4eefb216f69dfd  /oldhome/oroussel/tmp/wulflinc24/normalized-ooo.burch_dill.8.accl.ucl.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc24/normalized-ooo.burch_dill.8.accl.ucl.opb /oldhome/oroussel/tmp/wulflinc24/normalized-ooo.burch_dill.8.accl.ucl.opb
IDLAUNCH: 4060
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 3
cpu MHz		: 451.080
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:        835348 kB
Buffers:         34684 kB
Cached:         121560 kB
SwapCached:       3828 kB
Active:          53132 kB
Inactive:       109808 kB
HighTotal:      131008 kB
HighFree:         7140 kB
LowTotal:       903652 kB
LowFree:        828208 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30756 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:07:15 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 4060 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 60983 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[60963]---> BDD-cost:    1
c ---[60958]---> BDD-cost:    1
c ---[60944]---> BDD-cost:    1
c ---[60936]---> BDD-cost:    1
c ---[60892]---> BDD-cost:    1
c ---[60884]---> BDD-cost:    1
c ---[60870]---> BDD-cost:    1
c ---[60826]---> BDD-cost:    1
c ---[60812]---> BDD-cost:    1
c ---[60738]---> BDD-cost:    1
c ---[60730]---> BDD-cost:    1
c ---[60716]---> BDD-cost:    1
c ---[60675]---> BDD-cost:    1
c ---[60637]---> BDD-cost:    1
c ---[60617]---> BDD-cost:    1
c ---[60513]---> BDD-cost:    1
c ---[60505]---> BDD-cost:    1
c ---[60491]---> BDD-cost:    1
c ---[60450]---> BDD-cost:    1
c ---[60412]---> BDD-cost:    1
c ---[60374]---> BDD-cost:    1
c ---[60348]---> BDD-cost:    1
c ---[60211]---> BDD-cost:    1
c ---[60203]---> BDD-cost:    1
c ---[60189]---> BDD-cost:    1
c ---[60148]---> BDD-cost:    1
c ---[60110]---> BDD-cost:    1
c ---[60072]---> BDD-cost:    1
c ---[60034]---> BDD-cost:    1
c ---[60002]---> BDD-cost:    1
c ---[59829]---> BDD-cost:    1
c ---[59821]---> BDD-cost:    1
c ---[59807]---> BDD-cost:    1
c ---[59766]---> BDD-cost:    1
c ---[59728]---> BDD-cost:    1
c ---[59690]---> BDD-cost:    1
c ---[59652]---> BDD-cost:    1
c ---[59614]---> BDD-cost:    1
c ---[59576]---> BDD-cost:    1
c ---[59364]---> BDD-cost:    1
c ---[59356]---> BDD-cost:    1
c ---[59342]---> BDD-cost:    1
c ---[59301]---> BDD-cost:    1
c ---[59263]---> BDD-cost:    1
c ---[59225]---> BDD-cost:    1
c ---[59187]---> BDD-cost:    1
c ---[59149]---> BDD-cost:    1
c ---[59111]---> BDD-cost:    1
c ---[59067]---> BDD-cost:    1
c ---[58813]---> BDD-cost:    1
c ---[58805]---> BDD-cost:    1
c ---[58791]---> BDD-cost:    1
c ---[58750]---> BDD-cost:    1
c ---[58712]---> BDD-cost:    1
c ---[58674]---> BDD-cost:    1
c ---[58636]---> BDD-cost:    1
c ---[58598]---> BDD-cost:    1
c ---[58560]---> BDD-cost:    1
c ---[58522]---> BDD-cost:    1
c ---[58472]---> BDD-cost:    1
c ---[58146]---> BDD-cost:    1
c ---[58123]---> BDD-cost:    1
c ---[58115]---> BDD-cost:    1
c ---[58086]---> BDD-cost:    1
c ---[58078]---> BDD-cost:    1
c ---[58064]---> BDD-cost:    1
c ---[58041]---> BDD-cost:    1
c ---[58033]---> BDD-cost:    1
c ---[58025]---> BDD-cost:    1
c ---[58005]---> BDD-cost:    1
c ---[57973]---> BDD-cost:    1
c ---[57965]---> BDD-cost:    1
c ---[57957]---> BDD-cost:    1
c ---[57949]---> BDD-cost:    1
c ---[57923]---> BDD-cost:    1
c ---[57900]---> BDD-cost:    1
c ---[57892]---> BDD-cost:    1
c ---[57884]---> BDD-cost:    1
c ---[57876]---> BDD-cost:    1
c ---[57868]---> BDD-cost:    1
c ---[57836]---> BDD-cost:    1
c ---[57804]---> BDD-cost:    1
c ---[57796]---> BDD-cost:    1
c ---[57788]---> BDD-cost:    1
c ---[57780]---> BDD-cost:    1
c ---[57772]---> BDD-cost:    1
c ---[57764]---> BDD-cost:    1
c ---[57726]---> BDD-cost:    1
c ---[57703]---> BDD-cost:    1
c ---[57695]---> BDD-cost:    1
c ---[57687]---> BDD-cost:    1
c ---[57679]---> BDD-cost:    1
c ---[57671]---> BDD-cost:    1
c ---[57663]---> BDD-cost:    1
c ---[57655]---> BDD-cost:    1
c ---[57611]---> BDD-cost:    1
c ---[57579]---> BDD-cost:    1
c ---[57571]---> BDD-cost:    1
c ---[57563]---> BDD-cost:    1
c ---[57555]---> BDD-cost:    1
c ---[57547]---> BDD-cost:    1
c ---[57539]---> BDD-cost:    1
c ---[57531]---> BDD-cost:    1
c ---[57523]---> BDD-cost:    1
c ---[57473]---> BDD-cost:    1
c ---[57450]---> BDD-cost:    1
c ---[57442]---> BDD-cost:    1
c ---[57434]---> BDD-cost:    1
c ---[57426]---> BDD-cost:    1
c ---[57418]---> BDD-cost:    1
c ---[57410]---> BDD-cost:    1
c ---[57402]---> BDD-cost:    1
c ---[57394]---> BDD-cost:    1
c ---[57386]---> BDD-cost:    1
c ---[57330]---> BDD-cost:    1
c ---[57298]---> BDD-cost:    1
c ---[57290]---> BDD-cost:    1
c ---[57282]---> BDD-cost:    1
c ---[57274]---> BDD-cost:    1
c ---[57266]---> BDD-cost:    1
c ---[57258]---> BDD-cost:    1
c ---[57250]---> BDD-cost:    1
c ---[57242]---> BDD-cost:    1
c ---[57234]---> BDD-cost:    1
c ---[57226]---> BDD-cost:    1
c ---[57164]---> BDD-cost:    1
c ---[57141]---> BDD-cost:    1
c ---[57133]---> BDD-cost:    1
c ---[57125]---> BDD-cost:    1
c ---[57117]---> BDD-cost:    1
c ---[57109]---> BDD-cost:    1
c ---[57101]---> BDD-cost:    1
c ---[57093]---> BDD-cost:    1
c ---[57085]---> BDD-cost:    1
c ---[57077]---> BDD-cost:    1
c ---[57069]---> BDD-cost:    1
c ---[57061]---> BDD-cost:    1
c ---[56993]---> BDD-cost:    1
c ---[56961]---> BDD-cost:    1
c ---[56953]---> BDD-cost:    1
c ---[56945]---> BDD-cost:    1
c ---[56937]---> BDD-cost:    1
c ---[56929]---> BDD-cost:    1
c ---[56921]---> BDD-cost:    1
c ---[56913]---> BDD-cost:    1
c ---[56905]---> BDD-cost:    1
c ---[56897]---> BDD-cost:    1
c ---[56889]---> BDD-cost:    1
c ---[56881]---> BDD-cost:    1
c ---[56873]---> BDD-cost:    1
c ---[56799]---> BDD-cost:    1
c ---[56776]---> BDD-cost:    1
c ---[56768]---> BDD-cost:    1
c ---[56760]---> BDD-cost:    1
c ---[56752]---> BDD-cost:    1
c ---[56744]---> BDD-cost:    1
c ---[56736]---> BDD-cost:    1
c ---[56728]---> BDD-cost:    1
c ---[56720]---> BDD-cost:    1
c ---[56712]---> BDD-cost:    1
c ---[56704]---> BDD-cost:    1
c ---[56696]---> BDD-cost:    1
c ---[56688]---> BDD-cost:    1
c ---[56680]---> BDD-cost:    1
c ---[56600]---> BDD-cost:    1
c ---[56568]---> BDD-cost:    1
c ---[56560]---> BDD-cost:    1
c ---[56552]---> BDD-cost:    1
c ---[56544]---> BDD-cost:    1
c ---[56536]---> BDD-cost:    1
c ---[56528]---> BDD-cost:    1
c ---[56520]---> BDD-cost:    1
c ---[56512]---> BDD-cost:    1
c ---[56504]---> BDD-cost:    1
c ---[56496]---> BDD-cost:    1
c ---[56488]---> BDD-cost:    1
c ---[56480]---> BDD-cost:    1
c ---[56472]---> BDD-cost:    1
c ---[56464]---> BDD-cost:    1
c ---[56378]---> BDD-cost:    1
c ---[56355]---> BDD-cost:    1
c ---[56347]---> BDD-cost:    1
c ---[56339]---> BDD-cost:    1
c ---[56331]---> BDD-cost:    1
c ---[56323]---> BDD-cost:    1
c ---[56315]---> BDD-cost:    1
c ---[56307]---> BDD-cost:    1
c ---[56299]---> BDD-cost:    1
c ---[56291]---> BDD-cost:    1
c ---[56283]---> BDD-cost:    1
c ---[56275]---> BDD-cost:    1
c ---[56267]---> BDD-cost:    1
c ---[56259]---> BDD-cost:    1
c ---[56251]---> BDD-cost:    1
c ---[56243]---> BDD-cost:    1
c ---[56151]---> BDD-cost:    1
c ---[56114]---> BDD-cost:    1
c ---[56082]---> BDD-cost:    1
c ---[56035]---> BDD-cost:    1
c ---[55973]---> BDD-cost:    1
c ---[55896]---> BDD-cost:    1
c ---[55804]---> BDD-cost:    1
c ---[55700]---> BDD-cost:    1
c ---[55698]---> BDD-cost:    1
c ---[55696]---> BDD-cost:    1
c ---[55694]---> BDD-cost:    1
c ---[55692]---> BDD-cost:    1
c ---[55690]---> BDD-cost:    1
c ---[55688]---> BDD-cost:    1
c ---[55686]---> BDD-cost:    1
c ---[55684]---> BDD-cost:    1
c ---[55409]---> BDD-cost:    1
c ---[55401]---> BDD-cost:    1
c ---[55393]---> BDD-cost:    1
c ---[55385]---> BDD-cost:    1
c ---[55377]---> BDD-cost:    1
c ---[55369]---> BDD-cost:    1
c ---[55361]---> BDD-cost:    1
c ---[55353]---> BDD-cost:    1
c ---[55219]---> BDD-cost:    1
c ---[55211]---> BDD-cost:    1
c ---[55203]---> BDD-cost:    1
c ---[55195]---> BDD-cost:    1
c ---[55187]---> BDD-cost:    1
c ---[55179]---> BDD-cost:    1
c ---[55171]---> BDD-cost:    1
c ---[55163]---> BDD-cost:    1
c ---[55155]---> BDD-cost:    1
c ---[55147]---> BDD-cost:    1
c ---[55139]---> BDD-cost:    1
c ---[55131]---> BDD-cost:    1
c ---[55123]---> BDD-cost:    1
c ---[55115]---> BDD-cost:    1
c ---[55107]---> BDD-cost:    1
c ---[55099]---> BDD-cost:    1
c ---[55001]---> BDD-cost:    1
c ---[54996]---> BDD-cost:    1
c ---[54964]---> BDD-cost:    1
c ---[54935]---> BDD-cost:    1
c ---[54930]---> BDD-cost:    1
c ---[54925]---> BDD-cost:    1
c ---[54920]---> BDD-cost:    1
c ---[54915]---> BDD-cost:    1
c ---[54910]---> BDD-cost:    1
c ---[54905]---> BDD-cost:    1
c ---[54900]---> BDD-cost:    1
c ---[54895]---> BDD-cost:    1
c ---[54890]---> BDD-cost:    1
c ---[54885]---> BDD-cost:    1
c ---[54880]---> BDD-cost:    1
c ---[54875]---> BDD-cost:    1
c ---[54870]---> BDD-cost:    1
c ---[54865]---> BDD-cost:    1
c ---[54860]---> BDD-cost:    1
c ---[54750]---> BDD-cost:    1
c ---[54727]---> BDD-cost:    1
c ---[54707]---> BDD-cost:    1
c ---[54678]---> BDD-cost:    1
c ---[54613]---> BDD-cost:    1
c ---[54584]---> BDD-cost:    1
c ---[54537]---> BDD-cost:    1
c ---[54523]---> BDD-cost:    1
c ---[54506]---> BDD-cost:    1
c ---[54489]---> BDD-cost:    1
c ---[54472]---> BDD-cost:    1
c ---[54455]---> BDD-cost:    1
c ---[54438]---> BDD-cost:    1
c ---[54421]---> BDD-cost:    1
c ---[54404]---> BDD-cost:    1
c ---[54387]---> BDD-cost:    1
c ---[54370]---> BDD-cost:    1
c ---[54353]---> BDD-cost:    1
c ---[54336]---> BDD-cost:    1
c ---[54319]---> BDD-cost:    1
c ---[54302]---> BDD-cost:    1
c ---[54285]---> BDD-cost:    1
c ---[54163]---> BDD-cost:    1
c ---[54155]---> BDD-cost:    1
c ---[54150]---> BDD-cost:    1
c ---[54145]---> BDD-cost:    1
c ---[54125]---> BDD-cost:    1
c ---[54111]---> BDD-cost:    1
c ---[54079]---> BDD-cost:    1
c ---[53999]---> BDD-cost:    1
c ---[53949]---> BDD-cost:    1
c ---[53788]---> BDD-cost:    1
c ---[53735]---> BDD-cost:    1
c ---[53685]---> BDD-cost:    1
c ---[53575]---> BDD-cost:    1
c ---[53555]---> BDD-cost:    1
c ---[53532]---> BDD-cost:    1
c ---[53509]---> BDD-cost:    1
c ---[53486]---> BDD-cost:    1
c ---[53463]---> BDD-cost:    1
c ---[53440]---> BDD-cost:    1
c ---[53417]---> BDD-cost:    1
c ---[53394]---> BDD-cost:    1
c ---[53371]---> BDD-cost:    1
c ---[53348]---> BDD-cost:    1
c ---[53325]---> BDD-cost:    1
c ---[53302]---> BDD-cost:    1
c ---[53279]---> BDD-cost:    1
c ---[53256]---> BDD-cost:    1
c ---[53233]---> BDD-cost:    1
c ---[53099]---> BDD-cost:    1
c ---[53091]---> BDD-cost:    1
c ---[53086]---> BDD-cost:    1
c ---[53081]---> BDD-cost:    1
c ---[53076]---> BDD-cost:    1
c ---[53050]---> BDD-cost:    1
c ---[53036]---> BDD-cost:    1
c ---[53016]---> BDD-cost:    1
c ---[52972]---> BDD-cost:    1
c ---[52850]---> BDD-cost:    1
c ---[52791]---> BDD-cost:    1
c ---[52654]---> BDD-cost:    1
c ---[52370]---> BDD-cost:    1
c ---[52308]---> BDD-cost:    1
c ---[52249]---> BDD-cost:    1
c ---[52148]---> BDD-cost:    1
c ---[51960]---> BDD-cost:    1
c ---[51934]---> BDD-cost:    1
c ---[51905]---> BDD-cost:    1
c ---[51876]---> BDD-cost:    1
c ---[51847]---> BDD-cost:    1
c ---[51818]---> BDD-cost:    1
c ---[51789]---> BDD-cost:    1
c ---[51760]---> BDD-cost:    1
c ---[51731]---> BDD-cost:    1
c ---[51702]---> BDD-cost:    1
c ---[51673]---> BDD-cost:    1
c ---[51644]---> BDD-cost:    1
c ---[51615]---> BDD-cost:    1
c ---[51586]---> BDD-cost:    1
c ---[51557]---> BDD-cost:    1
c ---[51528]---> BDD-cost:    1
c ---[51382]---> BDD-cost:    1
c ---[51374]---> BDD-cost:    1
c ---[51369]---> BDD-cost:    1
c ---[51364]---> BDD-cost:    1
c ---[51359]---> BDD-cost:    1
c ---[51354]---> BDD-cost:    1
c ---[51322]---> BDD-cost:    1
c ---[51308]---> BDD-cost:    1
c ---[51288]---> BDD-cost:    1
c ---[51262]---> BDD-cost:    1
c ---[51206]---> BDD-cost:    1
c ---[51027]---> BDD-cost:    1
c ---[50956]---> BDD-cost:    1
c ---[50783]---> BDD-cost:    1
c ---[50526]---> BDD-cost:    1
c ---[50086]---> BDD-cost:    1
c ---[50012]---> BDD-cost:    1
c ---[49941]---> BDD-cost:    1
c ---[49816]---> BDD-cost:    1
c ---[49637]---> BDD-cost:    1
c ---[49347]---> BDD-cost:    1
c ---[49315]---> BDD-cost:    1
c ---[49280]---> BDD-cost:    1
c ---[49245]---> BDD-cost:    1
c ---[49210]---> BDD-cost:    1
c ---[49175]---> BDD-cost:    1
c ---[49140]---> BDD-cost:    1
c ---[49105]---> BDD-cost:    1
c ---[49070]---> BDD-cost:    1
c ---[49035]---> BDD-cost:    1
c ---[49000]---> BDD-cost:    1
c ---[48965]---> BDD-cost:    1
c ---[48930]---> BDD-cost:    1
c ---[48895]---> BDD-cost:    1
c ---[48860]---> BDD-cost:    1
c ---[48825]---> BDD-cost:    1
c ---[48667]---> BDD-cost:    1
c ---[48659]---> BDD-cost:    1
c ---[48654]---> BDD-cost:    1
c ---[48649]---> BDD-cost:    1
c ---[48644]---> BDD-cost:    1
c ---[48639]---> BDD-cost:    1
c ---[48634]---> BDD-cost:    1
c ---[48596]---> BDD-cost:    1
c ---[48582]---> BDD-cost:    1
c ---[48562]---> BDD-cost:    1
c ---[48536]---> BDD-cost:    1
c ---[48504]---> BDD-cost:    1
c ---[48436]---> BDD-cost:    1
c ---[48188]---> BDD-cost:    1
c ---[48105]---> BDD-cost:    1
c ---[47896]---> BDD-cost:    1
c ---[47585]---> BDD-cost:    1
c ---[47175]---> BDD-cost:    1
c ---[46543]---> BDD-cost:    1
c ---[46457]---> BDD-cost:    1
c ---[46374]---> BDD-cost:    1
c ---[46225]---> BDD-cost:    1
c ---[46010]---> BDD-cost:    1
c ---[45729]---> BDD-cost:    1
c ---[45313]---> BDD-cost:    1
c ---[45275]---> BDD-cost:    1
c ---[45234]---> BDD-cost:    1
c ---[45193]---> BDD-cost:    1
c ---[45152]---> BDD-cost:    1
c ---[45111]---> BDD-cost:    1
c ---[45070]---> BDD-cost:    1
c ---[45029]---> BDD-cost:    1
c ---[44988]---> BDD-cost:    1
c ---[44947]---> BDD-cost:    1
c ---[44906]---> BDD-cost:    1
c ---[44865]---> BDD-cost:    1
c ---[44824]---> BDD-cost:    1
c ---[44783]---> BDD-cost:    1
c ---[44742]---> BDD-cost:    1
c ---[44701]---> BDD-cost:    1
c ---[44531]---> BDD-cost:    1
c ---[44523]---> BDD-cost:    1
c ---[44518]---> BDD-cost:    1
c ---[44513]---> BDD-cost:    1
c ---[44508]---> BDD-cost:    1
c ---[44503]---> BDD-cost:    1
c ---[44498]---> BDD-cost:    1
c ---[44493]---> BDD-cost:    1
c ---[44449]---> BDD-cost:    1
c ---[44435]---> BDD-cost:    1
c ---[44415]---> BDD-cost:    1
c ---[44389]---> BDD-cost:    1
c ---[44357]---> BDD-cost:    1
c ---[44319]---> BDD-cost:    1
c ---[44239]---> BDD-cost:    1
c ---[43910]---> BDD-cost:    1
c ---[43815]---> BDD-cost:    1
c ---[43570]---> BDD-cost:    1
c ---[43205]---> BDD-cost:    1
c ---[42723]---> BDD-cost:    1
c ---[42124]---> BDD-cost:    1
c ---[41264]---> BDD-cost:    1
c ---[41166]---> BDD-cost:    1
c ---[41071]---> BDD-cost:    1
c ---[40898]---> BDD-cost:    1
c ---[40647]---> BDD-cost:    1
c ---[40318]---> BDD-cost:    1
c ---[39911]---> BDD-cost:    1
c ---[39345]---> BDD-cost:    1
c ---[39301]---> BDD-cost:    1
c ---[39254]---> BDD-cost:    1
c ---[39207]---> BDD-cost:    1
c ---[39160]---> BDD-cost:    1
c ---[39113]---> BDD-cost:    1
c ---[39066]---> BDD-cost:    1
c ---[39019]---> BDD-cost:    1
c ---[38972]---> BDD-cost:    1
c ---[38925]---> BDD-cost:    1
c ---[38878]---> BDD-cost:    1
c ---[38831]---> BDD-cost:    1
c ---[38784]---> BDD-cost:    1
c ---[38737]---> BDD-cost:    1
c ---[38690]---> BDD-cost:    1
c ---[38643]---> BDD-cost:    1
c ---[38461]---> BDD-cost:    1
c ---[38192]---> BDD-cost:    1
c ---[38139]---> BDD-cost:    1
c ---[38086]---> BDD-cost:    1
c ---[38033]---> BDD-cost:    1
c ---[37980]---> BDD-cost:    1
c ---[37927]---> BDD-cost:    1
c ---[37874]---> BDD-cost:    1
c ---[37821]---> BDD-cost:    1
c ---[37768]---> BDD-cost:    1
c ---[37715]---> BDD-cost:    1
c ---[37662]---> BDD-cost:    1
c ---[37609]---> BDD-cost:    1
c ---[37556]---> BDD-cost:    1
c ---[37503]---> BDD-cost:    1
c ---[37450]---> BDD-cost:    1
c ---[37397]---> BDD-cost:    1
c ---[37392]---> BDD-cost:    1
c ---[37384]---> BDD-cost:    1
c ---[37379]---> BDD-cost:    1
c ---[37374]---> BDD-cost:    1
c ---[37369]---> BDD-cost:    1
c ---[37364]---> BDD-cost:    1
c ---[37359]---> BDD-cost:    1
c ---[37189]---> BDD-cost:    1
c ---[37187]---> BDD-cost:    1
c ---[37185]---> BDD-cost:    1
c ---[37183]---> BDD-cost:    1
c ---[37181]---> BDD-cost:    1
c ---[37179]---> BDD-cost:    1
c ---[37177]---> BDD-cost:    1
c ---[37154]---> BDD-cost:    1
c ---[37152]---> BDD-cost:    1
c ---[37150]---> BDD-cost:    1
c ---[37148]---> BDD-cost:    1
c ---[37146]---> BDD-cost:    1
c ---[37144]---> BDD-cost:    1
c ---[37142]---> BDD-cost:    1
c ---[37110]---> BDD-cost:    1
c ---[37096]---> BDD-cost:    1
c ---[37094]---> BDD-cost:    1
c ---[37092]---> BDD-cost:    1
c ---[37090]---> BDD-cost:    1
c ---[37088]---> BDD-cost:    1
c ---[37086]---> BDD-cost:    1
c ---[37066]---> BDD-cost:    1
c ---[37064]---> BDD-cost:    1
c ---[37062]---> BDD-cost:    1
c ---[37060]---> BDD-cost:    1
c ---[37058]---> BDD-cost:    1
c ---[37056]---> BDD-cost:    1
c ---[37027]---> BDD-cost:    1
c ---[36998]---> BDD-cost:    1
c ---[36996]---> BDD-cost:    1
c ---[36994]---> BDD-cost:    1
c ---[36992]---> BDD-cost:    1
c ---[36990]---> BDD-cost:    1
c ---[36973]---> BDD-cost:    1
c ---[36971]---> BDD-cost:    1
c ---[36969]---> BDD-cost:    1
c ---[36967]---> BDD-cost:    1
c ---[36965]---> BDD-cost:    1
c ---[36939]---> BDD-cost:    1
c ---[36892]---> BDD-cost:    1
c ---[36890]---> BDD-cost:    1
c ---[36888]---> BDD-cost:    1
c ---[36886]---> BDD-cost:    1
c ---[36872]---> BDD-cost:    1
c ---[36870]---> BDD-cost:    1
c ---[36868]---> BDD-cost:    1
c ---[36866]---> BDD-cost:    1
c ---[36843]---> BDD-cost:    1
c ---[36775]---> BDD-cost:    1
c ---[36773]---> BDD-cost:    1
c ---[36771]---> BDD-cost:    1
c ---[36760]---> BDD-cost:    1
c ---[36758]---> BDD-cost:    1
c ---[36756]---> BDD-cost:    1
c ---[36736]---> BDD-cost:    1
c ---[36644]---> BDD-cost:    1
c ---[36642]---> BDD-cost:    1
c ---[36634]---> BDD-cost:    1
c ---[36632]---> BDD-cost:    1
c ---[36615]---> BDD-cost:    1
c ---[36496]---> BDD-cost:    1
c ---[36491]---> BDD-cost:    1
c ---[36477]---> BDD-cost:    1
c ---[36430]---> BDD-cost:    1
c ---[36146]---> BDD-cost:    1
c ---[35808]---> BDD-cost:    1
c ---[35704]---> BDD-cost:    1
c ---[35423]---> BDD-cost:    1
c ---[35004]---> BDD-cost:    1
c ---[34450]---> BDD-cost:    1
c ---[33761]---> BDD-cost:    1
c ---[32937]---> BDD-cost:    1
c ---[31954]---> BDD-cost:    1
c ---[31952]---> BDD-cost:    1
c ---[31950]---> BDD-cost:    1
c ---[31948]---> BDD-cost:    1
c ---[31946]---> BDD-cost:    1
c ---[31944]---> BDD-cost:    1
c ---[31942]---> BDD-cost:    1
c ---[31940]---> BDD-cost:    1
c ---[31779]---> BDD-cost:    1
c ---[31669]---> BDD-cost:    1
c ---[31565]---> BDD-cost:    1
c ---[31368]---> BDD-cost:    1
c ---[31081]---> BDD-cost:    1
c ---[30704]---> BDD-cost:    1
c ---[30237]---> BDD-cost:    1
c ---[29680]---> BDD-cost:    1
c ---[29018]---> BDD-cost:    1
c ---[29016]---> BDD-cost:    1
c ---[29014]---> BDD-cost:    1
c ---[29012]---> BDD-cost:    1
c ---[29010]---> BDD-cost:    1
c ---[29008]---> BDD-cost:    1
c ---[29006]---> BDD-cost:    1
c ---[29004]---> BDD-cost:    1
c ---[28963]---> BDD-cost:    1
c ---[28919]---> BDD-cost:    1
c ---[28785]---> BDD-cost:    1
c ---[28780]---> BDD-cost:    1
c ---[28775]---> BDD-cost:    1
c ---[28770]---> BDD-cost:    1
c ---[28765]---> BDD-cost:    1
c ---[28760]---> BDD-cost:    1
c ---[28710]---> BDD-cost:    1
c ---[28672]---> BDD-cost:    1
c ---[28520]---> BDD-cost:    1
c ---[28515]---> BDD-cost:    1
c ---[28510]---> BDD-cost:    1
c ---[28505]---> BDD-cost:    1
c ---[28500]---> BDD-cost:    1
c ---[28456]---> BDD-cost:    1
c ---[28424]---> BDD-cost:    1
c ---[28263]---> BDD-cost:    1
c ---[28258]---> BDD-cost:    1
c ---[28253]---> BDD-cost:    1
c ---[28248]---> BDD-cost:    1
c ---[28210]---> BDD-cost:    1
c ---[28184]---> BDD-cost:    1
c ---[28020]---> BDD-cost:    1
c ---[28015]---> BDD-cost:    1
c ---[28010]---> BDD-cost:    1
c ---[27978]---> BDD-cost:    1
c ---[27958]---> BDD-cost:    1
c ---[27797]---> BDD-cost:    1
c ---[27792]---> BDD-cost:    1
c ---[27766]---> BDD-cost:    1
c ---[27752]---> BDD-cost:    1
c ---[27600]---> BDD-cost:    1
c ---[27580]---> BDD-cost:    1
c ---[27509]---> BDD-cost:    1
c ---[27453]---> BDD-cost:    1
c ---[27433]---> BDD-cost:    1
c ---[27389]---> BDD-cost:    1
c ---[27357]---> BDD-cost:    1
c ---[27337]---> BDD-cost:    1
c ---[27320]---> BDD-cost:    1
c ---[27276]---> BDD-cost:    1
c ---[27259]---> BDD-cost:    1
c ---[27221]---> BDD-cost:    1
c ---[27201]---> BDD-cost:    1
c ---[27184]---> BDD-cost:    1
c ---[27167]---> BDD-cost:    1
c ---[27123]---> BDD-cost:    1
c ---[27106]---> BDD-cost:    1
c ---[27089]---> BDD-cost:    1
c ---[27045]---> BDD-cost:    1
c ---[27025]---> BDD-cost:    1
c ---[27008]---> BDD-cost:    1
c ---[26991]---> BDD-cost:    1
c ---[26974]---> BDD-cost:    1
c ---[26930]---> BDD-cost:    1
c ---[26913]---> BDD-cost:    1
c ---[26896]---> BDD-cost:    1
c ---[26879]---> BDD-cost:    1
c ---[26829]---> BDD-cost:    1
c ---[26809]---> BDD-cost:    1
c ---[26792]---> BDD-cost:    1
c ---[26775]---> BDD-cost:    1
c ---[26758]---> BDD-cost:    1
c ---[26741]---> BDD-cost:    1
c ---[26697]---> BDD-cost:    1
c ---[26680]---> BDD-cost:    1
c ---[26663]---> BDD-cost:    1
c ---[26646]---> BDD-cost:    1
c ---[26629]---> BDD-cost:    1
c ---[26573]---> BDD-cost:    1
c ---[26526]---> BDD-cost:    1
c ---[26524]---> BDD-cost:    1
c ---[26522]---> BDD-cost:    1
c ---[26520]---> BDD-cost:    1
c ---[26518]---> BDD-cost:    1
c ---[26516]---> BDD-cost:    1
c ---[26496]---> BDD-cost:    1
c ---[26494]---> BDD-cost:    1
c ---[26492]---> BDD-cost:    1
c ---[26490]---> BDD-cost:    1
c ---[26488]---> BDD-cost:    1
c ---[26486]---> BDD-cost:    1
c ---[26457]---> BDD-cost:    1
c ---[26455]---> BDD-cost:    1
c ---[26453]---> BDD-cost:    1
c ---[26451]---> BDD-cost:    1
c ---[26449]---> BDD-cost:    1
c ---[26447]---> BDD-cost:    1
c ---[26430]---> BDD-cost:    1
c ---[26428]---> BDD-cost:    1
c ---[26426]---> BDD-cost:    1
c ---[26424]---> BDD-cost:    1
c ---[26422]---> BDD-cost:    1
c ---[26396]---> BDD-cost:    1
c ---[26394]---> BDD-cost:    1
c ---[26392]---> BDD-cost:    1
c ---[26390]---> BDD-cost:    1
c ---[26388]---> BDD-cost:    1
c ---[26374]---> BDD-cost:    1
c ---[26372]---> BDD-cost:    1
c ---[26370]---> BDD-cost:    1
c ---[26368]---> BDD-cost:    1
c ---[26345]---> BDD-cost:    1
c ---[26343]---> BDD-cost:    1
c ---[26341]---> BDD-cost:    1
c ---[26339]---> BDD-cost:    1
c ---[26328]---> BDD-cost:    1
c ---[26326]---> BDD-cost:    1
c ---[26324]---> BDD-cost:    1
c ---[26304]---> BDD-cost:    1
c ---[26302]---> BDD-cost:    1
c ---[26300]---> BDD-cost:    1
c ---[26292]---> BDD-cost:    1
c ---[26290]---> BDD-cost:    1
c ---[26273]---> BDD-cost:    1
c ---[26271]---> BDD-cost:    1
c ---[26266]---> BDD-cost:    1
c ---[26252]---> BDD-cost:    1
c ---[26205]---> BDD-cost:    1
c ---[26188]---> BDD-cost:    1
c ---[26171]---> BDD-cost:    1
c ---[26154]---> BDD-cost:    1
c ---[26137]---> BDD-cost:    1
c ---[26120]---> BDD-cost:    1
c ---[26103]---> BDD-cost:    1
c ---[26080]---> BDD-cost:    1
c ---[26078]---> BDD-cost:    1
c ---[26076]---> BDD-cost:    1
c ---[26074]---> BDD-cost:    1
c ---[26072]---> BDD-cost:    1
c ---[26070]---> BDD-cost:    1
c ---[26068]---> BDD-cost:    1
c ---[26030]---> BDD-cost:    1
c ---[26013]---> BDD-cost:    1
c ---[25996]---> BDD-cost:    1
c ---[25979]---> BDD-cost:    1
c ---[25962]---> BDD-cost:    1
c ---[25945]---> BDD-cost:    1
c ---[25931]---> BDD-cost:    1
c ---[25929]---> BDD-cost:    1
c ---[25927]---> BDD-cost:    1
c ---[25925]---> BDD-cost:    1
c ---[25923]---> BDD-cost:    1
c ---[25921]---> BDD-cost:    1
c ---[25919]---> BDD-cost:    1
c ---[25878]---> BDD-cost:    1
c ---[25873]---> BDD-cost:    1
c ---[25868]---> BDD-cost:    1
c ---[25863]---> BDD-cost:    1
c ---[25858]---> BDD-cost:    1
c ---[25808]---> BDD-cost:    1
c ---[25803]---> BDD-cost:    1
c ---[25798]---> BDD-cost:    1
c ---[25793]---> BDD-cost:    1
c ---[25749]---> BDD-cost:    1
c ---[25744]---> BDD-cost:    1
c ---[25739]---> BDD-cost:    1
c ---[25701]---> BDD-cost:    1
c ---[25696]---> BDD-cost:    1
c ---[25664]---> BDD-cost:    1
c ---[25575]---> BDD-cost:    1
c ---[25372]---> BDD-cost:    1
c ---[25190]---> BDD-cost:    1
c ---[25026]---> BDD-cost:    1
c ---[24880]---> BDD-cost:    1
c ---[24752]---> BDD-cost:    1
c ---[24642]---> BDD-cost:    1
c ---[24598]---> BDD-cost:    1
c ---[24059]---> BDD-cost:    1
c ---[23859]---> BDD-cost:    1
c ---[23683]---> BDD-cost:    1
c ---[23531]---> BDD-cost:    1
c ---[23403]---> BDD-cost:    1
c ---[23299]---> BDD-cost:    1
c ---[23219]---> BDD-cost:    1
c ---[23163]---> BDD-cost:    1
c ---[22813]---> BDD-cost:    1
c ---[22577]---> BDD-cost:    1
c ---[22377]---> BDD-cost:    1
c ---[22195]---> BDD-cost:    1
c ---[22031]---> BDD-cost:    1
c ---[21885]---> BDD-cost:    1
c ---[21844]---> BDD-cost:    1
c ---[21359]---> BDD-cost:    1
c ---[21132]---> BDD-cost:    1
c ---[20929]---> BDD-cost:    1
c ---[20750]---> BDD-cost:    1
c ---[20595]---> BDD-cost:    1
c ---[20464]---> BDD-cost:    1
c ---[20357]---> BDD-cost:    1
c ---[20277]---> BDD-cost:    1
c ---[19921]---> BDD-cost:    1
c ---[19667]---> BDD-cost:    1
c ---[19458]---> BDD-cost:    1
c ---[19267]---> BDD-cost:    1
c ---[19094]---> BDD-cost:    1
c ---[19056]---> BDD-cost:    1
c ---[18625]---> BDD-cost:    1
c ---[18371]---> BDD-cost:    1
c ---[18141]---> BDD-cost:    1
c ---[17935]---> BDD-cost:    1
c ---[17753]---> BDD-cost:    1
c ---[17595]---> BDD-cost:    1
c ---[17464]---> BDD-cost:    1
c ---[17372]---> BDD-cost:    1
c ---[17013]---> BDD-cost:    1
c ---[16744]---> BDD-cost:    1
c ---[16526]---> BDD-cost:    1
c ---[16326]---> BDD-cost:    1
c ---[16291]---> BDD-cost:    1
c ---[15905]---> BDD-cost:    1
c ---[15624]---> BDD-cost:    1
c ---[15367]---> BDD-cost:    1
c ---[15134]---> BDD-cost:    1
c ---[14925]---> BDD-cost:    1
c ---[14743]---> BDD-cost:    1
c ---[14606]---> BDD-cost:    1
c ---[14499]---> BDD-cost:    1
c ---[14137]---> BDD-cost:    1
c ---[13853]---> BDD-cost:    1
c ---[13626]---> BDD-cost:    1
c ---[13594]---> BDD-cost:    1
c ---[13244]---> BDD-cost:    1
c ---[12936]---> BDD-cost:    1
c ---[12652]---> BDD-cost:    1
c ---[12392]---> BDD-cost:    1
c ---[12159]---> BDD-cost:    1
c ---[11977]---> BDD-cost:    1
c ---[11825]---> BDD-cost:    1
c ---[11703]---> BDD-cost:    1
c ---[11338]---> BDD-cost:    1
c ---[11039]---> BDD-cost:    1
c ---[11010]---> BDD-cost:    1
c ---[10687]---> BDD-cost:    1
c ---[10352]---> BDD-cost:    1
c ---[10041]---> BDD-cost:    1
c ---[9757]---> BDD-cost:    1
c ---[9530]---> BDD-cost:    1
c ---[9333]---> BDD-cost:    1
c ---[9166]---> BDD-cost:    1
c ---[9029]---> BDD-cost:    1
c ---[8661]---> BDD-cost:    1
c ---[8635]---> BDD-cost:    1
c ---[8279]---> BDD-cost:    1
c ---[7917]---> BDD-cost:    1
c ---[7582]---> BDD-cost:    1
c ---[7310]---> BDD-cost:    1
c ---[7068]---> BDD-cost:    1
c ---[6856]---> BDD-cost:    1
c ---[6674]---> BDD-cost:    1
c ---[6522]---> BDD-cost:    1
c ---[6151]---> BDD-cost:    1
c ---[6122]---> BDD-cost:    1
c ---[5676]---> BDD-cost:    1
c ---[5359]---> BDD-cost:    1
c ---[5072]---> BDD-cost:    1
c ---[4815]---> BDD-cost:    1
c ---[4588]---> BDD-cost:    1
c ---[4391]---> BDD-cost:    1
c ---[4224]---> BDD-cost:    1
c ---[3850]---> BDD-cost:    1
c ---[3827]---> BDD-cost:    1
c ---[3813]---> BDD-cost:    1
c ---[3793]---> BDD-cost:    1
c ---[3770]---> BDD-cost:    1
c ---[3744]---> BDD-cost:    1
c ---[3715]---> BDD-cost:    1
c ---[3683]---> BDD-cost:    1
c ---[3648]---> BDD-cost:    1
c ---[3607]---> BDD-cost:    1
c ---[3590]---> BDD-cost:    1
c ---[3570]---> BDD-cost:    1
c ---[3547]---> BDD-cost:    1
c ---[3521]---> BDD-cost:    1
c ---[3492]---> BDD-cost:    1
c ---[3460]---> BDD-cost:    1
c ---[2155]---> BDD-cost:   17
c ---[2154]---> BDD-cost:    1
c ---[2153]---> BDD-cost:   17
c ---[2152]---> BDD-cost:    1
c ---[2151]---> BDD-cost:    1
c ---[2150]---> BDD-cost:    1
c ---[2149]---> BDD-cost:   17
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:   17
c ---[2142]---> BDD-cost:    1
c ---[2141]---> BDD-cost:   14
c ---[2140]---> BDD-cost:   14
c ---[2139]---> BDD-cost:    1
c ---[2138]---> BDD-cost:    1
c ---[2137]---> BDD-cost:   17
c ---[2136]---> BDD-cost:    1
c ---[2135]---> BDD-cost:    1
c ---[2134]---> BDD-cost:   17
c ---[2133]---> BDD-cost:    1
c ---[2132]---> BDD-cost:    1
c ---[2131]---> BDD-cost:   17
c ---[2130]---> BDD-cost:    1
c ---[2129]---> BDD-cost:   24
c ---[2128]---> BDD-cost:    1
c ---[2127]---> BDD-cost:   21
c ---[2126]---> BDD-cost:    1
c ---[2125]---> BDD-cost:    1
c ---[2124]---> BDD-cost:    1
c ---[2123]---> BDD-cost:   14
c ---[2122]---> BDD-cost:   14
c ---[2121]---> BDD-cost:    1
c ---[2120]---> BDD-cost:    1
c ---[2119]---> BDD-cost:   14
c ---[2118]---> BDD-cost:   14
c ---[2117]---> BDD-cost:    1
c ---[2116]---> BDD-cost:    1
c ---[2115]---> BDD-cost:   14
c ---[2114]---> BDD-cost:   14
c ---[2113]---> BDD-cost:    1
c ---[2112]---> BDD-cost:    1
c ---[2111]---> BDD-cost:   14
c ---[2110]---> BDD-cost:   14
c ---[2109]---> BDD-cost:    1
c ---[2108]---> BDD-cost:    1
c ---[2107]---> BDD-cost:    1
c ---[2106]---> BDD-cost:    1
c ---[2105]---> BDD-cost:   21
c ---[2104]---> BDD-cost:    1
c ---[2103]---> BDD-cost:   24
c ---[2102]---> BDD-cost:    1
c ---[2101]---> BDD-cost:    1
c ---[2100]---> BDD-cost:    1
c ---[2099]---> BDD-cost:    1
c ---[2098]---> BDD-cost:    1
c ---[2097]---> BDD-cost:    1
c ---[2096]---> BDD-cost:   17
c ---[2095]---> BDD-cost:    1
c ---[2094]---> BDD-cost:    1
c ---[2093]---> BDD-cost:   17
c ---[2092]---> BDD-cost:    1
c ---[2091]---> BDD-cost:   21
c ---[2090]---> BDD-cost:    1
c ---[2089]---> BDD-cost:   21
c ---[2088]---> BDD-cost:    1
c ---[2087]---> BDD-cost:    1
c ---[2086]---> BDD-cost:    1
c ---[2085]---> BDD-cost:   14
c ---[2084]---> BDD-cost:   14
c ---[2083]---> BDD-cost:    1
c ---[2082]---> BDD-cost:    1
c ---[2081]---> BDD-cost:   14
c ---[2080]---> BDD-cost:   14
c ---[2079]---> BDD-cost:    1
c ---[2078]---> BDD-cost:    1
c ---[2077]---> BDD-cost:   14
c ---[2076]---> BDD-cost:   14
c ---[2075]---> BDD-cost:    1
c ---[2074]---> BDD-cost:    1
c ---[2073]---> BDD-cost:   14
c ---[2072]---> BDD-cost:   14
c ---[2071]---> BDD-cost:    1
c ---[2070]---> BDD-cost:    1
c ---[2069]---> BDD-cost:    1
c ---[2068]---> BDD-cost:    1
c ---[2067]---> BDD-cost:   21
c ---[2066]---> BDD-cost:    1
c ---[2065]---> BDD-cost:   21
c ---[2064]---> BDD-cost:    1
c ---[2063]---> BDD-cost:   24
c ---[2062]---> BDD-cost:    1
c ---[2061]---> BDD-cost:    1
c ---[2060]---> BDD-cost:    1
c ---[2059]---> BDD-cost:    1
c ---[2058]---> BDD-cost:    1
c ---[2057]---> BDD-cost:    1
c ---[2056]---> BDD-cost:    1
c ---[2055]---> BDD-cost:    1
c ---[2054]---> BDD-cost:    1
c ---[2053]---> BDD-cost:    1
c ---[2052]---> BDD-cost:   24
c ---[2051]---> BDD-cost:    1
c ---[2050]---> BDD-cost:    1
c ---[2049]---> BDD-cost:   17
c ---[2048]---> BDD-cost:    1
c ---[2047]---> BDD-cost:   19
c ---[2046]---> BDD-cost:    1
c ---[2045]---> BDD-cost:   16
c ---[2044]---> BDD-cost:    1
c ---[2043]---> BDD-cost:    1
c ---[2042]---> BDD-cost:    1
c ---[2041]---> BDD-cost:   14
c ---[2040]---> BDD-cost:   14
c ---[2039]---> BDD-cost:    1
c ---[2038]---> BDD-cost:    1
c ---[2037]---> BDD-cost:   14
c ---[2036]---> BDD-cost:   14
c ---[2035]---> BDD-cost:    1
c ---[2034]---> BDD-cost:    1
c ---[2033]---> BDD-cost:   14
c ---[2032]---> BDD-cost:   14
c ---[2031]---> BDD-cost:    1
c ---[2030]---> BDD-cost:    1
c ---[2029]---> BDD-cost:   14
c ---[2028]---> BDD-cost:   14
c ---[2027]---> BDD-cost:    1
c ---[2026]---> BDD-cost:    1
c ---[2025]---> BDD-cost:   14
c ---[2024]---> BDD-cost:   14
c ---[2023]---> BDD-cost:    1
c ---[2022]---> BDD-cost:    1
c ---[2021]---> BDD-cost:    1
c ---[2020]---> BDD-cost:    1
c ---[2019]---> BDD-cost:   16
c ---[2018]---> BDD-cost:    1
c ---[2017]---> BDD-cost:   19
c ---[2016]---> BDD-cost:    1
c ---[2015]---> BDD-cost:   19
c ---[2014]---> BDD-cost:    1
c ---[2013]---> BDD-cost:   22
c ---[2012]---> BDD-cost:    1
c ---[2011]---> BDD-cost:    1
c ---[2010]---> BDD-cost:    1
c ---[2009]---> BDD-cost:    1
c ---[2008]---> BDD-cost:    1
c ---[2007]---> BDD-cost:    1
c ---[2006]---> BDD-cost:    1
c ---[2005]---> BDD-cost:    1
c ---[2004]---> BDD-cost:    1
c ---[2003]---> BDD-cost:    1
c ---[2002]---> BDD-cost:    1
c ---[2001]---> BDD-cost:    1
c ---[2000]---> BDD-cost:    1
c ---[1999]---> BDD-cost:    1
c ---[1998]---> BDD-cost:   24
c ---[1997]---> BDD-cost:    1
c ---[1996]---> BDD-cost:    1
c ---[1995]---> BDD-cost:   17
c ---[1994]---> BDD-cost:    1
c ---[1993]---> BDD-cost:   16
c ---[1992]---> BDD-cost:    1
c ---[1991]---> BDD-cost:   16
c ---[1990]---> BDD-cost:    1
c ---[1989]---> BDD-cost:    1
c ---[1988]---> BDD-cost:    1
c ---[1987]---> BDD-cost:   14
c ---[1986]---> BDD-cost:   14
c ---[1985]---> BDD-cost:    1
c ---[1984]---> BDD-cost:    1
c ---[1983]---> BDD-cost:   14
c ---[1982]---> BDD-cost:   14
c ---[1981]---> BDD-cost:    1
c ---[1980]---> BDD-cost:    1
c ---[1979]---> BDD-cost:   14
c ---[1978]---> BDD-cost:   14
c ---[1977]---> BDD-cost:    1
c ---[1976]---> BDD-cost:    1
c ---[1975]---> BDD-cost:   14
c ---[1974]---> BDD-cost:   14
c ---[1973]---> BDD-cost:    1
c ---[1972]---> BDD-cost:    1
c ---[1971]---> BDD-cost:   14
c ---[1970]---> BDD-cost:   14
c ---[1969]---> BDD-cost:    1
c ---[1968]---> BDD-cost:    1
c ---[1967]---> BDD-cost:   14
c ---[1966]---> BDD-cost:   14
c ---[1965]---> BDD-cost:    1
c ---[1964]---> BDD-cost:    1
c ---[1963]---> BDD-cost:    1
c ---[1962]---> BDD-cost:    1
c ---[1961]---> BDD-cost:   16
c ---[1960]---> BDD-cost:    1
c ---[1959]---> BDD-cost:   16
c ---[1958]---> BDD-cost:    1
c ---[1957]---> BDD-cost:   19
c ---[1956]---> BDD-cost:    1
c ---[1955]---> BDD-cost:   19
c ---[1954]---> BDD-cost:    1
c ---[1953]---> BDD-cost:   22
c ---[1952]---> BDD-cost:    1
c ---[1951]---> BDD-cost:    1
c ---[1950]---> BDD-cost:    1
c ---[1949]---> BDD-cost:    1
c ---[1948]---> BDD-cost:    1
c ---[1947]---> BDD-cost:    1
c ---[1946]---> BDD-cost:    1
c ---[1945]---> BDD-cost:    1
c ---[1944]---> BDD-cost:    1
c ---[1943]---> BDD-cost:    1
c ---[1942]---> BDD-cost:    1
c ---[1941]---> BDD-cost:    1
c ---[1940]---> BDD-cost:    1
c ---[1939]---> BDD-cost:    1
c ---[1938]---> BDD-cost:    1
c ---[1937]---> BDD-cost:    1
c ---[1936]---> BDD-cost:    1
c ---[1935]---> BDD-cost:    1
c ---[1934]---> BDD-cost:   22
c ---[1933]---> BDD-cost:    1
c ---[1932]---> BDD-cost:    1
c ---[1931]---> BDD-cost:   17
c ---[1930]---> BDD-cost:    1
c ---[1929]---> BDD-cost:   16
c ---[1928]---> BDD-cost:    1
c ---[1927]---> BDD-cost:   16
c ---[1926]---> BDD-cost:    1
c ---[1925]---> BDD-cost:    1
c ---[1924]---> BDD-cost:    1
c ---[1923]---> BDD-cost:   14
c ---[1922]---> BDD-cost:   14
c ---[1921]---> BDD-cost:    1
c ---[1920]---> BDD-cost:    1
c ---[1919]---> BDD-cost:   14
c ---[1918]---> BDD-cost:   14
c ---[1917]---> BDD-cost:    1
c ---[1916]---> BDD-cost:    1
c ---[1915]---> BDD-cost:   14
c ---[1914]---> BDD-cost:   14
c ---[1913]---> BDD-cost:    1
c ---[1912]---> BDD-cost:    1
c ---[1911]---> BDD-cost:   14
c ---[1910]---> BDD-cost:   14
c ---[1909]---> BDD-cost:    1
c ---[1908]---> BDD-cost:    1
c ---[1907]---> BDD-cost:   14
c ---[1906]---> BDD-cost:   14
c ---[1905]---> BDD-cost:    1
c ---[1904]---> BDD-cost:    1
c ---[1903]---> BDD-cost:   14
c ---[1902]---> BDD-cost:   14
c ---[1901]---> BDD-cost:    1
c ---[1900]---> BDD-cost:    1
c ---[1899]---> BDD-cost:   14
c ---[1898]---> BDD-cost:   14
c ---[1897]---> BDD-cost:    1
c ---[1896]---> BDD-cost:    1
c ---[1895]---> BDD-cost:    1
c ---[1894]---> BDD-cost:    1
c ---[1893]---> BDD-cost:   16
c ---[1892]---> BDD-cost:    1
c ---[1891]---> BDD-cost:   16
c ---[1890]---> BDD-cost:    1
c ---[1889]---> BDD-cost:   16
c ---[1888]---> BDD-cost:    1
c ---[1887]---> BDD-cost:   21
c ---[1886]---> BDD-cost:    1
c ---[1885]---> BDD-cost:   21
c ---[1884]---> BDD-cost:    1
c ---[1883]---> BDD-cost:   24
c ---[1882]---> BDD-cost:    1
c ---[1881]---> BDD-cost:    1
c ---[1880]---> BDD-cost:    1
c ---[1879]---> BDD-cost:    1
c ---[1878]---> BDD-cost:    1
c ---[1877]---> BDD-cost:    1
c ---[1876]---> BDD-cost:    1
c ---[1875]---> BDD-cost:    1
c ---[1874]---> BDD-cost:    1
c ---[1873]---> BDD-cost:    1
c ---[1872]---> BDD-cost:    1
c ---[1871]---> BDD-cost:    1
c ---[1870]---> BDD-cost:    1
c ---[1869]---> BDD-cost:    1
c ---[1868]---> BDD-cost:    1
c ---[1867]---> BDD-cost:    1
c ---[1866]---> BDD-cost:    1
c ---[1865]---> BDD-cost:    1
c ---[1864]---> BDD-cost:    1
c ---[1863]---> BDD-cost:    1
c ---[1862]---> BDD-cost:    1
c ---[1861]---> BDD-cost:    1
c ---[1860]---> BDD-cost:   22
c ---[1859]---> BDD-cost:    1
c ---[1858]---> BDD-cost:    1
c ---[1857]---> BDD-cost:   17
c ---[1856]---> BDD-cost:    1
c ---[1855]---> BDD-cost:   16
c ---[1854]---> BDD-cost:    1
c ---[1853]---> BDD-cost:   16
c ---[1852]---> BDD-cost:    1
c ---[1851]---> BDD-cost:    1
c ---[1850]---> BDD-cost:    1
c ---[1849]---> BDD-cost:   14
c ---[1848]---> BDD-cost:   14
c ---[1847]---> BDD-cost:    1
c ---[1846]---> BDD-cost:    1
c ---[1845]---> BDD-cost:   14
c ---[1844]---> BDD-cost:   14
c ---[1843]---> BDD-cost:    1
c ---[1842]---> BDD-cost:    1
c ---[1841]---> BDD-cost:   14
c ---[1840]---> BDD-cost:   14
c ---[1839]---> BDD-cost:    1
c ---[1838]---> BDD-cost:    1
c ---[1837]---> BDD-cost:   14
c ---[1836]---> BDD-cost:   14
c ---[1835]---> BDD-cost:    1
c ---[1834]---> BDD-cost:    1
c ---[1833]---> BDD-cost:   14
c ---[1832]---> BDD-cost:   14
c ---[1831]---> BDD-cost:    1
c ---[1830]---> BDD-cost:    1
c ---[1829]---> BDD-cost:   14
c ---[1828]---> BDD-cost:   14
c ---[1827]---> BDD-cost:    1
c ---[1826]---> BDD-cost:    1
c ---[1825]---> BDD-cost:   14
c ---[1824]---> BDD-cost:   14
c ---[1823]---> BDD-cost:    1
c ---[1822]---> BDD-cost:    1
c ---[1821]---> BDD-cost:   14
c ---[1820]---> BDD-cost:   14
c ---[1819]---> BDD-cost:    1
c ---[1818]---> BDD-cost:    1
c ---[1817]---> BDD-cost:    1
c ---[1816]---> BDD-cost:    1
c ---[1815]---> BDD-cost:   16
c ---[1814]---> BDD-cost:    1
c ---[1813]---> BDD-cost:   16
c ---[1812]---> BDD-cost:    1
c ---[1811]---> BDD-cost:   16
c ---[1810]---> BDD-cost:    1
c ---[1809]---> BDD-cost:   16
c ---[1808]---> BDD-cost:    1
c ---[1807]---> BDD-cost:   21
c ---[1806]---> BDD-cost:    1
c ---[1805]---> BDD-cost:   21
c ---[1804]---> BDD-cost:    1
c ---[1803]---> BDD-cost:   24
c ---[1802]---> BDD-cost:    1
c ---[1801]---> BDD-cost:    1
c ---[1800]---> BDD-cost:    1
c ---[1799]---> BDD-cost:    1
c ---[1798]---> BDD-cost:    1
c ---[1797]---> BDD-cost:    1
c ---[1796]---> BDD-cost:    1
c ---[1795]---> BDD-cost:    1
c ---[1794]---> BDD-cost:    1
c ---[1793]---> BDD-cost:    1
c ---[1792]---> BDD-cost:    1
c ---[1791]---> BDD-cost:    1
c ---[1790]---> BDD-cost:    1
c ---[1789]---> BDD-cost:    1
c ---[1788]---> BDD-cost:    1
c ---[1787]---> BDD-cost:    1
c ---[1786]---> BDD-cost:    1
c ---[1785]---> BDD-cost:    1
c ---[1784]---> BDD-cost:    1
c ---[1783]---> BDD-cost:    1
c ---[1782]---> BDD-cost:    1
c ---[1781]---> BDD-cost:    1
c ---[1780]---> BDD-cost:    1
c ---[1779]---> BDD-cost:    1
c ---[1778]---> BDD-cost:    1
c ---[1777]---> BDD-cost:    1
c ---[1776]---> BDD-cost:   24
c ---[1775]---> BDD-cost:    1
c ---[1774]---> BDD-cost:    1
c ---[1773]---> BDD-cost:   17
c ---[1772]---> BDD-cost:    1
c ---[1771]---> BDD-cost:   14
c ---[1770]---> BDD-cost:    1
c ---[1769]---> BDD-cost:   11
c ---[1768]---> BDD-cost:    1
c ---[1767]---> BDD-cost:    1
c ---[1766]---> BDD-cost:    1
c ---[1765]---> BDD-cost:   14
c ---[1764]---> BDD-cost:   14
c ---[1763]---> BDD-cost:    1
c ---[1762]---> BDD-cost:    1
c ---[1761]---> BDD-cost:   14
c ---[1760]---> BDD-cost:   14
c ---[1759]---> BDD-cost:    1
c ---[1758]---> BDD-cost:    1
c ---[1757]---> BDD-cost:   14
c ---[1756]---> BDD-cost:   14
c ---[1755]---> BDD-cost:    1
c ---[1754]---> BDD-cost:    1
c ---[1753]---> BDD-cost:   14
c ---[1752]---> BDD-cost:   14
c ---[1751]---> BDD-cost:    1
c ---[1750]---> BDD-cost:    1
c ---[1749]---> BDD-cost:   14
c ---[1748]---> BDD-cost:   14
c ---[1747]---> BDD-cost:    1
c ---[1746]---> BDD-cost:    1
c ---[1745]---> BDD-cost:   14
c ---[1744]---> BDD-cost:   14
c ---[1743]---> BDD-cost:    1
c ---[1742]---> BDD-cost:    1
c ---[1741]---> BDD-cost:   14
c ---[1740]---> BDD-cost:   14
c ---[1739]---> BDD-cost:    1
c ---[1738]---> BDD-cost:    1
c ---[1737]---> BDD-cost:   14
c ---[1736]---> BDD-cost:   14
c ---[1735]---> BDD-cost:    1
c ---[1734]---> BDD-cost:    1
c ---[1733]---> BDD-cost:   14
c ---[1732]---> BDD-cost:   14
c ---[1731]---> BDD-cost:    1
c ---[1730]---> BDD-cost:    1
c ---[1729]---> BDD-cost:    1
c ---[1728]---> BDD-cost:    1
c ---[1727]---> BDD-cost:   11
c ---[1726]---> BDD-cost:    1
c ---[1725]---> BDD-cost:   14
c ---[1724]---> BDD-cost:    1
c ---[1723]---> BDD-cost:   14
c ---[1722]---> BDD-cost:    1
c ---[1721]---> BDD-cost:   14
c ---[1720]---> BDD-cost:    1
c ---[1719]---> BDD-cost:   14
c ---[1718]---> BDD-cost:    1
c ---[1717]---> BDD-cost:   17
c ---[1716]---> BDD-cost:    1
c ---[1715]---> BDD-cost:   17
c ---[1714]---> BDD-cost:    1
c ---[1713]---> BDD-cost:   20
c ---[1712]---> BDD-cost:    1
c ---[1711]---> BDD-cost:    1
c ---[1710]---> BDD-cost:    1
c ---[1709]---> BDD-cost:    1
c ---[1708]---> BDD-cost:    1
c ---[1707]---> BDD-cost:    1
c ---[1706]---> BDD-cost:    1
c ---[1705]---> BDD-cost:    1
c ---[1704]---> BDD-cost:    1
c ---[1703]---> BDD-cost:    1
c ---[1702]---> BDD-cost:    1
c ---[1701]---> BDD-cost:    1
c ---[1700]---> BDD-cost:    1
c ---[1699]---> BDD-cost:    1
c ---[1698]---> BDD-cost:    1
c ---[1697]---> BDD-cost:    1
c ---[1696]---> BDD-cost:    1
c ---[1695]---> BDD-cost:    1
c ---[1694]---> BDD-cost:    1
c ---[1693]---> BDD-cost:    1
c ---[1692]---> BDD-cost:    1
c ---[1691]---> BDD-cost:    1
c ---[1690]---> BDD-cost:    1
c ---[1689]---> BDD-cost:    1
c ---[1688]---> BDD-cost:    1
c ---[1687]---> BDD-cost:    1
c ---[1686]---> BDD-cost:    1
c ---[1685]---> BDD-cost:    1
c ---[1684]---> BDD-cost:    1
c ---[1683]---> BDD-cost:    1
c ---[1682]---> BDD-cost:   24
c ---[1681]---> BDD-cost:    1
c ---[1680]---> BDD-cost:    1
c ---[1679]---> BDD-cost:   17
c ---[1678]---> BDD-cost:    1
c ---[1677]---> BDD-cost:    8
c ---[1676]---> BDD-cost:    1
c ---[1675]---> BDD-cost:    1
c ---[1674]---> BDD-cost:    1
c ---[1673]---> BDD-cost:    1
c ---[1672]---> BDD-cost:    1
c ---[1671]---> BDD-cost:    1
c ---[1670]---> BDD-cost:   11
c ---[1669]---> BDD-cost:    1
c ---[1668]---> BDD-cost:    1
c ---[1667]---> BDD-cost:   17
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:    1
c ---[1660]---> BDD-cost:    1
c ---[1659]---> BDD-cost:   17
c ---[1658]---> BDD-cost:    1
c ---[1657]---> BDD-cost:    1
c ---[1656]---> BDD-cost:   17
c ---[1655]---> BDD-cost:    1
c ---[1654]---> BDD-cost:    1
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:    1
c ---[1645]---> BDD-cost:    1
c ---[1644]---> BDD-cost:   17
c ---[1643]---> BDD-cost:    1
c ---[1642]---> BDD-cost:    1
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:   17
c ---[1630]---> BDD-cost:    1
c ---[1629]---> BDD-cost:    1
c ---[1628]---> BDD-cost:   17
c ---[1627]---> BDD-cost:    1
c ---[1626]---> BDD-cost:    1
c ---[1625]---> BDD-cost:    1
c ---[1624]---> BDD-cost:    1
c ---[1623]---> BDD-cost:   17
c ---[1622]---> BDD-cost:   17
c ---[1621]---> BDD-cost:    1
c ---[1620]---> BDD-cost:    1
c ---[1619]---> BDD-cost:   17
c ---[1618]---> BDD-cost:   17
c ---[1617]---> BDD-cost:    1
c ---[1616]---> BDD-cost:    1
c ---[1615]---> BDD-cost:   17
c ---[1614]---> BDD-cost:   17
c ---[1613]---> BDD-cost:    1
c ---[1612]---> BDD-cost:    1
c ---[1611]---> BDD-cost:   17
c ---[1610]---> BDD-cost:    1
c ---[1609]---> BDD-cost:    1
c ---[1608]---> BDD-cost:   17
c ---[1607]---> BDD-cost:    1
c ---[1606]---> BDD-cost:    1
c ---[1605]---> BDD-cost:   21
c ---[1604]---> BDD-cost:    1
c ---[1603]---> BDD-cost:   17
c ---[1602]---> BDD-cost:   17
c ---[1601]---> BDD-cost:    1
c ---[1600]---> BDD-cost:    1
c ---[1599]---> BDD-cost:   17
c ---[1598]---> BDD-cost:   17
c ---[1597]---> BDD-cost:    1
c ---[1596]---> BDD-cost:    1
c ---[1595]---> BDD-cost:   17
c ---[1594]---> BDD-cost:   17
c ---[1593]---> BDD-cost:    1
c ---[1592]---> BDD-cost:    1
c ---[1591]---> BDD-cost:   17
c ---[1590]---> BDD-cost:   17
c ---[1589]---> BDD-cost:    1
c ---[1588]---> BDD-cost:    1
c ---[1587]---> BDD-cost:   17
c ---[1586]---> BDD-cost:    1
c ---[1585]---> BDD-cost:    1
c ---[1584]---> BDD-cost:   17
c ---[1583]---> BDD-cost:    1
c ---[1582]---> BDD-cost:    1
c ---[1581]---> BDD-cost:   21
c ---[1580]---> BDD-cost:    1
c ---[1579]---> BDD-cost:   17
c ---[1578]---> BDD-cost:   17
c ---[1577]---> BDD-cost:    1
c ---[1576]---> BDD-cost:    1
c ---[1575]---> BDD-cost:   17
c ---[1574]---> BDD-cost:   17
c ---[1573]---> BDD-cost:    1
c ---[1572]---> BDD-cost:    1
c ---[1571]---> BDD-cost:   17
c ---[1570]---> BDD-cost:   17
c ---[1569]---> BDD-cost:    1
c ---[1568]---> BDD-cost:    1
c ---[1567]---> BDD-cost:   17
c ---[1566]---> BDD-cost:   17
c ---[1565]---> BDD-cost:    1
c ---[1564]---> BDD-cost:    1
c ---[1563]---> BDD-cost:   17
c ---[1562]---> BDD-cost:   17
c ---[1561]---> BDD-cost:    1
c ---[1560]---> BDD-cost:    1
c ---[1559]---> BDD-cost:   17
c ---[1558]---> BDD-cost:    1
c ---[1557]---> BDD-cost:    1
c ---[1556]---> BDD-cost:   17
c ---[1555]---> BDD-cost:    1
c ---[1554]---> BDD-cost:    1
c ---[1553]---> BDD-cost:   21
c ---[1552]---> BDD-cost:    1
c ---[1551]---> BDD-cost:   17
c ---[1550]---> BDD-cost:   17
c ---[1549]---> BDD-cost:    1
c ---[1548]---> BDD-cost:    1
c ---[1547]---> BDD-cost:   17
c ---[1546]---> BDD-cost:   17
c ---[1545]---> BDD-cost:    1
c ---[1544]---> BDD-cost:    1
c ---[1543]---> BDD-cost:   17
c ---[1542]---> BDD-cost:   17
c ---[1541]---> BDD-cost:    1
c ---[1540]---> BDD-cost:    1
c ---[1539]---> BDD-cost:   17
c ---[1538]---> BDD-cost:   17
c ---[1537]---> BDD-cost:    1
c ---[1536]---> BDD-cost:    1
c ---[1535]---> BDD-cost:   17
c ---[1534]---> BDD-cost:   17
c ---[1533]---> BDD-cost:    1
c ---[1532]---> BDD-cost:    1
c ---[1531]---> BDD-cost:   17
c ---[1530]---> BDD-cost:   17
c ---[1529]---> BDD-cost:    1
c ---[1528]---> BDD-cost:    1
c ---[1527]---> BDD-cost:   17
c ---[1526]---> BDD-cost:    1
c ---[1525]---> BDD-cost:    1
c ---[1524]---> BDD-cost:   17
c ---[1523]---> BDD-cost:    1
c ---[1522]---> BDD-cost:    1
c ---[1521]---> BDD-cost:   21
c ---[1520]---> BDD-cost:    1
c ---[1519]---> BDD-cost:   17
c ---[1518]---> BDD-cost:   17
c ---[1517]---> BDD-cost:    1
c ---[1516]---> BDD-cost:    1
c ---[1515]---> BDD-cost:   17
c ---[1514]---> BDD-cost:   17
c ---[1513]---> BDD-cost:    1
c ---[1512]---> BDD-cost:    1
c ---[1511]---> BDD-cost:   17
c ---[1510]---> BDD-cost:   17
c ---[1509]---> BDD-cost:    1
c ---[1508]---> BDD-cost:    1
c ---[1507]---> BDD-cost:   17
c ---[1506]---> BDD-cost:   17
c ---[1505]---> BDD-cost:    1
c ---[1504]---> BDD-cost:    1
c ---[1503]---> BDD-cost:   17
c ---[1502]---> BDD-cost:   17
c ---[1501]---> BDD-cost:    1
c ---[1500]---> BDD-cost:    1
c ---[1499]---> BDD-cost:   17
c ---[1498]---> BDD-cost:   17
c ---[1497]---> BDD-cost:    1
c ---[1496]---> BDD-cost:    1
c ---[1495]---> BDD-cost:   17
c ---[1494]---> BDD-cost:   17
c ---[1493]---> BDD-cost:    1
c ---[1492]---> BDD-cost:    1
c ---[1491]---> BDD-cost:   17
c ---[1490]---> BDD-cost:    1
c ---[1489]---> BDD-cost:    1
c ---[1488]---> BDD-cost:   17
c ---[1487]---> BDD-cost:    1
c ---[1486]---> BDD-cost:    1
c ---[1485]---> BDD-cost:   16
c ---[1484]---> BDD-cost:    1
c ---[1483]---> BDD-cost:   17
c ---[1482]---> BDD-cost:   17
c ---[1481]---> BDD-cost:    1
c ---[1480]---> BDD-cost:    1
c ---[1479]---> BDD-cost:   17
c ---[1478]---> BDD-cost:   17
c ---[1477]---> BDD-cost:    1
c ---[1476]---> BDD-cost:    1
c ---[1475]---> BDD-cost:   17
c ---[1474]---> BDD-cost:   17
c ---[1473]---> BDD-cost:    1
c ---[1472]---> BDD-cost:    1
c ---[1471]---> BDD-cost:   17
c ---[1470]---> BDD-cost:   17
c ---[1469]---> BDD-cost:    1
c ---[1468]---> BDD-cost:    1
c ---[1467]---> BDD-cost:   17
c ---[1466]---> BDD-cost:   17
c ---[1465]---> BDD-cost:    1
c ---[1464]---> BDD-cost:    1
c ---[1463]---> BDD-cost:   17
c ---[1462]---> BDD-cost:   17
c ---[1461]---> BDD-cost:    1
c ---[1460]---> BDD-cost:    1
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:    1
c ---[1449]---> BDD-cost:    1
c ---[1448]---> BDD-cost:   17
c ---[1447]---> BDD-cost:    1
c ---[1446]---> BDD-cost:    1
c ---[1445]---> BDD-cost:   16
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:   17
c ---[1409]---> BDD-cost:    1
c ---[1408]---> BDD-cost:    1
c ---[1407]---> BDD-cost:   17
c ---[1406]---> BDD-cost:    1
c ---[1405]---> BDD-cost:    1
c ---[1404]---> BDD-cost:   17
c ---[1403]---> BDD-cost:    1
c ---[1402]---> BDD-cost:    1
c ---[1401]---> BDD-cost:   16
c ---[1400]---> BDD-cost:    1
c ---[1399]---> BDD-cost:   17
c ---[1398]---> BDD-cost:   17
c ---[1397]---> BDD-cost:    1
c ---[1396]---> BDD-cost:    1
c ---[1395]---> BDD-cost:   17
c ---[1394]---> BDD-cost:   17
c ---[1393]---> BDD-cost:    1
c ---[1392]---> BDD-cost:    1
c ---[1391]---> BDD-cost:   17
c ---[1390]---> BDD-cost:   17
c ---[1389]---> BDD-cost:    1
c ---[1388]---> BDD-cost:    1
c ---[1387]---> BDD-cost:   17
c ---[1386]---> BDD-cost:   17
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:    1
c ---[1357]---> BDD-cost:    1
c ---[1356]---> BDD-cost:   17
c ---[1355]---> BDD-cost:    1
c ---[1354]---> BDD-cost:    1
c ---[1353]---> BDD-cost:   16
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:    1
c ---[1305]---> BDD-cost:    1
c ---[1304]---> BDD-cost:   17
c ---[1303]---> BDD-cost:    1
c ---[1302]---> BDD-cost:    1
c ---[1301]---> BDD-cost:   21
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:    1
c ---[1249]---> BDD-cost:    1
c ---[1248]---> BDD-cost:   17
c ---[1247]---> BDD-cost:    1
c ---[1246]---> BDD-cost:    1
c ---[1245]---> BDD-cost:   21
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:    1
c ---[1189]---> BDD-cost:    1
c ---[1188]---> BDD-cost:   17
c ---[1187]---> BDD-cost:    1
c ---[1186]---> BDD-cost:    1
c ---[1185]---> BDD-cost:   21
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:    1
c ---[1125]---> BDD-cost:    1
c ---[1124]---> BDD-cost:   17
c ---[1123]---> BDD-cost:    1
c ---[1122]---> BDD-cost:    1
c ---[1121]---> BDD-cost:   21
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:   14
c ---[1058]---> BDD-cost:   14
c ---[1057]---> BDD-cost:    1
c ---[1056]---> BDD-cost:    1
c ---[1055]---> BDD-cost:   14
c ---[1054]---> BDD-cost:   14
c ---[1053]---> BDD-cost:    1
c ---[1052]---> BDD-cost:    1
c ---[1051]---> BDD-cost:   14
c ---[1050]---> BDD-cost:   14
c ---[1049]---> BDD-cost:    1
c ---[1048]---> BDD-cost:    1
c ---[1047]---> BDD-cost:   14
c ---[1046]---> BDD-cost:   14
c ---[1045]---> BDD-cost:    1
c ---[1044]---> BDD-cost:    1
c ---[1043]---> BDD-cost:   14
c ---[1042]---> BDD-cost:   14
c ---[1041]---> BDD-cost:    1
c ---[1040]---> BDD-cost:    1
c ---[1039]---> BDD-cost:   14
c ---[1038]---> BDD-cost:   14
c ---[1037]---> BDD-cost:    1
c ---[1036]---> BDD-cost:    1
c ---[1035]---> BDD-cost:   14
c ---[1034]---> BDD-cost:   14
c ---[1033]---> BDD-cost:    1
c ---[1032]---> BDD-cost:    1
c ---[1031]---> BDD-cost:   14
c ---[1030]---> BDD-cost:   14
c ---[1029]---> BDD-cost:    1
c ---[1028]---> BDD-cost:    1
c ---[1027]---> BDD-cost:   14
c ---[1026]---> BDD-cost:   14
c ---[1025]---> BDD-cost:    1
c ---[1024]---> BDD-cost:    1
c ---[1023]---> BDD-cost:   14
c ---[1022]---> BDD-cost:   14
c ---[1021]---> BDD-cost:    1
c ---[1020]---> BDD-cost:    1
c ---[1019]---> BDD-cost:   17
c ---[1018]---> BDD-cost:    1
c ---[1017]---> BDD-cost:    1
c ---[1016]---> BDD-cost:   17
c ---[1015]---> BDD-cost:    1
c ---[1014]---> BDD-cost:    1
c ---[1013]---> BDD-cost:   17
c ---[1012]---> BDD-cost:    1
c ---[1011]---> BDD-cost:    1
c ---[1010]---> BDD-cost:   21
c ---[1009]---> BDD-cost:    1
c ---[1008]---> BDD-cost:    1
c ---[1007]---> BDD-cost:    1
c ---[1006]---> BDD-cost:   21
c ---[1005]---> BDD-cost:    1
c ---[1004]---> BDD-cost:    1
c ---[1003]---> BDD-cost:    1
c ---[1002]---> BDD-cost:   16
c ---[1001]---> BDD-cost:    1
c ---[1000]---> BDD-cost:    1
c ---[ 999]---> BDD-cost:    1
c ---[ 998]---> BDD-cost:   16
c ---[ 997]---> BDD-cost:    1
c ---[ 996]---> BDD-cost:    1
c ---[ 995]---> BDD-cost:    1
c ---[ 994]---> BDD-cost:   16
c ---[ 993]---> BDD-cost:    1
c ---[ 992]---> BDD-cost:    1
c ---[ 991]---> BDD-cost:    1
c ---[ 990]---> BDD-cost:   16
c ---[ 989]---> BDD-cost:    1
c ---[ 988]---> BDD-cost:    1
c ---[ 987]---> BDD-cost:    1
c ---[ 986]---> BDD-cost:   11
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:   17
c ---[ 966]---> BDD-cost:   17
c ---[ 965]---> BDD-cost:    1
c ---[ 964]---> BDD-cost:    1
c ---[ 963]---> BDD-cost:   17
c ---[ 962]---> BDD-cost:   17
c ---[ 961]---> BDD-cost:    1
c ---[ 960]---> BDD-cost:    1
c ---[ 959]---> BDD-cost:   17
c ---[ 958]---> BDD-cost:   17
c ---[ 957]---> BDD-cost:    1
c ---[ 956]---> BDD-cost:    1
c ---[ 955]---> BDD-cost:   17
c ---[ 954]---> BDD-cost:   17
c ---[ 953]---> BDD-cost:    1
c ---[ 952]---> BDD-cost:    1
c ---[ 951]---> BDD-cost:   17
c ---[ 950]---> BDD-cost:   17
c ---[ 949]---> BDD-cost:    1
c ---[ 948]---> BDD-cost:    1
c ---[ 947]---> BDD-cost:   17
c ---[ 946]---> BDD-cost:   17
c ---[ 945]---> BDD-cost:    1
c ---[ 944]---> BDD-cost:    1
c ---[ 943]---> BDD-cost:   17
c ---[ 942]---> BDD-cost:   17
c ---[ 941]---> BDD-cost:    1
c ---[ 940]---> BDD-cost:    1
c ---[ 939]---> BDD-cost:   17
c ---[ 938]---> BDD-cost:   17
c ---[ 937]---> BDD-cost:    1
c ---[ 936]---> BDD-cost:    1
c ---[ 935]---> BDD-cost:   17
c ---[ 934]---> BDD-cost:   17
c ---[ 933]---> BDD-cost:    1
c ---[ 932]---> BDD-cost:    1
c ---[ 931]---> BDD-cost:   17
c ---[ 930]---> BDD-cost:   17
c ---[ 929]---> BDD-cost:    1
c ---[ 928]---> BDD-cost:    1
c ---[ 927]---> BDD-cost:   17
c ---[ 926]---> BDD-cost:   17
c ---[ 925]---> BDD-cost:    1
c ---[ 924]---> BDD-cost:    1
c ---[ 923]---> BDD-cost:   17
c ---[ 922]---> BDD-cost:   17
c ---[ 921]---> BDD-cost:    1
c ---[ 920]---> BDD-cost:    1
c ---[ 919]---> BDD-cost:   21
c ---[ 918]---> BDD-cost:    1
c ---[ 917]---> BDD-cost:    1
c ---[ 916]---> BDD-cost:    1
c ---[ 915]---> BDD-cost:   21
c ---[ 914]---> BDD-cost:    1
c ---[ 913]---> BDD-cost:    1
c ---[ 912]---> BDD-cost:    1
c ---[ 911]---> BDD-cost:   21
c ---[ 910]---> BDD-cost:    1
c ---[ 909]---> BDD-cost:    1
c ---[ 908]---> BDD-cost:    1
c ---[ 907]---> BDD-cost:   21
c ---[ 906]---> BDD-cost:    1
c ---[ 905]---> BDD-cost:    1
c ---[ 904]---> BDD-cost:    1
c ---[ 903]---> BDD-cost:    1
c ---[ 902]---> BDD-cost:    1
c ---[ 901]---> BDD-cost:    1
c ---[ 900]---> BDD-cost:    1
c ---[ 899]---> BDD-cost:    1
c ---[ 898]---> BDD-cost:    1
c ---[ 897]---> BDD-cost:    1
c ---[ 896]---> BDD-cost:    1
c ---[ 895]---> BDD-cost:   21
c ---[ 894]---> BDD-cost:    1
c ---[ 893]---> BDD-cost:    1
c ---[ 892]---> BDD-cost:    1
c ---[ 891]---> BDD-cost:   21
c ---[ 890]---> BDD-cost:    1
c ---[ 889]---> BDD-cost:    1
c ---[ 888]---> BDD-cost:    1
c ---[ 887]---> BDD-cost:   21
c ---[ 886]---> BDD-cost:    1
c ---[ 885]---> BDD-cost:    1
c ---[ 884]---> BDD-cost:    1
c ---[ 883]---> BDD-cost:   21
c ---[ 882]---> BDD-cost:    1
c ---[ 881]---> BDD-cost:    1
c ---[ 880]---> BDD-cost:    1
c ---[ 879]---> BDD-cost:   21
c ---[ 878]---> BDD-cost:    1
c ---[ 877]---> BDD-cost:    1
c ---[ 876]---> BDD-cost:    1
c ---[ 875]---> BDD-cost:   21
c ---[ 874]---> BDD-cost:    1
c ---[ 873]---> BDD-cost:    1
c ---[ 872]---> BDD-cost:    1
c ---[ 871]---> BDD-cost:   16
c ---[ 870]---> BDD-cost:    1
c ---[ 869]---> BDD-cost:    1
c ---[ 868]---> BDD-cost:    1
c ---[ 867]---> BDD-cost:   16
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:   17
c ---[ 854]---> BDD-cost:   17
c ---[ 853]---> BDD-cost:    1
c ---[ 852]---> BDD-cost:    1
c ---[ 851]---> BDD-cost:   17
c ---[ 850]---> BDD-cost:   17
c ---[ 849]---> BDD-cost:    1
c ---[ 848]---> BDD-cost:    1
c ---[ 847]---> BDD-cost:   17
c ---[ 846]---> BDD-cost:   17
c ---[ 845]---> BDD-cost:    1
c ---[ 844]---> BDD-cost:    1
c ---[ 843]---> BDD-cost:   17
c ---[ 842]---> BDD-cost:   17
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:   17
c ---[ 830]---> BDD-cost:   17
c ---[ 829]---> BDD-cost:    1
c ---[ 828]---> BDD-cost:    1
c ---[ 827]---> BDD-cost:   17
c ---[ 826]---> BDD-cost:   17
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:   17
c ---[ 818]---> BDD-cost:   17
c ---[ 817]---> BDD-cost:    1
c ---[ 816]---> BDD-cost:    1
c ---[ 815]---> BDD-cost:   21
c ---[ 814]---> BDD-cost:    1
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:   21
c ---[ 798]---> BDD-cost:    1
c ---[ 797]---> BDD-cost:    1
c ---[ 796]---> BDD-cost:    1
c ---[ 795]---> BDD-cost:   21
c ---[ 794]---> BDD-cost:    1
c ---[ 793]---> BDD-cost:    1
c ---[ 792]---> BDD-cost:    1
c ---[ 791]---> BDD-cost:   21
c ---[ 790]---> BDD-cost:    1
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:    1
c ---[ 782]---> BDD-cost:    1
c ---[ 781]---> BDD-cost:    1
c ---[ 780]---> BDD-cost:    1
c ---[ 779]---> BDD-cost:    1
c ---[ 778]---> BDD-cost:    1
c ---[ 777]---> BDD-cost:    1
c ---[ 776]---> BDD-cost:    1
c ---[ 775]---> BDD-cost:   21
c ---[ 774]---> BDD-cost:    1
c ---[ 773]---> BDD-cost:    1
c ---[ 772]---> BDD-cost:    1
c ---[ 771]---> BDD-cost:   21
c ---[ 770]---> BDD-cost:    1
c ---[ 769]---> BDD-cost:    1
c ---[ 768]---> BDD-cost:    1
c ---[ 767]---> BDD-cost:   21
c ---[ 766]---> BDD-cost:    1
c ---[ 765]---> BDD-cost:    1
c ---[ 764]---> BDD-cost:    1
c ---[ 763]---> BDD-cost:   21
c ---[ 762]---> BDD-cost:    1
c ---[ 761]---> BDD-cost:    1
c ---[ 760]---> BDD-cost:    1
c ---[ 759]---> BDD-cost:   21
c ---[ 758]---> BDD-cost:    1
c ---[ 757]---> BDD-cost:    1
c ---[ 756]---> BDD-cost:    1
c ---[ 755]---> BDD-cost:   21
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:   17
c ---[ 742]---> BDD-cost:   17
c ---[ 741]---> BDD-cost:    1
c ---[ 740]---> BDD-cost:    1
c ---[ 739]---> BDD-cost:   17
c ---[ 738]---> BDD-cost:   17
c ---[ 737]---> BDD-cost:    1
c ---[ 736]---> BDD-cost:    1
c ---[ 735]---> BDD-cost:   21
c ---[ 734]---> BDD-cost:    1
c ---[ 733]---> BDD-cost:    1
c ---[ 732]---> BDD-cost:    1
c ---[ 731]---> BDD-cost:   21
c ---[ 730]---> BDD-cost:    1
c ---[ 729]---> BDD-cost:    1
c ---[ 728]---> BDD-cost:    1
c ---[ 727]---> BDD-cost:   21
c ---[ 726]---> BDD-cost:    1
c ---[ 725]---> BDD-cost:    1
c ---[ 724]---> BDD-cost:    1
c ---[ 723]---> BDD-cost:   21
c ---[ 722]---> BDD-cost:    1
c ---[ 721]---> BDD-cost:    1
c ---[ 720]---> BDD-cost:    1
c ---[ 719]---> BDD-cost:   17
c ---[ 718]---> BDD-cost:   17
c ---[ 717]---> BDD-cost:    1
c ---[ 716]---> BDD-cost:    1
c ---[ 715]---> BDD-cost:   17
c ---[ 714]---> BDD-cost:   17
c ---[ 713]---> BDD-cost:    1
c ---[ 712]---> BDD-cost:    1
c ---[ 711]---> BDD-cost:   21
c ---[ 710]---> BDD-cost:    1
c ---[ 709]---> BDD-cost:    1
c ---[ 708]---> BDD-cost:    1
c ---[ 707]---> BDD-cost:   21
c ---[ 706]---> BDD-cost:    1
c ---[ 705]---> BDD-cost:    1
c ---[ 704]---> BDD-cost:    1
c ---[ 703]---> BDD-cost:   21
c ---[ 702]---> BDD-cost:    1
c ---[ 701]---> BDD-cost:    1
c ---[ 700]---> BDD-cost:    1
c ---[ 699]---> BDD-cost:   21
c ---[ 698]---> BDD-cost:    1
c ---[ 697]---> BDD-cost:    1
c ---[ 696]---> BDD-cost:    1
c ---[ 695]---> BDD-cost:   16
c ---[ 694]---> BDD-cost:    1
c ---[ 693]---> BDD-cost:    1
c ---[ 692]---> BDD-cost:    1
c ---[ 691]---> BDD-cost:   16
c ---[ 690]---> BDD-cost:    1
c ---[ 689]---> BDD-cost:    1
c ---[ 688]---> BDD-cost:    1
c ---[ 687]---> BDD-cost:   16
c ---[ 686]---> BDD-cost:    1
c ---[ 685]---> BDD-cost:    1
c ---[ 684]---> BDD-cost:    1
c ---[ 683]---> BDD-cost:   16
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:    1
c ---[ 662]---> BDD-cost:    1
c ---[ 661]---> BDD-cost:    1
c ---[ 660]---> BDD-cost:    1
c ---[ 659]---> BDD-cost:    1
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:   17
c ---[ 630]---> BDD-cost:   17
c ---[ 629]---> BDD-cost:    1
c ---[ 628]---> BDD-cost:    1
c ---[ 627]---> BDD-cost:   17
c ---[ 626]---> BDD-cost:   17
c ---[ 625]---> BDD-cost:    1
c ---[ 624]---> BDD-cost:    1
c ---[ 623]---> BDD-cost:   21
c ---[ 622]---> BDD-cost:    1
c ---[ 621]---> BDD-cost:    1
c ---[ 620]---> BDD-cost:    1
c ---[ 619]---> BDD-cost:   21
c ---[ 618]---> BDD-cost:    1
c ---[ 617]---> BDD-cost:    1
c ---[ 616]---> BDD-cost:    1
c ---[ 615]---> BDD-cost:   16
c ---[ 614]---> BDD-cost:    1
c ---[ 613]---> BDD-cost:    1
c ---[ 612]---> BDD-cost:    1
c ---[ 611]---> BDD-cost:   16
c ---[ 610]---> BDD-cost:    1
c ---[ 609]---> BDD-cost:    1
c ---[ 608]---> BDD-cost:    1
c ---[ 607]---> BDD-cost:   16
c ---[ 606]---> BDD-cost:    1
c ---[ 605]---> BDD-cost:    1
c ---[ 604]---> BDD-cost:    1
c ---[ 603]---> BDD-cost:   16
c ---[ 602]---> BDD-cost:    1
c ---[ 601]---> BDD-cost:    1
c ---[ 600]---> BDD-cost:    1
c ---[ 599]---> BDD-cost:   17
c ---[ 598]---> BDD-cost:   17
c ---[ 597]---> BDD-cost:    1
c ---[ 596]---> BDD-cost:    1
c ---[ 595]---> BDD-cost:   17
c ---[ 594]---> BDD-cost:   17
c ---[ 593]---> BDD-cost:    1
c ---[ 592]---> BDD-cost:    1
c ---[ 591]---> BDD-cost:   21
c ---[ 590]---> BDD-cost:    1
c ---[ 589]---> BDD-cost:    1
c ---[ 588]---> BDD-cost:    1
c ---[ 587]---> BDD-cost:   21
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:   16
c ---[ 574]---> BDD-cost:    1
c ---[ 573]---> BDD-cost:    1
c ---[ 572]---> BDD-cost:    1
c ---[ 571]---> BDD-cost:   16
c ---[ 570]---> BDD-cost:    1
c ---[ 569]---> BDD-cost:    1
c ---[ 568]---> BDD-cost:    1
c ---[ 567]---> BDD-cost:   16
c ---[ 566]---> BDD-cost:    1
c ---[ 565]---> BDD-cost:    1
c ---[ 564]---> BDD-cost:    1
c ---[ 563]---> BDD-cost:   16
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:    1
c ---[ 526]---> BDD-cost:    1
c ---[ 525]---> BDD-cost:    1
c ---[ 524]---> BDD-cost:    1
c ---[ 523]---> BDD-cost:    1
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:   17
c ---[ 502]---> BDD-cost:   17
c ---[ 501]---> BDD-cost:    1
c ---[ 500]---> BDD-cost:    1
c ---[ 499]---> BDD-cost:   17
c ---[ 498]---> BDD-cost:   17
c ---[ 497]---> BDD-cost:    1
c ---[ 496]---> BDD-cost:    1
c ---[ 495]---> BDD-cost:   21
c ---[ 494]---> BDD-cost:    1
c ---[ 493]---> BDD-cost:    1
c ---[ 492]---> BDD-cost:    1
c ---[ 491]---> BDD-cost:   21
c ---[ 490]---> BDD-cost:    1
c ---[ 489]---> BDD-cost:    1
c ---[ 488]---> BDD-cost:    1
c ---[ 487]---> BDD-cost:   16
c ---[ 486]---> BDD-cost:    1
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:   17
c ---[ 462]---> BDD-cost:   17
c ---[ 461]---> BDD-cost:    1
c ---[ 460]---> BDD-cost:    1
c ---[ 459]---> BDD-cost:   17
c ---[ 458]---> BDD-cost:   17
c ---[ 457]---> BDD-cost:    1
c ---[ 456]---> BDD-cost:    1
c ---[ 455]---> BDD-cost:   21
c ---[ 454]---> BDD-cost:    1
c ---[ 453]---> BDD-cost:    1
c ---[ 452]---> BDD-cost:    1
c ---[ 451]---> BDD-cost:   21
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:   16
c ---[ 434]---> BDD-cost:    1
c ---[ 433]---> BDD-cost:    1
c ---[ 432]---> BDD-cost:    1
c ---[ 431]---> BDD-cost:   16
c ---[ 430]---> BDD-cost:    1
c ---[ 429]---> BDD-cost:    1
c ---[ 428]---> BDD-cost:    1
c ---[ 427]---> BDD-cost:   16
c ---[ 426]---> BDD-cost:    1
c ---[ 425]---> BDD-cost:    1
c ---[ 424]---> BDD-cost:    1
c ---[ 423]---> BDD-cost:   16
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:   16
c ---[ 386]---> BDD-cost:    1
c ---[ 385]---> BDD-cost:    1
c ---[ 384]---> BDD-cost:    1
c ---[ 383]---> BDD-cost:   16
c ---[ 382]---> BDD-cost:    1
c ---[ 381]---> BDD-cost:    1
c ---[ 380]---> BDD-cost:    1
c ---[ 379]---> BDD-cost:   16
c ---[ 378]---> BDD-cost:    1
c ---[ 377]---> BDD-cost:    1
c ---[ 376]---> BDD-cost:    1
c ---[ 375]---> BDD-cost:    1
c ---[ 374]---> BDD-cost:    1
c ---[ 373]---> BDD-cost:    1
c ---[ 372]---> BDD-cost:    1
c ---[ 371]---> BDD-cost:    1
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:   17
c ---[ 358]---> BDD-cost:   17
c ---[ 357]---> BDD-cost:    1
c ---[ 356]---> BDD-cost:    1
c ---[ 355]---> BDD-cost:   17
c ---[ 354]---> BDD-cost:   17
c ---[ 353]---> BDD-cost:    1
c ---[ 352]---> BDD-cost:    1
c ---[ 351]---> BDD-cost:   21
c ---[ 350]---> BDD-cost:    1
c ---[ 349]---> BDD-cost:    1
c ---[ 348]---> BDD-cost:    1
c ---[ 347]---> BDD-cost:   21
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:   16
c ---[ 338]---> BDD-cost:    1
c ---[ 337]---> BDD-cost:    1
c ---[ 336]---> BDD-cost:    1
c ---[ 335]---> BDD-cost:   16
c ---[ 334]---> BDD-cost:    1
c ---[ 333]---> BDD-cost:    1
c ---[ 332]---> BDD-cost:    1
c ---[ 331]---> BDD-cost:   16
c ---[ 330]---> BDD-cost:    1
c ---[ 329]---> BDD-cost:    1
c ---[ 328]---> BDD-cost:    1
c ---[ 327]---> BDD-cost:   16
c ---[ 326]---> BDD-cost:    1
c ---[ 325]---> BDD-cost:    1
c ---[ 324]---> BDD-cost:    1
c ---[ 323]---> BDD-cost:   16
c ---[ 322]---> BDD-cost:    1
c ---[ 321]---> BDD-cost:    1
c ---[ 320]---> BDD-cost:    1
c ---[ 319]---> BDD-cost:   16
c ---[ 318]---> BDD-cost:    1
c ---[ 317]---> BDD-cost:    1
c ---[ 316]---> BDD-cost:    1
c ---[ 315]---> BDD-cost:   16
c ---[ 314]---> BDD-cost:    1
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:   16
c ---[ 294]---> BDD-cost:    1
c ---[ 293]---> BDD-cost:    1
c ---[ 292]---> BDD-cost:    1
c ---[ 291]---> BDD-cost:   16
c ---[ 290]---> BDD-cost:    1
c ---[ 289]---> BDD-cost:    1
c ---[ 288]---> BDD-cost:    1
c ---[ 287]---> BDD-cost:   16
c ---[ 286]---> BDD-cost:    1
c ---[ 285]---> BDD-cost:    1
c ---[ 284]---> BDD-cost:    1
c ---[ 283]---> BDD-cost:   16
c ---[ 282]---> BDD-cost:    1
c ---[ 281]---> BDD-cost:    1
c ---[ 280]---> BDD-cost:    1
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:    1
c ---[ 277]---> BDD-cost:    1
c ---[ 276]---> BDD-cost:    1
c ---[ 275]---> BDD-cost:   16
c ---[ 274]---> BDD-cost:    1
c ---[ 273]---> BDD-cost:    1
c ---[ 272]---> BDD-cost:    1
c ---[ 271]---> BDD-cost:   16
c ---[ 270]---> BDD-cost:    1
c ---[ 269]---> BDD-cost:    1
c ---[ 268]---> BDD-cost:    1
c ---[ 267]---> BDD-cost:   16
c ---[ 266]---> BDD-cost:    1
c ---[ 265]---> BDD-cost:    1
c ---[ 264]---> BDD-cost:    1
c ---[ 263]---> BDD-cost:   16
c ---[ 262]---> BDD-cost:    1
c ---[ 261]---> BDD-cost:    1
c ---[ 260]---> BDD-cost:    1
c ---[ 259]---> BDD-cost:   16
c ---[ 258]---> BDD-cost:    1
c ---[ 257]---> BDD-cost:    1
c ---[ 256]---> BDD-cost:    1
c ---[ 255]---> BDD-cost:   16
c ---[ 254]---> BDD-cost:    1
c ---[ 253]---> BDD-cost:    1
c ---[ 252]---> BDD-cost:    1
c ---[ 251]---> BDD-cost:   16
c ---[ 250]---> BDD-cost:    1
c ---[ 249]---> BDD-cost:    1
c ---[ 248]---> BDD-cost:    1
c ---[ 247]---> BDD-cost:   16
c ---[ 246]---> BDD-cost:    1
c ---[ 245]---> BDD-cost:    1
c ---[ 244]---> BDD-cost:    1
c ---[ 243]---> BDD-cost:   16
c ---[ 242]---> BDD-cost:    1
c ---[ 241]---> BDD-cost:    1
c ---[ 240]---> BDD-cost:    1
c ---[ 239]---> BDD-cost:   16
c ---[ 238]---> BDD-cost:    1
c ---[ 237]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 235]---> BDD-cost:   16
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:   16
c ---[ 214]---> BDD-cost:    1
c ---[ 213]---> BDD-cost:    1
c ---[ 212]---> BDD-cost:    1
c ---[ 211]---> BDD-cost:   16
c ---[ 210]---> BDD-cost:    1
c ---[ 209]---> BDD-cost:    1
c ---[ 208]---> BDD-cost:    1
c ---[ 207]---> BDD-cost:    1
c ---[ 206]---> BDD-cost:    1
c ---[ 205]---> BDD-cost:    1
c ---[ 204]---> BDD-cost:    1
c ---[ 203]---> BDD-cost:    1
c ---[ 202]---> BDD-cost:    1
c ---[ 201]---> BDD-cost:    1
c ---[ 200]---> BDD-cost:    1
c ---[ 199]---> BDD-cost:   11
c ---[ 198]---> BDD-cost:    1
c ---[ 197]---> BDD-cost:    1
c ---[ 196]---> BDD-cost:    1
c ---[ 195]---> BDD-cost:   11
c ---[ 194]---> BDD-cost:    1
c ---[ 193]---> BDD-cost:    1
c ---[ 192]---> BDD-cost:    1
c ---[ 191]---> BDD-cost:   11
c ---[ 190]---> BDD-cost:    1
c ---[ 189]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 187]---> BDD-cost:   11
c ---[ 186]---> BDD-cost:    1
c ---[ 185]---> BDD-cost:    1
c ---[ 184]---> BDD-cost:    1
c ---[ 183]---> BDD-cost:   11
c ---[ 182]---> BDD-cost:    1
c ---[ 181]---> BDD-cost:    1
c ---[ 180]---> BDD-cost:    1
c ---[ 179]---> BDD-cost:   11
c ---[ 178]---> BDD-cost:    1
c ---[ 177]---> BDD-cost:    1
c ---[ 176]---> BDD-cost:    1
c ---[ 175]---> BDD-cost:   11
c ---[ 174]---> BDD-cost:    1
c ---[ 173]---> BDD-cost:    1
c ---[ 172]---> BDD-cost:    1
c ---[ 171]---> BDD-cost:   11
c ---[ 170]---> BDD-cost:    1
c ---[ 169]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 167]---> BDD-cost:   11
c ---[ 166]---> BDD-cost:    1
c ---[ 165]---> BDD-cost:    1
c ---[ 164]---> BDD-cost:    1
c ---[ 163]---> BDD-cost:   11
c ---[ 162]---> BDD-cost:    1
c ---[ 161]---> BDD-cost:    1
c ---[ 160]---> BDD-cost:    1
c ---[ 159]---> BDD-cost:   11
c ---[ 158]---> BDD-cost:    1
c ---[ 157]---> BDD-cost:    1
c ---[ 156]---> BDD-cost:    1
c ---[ 155]---> BDD-cost:   11
c ---[ 154]---> BDD-cost:    1
c ---[ 153]---> BDD-cost:    1
c ---[ 152]---> BDD-cost:    1
c ---[ 151]---> BDD-cost:   11
c ---[ 150]---> BDD-cost:    1
c ---[ 149]---> BDD-cost:    1
c ---[ 148]---> BDD-cost:    1
c ---[ 147]---> BDD-cost:   11
c ---[ 146]---> BDD-cost:    1
c ---[ 145]---> BDD-cost:    1
c ---[ 144]---> BDD-cost:    1
c ---[ 143]---> BDD-cost:   11
c ---[ 142]---> BDD-cost:    1
c ---[ 141]---> BDD-cost:    1
c ---[ 140]---> BDD-cost:    1
c ---[ 139]---> BDD-cost:   11
c ---[ 138]---> BDD-cost:    1
c ---[ 137]---> BDD-cost:    1
c ---[ 136]---> BDD-cost:    1
c ---[ 135]---> BDD-cost:   17
c ---[ 134]---> BDD-cost:   17
c ---[ 133]---> BDD-cost:    1
c ---[ 132]---> BDD-cost:    1
c ---[ 131]---> BDD-cost:   17
c ---[ 130]---> BDD-cost:   17
c ---[ 129]---> BDD-cost:    1
c ---[ 128]---> BDD-cost:    1
c ---[ 127]---> BDD-cost:   21
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:   21
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:   16
c ---[ 114]---> BDD-cost:    1
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:   16
c ---[ 110]---> BDD-cost:    1
c ---[ 109]---> BDD-cost:    1
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:   16
c ---[ 106]---> BDD-cost:    1
c ---[ 105]---> BDD-cost:    1
c ---[ 104]---> BDD-cost:    1
c ---[ 103]---> BDD-cost:   16
c ---[ 102]---> BDD-cost:    1
c ---[ 101]---> BDD-cost:    1
c ---[ 100]---> BDD-cost:    1
c ---[  99]---> BDD-cost:   16
c ---[  98]---> BDD-cost:    1
c ---[  97]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  95]---> BDD-cost:   16
c ---[  94]---> BDD-cost:    1
c ---[  93]---> BDD-cost:    1
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:   16
c ---[  90]---> BDD-cost:    1
c ---[  89]---> BDD-cost:    1
c ---[  88]---> BDD-cost:    1
c ---[  87]---> BDD-cost:   16
c ---[  86]---> BDD-cost:    1
c ---[  85]---> BDD-cost:    1
c ---[  84]---> BDD-cost:    1
c ---[  83]---> BDD-cost:   16
c ---[  82]---> BDD-cost:    1
c ---[  81]---> BDD-cost:    1
c ---[  80]---> BDD-cost:    1
c ---[  79]---> BDD-cost:   17
c ---[  78]---> BDD-cost:   17
c ---[  77]---> BDD-cost:    1
c ---[  76]---> BDD-cost:    1
c ---[  75]---> BDD-cost:   17
c ---[  74]---> BDD-cost:   17
c ---[  73]---> BDD-cost:    1
c ---[  72]---> BDD-cost:    1
c ---[  71]---> BDD-cost:   21
c ---[  70]---> BDD-cost:    1
c ---[  69]---> BDD-cost:    1
c ---[  68]---> BDD-cost:    1
c ---[  67]---> BDD-cost:   21
c ---[  66]---> BDD-cost:    1
c ---[  65]---> BDD-cost:    1
c ---[  64]---> BDD-cost:    1
c ---[  63]---> BDD-cost:   16
c ---[  62]---> BDD-cost:    1
c ---[  61]---> BDD-cost:    1
c ---[  60]---> BDD-cost:    1
c ---[  59]---> BDD-cost:   16
c ---[  58]---> BDD-cost:    1
c ---[  57]---> BDD-cost:    1
c ---[  56]---> BDD-cost:    1
c ---[  55]---> BDD-cost:   16
c ---[  54]---> BDD-cost:    1
c ---[  53]---> BDD-cost:    1
c ---[  52]---> BDD-cost:    1
c ---[  51]---> BDD-cost:   16
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost:    1
c ---[  48]---> BDD-cost:    1
c ---[  47]---> BDD-cost:   16
c ---[  46]---> BDD-cost:    1
c ---[  45]---> BDD-cost:    1
c ---[  44]---> BDD-cost:    1
c ---[  43]---> BDD-cost:   16
c ---[  42]---> BDD-cost:    1
c ---[  41]---> BDD-cost:    1
c ---[  40]---> BDD-cost:    1
c ---[  39]---> BDD-cost:   16
c ---[  38]---> BDD-cost:    1
c ---[  37]---> BDD-cost:    1
c ---[  36]---> BDD-cost:    1
c ---[  35]---> BDD-cost:   16
c ---[  34]---> BDD-cost:    1
c ---[  33]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  31]---> BDD-cost:   16
c ---[  30]---> BDD-cost:    1
c ---[  29]---> BDD-cost:    1
c ---[  28]---> BDD-cost:    1
c ---[  27]---> BDD-cost:   16
c ---[  26]---> BDD-cost:    1
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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  107830   271051 |   32348       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/32674          
c   -- var.elim.:  2000/32674          
c   -- var.elim.:  3000/32674          
c   -- var.elim.:  4000/32674          
c   -- var.elim.:  5000/32674          
c   -- var.elim.:  6000/32674          
c   -- var.elim.:  7000/32674          
c   -- var.elim.:  8000/32674          
c   -- var.elim.:  9000/32674          
c   -- var.elim.:  10000/32674          
c   -- var.elim.:  11000/32674          
c   -- var.elim.:  12000/32674          
c   -- var.elim.:  13000/32674          
c   -- var.elim.:  14000/32674          
c   -- var.elim.:  15000/32674          
c   -- var.elim.:  16000/32674          
c   -- var.elim.:  17000/32674          
c   -- var.elim.:  18000/32674          
c   -- var.elim.:  19000/32674          
c   -- var.elim.:  20000/32674          
c   -- var.elim.:  21000/32674          
c   -- var.elim.:  22000/32674          
c   -- var.elim.:  23000/32674          
c   -- var.elim.:  24000/32674          
c   -- var.elim.:  25000/32674          
c   -- var.elim.:  26000/32674          
c   -- var.elim.:  27000/32674          
c   -- var.elim.:  28000/32674          
c   -- var.elim.:  29000/32674          
c   -- var.elim.:  30000/32674          
c   -- var.elim.:  31000/32674          
c   -- var.elim.:  32000/32674          
c   -- var.elim.:  32674/32674          
c   -- var.elim.:  1000/10599          
c   -- var.elim.:  2000/10599          
c   -- var.elim.:  3000/10599          
c   -- var.elim.:  4000/10599          
c   -- var.elim.:  5000/10599          
c   -- var.elim.:  6000/10599          
c   -- var.elim.:  7000/10599          
c   -- var.elim.:  8000/10599          
c   -- var.elim.:  9000/10599          
c   -- var.elim.:  10000/10599          
c   -- var.elim.:  10599/10599          
c   -- var.elim.:  810/810          
c   -- var.elim.:  358/358          
c   -- var.elim.:  327/327          
c   -- var.elim.:  201/201          
c   -- var.elim.:  140/140          
c   -- var.elim.:  154/154          
c   -- var.elim.:  173/173          
c   -- var.elim.:  178/178          
c   -- var.elim.:  58/58          
c   -- subsuming                       
c   -- var.elim.:  1000/3430          
c   -- var.elim.:  2000/3430          
c   -- var.elim.:  3000/3430          
c   -- var.elim.:  3430/3430          
c   -- var.elim.:  1000/1325          
c   -- var.elim.:  1325/1325          
c   -- var.elim.:  92/92          
c   -- var.elim.:  28/28          
c   -- subsuming                       
c   -- var.elim.:  137/137          
c   -- var.elim.:  18/18          
c |         0 |   58431   194288 |      --       0       --      -- |     --   | -49399/-72901
c |         0 |   58431   194288 |   23372       0        0     nan |  0.000 % |
c |       100 |   58431   194288 |   25709     100     1650    16.5 | 24.617 % |
c |       251 |   52877   172276 |   25592     249     3941    15.8 | 28.245 % |
c |       476 |   52877   172276 |   28151     474     9347    19.7 | 28.245 % |
c |       821 |   52877   172276 |   30966     819    15842    19.3 | 28.245#### 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.87 0.94 0.90 2/54 1991
Raw data (stat): 1991 (runsolver) R 1990 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480381334 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99972 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 6775 0 0 0 970 27 0 0 25 0 1 0 480381334 29913088 6373 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7303 6373 603 41 0 7262 0
vsize: 29212
[startup+20.0026 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 7489 0 0 0 1968 29 0 0 25 0 1 0 480381334 32964608 7087 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8048 7087 603 41 0 8007 0
vsize: 32192
[startup+30.0031 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 8163 0 0 0 2966 31 0 0 25 0 1 0 480381334 35725312 7761 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8722 7761 603 41 0 8681 0
vsize: 34888
[startup+40.0037 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 8509 0 0 0 3964 32 0 0 25 0 1 0 480381334 37060608 8107 4294967295 134512640 134672761 3221224528 3221223664 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9048 8107 603 41 0 9007 0
vsize: 36192
[startup+50.0047 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 9691 0 0 0 4960 36 0 0 25 0 1 0 480381334 42074112 9289 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10272 9289 603 41 0 10231 0
vsize: 41088
[startup+60.0041 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 10871 0 0 0 5955 41 0 0 25 0 1 0 480381334 46845952 10469 4294967295 134512640 134672761 3221224528 3221223712 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11437 10469 603 41 0 11396 0
vsize: 45748
[startup+70.005 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 12182 0 0 0 6952 45 0 0 25 0 1 0 480381334 52281344 11780 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12764 11780 603 41 0 12723 0
vsize: 51056
[startup+80.0058 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 13281 0 0 0 7950 47 0 0 25 0 1 0 480381334 56774656 12879 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13861 12879 603 41 0 13820 0
vsize: 55444
[startup+90.0062 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 14298 0 0 0 8946 51 0 0 25 0 1 0 480381334 60907520 13896 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14870 13896 603 41 0 14829 0
vsize: 59480
[startup+100.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 15307 0 0 0 9944 53 0 0 25 0 1 0 480381334 65007616 14905 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15871 14905 603 41 0 15830 0
vsize: 63484
[startup+110.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 16608 0 0 0 10941 57 0 0 25 0 1 0 480381334 70668288 16206 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17253 16206 603 41 0 17212 0
vsize: 69012
[startup+120.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 17436 0 0 0 11939 59 0 0 25 0 1 0 480381334 73953280 17034 4294967295 134512640 134672761 3221224528 3221223568 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18055 17034 603 41 0 18014 0
vsize: 72220
[startup+130.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 18279 0 0 0 12937 62 0 0 25 0 1 0 480381334 77500416 17877 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18921 17877 603 41 0 18880 0
vsize: 75684
[startup+140.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 19237 0 0 0 13933 65 0 0 25 0 1 0 480381334 81342464 18835 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19859 18835 603 41 0 19818 0
vsize: 79436
[startup+150.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 20209 0 0 0 14930 69 0 0 25 0 1 0 480381334 85327872 19807 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20832 19807 603 41 0 20791 0
vsize: 83328
[startup+160.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 21067 0 0 0 15929 70 0 0 25 0 1 0 480381334 88739840 20665 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21665 20665 603 41 0 21624 0
vsize: 86660
[startup+170.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 21855 0 0 0 16927 72 0 0 25 0 1 0 480381334 92020736 21453 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22466 21453 603 41 0 22425 0
vsize: 89864
[startup+180.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22415 0 0 0 17925 74 0 0 25 0 1 0 480381334 94121984 21919 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21919 603 41 0 22938 0
vsize: 91916
[startup+190.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22415 0 0 0 18926 74 0 0 25 0 1 0 480381334 94121984 21919 4294967295 134512640 134672761 3221224528 3221223728 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21919 603 41 0 22938 0
vsize: 91916
[startup+200.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22415 0 0 0 19926 74 0 0 25 0 1 0 480381334 94121984 21919 4294967295 134512640 134672761 3221224528 3221223712 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21919 603 41 0 22938 0
vsize: 91916
[startup+210.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22415 0 0 0 20926 74 0 0 25 0 1 0 480381334 94121984 21919 4294967295 134512640 134672761 3221224528 3221223712 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21919 603 41 0 22938 0
vsize: 91916
[startup+220.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22415 0 0 0 21926 74 0 0 25 0 1 0 480381334 94121984 21919 4294967295 134512640 134672761 3221224528 3221223712 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21919 603 41 0 22938 0
vsize: 91916
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22415 0 0 0 22926 74 0 0 25 0 1 0 480381334 94121984 21919 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21919 603 41 0 22938 0
vsize: 91916
[startup+240.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22417 0 0 0 23926 74 0 0 25 0 1 0 480381334 94121984 21921 4294967295 134512640 134672761 3221224528 3221223568 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21921 603 41 0 22938 0
vsize: 91916
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22419 0 0 0 24927 74 0 0 25 0 1 0 480381334 94121984 21923 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21923 603 41 0 22938 0
vsize: 91916
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22419 0 0 0 25927 74 0 0 25 0 1 0 480381334 94121984 21923 4294967295 134512640 134672761 3221224528 3221223712 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21923 603 41 0 22938 0
vsize: 91916
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22419 0 0 0 26927 74 0 0 25 0 1 0 480381334 94121984 21923 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21923 603 41 0 22938 0
vsize: 91916
[startup+280.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22419 0 0 0 27927 74 0 0 25 0 1 0 480381334 94121984 21923 4294967295 134512640 134672761 3221224528 3221223712 134615734 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21923 603 41 0 22938 0
vsize: 91916
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22419 0 0 0 28927 74 0 0 25 0 1 0 480381334 94121984 21923 4294967295 134512640 134672761 3221224528 3221223712 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21923 603 41 0 22938 0
vsize: 91916
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22419 0 0 0 29928 74 0 0 25 0 1 0 480381334 94121984 21923 4294967295 134512640 134672761 3221224528 3221223568 134612572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22979 21923 603 41 0 22938 0
vsize: 91916
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 22558 0 0 0 30927 75 0 0 25 0 1 0 480381334 94785536 22062 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23141 22062 603 41 0 23100 0
vsize: 92564
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 23107 0 0 0 31926 76 0 0 25 0 1 0 480381334 97083392 22611 4294967295 134512640 134672761 3221224528 3221223392 1075349719 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23702 22611 603 41 0 23661 0
vsize: 94808
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 23749 0 0 0 32924 78 0 0 25 0 1 0 480381334 99790848 23253 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24363 23253 603 41 0 24322 0
vsize: 97452
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 24475 0 0 0 33922 80 0 0 25 0 1 0 480381334 102719488 23979 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25078 23979 603 41 0 25037 0
vsize: 100312
[startup+350.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 25237 0 0 0 34920 82 0 0 25 0 1 0 480381334 105910272 24741 4294967295 134512640 134672761 3221224528 3221223692 134614558 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25857 24741 603 41 0 25816 0
vsize: 103428
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 25941 0 0 0 35918 84 0 0 25 0 1 0 480381334 108728320 25445 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26545 25445 603 41 0 26504 0
vsize: 106180
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 26587 0 0 0 36917 86 0 0 25 0 1 0 480381334 111390720 26091 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27195 26091 603 41 0 27154 0
vsize: 108780
[startup+380.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27188 0 0 0 37915 88 0 0 25 0 1 0 480381334 113909760 26692 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27810 26692 603 41 0 27769 0
vsize: 111240
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27525 0 0 0 38914 89 0 0 25 0 1 0 480381334 115130368 26997 4294967295 134512640 134672761 3221224528 3221223624 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28108 26997 603 41 0 28067 0
vsize: 112432
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27525 0 0 0 39914 89 0 0 25 0 1 0 480381334 114606080 26894 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26894 603 41 0 27939 0
vsize: 111920
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27526 0 0 0 40914 89 0 0 25 0 1 0 480381334 114606080 26895 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26895 603 41 0 27939 0
vsize: 111920
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27527 0 0 0 41914 89 0 0 25 0 1 0 480381334 114606080 26896 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26896 603 41 0 27939 0
vsize: 111920
[startup+430.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27527 0 0 0 42914 89 0 0 25 0 1 0 480381334 114606080 26896 4294967295 134512640 134672761 3221224528 3221223568 134612975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26896 603 41 0 27939 0
vsize: 111920
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27527 0 0 0 43915 89 0 0 25 0 1 0 480381334 114606080 26896 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26896 603 41 0 27939 0
vsize: 111920
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27527 0 0 0 44915 89 0 0 25 0 1 0 480381334 114606080 26896 4294967295 134512640 134672761 3221224528 3221223664 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26896 603 41 0 27939 0
vsize: 111920
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27527 0 0 0 45915 89 0 0 25 0 1 0 480381334 114606080 26896 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26896 603 41 0 27939 0
vsize: 111920
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27528 0 0 0 46915 89 0 0 25 0 1 0 480381334 114606080 26897 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26897 603 41 0 27939 0
vsize: 111920
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27528 0 0 0 47915 89 0 0 25 0 1 0 480381334 114606080 26897 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26897 603 41 0 27939 0
vsize: 111920
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27529 0 0 0 48916 89 0 0 25 0 1 0 480381334 114606080 26898 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26898 603 41 0 27939 0
vsize: 111920
[startup+500.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27532 0 0 0 49916 89 0 0 25 0 1 0 480381334 114606080 26901 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26901 603 41 0 27939 0
vsize: 111920
[startup+510.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27532 0 0 0 50916 89 0 0 25 0 1 0 480381334 114606080 26901 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26901 603 41 0 27939 0
vsize: 111920
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27533 0 0 0 51916 89 0 0 25 0 1 0 480381334 114606080 26902 4294967295 134512640 134672761 3221224528 3221223568 134613809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26902 603 41 0 27939 0
vsize: 111920
[startup+530.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27533 0 0 0 52916 89 0 0 25 0 1 0 480381334 114606080 26902 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26902 603 41 0 27939 0
vsize: 111920
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27534 0 0 0 53916 89 0 0 25 0 1 0 480381334 114606080 26903 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26903 603 41 0 27939 0
vsize: 111920
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27534 0 0 0 54917 89 0 0 25 0 1 0 480381334 114606080 26903 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26903 603 41 0 27939 0
vsize: 111920
[startup+560.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27534 0 0 0 55917 89 0 0 25 0 1 0 480381334 114606080 26903 4294967295 134512640 134672761 3221224528 3221223712 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26903 603 41 0 27939 0
vsize: 111920
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27536 0 0 0 56917 90 0 0 25 0 1 0 480381334 114606080 26905 4294967295 134512640 134672761 3221224528 3221223664 134614814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26905 603 41 0 27939 0
vsize: 111920
[startup+580.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27540 0 0 0 57917 90 0 0 25 0 1 0 480381334 114606080 26909 4294967295 134512640 134672761 3221224528 3221223712 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27980 26909 603 41 0 27939 0
vsize: 111920
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 58917 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 59917 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 60917 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 61918 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223672 134616247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 62918 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 63918 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+650.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 64918 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223568 134614254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 65918 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 66919 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 67919 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+690.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 68919 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 69919 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223728 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 70919 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 71920 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223568 134614256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 72920 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 73920 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27655 0 0 0 74920 90 0 0 25 0 1 0 480381334 114597888 26913 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26913 603 41 0 27937 0
vsize: 111912
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27656 0 0 0 75920 90 0 0 25 0 1 0 480381334 114597888 26914 4294967295 134512640 134672761 3221224528 3221223712 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26914 603 41 0 27937 0
vsize: 111912
[startup+770.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1991
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27656 0 0 0 76921 90 0 0 25 0 1 0 480381334 114597888 26914 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26914 603 41 0 27937 0
vsize: 111912
[startup+780.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2044
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27656 0 0 0 77921 90 0 0 25 0 1 0 480381334 114597888 26914 4294967295 134512640 134672761 3221224528 3221223400 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26914 603 41 0 27937 0
vsize: 111912
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2044
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27656 0 0 0 78921 90 0 0 25 0 1 0 480381334 114597888 26914 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26914 603 41 0 27937 0
vsize: 111912
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2044
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27656 0 0 0 79921 90 0 0 25 0 1 0 480381334 114597888 26914 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26914 603 41 0 27937 0
vsize: 111912
[startup+810.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2044
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27656 0 0 0 80921 90 0 0 25 0 1 0 480381334 114597888 26914 4294967295 134512640 134672761 3221224528 3221223712 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27978 26914 603 41 0 27937 0
vsize: 111912
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2044
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 27860 0 0 0 81920 91 0 0 25 0 1 0 480381334 115519488 27118 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28203 27118 603 41 0 28162 0
vsize: 112812
[startup+830.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2044
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 28311 0 0 0 82920 92 0 0 25 0 1 0 480381334 117358592 27569 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28652 27569 603 41 0 28611 0
vsize: 114608
[startup+840.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2044
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 28807 0 0 0 83919 93 0 0 25 0 1 0 480381334 119324672 28065 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29132 28065 603 41 0 29091 0
vsize: 116528
[startup+850.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 29276 0 0 0 84917 95 0 0 25 0 1 0 480381334 121335808 28534 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29623 28534 603 41 0 29582 0
vsize: 118492
[startup+860.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 29730 0 0 0 85916 96 0 0 25 0 1 0 480381334 123187200 28988 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30075 28988 603 41 0 30034 0
vsize: 120300
[startup+870.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30068 0 0 0 86915 97 0 0 25 0 1 0 480381334 124489728 29326 4294967295 134512640 134672761 3221224528 3221223584 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30393 29326 603 41 0 30352 0
vsize: 121572
[startup+880.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30075 0 0 0 87915 97 0 0 25 0 1 0 480381334 123965440 29214 4294967295 134512640 134672761 3221224528 3221223568 134603506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29214 603 41 0 30224 0
vsize: 121060
[startup+890.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30075 0 0 0 88916 97 0 0 25 0 1 0 480381334 123965440 29214 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29214 603 41 0 30224 0
vsize: 121060
[startup+900.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30075 0 0 0 89916 97 0 0 25 0 1 0 480381334 123965440 29214 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29214 603 41 0 30224 0
vsize: 121060
[startup+910.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30075 0 0 0 90916 97 0 0 25 0 1 0 480381334 123965440 29214 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29214 603 41 0 30224 0
vsize: 121060
[startup+920.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30075 0 0 0 91916 97 0 0 25 0 1 0 480381334 123965440 29214 4294967295 134512640 134672761 3221224528 3221223716 1075346949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29214 603 41 0 30224 0
vsize: 121060
[startup+930.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30075 0 0 0 92916 97 0 0 25 0 1 0 480381334 123965440 29214 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29214 603 41 0 30224 0
vsize: 121060
[startup+940.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 93917 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+950.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 94917 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223664 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+960.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 95917 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+970.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 96917 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+980.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 97917 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+990.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 98917 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 99918 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 100918 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 101918 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 102918 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 103918 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 104919 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223340 1075349950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 105919 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223568 134614254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 106919 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 107919 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 108919 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 109919 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30077 0 0 0 110920 97 0 0 25 0 1 0 480381334 123965440 29216 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29216 603 41 0 30224 0
vsize: 121060
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30079 0 0 0 111920 97 0 0 25 0 1 0 480381334 123965440 29218 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29218 603 41 0 30224 0
vsize: 121060
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30081 0 0 0 112920 97 0 0 25 0 1 0 480381334 123965440 29220 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29220 603 41 0 30224 0
vsize: 121060
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2046
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30084 0 0 0 113920 97 0 0 25 0 1 0 480381334 123965440 29223 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30265 29223 603 41 0 30224 0
vsize: 121060
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2048
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30087 0 0 0 114920 97 0 0 25 0 1 0 480381334 124489728 29226 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30393 29226 603 41 0 30352 0
vsize: 121572
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2048
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 30590 0 0 0 115920 98 0 0 25 0 1 0 480381334 126599168 29729 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30908 29729 603 41 0 30867 0
vsize: 123632
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2048
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 31084 0 0 0 116918 100 0 0 25 0 1 0 480381334 128782336 30223 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31441 30223 603 41 0 31400 0
vsize: 125764
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2048
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 31415 0 0 0 117917 101 0 0 25 0 1 0 480381334 129220608 30387 4294967295 134512640 134672761 3221224528 3221223712 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31548 30387 603 41 0 31507 0
vsize: 126192
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2048
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 31415 0 0 0 118917 101 0 0 25 0 1 0 480381334 129220608 30387 4294967295 134512640 134672761 3221224528 3221223568 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31548 30387 603 41 0 31507 0
vsize: 126192
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2048
Raw data (stat): 1991 (minisat+) R 1990 28546 28545 0 -1 0 31415 0 0 0 119917 101 0 0 25 0 1 0 480381334 129220608 30387 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31548 30387 603 41 0 31507 0
vsize: 126192
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 2048
Raw data (stat): 1991 (minisat+) Z 1990 28546 28545 0 -1 12 31415 0 0 0 119918 107 0 0 25 0 1 0 480381334 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.08
CPU time (s): 1200.25
CPU user time (s): 1199.18
CPU system time (s): 1.07084
CPU usage (%): 100.014
Max. virtual memory (Kb): 126192
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####