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 6359

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        890188 kB
Buffers:         36096 kB
Cached:          88464 kB
SwapCached:         16 kB
Active:          64600 kB
Inactive:        62872 kB
HighTotal:      131008 kB
HighFree:        38556 kB
LowTotal:       903652 kB
LowFree:        851632 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11356 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 04:51:33 (client local time) WITH STATUS 0 IN 1200.06 SECONDS
stats: 4812 7 1200.06 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  107830   271051 |   35943       0        0     nan |  0.000 % |
c |       101 |  107830   271051 |   39537     101      975     9.7 |  8.625 % |
c |       252 |  107830   271051 |   43491     252     3377    13.4 |  8.625 % |
c |       477 |   98944   250796 |   47840     474     6382    13.5 | 15.459 % |
c |       814 |   98944   250796 |   52624     811    18433    22.7 | 15.459 % |
c |      1321 |   98944   250796 |   57886    1318    28197    21.4 | 15.459 % |
c |      2081 |   98944   250796 |   63675    2078    49604    23.9 | 15.459 % |
c |      3220 |   98944   250796 |   70042    3217   135717    42.2 | 15.459 % |
c |      4928 |   98944   250796 |   77047    4925   270954    55.0 | 15.459 % |
c |      7490 |   98944   250796 |   84751    7487   579536    77.4 | 15.459 % |
c |     11335 |   98944   250796 |   93226   11332   642367    56.7 | 15.459 % |
c |     17102 |   98944   250796 |  102549   17099  1242601    72.7 | 15.459 % |
c |     25751 |   78302   202801 |  112804   24834  1458227    58.7 | 33.931 % |
c |     38725 |   78302   202801 |  124084   37808  2156538    57.0 | 33.931 % |
c |     58187 |   78302   202801 |  136493   57270  3267578    57.1 | 33.931 % |
c |     87380 |   78302   202801 |  150142   86463  4578397    53.0 | 33.931 % |
c |    131170 |   78302   202801 |  165157  130253  6825637    52.4 | 33.931 % |
c |    196854 |   78302   202801 |  181672   31812  1246573    39.2 | 33.931 % |
c |    295380 |   78302   202801 |  199840  130338  6447419    49.5 | 33.931 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.79 0.93 0.90 2/54 538
Raw data (stat): 538 (runsolver) R 537 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423506527 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 5089 0 0 0 982 16 0 0 25 0 1 0 423506527 22822912 4874 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5572 4874 603 41 0 5531 0
vsize: 22288
[startup+20.0079 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 5089 0 0 0 1983 16 0 0 25 0 1 0 423506527 22822912 4874 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5572 4874 603 41 0 5531 0
vsize: 22288
[startup+30.0088 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 5104 0 0 0 2982 17 0 0 25 0 1 0 423506527 22822912 4889 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5572 4889 603 41 0 5531 0
vsize: 22288
[startup+40.0091 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 5418 0 0 0 3981 18 0 0 25 0 1 0 423506527 24096768 5203 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5883 5203 603 41 0 5842 0
vsize: 23532
[startup+50.0094 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 5568 0 0 0 4980 19 0 0 25 0 1 0 423506527 24772608 5353 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6048 5353 603 41 0 6007 0
vsize: 24192
[startup+60.0093 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 5925 0 0 0 5978 20 0 0 25 0 1 0 423506527 26234880 5710 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6405 5710 603 41 0 6364 0
vsize: 25620
[startup+70.0105 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 6196 0 0 0 6978 21 0 0 25 0 1 0 423506527 27443200 5981 4294967295 134512640 134672761 3221224528 3221223712 134558885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6700 5981 603 41 0 6659 0
vsize: 26800
[startup+80.0114 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 6496 0 0 0 7977 22 0 0 25 0 1 0 423506527 28659712 6281 4294967295 134512640 134672761 3221224528 3221223712 134558890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6997 6281 603 41 0 6956 0
vsize: 27988
[startup+90.0107 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 6820 0 0 0 8975 24 0 0 25 0 1 0 423506527 30007296 6605 4294967295 134512640 134672761 3221224528 3221223712 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7326 6605 603 41 0 7285 0
vsize: 29304
[startup+100.011 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 7128 0 0 0 9974 25 0 0 25 0 1 0 423506527 31207424 6913 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7619 6913 603 41 0 7578 0
vsize: 30476
[startup+110.011 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 7415 0 0 0 10973 26 0 0 25 0 1 0 423506527 32428032 7200 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7917 7200 603 41 0 7876 0
vsize: 31668
[startup+120.012 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 7675 0 0 0 11971 27 0 0 25 0 1 0 423506527 33492992 7460 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8177 7460 603 41 0 8136 0
vsize: 32708
[startup+130.013 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 7836 0 0 0 12971 28 0 0 25 0 1 0 423506527 34066432 7621 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8317 7621 603 41 0 8276 0
vsize: 33268
[startup+140.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 7955 0 0 0 13970 28 0 0 25 0 1 0 423506527 34664448 7740 4294967295 134512640 134672761 3221224528 3221223712 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8463 7740 603 41 0 8422 0
vsize: 33852
[startup+150.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 8215 0 0 0 14969 29 0 0 25 0 1 0 423506527 35987456 8000 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8786 8000 603 41 0 8745 0
vsize: 35144
[startup+160.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 8483 0 0 0 15968 30 0 0 25 0 1 0 423506527 37048320 8268 4294967295 134512640 134672761 3221224528 3221223712 134558925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9045 8268 603 41 0 9004 0
vsize: 36180
[startup+170.013 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 8780 0 0 0 16967 31 0 0 25 0 1 0 423506527 38240256 8565 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9336 8565 603 41 0 9295 0
vsize: 37344
[startup+180.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 9068 0 0 0 17965 33 0 0 25 0 1 0 423506527 39464960 8853 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9635 8853 603 41 0 9594 0
vsize: 38540
[startup+190.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 9348 0 0 0 18963 35 0 0 25 0 1 0 423506527 40677376 9133 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9931 9133 603 41 0 9890 0
vsize: 39724
[startup+200.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 9571 0 0 0 19962 36 0 0 25 0 1 0 423506527 41504768 9356 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10133 9356 603 41 0 10092 0
vsize: 40532
[startup+210.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 9782 0 0 0 20960 38 0 0 25 0 1 0 423506527 42438656 9567 4294967295 134512640 134672761 3221224528 3221223696 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10361 9567 603 41 0 10320 0
vsize: 41444
[startup+220.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 9998 0 0 0 21959 39 0 0 25 0 1 0 423506527 43233280 9783 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10555 9783 603 41 0 10514 0
vsize: 42220
[startup+230.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 10214 0 0 0 22958 40 0 0 25 0 1 0 423506527 44158976 9999 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10781 9999 603 41 0 10740 0
vsize: 43124
[startup+240.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 10390 0 0 0 23956 41 0 0 25 0 1 0 423506527 44834816 10175 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10946 10175 603 41 0 10905 0
vsize: 43784
[startup+250.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 10522 0 0 0 24956 42 0 0 25 0 1 0 423506527 45367296 10307 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11076 10307 603 41 0 11035 0
vsize: 44304
[startup+260.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 10662 0 0 0 25955 43 0 0 25 0 1 0 423506527 45920256 10447 4294967295 134512640 134672761 3221224528 3221223696 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11211 10447 603 41 0 11170 0
vsize: 44844
[startup+270.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 10863 0 0 0 26954 44 0 0 25 0 1 0 423506527 46723072 10648 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11407 10648 603 41 0 11366 0
vsize: 45628
[startup+280.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 11012 0 0 0 27953 45 0 0 25 0 1 0 423506527 47394816 10797 4294967295 134512640 134672761 3221224528 3221223696 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11571 10797 603 41 0 11530 0
vsize: 46284
[startup+290.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 11152 0 0 0 28952 45 0 0 25 0 1 0 423506527 47931392 10937 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11702 10937 603 41 0 11661 0
vsize: 46808
[startup+300.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 11306 0 0 0 29952 46 0 0 25 0 1 0 423506527 48488448 11091 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11838 11091 603 41 0 11797 0
vsize: 47352
[startup+310.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 11469 0 0 0 30951 47 0 0 25 0 1 0 423506527 49160192 11254 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12002 11254 603 41 0 11961 0
vsize: 48008
[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 11619 0 0 0 31949 48 0 0 25 0 1 0 423506527 49917952 11404 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12187 11404 603 41 0 12146 0
vsize: 48748
[startup+330.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 11854 0 0 0 32948 49 0 0 25 0 1 0 423506527 50868224 11639 4294967295 134512640 134672761 3221224528 3221223664 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12419 11639 603 41 0 12378 0
vsize: 49676
[startup+340.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 12130 0 0 0 33947 51 0 0 25 0 1 0 423506527 52072448 11915 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12713 11915 603 41 0 12672 0
vsize: 50852
[startup+350.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 12345 0 0 0 34946 52 0 0 25 0 1 0 423506527 53444608 12130 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13048 12130 603 41 0 13007 0
vsize: 52192
[startup+360.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 12504 0 0 0 35945 52 0 0 25 0 1 0 423506527 54104064 12289 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13209 12289 603 41 0 13168 0
vsize: 52836
[startup+370.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 12704 0 0 0 36944 53 0 0 25 0 1 0 423506527 54902784 12489 4294967295 134512640 134672761 3221224528 3221223632 134560287 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13404 12489 603 41 0 13363 0
vsize: 53616
[startup+380.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 12791 0 0 0 37944 53 0 0 25 0 1 0 423506527 55332864 12576 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13509 12576 603 41 0 13468 0
vsize: 54036
[startup+390.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 12888 0 0 0 38943 54 0 0 25 0 1 0 423506527 55595008 12673 4294967295 134512640 134672761 3221224528 3221223696 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13573 12673 603 41 0 13532 0
vsize: 54292
[startup+400.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 13019 0 0 0 39942 55 0 0 25 0 1 0 423506527 56123392 12804 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13702 12804 603 41 0 13661 0
vsize: 54808
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 13286 0 0 0 40941 56 0 0 25 0 1 0 423506527 57323520 13071 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13995 13071 603 41 0 13954 0
vsize: 55980
[startup+420.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 13563 0 0 0 41940 57 0 0 25 0 1 0 423506527 58396672 13348 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14257 13348 603 41 0 14216 0
vsize: 57028
[startup+430.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 13845 0 0 0 42939 58 0 0 25 0 1 0 423506527 59596800 13630 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14550 13630 603 41 0 14509 0
vsize: 58200
[startup+440.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14063 0 0 0 43938 59 0 0 25 0 1 0 423506527 60530688 13848 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14778 13848 603 41 0 14737 0
vsize: 59112
[startup+450.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14216 0 0 0 44937 60 0 0 25 0 1 0 423506527 61054976 14001 4294967295 134512640 134672761 3221224528 3221223696 134560808 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14906 14001 603 41 0 14865 0
vsize: 59624
[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14321 0 0 0 45937 60 0 0 25 0 1 0 423506527 61448192 14106 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15002 14106 603 41 0 14961 0
vsize: 60008
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14436 0 0 0 46936 61 0 0 25 0 1 0 423506527 61988864 14221 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15134 14221 603 41 0 15093 0
vsize: 60536
[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14599 0 0 0 47935 61 0 0 25 0 1 0 423506527 62660608 14384 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15298 14384 603 41 0 15257 0
vsize: 61192
[startup+490.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14786 0 0 0 48934 62 0 0 25 0 1 0 423506527 63459328 14571 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15493 14571 603 41 0 15452 0
vsize: 61972
[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14955 0 0 0 49934 63 0 0 25 0 1 0 423506527 64131072 14740 4294967295 134512640 134672761 3221224528 3221223680 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14740 603 41 0 15616 0
vsize: 62628
[startup+510.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14961 0 0 0 50933 64 0 0 25 0 1 0 423506527 64131072 14746 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14746 603 41 0 15616 0
vsize: 62628
[startup+520.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14961 0 0 0 51933 64 0 0 25 0 1 0 423506527 64131072 14746 4294967295 134512640 134672761 3221224528 3221223632 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14746 603 41 0 15616 0
vsize: 62628
[startup+530.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14961 0 0 0 52932 64 0 0 25 0 1 0 423506527 64131072 14746 4294967295 134512640 134672761 3221224528 3221223672 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14746 603 41 0 15616 0
vsize: 62628
[startup+540.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14961 0 0 0 53932 64 0 0 25 0 1 0 423506527 64131072 14746 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14746 603 41 0 15616 0
vsize: 62628
[startup+550.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14962 0 0 0 54932 65 0 0 25 0 1 0 423506527 64131072 14747 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14747 603 41 0 15616 0
vsize: 62628
[startup+560.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14962 0 0 0 55931 65 0 0 25 0 1 0 423506527 64131072 14747 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14747 603 41 0 15616 0
vsize: 62628
[startup+570.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14962 0 0 0 56930 66 0 0 25 0 1 0 423506527 64131072 14747 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14747 603 41 0 15616 0
vsize: 62628
[startup+580.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14962 0 0 0 57930 66 0 0 25 0 1 0 423506527 64131072 14747 4294967295 134512640 134672761 3221224528 3221223632 134559910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14747 603 41 0 15616 0
vsize: 62628
[startup+590.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14962 0 0 0 58929 67 0 0 25 0 1 0 423506527 64131072 14747 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14747 603 41 0 15616 0
vsize: 62628
[startup+600.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14962 0 0 0 59929 67 0 0 25 0 1 0 423506527 64131072 14747 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14747 603 41 0 15616 0
vsize: 62628
[startup+610.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14962 0 0 0 60928 67 0 0 25 0 1 0 423506527 64131072 14747 4294967295 134512640 134672761 3221224528 3221223696 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14747 603 41 0 15616 0
vsize: 62628
[startup+620.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14962 0 0 0 61928 67 0 0 25 0 1 0 423506527 64131072 14747 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14747 603 41 0 15616 0
vsize: 62628
[startup+630.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14962 0 0 0 62928 68 0 0 25 0 1 0 423506527 64131072 14747 4294967295 134512640 134672761 3221224528 3221223712 134559607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14747 603 41 0 15616 0
vsize: 62628
[startup+640.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 14974 0 0 0 63927 68 0 0 25 0 1 0 423506527 64131072 14759 4294967295 134512640 134672761 3221224528 3221223632 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15657 14759 603 41 0 15616 0
vsize: 62628
[startup+650.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15011 0 0 0 64927 69 0 0 25 0 1 0 423506527 64393216 14796 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14796 603 41 0 15680 0
vsize: 62884
[startup+660.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15015 0 0 0 65926 69 0 0 25 0 1 0 423506527 64393216 14800 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14800 603 41 0 15680 0
vsize: 62884
[startup+670.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15016 0 0 0 66927 69 0 0 25 0 1 0 423506527 64393216 14801 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14801 603 41 0 15680 0
vsize: 62884
[startup+680.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15017 0 0 0 67926 69 0 0 25 0 1 0 423506527 64393216 14802 4294967295 134512640 134672761 3221224528 3221223632 134560169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14802 603 41 0 15680 0
vsize: 62884
[startup+690.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15018 0 0 0 68925 70 0 0 25 0 1 0 423506527 64393216 14803 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14803 603 41 0 15680 0
vsize: 62884
[startup+700.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15018 0 0 0 69925 70 0 0 25 0 1 0 423506527 64393216 14803 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14803 603 41 0 15680 0
vsize: 62884
[startup+710.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15018 0 0 0 70925 70 0 0 25 0 1 0 423506527 64393216 14803 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14803 603 41 0 15680 0
vsize: 62884
[startup+720.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15018 0 0 0 71925 71 0 0 25 0 1 0 423506527 64393216 14803 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14803 603 41 0 15680 0
vsize: 62884
[startup+730.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15018 0 0 0 72924 71 0 0 25 0 1 0 423506527 64393216 14803 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14803 603 41 0 15680 0
vsize: 62884
[startup+740.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15019 0 0 0 73924 71 0 0 25 0 1 0 423506527 64393216 14804 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14804 603 41 0 15680 0
vsize: 62884
[startup+750.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15023 0 0 0 74923 72 0 0 25 0 1 0 423506527 64393216 14808 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14808 603 41 0 15680 0
vsize: 62884
[startup+760.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15024 0 0 0 75923 72 0 0 25 0 1 0 423506527 64393216 14809 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14809 603 41 0 15680 0
vsize: 62884
[startup+770.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15025 0 0 0 76923 73 0 0 25 0 1 0 423506527 64393216 14810 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14810 603 41 0 15680 0
vsize: 62884
[startup+780.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15025 0 0 0 77922 73 0 0 25 0 1 0 423506527 64393216 14810 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14810 603 41 0 15680 0
vsize: 62884
[startup+790.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15025 0 0 0 78922 73 0 0 25 0 1 0 423506527 64393216 14810 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14810 603 41 0 15680 0
vsize: 62884
[startup+800.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15026 0 0 0 79922 74 0 0 25 0 1 0 423506527 64393216 14811 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14811 603 41 0 15680 0
vsize: 62884
[startup+810.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15026 0 0 0 80921 74 0 0 25 0 1 0 423506527 64393216 14811 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14811 603 41 0 15680 0
vsize: 62884
[startup+820.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15026 0 0 0 81921 74 0 0 25 0 1 0 423506527 64393216 14811 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14811 603 41 0 15680 0
vsize: 62884
[startup+830.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15027 0 0 0 82921 74 0 0 25 0 1 0 423506527 64393216 14812 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14812 603 41 0 15680 0
vsize: 62884
[startup+840.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15027 0 0 0 83921 74 0 0 25 0 1 0 423506527 64393216 14812 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 14812 603 41 0 15680 0
vsize: 62884
[startup+850.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15032 0 0 0 84921 74 0 0 25 0 1 0 423506527 64393216 14817 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15721 14817 603 41 0 15680 0
vsize: 62884
[startup+860.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15032 0 0 0 85921 74 0 0 25 0 1 0 423506527 64393216 14817 4294967295 134512640 134672761 3221224528 3221223680 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15721 14817 603 41 0 15680 0
vsize: 62884
[startup+870.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15033 0 0 0 86921 74 0 0 25 0 1 0 423506527 64393216 14818 4294967295 134512640 134672761 3221224528 3221223728 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15721 14818 603 41 0 15680 0
vsize: 62884
[startup+880.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15033 0 0 0 87921 74 0 0 25 0 1 0 423506527 64393216 14818 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15721 14818 603 41 0 15680 0
vsize: 62884
[startup+890.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15033 0 0 0 88922 74 0 0 25 0 1 0 423506527 64393216 14818 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15721 14818 603 41 0 15680 0
vsize: 62884
[startup+900.049 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15033 0 0 0 89922 74 0 0 25 0 1 0 423506527 64393216 14818 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15721 14818 603 41 0 15680 0
vsize: 62884
[startup+910.049 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15034 0 0 0 90922 74 0 0 25 0 1 0 423506527 64393216 14819 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15721 14819 603 41 0 15680 0
vsize: 62884
[startup+920.051 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15034 0 0 0 91922 74 0 0 25 0 1 0 423506527 64393216 14819 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15721 14819 603 41 0 15680 0
vsize: 62884
[startup+930.051 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15034 0 0 0 92922 74 0 0 25 0 1 0 423506527 64393216 14819 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15721 14819 603 41 0 15680 0
vsize: 62884
[startup+940.051 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15034 0 0 0 93923 74 0 0 25 0 1 0 423506527 64393216 14819 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15721 14819 603 41 0 15680 0
vsize: 62884
[startup+950.051 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15034 0 0 0 94923 74 0 0 25 0 1 0 423506527 64393216 14819 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15721 14819 603 41 0 15680 0
vsize: 62884
[startup+960.05 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15034 0 0 0 95923 74 0 0 25 0 1 0 423506527 64393216 14819 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15721 14819 603 41 0 15680 0
vsize: 62884
[startup+970.051 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15183 0 0 0 96923 75 0 0 25 0 1 0 423506527 64929792 14968 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15852 14968 603 41 0 15811 0
vsize: 63408
[startup+980.052 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15423 0 0 0 97923 75 0 0 25 0 1 0 423506527 66002944 15208 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16114 15208 603 41 0 16073 0
vsize: 64456
[startup+990.051 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15617 0 0 0 98922 76 0 0 25 0 1 0 423506527 66674688 15402 4294967295 134512640 134672761 3221224528 3221223696 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16278 15402 603 41 0 16237 0
vsize: 65112
[startup+1000.05 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 15830 0 0 0 99921 77 0 0 25 0 1 0 423506527 67600384 15615 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16504 15615 603 41 0 16463 0
vsize: 66016
[startup+1010.05 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 16030 0 0 0 100921 77 0 0 25 0 1 0 423506527 68390912 15815 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16697 15815 603 41 0 16656 0
vsize: 66788
[startup+1020.05 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 16207 0 0 0 101921 78 0 0 25 0 1 0 423506527 69062656 15992 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16861 15992 603 41 0 16820 0
vsize: 67444
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 16405 0 0 0 102920 78 0 0 25 0 1 0 423506527 70000640 16190 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17090 16190 603 41 0 17049 0
vsize: 68360
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 16601 0 0 0 103920 79 0 0 25 0 1 0 423506527 70811648 16386 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17288 16386 603 41 0 17247 0
vsize: 69152
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 16785 0 0 0 104919 80 0 0 25 0 1 0 423506527 71479296 16570 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17451 16570 603 41 0 17410 0
vsize: 69804
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 16976 0 0 0 105919 80 0 0 25 0 1 0 423506527 72286208 16761 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17648 16761 603 41 0 17607 0
vsize: 70592
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 17146 0 0 0 106919 81 0 0 25 0 1 0 423506527 72949760 16931 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17810 16931 603 41 0 17769 0
vsize: 71240
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 17320 0 0 0 107919 81 0 0 25 0 1 0 423506527 73682944 17105 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17989 17105 603 41 0 17948 0
vsize: 71956
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 17497 0 0 0 108919 81 0 0 25 0 1 0 423506527 74481664 17282 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18184 17282 603 41 0 18143 0
vsize: 72736
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 17654 0 0 0 109918 81 0 0 25 0 1 0 423506527 75014144 17439 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18314 17439 603 41 0 18273 0
vsize: 73256
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 17813 0 0 0 110918 82 0 0 25 0 1 0 423506527 75681792 17598 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18477 17598 603 41 0 18436 0
vsize: 73908
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 17975 0 0 0 111918 82 0 0 25 0 1 0 423506527 76382208 17760 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18648 17760 603 41 0 18607 0
vsize: 74592
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 18102 0 0 0 112918 83 0 0 25 0 1 0 423506527 76914688 17887 4294967295 134512640 134672761 3221224528 3221223632 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18778 17887 603 41 0 18737 0
vsize: 75112
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 18102 0 0 0 113918 83 0 0 25 0 1 0 423506527 76914688 17887 4294967295 134512640 134672761 3221224528 3221223632 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18778 17887 603 41 0 18737 0
vsize: 75112
[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 18102 0 0 0 114918 83 0 0 25 0 1 0 423506527 76914688 17887 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18778 17887 603 41 0 18737 0
vsize: 75112
[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 18102 0 0 0 115919 83 0 0 25 0 1 0 423506527 76914688 17887 4294967295 134512640 134672761 3221224528 3221223632 134554665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18778 17887 603 41 0 18737 0
vsize: 75112
[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 18102 0 0 0 116919 83 0 0 25 0 1 0 423506527 76914688 17887 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18778 17887 603 41 0 18737 0
vsize: 75112
[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 18102 0 0 0 117919 83 0 0 25 0 1 0 423506527 76914688 17887 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18778 17887 603 41 0 18737 0
vsize: 75112
[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 18102 0 0 0 118919 83 0 0 25 0 1 0 423506527 76914688 17887 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18778 17887 603 41 0 18737 0
vsize: 75112
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 538
Raw data (stat): 538 (minisat+) R 537 25285 25284 0 -1 0 18102 0 0 0 119919 83 0 0 25 0 1 0 423506527 76914688 17887 4294967295 134512640 134672761 3221224528 3221223696 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18778 17887 603 41 0 18737 0
vsize: 75112
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 538
Raw data (stat): 538 (minisat+) Z 537 25285 25284 0 -1 12 18104 0 0 0 119919 86 0 0 25 0 1 0 423506527 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.09
CPU time (s): 1200.06
CPU user time (s): 1199.2
CPU system time (s): 0.864868
CPU usage (%): 99.9977
Max. virtual memory (Kb): 75112
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####