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 5019

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        910516 kB
Buffers:         34840 kB
Cached:          67328 kB
SwapCached:       2144 kB
Active:          61924 kB
Inactive:        45300 kB
HighTotal:      131008 kB
HighFree:        59640 kB
LowTotal:       903652 kB
LowFree:        850876 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11340 kB
Committed_AS:    63508 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 21:41:05 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 2696 7 1200.19 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      950     9.4 |  8.625 % |
c |       252 |  107830   271051 |   43491     252     2874    11.4 |  8.625 % |
c |       477 |   98949   250807 |   47840     472     5638    11.9 | 15.454 % |
c |       816 |   98949   250807 |   52624     811    15464    19.1 | 15.454 % |
c |      1322 |   98949   250807 |   57886    1317    23186    17.6 | 15.454 % |
c |      2082 |   98949   250807 |   63675    2077    69625    33.5 | 15.454 % |
c |      3223 |   98949   250807 |   70042    3218    86620    26.9 | 15.454 % |
c |      4931 |   98949   250807 |   77047    4926   198675    40.3 | 15.454 % |
c |      7493 |   98949   250807 |   84751    7488   304200    40.6 | 15.454 % |
c |     11339 |   98949   250807 |   93226   11334   369558    32.6 | 15.454 % |
c |     17106 |   98949   250807 |  102549   17101   760759    44.5 | 15.454 % |
c |     25755 |   98949   250807 |  112804   25750  1010223    39.2 | 15.454 % |
c |     38729 |   98949   250807 |  124084   38724  2206873    57.0 | 15.454 % |
c |     58190 |   98949   250807 |  136493   58185  3767180    64.7 | 15.454 % |
c |     87382 |   98949   250807 |  150142   87377  5277825    60.4 | 15.454 % |
c |    131172 |   98949   250807 |  165157  131167  8099880    61.8 | 15.454 % |
c |    196856 |   98949   250807 |  181672   35854  1952372    54.5 | 15.454 % |
c |    295382 |   98949   250807 |  199840  134380  8907817    66.3 | 15.454 % |
#### 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.64 0.85 0.88 2/54 1655
Raw data (stat): 1655 (runsolver) R 1653 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420923441 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.70 0.85 0.88 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 5079 0 0 0 983 14 0 0 25 0 1 0 420923441 22822912 4864 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5572 4864 603 41 0 5531 0
vsize: 22288
[startup+20.001 s]
Raw data (loadavg): 0.74 0.86 0.88 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 5084 0 0 0 1983 14 0 0 25 0 1 0 420923441 22822912 4869 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5572 4869 603 41 0 5531 0
vsize: 22288
[startup+30.0028 s]
Raw data (loadavg): 0.78 0.86 0.88 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 5099 0 0 0 2983 14 0 0 25 0 1 0 420923441 22822912 4884 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5572 4884 603 41 0 5531 0
vsize: 22288
[startup+40.003 s]
Raw data (loadavg): 0.81 0.87 0.88 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 5099 0 0 0 3982 15 0 0 25 0 1 0 420923441 22822912 4884 4294967295 134512640 134672761 3221224624 3221223808 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5572 4884 603 41 0 5531 0
vsize: 22288
[startup+50.0035 s]
Raw data (loadavg): 0.84 0.87 0.88 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 5099 0 0 0 4982 15 0 0 25 0 1 0 420923441 22822912 4884 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5572 4884 603 41 0 5531 0
vsize: 22288
[startup+60.0033 s]
Raw data (loadavg): 0.87 0.87 0.88 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 5283 0 0 0 5982 15 0 0 25 0 1 0 420923441 23498752 5068 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5737 5068 603 41 0 5696 0
vsize: 22948
[startup+70.0034 s]
Raw data (loadavg): 0.89 0.88 0.88 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 5573 0 0 0 6981 16 0 0 25 0 1 0 420923441 24702976 5358 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6031 5358 603 41 0 5990 0
vsize: 24124
[startup+80.0039 s]
Raw data (loadavg): 0.90 0.88 0.88 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 6036 0 0 0 7980 18 0 0 25 0 1 0 420923441 26841088 5821 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6553 5821 603 41 0 6512 0
vsize: 26212
[startup+90.0037 s]
Raw data (loadavg): 0.92 0.88 0.89 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 6557 0 0 0 8979 19 0 0 25 0 1 0 420923441 28876800 6342 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7050 6342 603 41 0 7009 0
vsize: 28200
[startup+100.005 s]
Raw data (loadavg): 0.93 0.89 0.89 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 6811 0 0 0 9979 19 0 0 25 0 1 0 420923441 29945856 6596 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7311 6596 603 41 0 7270 0
vsize: 29244
[startup+110.005 s]
Raw data (loadavg): 0.94 0.89 0.89 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 7140 0 0 0 10978 20 0 0 25 0 1 0 420923441 31277056 6925 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7636 6925 603 41 0 7595 0
vsize: 30544
[startup+120.005 s]
Raw data (loadavg): 0.95 0.89 0.89 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 7457 0 0 0 11978 20 0 0 25 0 1 0 420923441 32608256 7242 4294967295 134512640 134672761 3221224624 3221223728 134560279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7961 7242 603 41 0 7920 0
vsize: 31844
[startup+130.005 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 7705 0 0 0 12977 21 0 0 25 0 1 0 420923441 33685504 7490 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8224 7490 603 41 0 8183 0
vsize: 32896
[startup+140.006 s]
Raw data (loadavg): 0.96 0.90 0.89 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 8126 0 0 0 13976 23 0 0 25 0 1 0 420923441 35414016 7911 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8646 7911 603 41 0 8605 0
vsize: 34584
[startup+150.007 s]
Raw data (loadavg): 0.97 0.90 0.89 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 8437 0 0 0 14976 23 0 0 25 0 1 0 420923441 36605952 8222 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8937 8222 603 41 0 8896 0
vsize: 35748
[startup+160.007 s]
Raw data (loadavg): 0.97 0.91 0.89 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 8782 0 0 0 15975 25 0 0 25 0 1 0 420923441 38199296 8567 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9326 8567 603 41 0 9285 0
vsize: 37304
[startup+170.006 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 9145 0 0 0 16973 26 0 0 25 0 1 0 420923441 39686144 8930 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9689 8930 603 41 0 9648 0
vsize: 38756
[startup+180.007 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 9487 0 0 0 17972 27 0 0 25 0 1 0 420923441 41058304 9272 4294967295 134512640 134672761 3221224624 3221223760 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10024 9272 603 41 0 9983 0
vsize: 40096
[startup+190.007 s]
Raw data (loadavg): 0.98 0.91 0.89 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 9738 0 0 0 18972 28 0 0 25 0 1 0 420923441 42119168 9523 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10283 9523 603 41 0 10242 0
vsize: 41132
[startup+200.008 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 10072 0 0 0 19970 30 0 0 25 0 1 0 420923441 43446272 9857 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10607 9857 603 41 0 10566 0
vsize: 42428
[startup+210.009 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 10376 0 0 0 20968 31 0 0 25 0 1 0 420923441 44806144 10161 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10939 10161 603 41 0 10898 0
vsize: 43756
[startup+220.009 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 10600 0 0 0 21967 32 0 0 25 0 1 0 420923441 45731840 10385 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11165 10385 603 41 0 11124 0
vsize: 44660
[startup+230.009 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 10802 0 0 0 22967 33 0 0 25 0 1 0 420923441 46534656 10587 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11361 10587 603 41 0 11320 0
vsize: 45444
[startup+240.009 s]
Raw data (loadavg): 0.99 0.92 0.90 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 10974 0 0 0 23966 34 0 0 25 0 1 0 420923441 47194112 10759 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11522 10759 603 41 0 11481 0
vsize: 46088
[startup+250.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 11285 0 0 0 24966 34 0 0 25 0 1 0 420923441 48521216 11070 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11846 11070 603 41 0 11805 0
vsize: 47384
[startup+260.011 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 11482 0 0 0 25966 35 0 0 25 0 1 0 420923441 49324032 11267 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12042 11267 603 41 0 12001 0
vsize: 48168
[startup+270.011 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 11726 0 0 0 26965 36 0 0 25 0 1 0 420923441 50274304 11511 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12274 11511 603 41 0 12233 0
vsize: 49096
[startup+280.011 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 11948 0 0 0 27964 37 0 0 25 0 1 0 420923441 51204096 11733 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12501 11733 603 41 0 12460 0
vsize: 50004
[startup+290.01 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 12248 0 0 0 28964 37 0 0 25 0 1 0 420923441 52465664 12033 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12809 12033 603 41 0 12768 0
vsize: 51236
[startup+300.011 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 12568 0 0 0 29963 38 0 0 25 0 1 0 420923441 53661696 12353 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13101 12353 603 41 0 13060 0
vsize: 52404
[startup+310.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 12787 0 0 0 30962 40 0 0 25 0 1 0 420923441 54595584 12572 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13329 12572 603 41 0 13288 0
vsize: 53316
[startup+320.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 12979 0 0 0 31961 40 0 0 25 0 1 0 420923441 55390208 12764 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13523 12764 603 41 0 13482 0
vsize: 54092
[startup+330.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 13137 0 0 0 32961 41 0 0 25 0 1 0 420923441 56057856 12922 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13686 12922 603 41 0 13645 0
vsize: 54744
[startup+340.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 13258 0 0 0 33960 42 0 0 25 0 1 0 420923441 56979456 13043 4294967295 134512640 134672761 3221224624 3221223776 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13911 13043 603 41 0 13870 0
vsize: 55644
[startup+350.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 13452 0 0 0 34958 43 0 0 25 0 1 0 420923441 57782272 13237 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14107 13237 603 41 0 14066 0
vsize: 56428
[startup+360.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 13721 0 0 0 35956 44 0 0 25 0 1 0 420923441 59150336 13506 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14441 13506 603 41 0 14400 0
vsize: 57764
[startup+370.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 13846 0 0 0 36956 45 0 0 25 0 1 0 420923441 59547648 13631 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14538 13631 603 41 0 14497 0
vsize: 58152
[startup+380.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 13968 0 0 0 37956 45 0 0 25 0 1 0 420923441 60076032 13753 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14667 13753 603 41 0 14626 0
vsize: 58668
[startup+390.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 14173 0 0 0 38955 45 0 0 25 0 1 0 420923441 60870656 13958 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14861 13958 603 41 0 14820 0
vsize: 59444
[startup+400.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 14379 0 0 0 39955 46 0 0 25 0 1 0 420923441 61665280 14164 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15055 14164 603 41 0 15014 0
vsize: 60220
[startup+410.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 14532 0 0 0 40955 46 0 0 25 0 1 0 420923441 62332928 14317 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15218 14317 603 41 0 15177 0
vsize: 60872
[startup+420.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 14756 0 0 0 41954 47 0 0 25 0 1 0 420923441 63283200 14541 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15450 14541 603 41 0 15409 0
vsize: 61800
[startup+430.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 14983 0 0 0 42953 49 0 0 25 0 1 0 420923441 64184320 14768 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15670 14768 603 41 0 15629 0
vsize: 62680
[startup+440.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 15147 0 0 0 43953 49 0 0 25 0 1 0 420923441 64843776 14932 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15831 14932 603 41 0 15790 0
vsize: 63324
[startup+450.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 15271 0 0 0 44953 49 0 0 25 0 1 0 420923441 65523712 15056 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15997 15056 603 41 0 15956 0
vsize: 63988
[startup+460.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 15430 0 0 0 45953 49 0 0 25 0 1 0 420923441 66191360 15215 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16160 15215 603 41 0 16119 0
vsize: 64640
[startup+470.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 15590 0 0 0 46953 50 0 0 25 0 1 0 420923441 66727936 15375 4294967295 134512640 134672761 3221224624 3221223728 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16291 15375 603 41 0 16250 0
vsize: 65164
[startup+480.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 15761 0 0 0 47953 50 0 0 25 0 1 0 420923441 67543040 15546 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16490 15546 603 41 0 16449 0
vsize: 65960
[startup+490.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 15881 0 0 0 48953 50 0 0 25 0 1 0 420923441 67940352 15666 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16587 15666 603 41 0 16546 0
vsize: 66348
[startup+500.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16068 0 0 0 49953 50 0 0 25 0 1 0 420923441 68784128 15853 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16793 15853 603 41 0 16752 0
vsize: 67172
[startup+510.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16215 0 0 0 50952 51 0 0 25 0 1 0 420923441 69439488 16000 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16953 16000 603 41 0 16912 0
vsize: 67812
[startup+520.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16405 0 0 0 51952 51 0 0 25 0 1 0 420923441 70361088 16190 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17178 16190 603 41 0 17137 0
vsize: 68712
[startup+530.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16635 0 0 0 52951 52 0 0 25 0 1 0 420923441 71163904 16420 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17374 16420 603 41 0 17333 0
vsize: 69496
[startup+540.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16843 0 0 0 53950 53 0 0 25 0 1 0 420923441 72085504 16628 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16628 603 41 0 17558 0
vsize: 70396
[startup+550.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16861 0 0 0 54951 53 0 0 25 0 1 0 420923441 72085504 16646 4294967295 134512640 134672761 3221224624 3221223728 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16646 603 41 0 17558 0
vsize: 70396
[startup+560.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16861 0 0 0 55951 53 0 0 25 0 1 0 420923441 72085504 16646 4294967295 134512640 134672761 3221224624 3221223728 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16646 603 41 0 17558 0
vsize: 70396
[startup+570.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16861 0 0 0 56951 53 0 0 25 0 1 0 420923441 72085504 16646 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16646 603 41 0 17558 0
vsize: 70396
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16861 0 0 0 57951 53 0 0 25 0 1 0 420923441 72085504 16646 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16646 603 41 0 17558 0
vsize: 70396
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16861 0 0 0 58952 53 0 0 25 0 1 0 420923441 72085504 16646 4294967295 134512640 134672761 3221224624 3221223760 134560652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16646 603 41 0 17558 0
vsize: 70396
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16861 0 0 0 59952 53 0 0 25 0 1 0 420923441 72085504 16646 4294967295 134512640 134672761 3221224624 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16646 603 41 0 17558 0
vsize: 70396
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16861 0 0 0 60952 53 0 0 25 0 1 0 420923441 72085504 16646 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17599 16646 603 41 0 17558 0
vsize: 70396
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16861 0 0 0 61952 53 0 0 25 0 1 0 420923441 72085504 16646 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16646 603 41 0 17558 0
vsize: 70396
[startup+630.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16862 0 0 0 62952 53 0 0 25 0 1 0 420923441 72085504 16647 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16647 603 41 0 17558 0
vsize: 70396
[startup+640.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16862 0 0 0 63952 53 0 0 25 0 1 0 420923441 72085504 16647 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16647 603 41 0 17558 0
vsize: 70396
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16862 0 0 0 64952 53 0 0 25 0 1 0 420923441 72085504 16647 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16647 603 41 0 17558 0
vsize: 70396
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16862 0 0 0 65952 53 0 0 25 0 1 0 420923441 72085504 16647 4294967295 134512640 134672761 3221224624 3221223808 134559324 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16647 603 41 0 17558 0
vsize: 70396
[startup+670.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16863 0 0 0 66952 53 0 0 25 0 1 0 420923441 72085504 16648 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16648 603 41 0 17558 0
vsize: 70396
[startup+680.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16863 0 0 0 67953 53 0 0 25 0 1 0 420923441 72085504 16648 4294967295 134512640 134672761 3221224624 3221223728 134560231 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16648 603 41 0 17558 0
vsize: 70396
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16863 0 0 0 68953 53 0 0 25 0 1 0 420923441 72085504 16648 4294967295 134512640 134672761 3221224624 3221223728 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16648 603 41 0 17558 0
vsize: 70396
[startup+700.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16863 0 0 0 69953 53 0 0 25 0 1 0 420923441 72085504 16648 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16648 603 41 0 17558 0
vsize: 70396
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16863 0 0 0 70953 53 0 0 25 0 1 0 420923441 72085504 16648 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16648 603 41 0 17558 0
vsize: 70396
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16865 0 0 0 71953 53 0 0 25 0 1 0 420923441 72085504 16650 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16650 603 41 0 17558 0
vsize: 70396
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16865 0 0 0 72954 53 0 0 25 0 1 0 420923441 72085504 16650 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16650 603 41 0 17558 0
vsize: 70396
[startup+740.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16865 0 0 0 73954 53 0 0 25 0 1 0 420923441 72085504 16650 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16650 603 41 0 17558 0
vsize: 70396
[startup+750.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16865 0 0 0 74954 53 0 0 25 0 1 0 420923441 72085504 16650 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16650 603 41 0 17558 0
vsize: 70396
[startup+760.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16865 0 0 0 75954 53 0 0 25 0 1 0 420923441 72085504 16650 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16650 603 41 0 17558 0
vsize: 70396
[startup+770.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16865 0 0 0 76954 53 0 0 25 0 1 0 420923441 72085504 16650 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16650 603 41 0 17558 0
vsize: 70396
[startup+780.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16865 0 0 0 77954 53 0 0 25 0 1 0 420923441 72085504 16650 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16650 603 41 0 17558 0
vsize: 70396
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16865 0 0 0 78955 53 0 0 25 0 1 0 420923441 72085504 16650 4294967295 134512640 134672761 3221224624 3221223760 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16650 603 41 0 17558 0
vsize: 70396
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16865 0 0 0 79955 53 0 0 25 0 1 0 420923441 72085504 16650 4294967295 134512640 134672761 3221224624 3221223728 134560424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16650 603 41 0 17558 0
vsize: 70396
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16865 0 0 0 80955 53 0 0 25 0 1 0 420923441 72085504 16650 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16650 603 41 0 17558 0
vsize: 70396
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16865 0 0 0 81955 53 0 0 25 0 1 0 420923441 72085504 16650 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16650 603 41 0 17558 0
vsize: 70396
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16865 0 0 0 82955 53 0 0 25 0 1 0 420923441 72085504 16650 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16650 603 41 0 17558 0
vsize: 70396
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16867 0 0 0 83955 53 0 0 25 0 1 0 420923441 72085504 16652 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16652 603 41 0 17558 0
vsize: 70396
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16867 0 0 0 84956 53 0 0 25 0 1 0 420923441 72085504 16652 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16652 603 41 0 17558 0
vsize: 70396
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16867 0 0 0 85956 53 0 0 25 0 1 0 420923441 72085504 16652 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16652 603 41 0 17558 0
vsize: 70396
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16868 0 0 0 86956 53 0 0 25 0 1 0 420923441 72085504 16653 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16653 603 41 0 17558 0
vsize: 70396
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16868 0 0 0 87956 53 0 0 25 0 1 0 420923441 72085504 16653 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16653 603 41 0 17558 0
vsize: 70396
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16869 0 0 0 88956 53 0 0 25 0 1 0 420923441 72085504 16654 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17599 16654 603 41 0 17558 0
vsize: 70396
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16906 0 0 0 89956 53 0 0 25 0 1 0 420923441 72347648 16691 4294967295 134512640 134672761 3221224624 3221223808 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17663 16691 603 41 0 17622 0
vsize: 70652
[startup+910.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16907 0 0 0 90955 53 0 0 25 0 1 0 420923441 72347648 16692 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17663 16692 603 41 0 17622 0
vsize: 70652
[startup+920.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16907 0 0 0 91956 53 0 0 25 0 1 0 420923441 72347648 16692 4294967295 134512640 134672761 3221224624 3221223728 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17663 16692 603 41 0 17622 0
vsize: 70652
[startup+930.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16908 0 0 0 92956 53 0 0 25 0 1 0 420923441 72347648 16693 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17663 16693 603 41 0 17622 0
vsize: 70652
[startup+940.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16908 0 0 0 93956 53 0 0 25 0 1 0 420923441 72347648 16693 4294967295 134512640 134672761 3221224624 3221223728 134560254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17663 16693 603 41 0 17622 0
vsize: 70652
[startup+950.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16908 0 0 0 94956 53 0 0 25 0 1 0 420923441 72347648 16693 4294967295 134512640 134672761 3221224624 3221223728 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17663 16693 603 41 0 17622 0
vsize: 70652
[startup+960.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16908 0 0 0 95956 53 0 0 25 0 1 0 420923441 72347648 16693 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17663 16693 603 41 0 17622 0
vsize: 70652
[startup+970.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16909 0 0 0 96956 53 0 0 25 0 1 0 420923441 72347648 16694 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17663 16694 603 41 0 17622 0
vsize: 70652
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16909 0 0 0 97957 53 0 0 25 0 1 0 420923441 72347648 16694 4294967295 134512640 134672761 3221224624 3221223728 134560352 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17663 16694 603 41 0 17622 0
vsize: 70652
[startup+990.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16925 0 0 0 98957 53 0 0 25 0 1 0 420923441 72347648 16710 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17663 16710 603 41 0 17622 0
vsize: 70652
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16929 0 0 0 99957 53 0 0 25 0 1 0 420923441 72347648 16714 4294967295 134512640 134672761 3221224624 3221223728 134559976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17663 16714 603 41 0 17622 0
vsize: 70652
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 16930 0 0 0 100957 53 0 0 25 0 1 0 420923441 72347648 16715 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17663 16715 603 41 0 17622 0
vsize: 70652
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 17075 0 0 0 101957 54 0 0 25 0 1 0 420923441 73019392 16860 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17827 16860 603 41 0 17786 0
vsize: 71308
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 17241 0 0 0 102956 55 0 0 25 0 1 0 420923441 73682944 17026 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17989 17026 603 41 0 17948 0
vsize: 71956
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 17386 0 0 0 103955 55 0 0 25 0 1 0 420923441 74219520 17171 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18120 17171 603 41 0 18079 0
vsize: 72480
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 17550 0 0 0 104955 56 0 0 25 0 1 0 420923441 74883072 17335 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18282 17335 603 41 0 18241 0
vsize: 73128
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 17778 0 0 0 105954 57 0 0 25 0 1 0 420923441 75821056 17563 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18511 17563 603 41 0 18470 0
vsize: 74044
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 18018 0 0 0 106954 58 0 0 25 0 1 0 420923441 76759040 17803 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18740 17803 603 41 0 18699 0
vsize: 74960
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 18228 0 0 0 107953 58 0 0 25 0 1 0 420923441 77819904 18013 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18999 18013 603 41 0 18958 0
vsize: 75996
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 18320 0 0 0 108953 58 0 0 25 0 1 0 420923441 78086144 18105 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19064 18105 603 41 0 19023 0
vsize: 76256
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 18531 0 0 0 109953 59 0 0 25 0 1 0 420923441 79015936 18316 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19291 18316 603 41 0 19250 0
vsize: 77164
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 18750 0 0 0 110953 59 0 0 25 0 1 0 420923441 79810560 18535 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19485 18535 603 41 0 19444 0
vsize: 77940
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 18893 0 0 0 111953 60 0 0 25 0 1 0 420923441 80465920 18678 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19645 18678 603 41 0 19604 0
vsize: 78580
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 18997 0 0 0 112952 60 0 0 25 0 1 0 420923441 80863232 18782 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19742 18783 603 41 0 19701 0
vsize: 78968
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 19156 0 0 0 113952 61 0 0 25 0 1 0 420923441 81764352 18941 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19962 18941 603 41 0 19921 0
vsize: 79848
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 19231 0 0 0 114952 61 0 0 25 0 1 0 420923441 82030592 19016 4294967295 134512640 134672761 3221224624 3221223728 134560350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20027 19016 603 41 0 19986 0
vsize: 80108
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 19439 0 0 0 115952 61 0 0 25 0 1 0 420923441 82821120 19224 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20220 19224 603 41 0 20179 0
vsize: 80880
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 19647 0 0 0 116951 62 0 0 25 0 1 0 420923441 83755008 19432 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20448 19432 603 41 0 20407 0
vsize: 81792
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 19834 0 0 0 117951 62 0 0 25 0 1 0 420923441 84422656 19619 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20611 19619 603 41 0 20570 0
vsize: 82444
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 20019 0 0 0 118951 63 0 0 25 0 1 0 420923441 85225472 19804 4294967295 134512640 134672761 3221224624 3221223792 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20807 19804 603 41 0 20766 0
vsize: 83228
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1655
Raw data (stat): 1655 (minisat+) R 1653 29151 29150 0 -1 0 20175 0 0 0 119950 63 0 0 25 0 1 0 420923441 85757952 19960 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20937 19960 603 41 0 20896 0
vsize: 83748
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 1655
Raw data (stat): 1655 (minisat+) Z 1653 29151 29150 0 -1 12 20177 0 0 0 119950 67 0 0 25 0 1 0 420923441 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.19
CPU user time (s): 1199.51
CPU system time (s): 0.676897
CPU usage (%): 100.01
Max. virtual memory (Kb): 83748
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####