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/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-sp97ar.opb
MD5SUM	978e3479aff123296d0a3461e698e01d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	14101
Biggest coefficient in the objective function	292878668
Number of bits for the biggest coefficient in the objective function	29
Sum of the numbers in the objective function	975388850291
Number of bits of the sum of numbers in the objective function	40
Biggest number in a constraint	292878668
Number of bits of the biggest number in a constraint	29
Biggest sum of numbers in a constraint	975388850291
Number of bits of the biggest sum of numbers	40
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	10.9833
Number of variables	14101
Total number of constraints	15862
Number of constraints which are clauses	181
Number of constraints which are cardinality constraints (but not clauses)	15263
Number of constraints which are nor clauses,nor cardinality constraints	418
Minimum length of a constraint	1
Maximum length of a constraint	2463
Trace number 14172

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-20 23:24:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20240 boxname=wulflinc8 idbench=1557 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  978e3479aff123296d0a3461e698e01d  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-sp97ar.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-sp97ar.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-13-7-sp97ar.opb
IDLAUNCH: 20240
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        652448 kB
Buffers:         33812 kB
Cached:         325024 kB
SwapCached:          0 kB
Active:         122152 kB
Inactive:       239564 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        652196 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14872 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:27:25 (client local time) WITH STATUS 1 IN 182.665 SECONDS
stats: 20240 7 182.665 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1739 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ===========
c   -- Clauses(.)/Splits(s): s...s.ssssssss.ss........ss...ssss..ss.s..ss.s..s..ssssssssssss...s.s.ss.s.s..s.s..s..s...sss.ss.s...s.s.s..ssss..s.ss.s..ss.s.s......sss..ss.ss...sssss.s..ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.ssssssssss.ssssssssssssssss.ssss..sss..s..s...sss...s.s..ssssss.ss.ssss.sss...s....ssssssss..s.ss....sssssss.s.sssssssssssssss.ss.ss.ssss.s..sssssssssss..ss.ssssss.sss.sss..ss..s...ss.s.ss.sss.ssssss...ss.sssssssss.sss.ss.ss.s.sssssssss.ssss..ss..s.ssss.s.s.....ssss...s.s..sssss.ss....s...s.
c ---[2139]---> BDD-cost:   19
c ---[2138]---> BDD-cost:   27
c ---[2137]---> BDD-cost:   27
c ---[2136]---> BDD-cost:   27
c ---[2135]---> BDD-cost:   25
c ---[2134]---> BDD-cost:   25
c ---[2133]---> BDD-cost:    3
c ---[2132]---> BDD-cost:   19
c ---[2130]---> BDD-cost:    3
c ---[2127]---> BDD-cost:    7
c ---[2126]---> BDD-cost:   11
c ---[2125]---> BDD-cost:   19
c ---[2124]---> BDD-cost:   11
c ---[2123]---> BDD-cost:   19
c ---[2122]---> BDD-cost:    9
c ---[2121]---> BDD-cost:   11
c ---[2120]---> BDD-cost:    7
c ---[2119]---> BDD-cost:    7
c ---[2117]---> BDD-cost:   31
c ---[2116]---> BDD-cost:   31
c ---[2115]---> BDD-cost:   21
c ---[2114]---> BDD-cost:   23
c ---[2113]---> BDD-cost:   19
c ---[2112]---> BDD-cost:   19
c ---[2111]---> BDD-cost:   27
c ---[2110]---> BDD-cost:   33
c ---[2109]---> BDD-cost:   29
c ---[2108]---> BDD-cost:   27
c ---[2106]---> BDD-cost:    7
c ---[2105]---> BDD-cost:   27
c ---[2104]---> BDD-cost:   33
c ---[2103]---> BDD-cost:   37
c ---[2102]---> BDD-cost:   37
c ---[2101]---> BDD-cost:   37
c ---[2100]---> BDD-cost:   37
c ---[2099]---> BDD-cost:   37
c ---[2098]---> BDD-cost:    7
c ---[2097]---> BDD-cost:   19
c ---[2095]---> BDD-cost:    9
c ---[2094]---> BDD-cost:    7
c ---[2093]---> BDD-cost:    5
c ---[2092]---> BDD-cost:   19
c ---[2091]---> BDD-cost:   23
c ---[2090]---> BDD-cost:    3
c ---[2089]---> BDD-cost:   27
c ---[2088]---> BDD-cost:   27
c ---[2087]---> BDD-cost:   29
c ---[2086]---> BDD-cost:   19
c ---[2084]---> BDD-cost:   19
c ---[2083]---> BDD-cost:   19
c ---[2082]---> BDD-cost:   31
c ---[2081]---> BDD-cost:   37
c ---[2080]---> BDD-cost:   31
c ---[2079]---> BDD-cost:   37
c ---[2078]---> BDD-cost:   11
c ---[2077]---> BDD-cost:   13
c ---[2076]---> BDD-cost:   13
c ---[2075]---> BDD-cost:   37
c ---[2073]---> BDD-cost:   37
c ---[2072]---> BDD-cost:   37
c ---[2071]---> BDD-cost:   37
c ---[2070]---> BDD-cost:   31
c ---[2069]---> BDD-cost:   37
c ---[2068]---> BDD-cost:   31
c ---[2067]---> BDD-cost:   37
c ---[2066]---> BDD-cost:   19
c ---[2065]---> BDD-cost:   19
c ---[2064]---> BDD-cost:    7
c ---[2062]---> BDD-cost:   11
c ---[2061]---> BDD-cost:   27
c ---[2060]---> BDD-cost:   31
c ---[2059]---> BDD-cost:   37
c ---[2058]---> BDD-cost:   27
c ---[2057]---> BDD-cost:   37
c ---[2056]---> BDD-cost:   29
c ---[2055]---> BDD-cost:    7
c ---[2054]---> BDD-cost:    7
c ---[2053]---> BDD-cost:    7
c ---[2051]---> BDD-cost:    7
c ---[2050]---> BDD-cost:   27
c ---[2049]---> BDD-cost:   27
c ---[2048]---> BDD-cost:   37
c ---[2047]---> BDD-cost:   11
c ---[2046]---> BDD-cost:   37
c ---[2045]---> BDD-cost:    7
c ---[2044]---> BDD-cost:   11
c ---[2043]---> BDD-cost:   23
c ---[2042]---> BDD-cost:   29
c ---[2040]---> BDD-cost:   37
c ---[2039]---> BDD-cost:   29
c ---[2038]---> BDD-cost:    7
c ---[2037]---> BDD-cost:   29
c ---[2036]---> BDD-cost:   37
c ---[2035]---> BDD-cost:   19
c ---[2034]---> BDD-cost:   29
c ---[2033]---> BDD-cost:   37
c ---[2032]---> BDD-cost:   27
c ---[2031]---> BDD-cost:    9
c ---[2028]---> BDD-cost:   27
c ---[2027]---> BDD-cost:   27
c ---[2026]---> BDD-cost:   21
c ---[2025]---> BDD-cost:    9
c ---[2024]---> BDD-cost:   11
c ---[2023]---> BDD-cost:   29
c ---[2022]---> BDD-cost:   37
c ---[2021]---> BDD-cost:   37
c ---[2020]---> BDD-cost:   37
c ---[2019]---> BDD-cost:   37
c ---[2017]---> BDD-cost:   37
c ---[2016]---> BDD-cost:   27
c ---[2015]---> BDD-cost:   19
c ---[2014]---> BDD-cost:   27
c ---[2013]---> BDD-cost:   27
c ---[2012]---> BDD-cost:   37
c ---[2011]---> BDD-cost:   25
c ---[2010]---> BDD-cost:    9
c ---[2009]---> BDD-cost:   19
c ---[2008]---> BDD-cost:    9
c ---[2006]---> BDD-cost:    9
c ---[2005]---> BDD-cost:    9
c ---[2004]---> BDD-cost:    7
c ---[2003]---> BDD-cost:    5
c ---[2002]---> BDD-cost:   19
c ---[2001]---> BDD-cost:    3
c ---[2000]---> BDD-cost:    5
c ---[1999]---> BDD-cost:   19
c ---[1998]---> BDD-cost:   19
c ---[1997]---> BDD-cost:   27
c ---[1994]---> BDD-cost:   27
c ---[1993]---> BDD-cost:   27
c ---[1991]---> BDD-cost:    7
c ---[1990]---> BDD-cost:    3
c ---[1989]---> BDD-cost:    9
c ---[1988]---> BDD-cost:    7
c ---[1985]---> BDD-cost:    9
c ---[1984]---> BDD-cost:   27
c ---[1983]---> BDD-cost:   25
c ---[1982]---> BDD-cost:   27
c ---[1981]---> BDD-cost:   27
c ---[1979]---> BDD-cost:    3
c ---[1977]---> BDD-cost:    9
c ---[1976]---> BDD-cost:    9
c ---[1975]---> BDD-cost:   23
c ---[1974]---> BDD-cost:   19
c ---[1973]---> BDD-cost:   19
c ---[1972]---> BDD-cost:   19
c ---[1971]---> BDD-cost:   23
c ---[1970]---> BDD-cost:   37
c ---[1969]---> BDD-cost:   27
c ---[1968]---> BDD-cost:   19
c ---[1966]---> BDD-cost:   19
c ---[1965]---> BDD-cost:   19
c ---[1964]---> BDD-cost:   37
c ---[1963]---> BDD-cost:   19
c ---[1962]---> BDD-cost:   19
c ---[1961]---> BDD-cost:   23
c ---[1960]---> BDD-cost:   23
c ---[1959]---> BDD-cost:   23
c ---[1958]---> BDD-cost:   19
c ---[1957]---> BDD-cost:   23
c ---[1955]---> BDD-cost:    7
c ---[1953]---> BDD-cost:    5
c ---[1952]---> BDD-cost:    5
c ---[1951]---> BDD-cost:    7
c ---[1949]---> BDD-cost:    5
c ---[1947]---> BDD-cost:    5
c ---[1946]---> BDD-cost:   27
c ---[1944]---> BDD-cost:   27
c ---[1943]---> BDD-cost:   19
c ---[1942]---> BDD-cost:   19
c ---[1941]---> BDD-cost:   19
c ---[1940]---> BDD-cost:   19
c ---[1939]---> BDD-cost:   19
c ---[1938]---> BDD-cost:    7
c ---[1937]---> BDD-cost:   19
c ---[1936]---> BDD-cost:   27
c ---[1935]---> BDD-cost:    7
c ---[1933]---> BDD-cost:    7
c ---[1932]---> BDD-cost:   27
c ---[1931]---> BDD-cost:   27
c ---[1930]---> BDD-cost:    7
c ---[1929]---> BDD-cost:    7
c ---[1928]---> BDD-cost:   19
c ---[1927]---> BDD-cost:    7
c ---[1926]---> BDD-cost:   19
c ---[1925]---> BDD-cost:    7
c ---[1924]---> BDD-cost:    7
c ---[1921]---> BDD-cost:   19
c ---[1920]---> BDD-cost:   19
c ---[1919]---> BDD-cost:   19
c ---[1918]---> BDD-cost:   19
c ---[1917]---> BDD-cost:   31
c ---[1916]---> BDD-cost:   19
c ---[1915]---> BDD-cost:   19
c ---[1914]---> BDD-cost:    7
c ---[1913]---> BDD-cost:   19
c ---[1912]---> BDD-cost:   19
c ---[1910]---> BDD-cost:   19
c ---[1909]---> BDD-cost:   27
c ---[1908]---> BDD-cost:   27
c ---[1907]---> BDD-cost:    7
c ---[1906]---> BDD-cost:    7
c ---[1905]---> BDD-cost:    7
c ---[1904]---> BDD-cost:   27
c ---[1903]---> BDD-cost:    7
c ---[1902]---> BDD-cost:   19
c ---[1901]---> BDD-cost:   37
c ---[1899]---> BDD-cost:   27
c ---[1898]---> BDD-cost:   19
c ---[1897]---> BDD-cost:    7
c ---[1896]---> BDD-cost:   37
c ---[1895]---> BDD-cost:   37
c ---[1894]---> BDD-cost:   37
c ---[1893]---> BDD-cost:   19
c ---[1892]---> BDD-cost:   27
c ---[1891]---> BDD-cost:   33
c ---[1890]---> BDD-cost:   37
c ---[1888]---> BDD-cost:    7
c ---[1887]---> BDD-cost:    7
c ---[1886]---> BDD-cost:    9
c ---[1885]---> BDD-cost:    3
c ---[1884]---> BDD-cost:    3
c ---[1883]---> BDD-cost:    7
c ---[1882]---> BDD-cost:    7
c ---[1881]---> BDD-cost: 1710
c ---[1880]---> BDD-cost:   11
c ---[1879]---> BDD-cost:    7
c ---[1878]---> BDD-cost:    7
c ---[1877]---> BDD-cost:    7
c ---[1876]---> BDD-cost:   27
c ---[1875]---> BDD-cost:    7
c ---[1874]---> BDD-cost:    7
c ---[1873]---> BDD-cost:    3
c ---[1872]---> BDD-cost:    3
c ---[1870]---> BDD-cost:    7
c ---[1869]---> BDD-cost:    7
c ---[1868]---> BDD-cost:    5
c ---[1867]---> BDD-cost:    7
c ---[1866]---> BDD-cost:    7
c ---[1865]---> BDD-cost:    3
c ---[1864]---> BDD-cost:   19
c ---[1863]---> BDD-cost:   13
c ---[1862]---> BDD-cost:   19
c ---[1861]---> BDD-cost:   31
c ---[1859]---> BDD-cost:   37
c ---[1858]---> BDD-cost:   13
c ---[1857]---> BDD-cost:   37
c ---[1856]---> BDD-cost:   27
c ---[1855]---> BDD-cost:   27
c ---[1854]---> BDD-cost:   19
c ---[1853]---> BDD-cost:   31
c ---[1852]---> BDD-cost:   37
c ---[1851]---> BDD-cost:   15
c ---[1850]---> BDD-cost:   37
c ---[1848]---> BDD-cost:   19
c ---[1847]---> BDD-cost:   27
c ---[1846]---> BDD-cost:   19
c ---[1845]---> BDD-cost:   19
c ---[1844]---> BDD-cost:   19
c ---[1843]---> BDD-cost:   29
c ---[1842]---> BDD-cost:   37
c ---[1841]---> BDD-cost:   19
c ---[1840]---> BDD-cost:   15
c ---[1839]---> BDD-cost:   37
c ---[1837]---> BDD-cost:   27
c ---[1836]---> BDD-cost:   27
c ---[1835]---> BDD-cost:   19
c ---[1834]---> BDD-cost:   27
c ---[1833]---> BDD-cost:   31
c ---[1832]---> BDD-cost:   37
c ---[1831]---> BDD-cost:   17
c ---[1830]---> BDD-cost:   37
c ---[1829]---> BDD-cost:   15
c ---[1828]---> BDD-cost:   27
c ---[1826]---> BDD-cost:   27
c ---[1825]---> BDD-cost:   27
c ---[1824]---> BDD-cost:   27
c ---[1823]---> BDD-cost:   37
c ---[1822]---> BDD-cost:   27
c ---[1821]---> BDD-cost:    3
c ---[1820]---> BDD-cost:   27
c ---[1819]---> BDD-cost:    7
c ---[1818]---> BDD-cost:    9
c ---[1817]---> BDD-cost:    5
c ---[1814]---> BDD-cost:   11
c ---[1813]---> BDD-cost:   29
c ---[1812]---> BDD-cost:   27
c ---[1811]---> BDD-cost:   23
c ---[1810]---> BDD-cost:   19
c ---[1809]---> BDD-cost:   27
c ---[1808]---> BDD-cost:   27
c ---[1806]---> BDD-cost:    3
c ---[1805]---> BDD-cost:    9
c ---[1802]---> BDD-cost:    5
c ---[1801]---> BDD-cost:    5
c ---[1800]---> BDD-cost:    3
c ---[1799]---> BDD-cost:    3
c ---[1798]---> BDD-cost:    9
c ---[1797]---> BDD-cost:    3
c ---[1796]---> BDD-cost:    9
c ---[1795]---> BDD-cost:    9
c ---[1791]---> BDD-cost:    9
c ---[1790]---> BDD-cost:   11
c ---[1789]---> BDD-cost:    3
c ---[1788]---> BDD-cost:   13
c ---[1786]---> BDD-cost:   13
c ---[1785]---> BDD-cost:    9
c ---[1784]---> BDD-cost:   37
c ---[1783]---> BDD-cost:   37
c ---[1781]---> BDD-cost:   31
c ---[1780]---> BDD-cost:    5
c ---[1779]---> BDD-cost:    7
c ---[1778]---> BDD-cost:    9
c ---[1777]---> BDD-cost:   11
c ---[1776]---> BDD-cost:   11
c ---[1775]---> BDD-cost:   29
c ---[1774]---> BDD-cost:   21
c ---[1773]---> BDD-cost:   37
c ---[1772]---> BDD-cost:   27
c ---[1770]---> BDD-cost:   37
c ---[1769]---> BDD-cost:   29
c ---[1768]---> BDD-cost:    5
c ---[1767]---> BDD-cost:    7
c ---[1766]---> BDD-cost:    9
c ---[1765]---> BDD-cost:   11
c ---[1764]---> BDD-cost:   11
c ---[1763]---> BDD-cost:   31
c ---[1762]---> BDD-cost:   21
c ---[1761]---> BDD-cost:   11
c ---[1759]---> BDD-cost:   29
c ---[1758]---> BDD-cost:   29
c ---[1757]---> BDD-cost:   11
c ---[1756]---> BDD-cost:   31
c ---[1755]---> BDD-cost:   27
c ---[1754]---> BDD-cost:   37
c ---[1753]---> BDD-cost:   35
c ---[1752]---> BDD-cost:   19
c ---[1751]---> BDD-cost:   31
c ---[1750]---> BDD-cost:   15
c ---[1748]---> BDD-cost:   31
c ---[1747]---> BDD-cost:   31
c ---[1746]---> BDD-cost:   31
c ---[1745]---> BDD-cost:   15
c ---[1744]---> BDD-cost:   27
c ---[1743]---> BDD-cost:   27
c ---[1742]---> BDD-cost:   29
c ---[1741]---> BDD-cost:   15
c ---[1740]---> BDD-cost:   19
c ---[1739]---> BDD-cost:   29
c ---[1737]---> BDD-cost:   19
c ---[1736]---> BDD-cost:   37
c ---[1735]---> BDD-cost:   37
c ---[1734]---> BDD-cost:   35
c ---[1733]---> BDD-cost:   29
c ---[1732]---> BDD-cost:   37
c ---[1731]---> BDD-cost:   29
c ---[1730]---> BDD-cost:   19
c ---[1729]---> BDD-cost:   37
c ---[1728]---> BDD-cost:   27
c ---[1726]---> BDD-cost:   19
c ---[1725]---> BDD-cost:   29
c ---[1724]---> BDD-cost:   27
c ---[1723]---> BDD-cost:   19
c ---[1722]---> BDD-cost:   31
c ---[1721]---> BDD-cost:   31
c ---[1720]---> BDD-cost:   29
c ---[1719]---> BDD-cost:   15
c ---[1718]---> BDD-cost:   25
c ---[1717]---> BDD-cost:    7
c ---[1715]---> BDD-cost:   19
c ---[1714]---> BDD-cost:    3
c ---[1713]---> BDD-cost:   27
c ---[1712]---> BDD-cost:   27
c ---[1711]---> BDD-cost:   31
c ---[1710]---> BDD-cost:   29
c ---[1709]---> BDD-cost:   31
c ---[1708]---> BDD-cost:   29
c ---[1707]---> BDD-cost:    7
c ---[1706]---> BDD-cost:   27
c ---[1703]---> BDD-cost:   19
c ---[1702]---> BDD-cost:   11
c ---[1701]---> BDD-cost:   27
c ---[1700]---> BDD-cost:   19
c ---[1699]---> BDD-cost:   37
c ---[1698]---> BDD-cost:   29
c ---[1697]---> BDD-cost:   31
c ---[1696]---> BDD-cost:   19
c ---[1695]---> BDD-cost:   19
c ---[1694]---> BDD-cost:   37
c ---[1692]---> BDD-cost:   21
c ---[1691]---> BDD-cost:   37
c ---[1690]---> BDD-cost:   27
c ---[1689]---> BDD-cost:   27
c ---[1688]---> BDD-cost:   19
c ---[1687]---> BDD-cost:   19
c ---[1686]---> BDD-cost:   31
c ---[1685]---> BDD-cost:   31
c ---[1684]---> BDD-cost:   19
c ---[1683]---> BDD-cost:   13
c ---[1681]---> BDD-cost:    7
c ---[1680]---> BDD-cost:   11
c ---[1679]---> BDD-cost:    5
c ---[1678]---> BDD-cost:    7
c ---[1677]---> BDD-cost:    7
c ---[1676]---> BDD-cost:    7
c ---[1675]---> BDD-cost:   27
c ---[1674]---> BDD-cost:   27
c ---[1673]---> BDD-cost:    7
c ---[1672]---> BDD-cost:    7
c ---[1670]---> BDD-cost:    7
c ---[1669]---> BDD-cost:    7
c ---[1668]---> BDD-cost:    3
c ---[1667]---> BDD-cost:    7
c ---[1666]---> BDD-cost:    7
c ---[1664]---> BDD-cost:    3
c ---[1663]---> BDD-cost:    9
c ---[1662]---> BDD-cost:    9
c ---[1660]---> BDD-cost:    9
c ---[1659]---> BDD-cost:   29
c ---[1658]---> BDD-cost:   29
c ---[1657]---> BDD-cost:   31
c ---[1656]---> BDD-cost:   31
c ---[1655]---> BDD-cost:   37
c ---[1654]---> BDD-cost:   37
c ---[1653]---> BDD-cost:   31
c ---[1652]---> BDD-cost:   25
c ---[1651]---> BDD-cost:   25
c ---[1649]---> BDD-cost:   33
c ---[1648]---> BDD-cost:   37
c ---[1647]---> BDD-cost:   31
c ---[1646]---> BDD-cost:   29
c ---[1645]---> BDD-cost:   29
c ---[1644]---> BDD-cost:   37
c ---[1643]---> BDD-cost:   31
c ---[1642]---> BDD-cost:   37
c ---[1641]---> BDD-cost:   15
c ---[1640]---> BDD-cost:   31
c ---[1638]---> BDD-cost:   37
c ---[1637]---> BDD-cost:   29
c ---[1636]---> BDD-cost:   29
c ---[1635]---> BDD-cost:   37
c ---[1634]---> BDD-cost:   29
c ---[1633]---> BDD-cost:   25
c ---[1632]---> BDD-cost:   31
c ---[1631]---> BDD-cost:   37
c ---[1629]---> BDD-cost:    9
c ---[1626]---> BDD-cost:   37
c ---[1625]---> BDD-cost:   25
c ---[1624]---> BDD-cost:   37
c ---[1623]---> BDD-cost:   25
c ---[1622]---> BDD-cost:   37
c ---[1621]---> BDD-cost:   11
c ---[1620]---> BDD-cost:   37
c ---[1619]---> BDD-cost:   37
c ---[1618]---> BDD-cost:   31
c ---[1616]---> BDD-cost:   29
c ---[1615]---> BDD-cost:   37
c ---[1614]---> BDD-cost:   27
c ---[1613]---> BDD-cost:   37
c ---[1612]---> BDD-cost:   37
c ---[1611]---> BDD-cost:   15
c ---[1610]---> BDD-cost:    7
c ---[1609]---> BDD-cost:   29
c ---[1608]---> BDD-cost:   31
c ---[1607]---> BDD-cost:   13
c ---[1605]---> BDD-cost:   37
c ---[1603]---> BDD-cost:    7
c ---[1602]---> BDD-cost:   19
c ---[1601]---> BDD-cost:    7
c ---[1600]---> BDD-cost:    5
c ---[1599]---> BDD-cost:   19
c ---[1598]---> BDD-cost:   19
c ---[1597]---> BDD-cost:   19
c ---[1596]---> BDD-cost:   27
c ---[1593]---> BDD-cost:    3
c ---[1592]---> BDD-cost:   37
c ---[1591]---> BDD-cost:   37
c ---[1590]---> BDD-cost:   37
c ---[1589]---> BDD-cost:   37
c ---[1588]---> BDD-cost:    3
c ---[1587]---> BDD-cost:   37
c ---[1586]---> BDD-cost:   27
c ---[1585]---> BDD-cost:   33
c ---[1584]---> BDD-cost:   37
c ---[1582]---> BDD-cost:   37
c ---[1581]---> BDD-cost:   25
c ---[1580]---> BDD-cost:   37
c ---[1579]---> BDD-cost:   37
c ---[1578]---> BDD-cost:    9
c ---[1577]---> BDD-cost:    9
c ---[1576]---> BDD-cost:    3
c ---[1572]---> BDD-cost:    5
c ---[1570]---> BDD-cost:    5
c ---[1569]---> BDD-cost:    5
c ---[1568]---> BDD-cost:    5
c ---[1567]---> BDD-cost:   27
c ---[1566]---> BDD-cost:   27
c ---[1565]---> BDD-cost:   27
c ---[1564]---> BDD-cost:   27
c ---[1562]---> BDD-cost:    9
c ---[1561]---> BDD-cost:    9
c ---[1560]---> BDD-cost:   27
c ---[1559]---> BDD-cost:   19
c ---[1558]---> BDD-cost:   19
c ---[1557]---> BDD-cost:    5
c ---[1556]---> BDD-cost:   11
c ---[1555]---> BDD-cost:    5
c ---[1554]---> BDD-cost:   11
c ---[1553]---> BDD-cost:   31
c ---[1551]---> BDD-cost:   31
c ---[1550]---> BDD-cost:   31
c ---[1549]---> BDD-cost:    7
c ---[1548]---> BDD-cost:   11
c ---[1547]---> BDD-cost:   27
c ---[1546]---> BDD-cost:   27
c ---[1545]---> BDD-cost:   19
c ---[1544]---> BDD-cost:    5
c ---[1543]---> BDD-cost:    3
c ---[1542]---> BDD-cost:   23
c ---[1540]---> BDD-cost:   37
c ---[1539]---> BDD-cost:   19
c ---[1538]---> BDD-cost:   19
c ---[1537]---> BDD-cost:   19
c ---[1536]---> BDD-cost:   19
c ---[1535]---> BDD-cost:   27
c ---[1534]---> BDD-cost:   19
c ---[1533]---> BDD-cost:   19
c ---[1532]---> BDD-cost:   27
c ---[1531]---> BDD-cost:   25
c ---[1529]---> BDD-cost:   27
c ---[1528]---> BDD-cost:   27
c ---[1527]---> BDD-cost:   27
c ---[1526]---> BDD-cost:   27
c ---[1525]---> BDD-cost:   19
c ---[1524]---> BDD-cost:   27
c ---[1523]---> BDD-cost:   27
c ---[1522]---> BDD-cost:   37
c ---[1521]---> BDD-cost:   27
c ---[1520]---> BDD-cost:    5
c ---[1518]---> BDD-cost:   19
c ---[1517]---> BDD-cost:    5
c ---[1516]---> BDD-cost:    5
c ---[1515]---> BDD-cost:    5
c ---[1514]---> BDD-cost:    5
c ---[1513]---> BDD-cost:    5
c ---[1512]---> BDD-cost:    5
c ---[1511]---> BDD-cost:    9
c ---[1510]---> BDD-cost:   27
c ---[1509]---> BDD-cost:    5
c ---[1507]---> BDD-cost:    3
c ---[1506]---> BDD-cost:    3
c ---[1505]---> BDD-cost:    3
c ---[1504]---> BDD-cost:    5
c ---[1503]---> BDD-cost:    5
c ---[1502]---> BDD-cost:    5
c ---[1501]---> BDD-cost:   27
c ---[1500]---> BDD-cost:   35
c ---[1499]---> BDD-cost:   15
c ---[1498]---> BDD-cost:   27
c ---[1496]---> BDD-cost:   27
c ---[1495]---> BDD-cost:   27
c ---[1494]---> BDD-cost:   37
c ---[1493]---> BDD-cost:   27
c ---[1492]---> BDD-cost:   37
c ---[1491]---> BDD-cost:    9
c ---[1490]---> BDD-cost:    9
c ---[1489]---> BDD-cost:    9
c ---[1484]---> BDD-cost:   11
c ---[1483]---> BDD-cost:    3
c ---[1482]---> BDD-cost:   13
c ---[1481]---> BDD-cost:    9
c ---[1480]---> BDD-cost:   19
c ---[1479]---> BDD-cost:   27
c ---[1478]---> BDD-cost:   19
c ---[1477]---> BDD-cost:   27
c ---[1476]---> BDD-cost:   27
c ---[1475]---> BDD-cost:   27
c ---[1473]---> BDD-cost:   27
c ---[1472]---> BDD-cost:    3
c ---[1471]---> BDD-cost:   37
c ---[1470]---> BDD-cost:   29
c ---[1469]---> BDD-cost:   33
c ---[1468]---> BDD-cost:   29
c ---[1467]---> BDD-cost:   37
c ---[1466]---> BDD-cost:    3
c ---[1464]---> BDD-cost:    3
c ---[1462]---> BDD-cost:    3
c ---[1461]---> BDD-cost:    3
c ---[1460]---> BDD-cost:    3
c ---[1459]---> BDD-cost:    5
c ---[1458]---> BDD-cost:   27
c ---[1457]---> BDD-cost:   19
c ---[1456]---> BDD-cost:    5
c ---[1455]---> BDD-cost:    7
c ---[1453]---> BDD-cost:    9
c ---[1452]---> BDD-cost:   13
c ---[1451]---> BDD-cost:    7
c ---[1450]---> BDD-cost:   19
c ---[1449]---> BDD-cost:   23
c ---[1448]---> BDD-cost:    5
c ---[1447]---> BDD-cost:    5
c ---[1446]---> BDD-cost:   19
c ---[1445]---> BDD-cost:   27
c ---[1444]---> BDD-cost:    5
c ---[1442]---> BDD-cost:   19
c ---[1441]---> BDD-cost:   27
c ---[1440]---> BDD-cost:   27
c ---[1439]---> BDD-cost:   27
c ---[1438]---> BDD-cost:   27
c ---[1437]---> BDD-cost:   27
c ---[1436]---> BDD-cost:   25
c ---[1435]---> BDD-cost:   19
c ---[1434]---> BDD-cost:   23
c ---[1433]---> BDD-cost:    3
c ---[1431]---> BDD-cost:   27
c ---[1430]---> BDD-cost:   27
c ---[1429]---> BDD-cost:   27
c ---[1428]---> BDD-cost:   27
c ---[1427]---> BDD-cost:   27
c ---[1426]---> BDD-cost:   27
c ---[1425]---> BDD-cost:    3
c ---[1424]---> BDD-cost:    3
c ---[1423]---> BDD-cost:    3
c ---[1422]---> BDD-cost:    3
c ---[1420]---> BDD-cost:    7
c ---[1419]---> BDD-cost:    7
c ---[1417]---> BDD-cost:    3
c ---[1416]---> BDD-cost:    7
c ---[1415]---> BDD-cost:    7
c ---[1413]---> BDD-cost:   27
c ---[1409]---> BDD-cost:   19
c ---[1408]---> BDD-cost:   37
c ---[1407]---> BDD-cost:   19
c ---[1406]---> BDD-cost:   23
c ---[1405]---> BDD-cost:   29
c ---[1404]---> BDD-cost:   31
c ---[1403]---> BDD-cost:   31
c ---[1401]---> BDD-cost:   37
c ---[1400]---> BDD-cost:   11
c ---[1399]---> BDD-cost:   11
c ---[1398]---> BDD-cost:    5
c ---[1396]---> BDD-cost:    5
c ---[1395]---> BDD-cost:   11
c ---[1394]---> BDD-cost:   21
c ---[1393]---> BDD-cost:   37
c ---[1392]---> BDD-cost:   31
c ---[1390]---> BDD-cost:    5
c ---[1389]---> BDD-cost:   31
c ---[1388]---> BDD-cost:   19
c ---[1387]---> BDD-cost:   29
c ---[1386]---> BDD-cost:   37
c ---[1385]---> BDD-cost:   29
c ---[1384]---> BDD-cost:   31
c ---[1383]---> BDD-cost:   21
c ---[1382]---> BDD-cost:    5
c ---[1378]---> BDD-cost:   31
c ---[1377]---> BDD-cost:   37
c ---[1376]---> BDD-cost:   29
c ---[1375]---> BDD-cost:   31
c ---[1374]---> BDD-cost:   27
c ---[1373]---> BDD-cost:   19
c ---[1372]---> BDD-cost:   37
c ---[1371]---> BDD-cost:   37
c ---[1370]---> BDD-cost:   29
c ---[1369]---> BDD-cost:   19
c ---[1367]---> BDD-cost:   37
c ---[1366]---> BDD-cost:   23
c ---[1365]---> BDD-cost:   35
c ---[1364]---> BDD-cost:   37
c ---[1363]---> BDD-cost:   19
c ---[1362]---> BDD-cost:   19
c ---[1361]---> BDD-cost:   23
c ---[1360]---> BDD-cost:   15
c ---[1359]---> BDD-cost:   15
c ---[1358]---> BDD-cost:    9
c ---[1357]---> BDD-cost: 6392
c ---[1356]---> BDD-cost:    3
c ---[1355]---> BDD-cost:   21
c ---[1354]---> BDD-cost:   23
c ---[1353]---> BDD-cost:   19
c ---[1352]---> BDD-cost:   19
c ---[1351]---> BDD-cost:   23
c ---[1350]---> BDD-cost:    7
c ---[1349]---> BDD-cost:   27
c ---[1348]---> BDD-cost:   37
c ---[1347]---> BDD-cost:   29
c ---[1346]---> BDD-cost:19596
c ---[1345]---> BDD-cost:   37
c ---[1344]---> BDD-cost:   15
c ---[1343]---> BDD-cost:   27
c ---[1342]---> BDD-cost:   27
c ---[1341]---> BDD-cost:   27
c ---[1340]---> BDD-cost:   27
c ---[1339]---> BDD-cost:   27
c ---[1338]---> BDD-cost:   31
c ---[1337]---> BDD-cost:   25
c ---[1336]---> BDD-cost:   27
c ---[1334]---> BDD-cost:   27
c ---[1333]---> BDD-cost:   27
c ---[1332]---> BDD-cost:   37
c ---[1331]---> BDD-cost:   15
c ---[1330]---> BDD-cost:    3
c ---[1329]---> BDD-cost:    7
c ---[1328]---> BDD-cost:    5
c ---[1327]---> BDD-cost:    5
c ---[1325]---> BDD-cost:   27
c ---[1324]---> BDD-cost:   27
c ---[1323]---> BDD-cost:   27
c ---[1322]---> BDD-cost:   27
c ---[1321]---> BDD-cost:   11
c ---[1319]---> BDD-cost:    3
c ---[1317]---> BDD-cost:    3
c ---[1316]---> BDD-cost:    3
c ---[1305]---> BDD-cost: 6529
c ---[1225]---> BDD-cost: 4492
c ---[1160]---> BDD-cost:11514
c ---[1135]---> BDD-cost: 6076
c ---[1115]---> BDD-cost:   19
c ---[1054]---> BDD-cost: 2103
c ---[ 898]---> BDD-cost:   19
c ---[ 897]---> BDD-cost:   19
c ---[ 896]---> BDD-cost:   27
c ---[ 895]---> BDD-cost:   27
c ---[ 894]---> BDD-cost:   15
c ---[ 893]---> BDD-cost:   29
c ---[ 892]---> BDD-cost:   23
c ---[ 891]---> BDD-cost:   29
c ---[ 890]---> BDD-cost:   27
c ---[ 889]---> BDD-cost:   29
c ---[ 887]---> BDD-cost:   19
c ---[ 886]---> BDD-cost:    0
c ---[ 885]---> BDD-cost:   17
c ---[ 884]---> BDD-cost:   29
c ---[ 883]---> BDD-cost:   37
c ---[ 882]---> BDD-cost:   37
c ---[ 881]---> BDD-cost:   37
c ---[ 880]---> BDD-cost:   27
c ---[ 879]---> BDD-cost:   27
c ---[ 878]---> BDD-cost:   27
c ---[ 876]---> BDD-cost:   19
c ---[ 875]---> BDD-cost:   27
c ---[ 874]---> BDD-cost:   19
c ---[ 873]---> BDD-cost:   37
c ---[ 872]---> BDD-cost:   15
c ---[ 871]---> BDD-cost:   27
c ---[ 870]---> BDD-cost:   15
c ---[ 869]---> BDD-cost:    5
c ---[ 868]---> BDD-cost:   19
c ---[ 867]---> BDD-cost:   27
c ---[ 865]---> BDD-cost:   23
c ---[ 864]---> BDD-cost:   23
c ---[ 863]---> BDD-cost:   23
c ---[ 862]---> BDD-cost:   23
c ---[ 861]---> BDD-cost:   19
c ---[ 860]---> BDD-cost:   31
c ---[ 859]---> BDD-cost:   19
c ---[ 858]---> BDD-cost:   19
c ---[ 857]---> BDD-cost:    3
c ---[ 856]---> BDD-cost:   19
c ---[ 854]---> BDD-cost:    5
c ---[ 853]---> BDD-cost:   27
c ---[ 852]---> BDD-cost:   19
c ---[ 851]---> BDD-cost:   19
c ---[ 850]---> BDD-cost:   19
c ---[ 849]---> BDD-cost:    9
c ---[ 848]---> BDD-cost:   27
c ---[ 847]---> BDD-cost:   19
c ---[ 846]---> BDD-cost:   23
c ---[ 845]---> BDD-cost:   23
c ---[ 842]---> BDD-cost:   23
c ---[ 841]---> BDD-cost:    3
c ---[ 840]---> BDD-cost:   19
c ---[ 839]---> BDD-cost:   19
c ---[ 838]---> BDD-cost:   23
c ---[ 837]---> BDD-cost:   19
c ---[ 836]---> BDD-cost:   19
c ---[ 835]---> BDD-cost:   19
c ---[ 834]---> BDD-cost:   19
c ---[ 833]---> BDD-cost:   19
c ---[ 831]---> BDD-cost:   23
c ---[ 830]---> BDD-cost:   23
c ---[ 829]---> BDD-cost:   19
c ---[ 828]---> BDD-cost:   19
c ---[ 827]---> BDD-cost:   19
c ---[ 826]---> BDD-cost:    5
c ---[ 825]---> BDD-cost:   27
c ---[ 824]---> BDD-cost:   23
c ---[ 823]---> BDD-cost:   19
c ---[ 822]---> BDD-cost:   19
c ---[ 820]---> BDD-cost:   19
c ---[ 819]---> BDD-cost:   19
c ---[ 818]---> BDD-cost:   19
c ---[ 817]---> BDD-cost:   23
c ---[ 816]---> BDD-cost:   23
c ---[ 815]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:   23
c ---[ 813]---> BDD-cost:    5
c ---[ 812]---> BDD-cost:   19
c ---[ 811]---> BDD-cost:   19
c ---[ 809]---> BDD-cost:   19
c ---[ 808]---> BDD-cost:   19
c ---[ 807]---> BDD-cost:   19
c ---[ 806]---> BDD-cost:   19
c ---[ 805]---> BDD-cost:   19
c ---[ 804]---> BDD-cost:   19
c ---[ 803]---> BDD-cost:   19
c ---[ 802]---> BDD-cost:   19
c ---[ 801]---> BDD-cost:   25
c ---[ 800]---> BDD-cost:   25
c ---[ 799]---> BDD-cost: 7839
c ---[ 798]---> BDD-cost:   23
c ---[ 797]---> BDD-cost:   23
c ---[ 796]---> BDD-cost:   23
c ---[ 795]---> BDD-cost:   25
c ---[ 794]---> BDD-cost:   23
c ---[ 793]---> BDD-cost:   25
c ---[ 792]---> BDD-cost:    5
c ---[ 791]---> BDD-cost:   31
c ---[ 790]---> BDD-cost:   27
c ---[ 789]---> BDD-cost:    3
c ---[ 787]---> BDD-cost:    3
c ---[ 786]---> BDD-cost:   27
c ---[ 785]---> BDD-cost:   27
c ---[ 784]---> BDD-cost:   27
c ---[ 783]---> BDD-cost:   27
c ---[ 782]---> BDD-cost:   27
c ---[ 781]---> BDD-cost:    9
c ---[ 780]---> BDD-cost:    5
c ---[ 779]---> BDD-cost:    3
c ---[ 778]---> BDD-cost:    3
c ---[ 777]---> BDD-cost: 6871
c ---[ 776]---> BDD-cost:    3
c ---[ 775]---> BDD-cost:   25
c ---[ 774]---> BDD-cost:   27
c ---[ 773]---> BDD-cost:   29
c ---[ 772]---> BDD-cost:   27
c ---[ 771]---> BDD-cost:   27
c ---[ 770]---> BDD-cost:   29
c ---[ 769]---> BDD-cost:   27
c ---[ 768]---> BDD-cost:   25
c ---[ 767]---> BDD-cost:   37
c ---[ 766]---> BDD-cost:28640
c ---[ 765]---> BDD-cost:   37
c ---[ 764]---> BDD-cost:   27
c ---[ 763]---> BDD-cost:   37
c ---[ 762]---> BDD-cost:   27
c ---[ 761]---> BDD-cost:   27
c ---[ 760]---> BDD-cost:   27
c ---[ 759]---> BDD-cost:   27
c ---[ 758]---> BDD-cost:   27
c ---[ 757]---> BDD-cost:   31
c ---[ 756]---> BDD-cost:   31
c ---[ 754]---> BDD-cost:   27
c ---[ 753]---> BDD-cost:   25
c ---[ 752]---> BDD-cost:   37
c ---[ 751]---> BDD-cost:   37
c ---[ 750]---> BDD-cost:   37
c ---[ 749]---> BDD-cost:   27
c ---[ 748]---> BDD-cost:   25
c ---[ 747]---> BDD-cost:   27
c ---[ 746]---> BDD-cost:    9
c ---[ 745]---> BDD-cost:   25
c ---[ 743]---> BDD-cost:   27
c ---[ 742]---> BDD-cost:   27
c ---[ 741]---> BDD-cost:   27
c ---[ 740]---> BDD-cost:   37
c ---[ 739]---> BDD-cost:   37
c ---[ 738]---> BDD-cost:   27
c ---[ 737]---> BDD-cost:   27
c ---[ 736]---> BDD-cost:   27
c ---[ 735]---> BDD-cost:   37
c ---[ 734]---> BDD-cost:   27
c ---[ 731]---> BDD-cost:   27
c ---[ 730]---> BDD-cost:   37
c ---[ 729]---> BDD-cost:    5
c ---[ 728]---> BDD-cost:    5
c ---[ 727]---> BDD-cost:   37
c ---[ 725]---> BDD-cost:   27
c ---[ 724]---> BDD-cost:   31
c ---[ 723]---> BDD-cost:   19
c ---[ 720]---> BDD-cost:   27
c ---[ 719]---> BDD-cost:   27
c ---[ 718]---> BDD-cost:   37
c ---[ 717]---> BDD-cost:   37
c ---[ 716]---> BDD-cost:   19
c ---[ 715]---> BDD-cost:   27
c ---[ 714]---> BDD-cost:   23
c ---[ 712]---> BDD-cost:    3
c ---[ 711]---> BDD-cost:   27
c ---[ 709]---> BDD-cost:    5
c ---[ 708]---> BDD-cost:    7
c ---[ 707]---> BDD-cost:   27
c ---[ 706]---> BDD-cost:   27
c ---[ 705]---> BDD-cost:   27
c ---[ 704]---> BDD-cost:   27
c ---[ 703]---> BDD-cost:   27
c ---[ 702]---> BDD-cost:   27
c ---[ 701]---> BDD-cost:   27
c ---[ 700]---> BDD-cost:   27
c ---[ 698]---> BDD-cost:   27
c ---[ 697]---> BDD-cost:   27
c ---[ 696]---> BDD-cost:   19
c ---[ 695]---> BDD-cost:    3
c ---[ 694]---> BDD-cost:    7
c ---[ 693]---> BDD-cost:   19
c ---[ 692]---> BDD-cost:    9
c ---[ 691]---> BDD-cost:   37
c ---[ 690]---> BDD-cost:   37
c ---[ 689]---> BDD-cost:   37
c ---[ 687]---> BDD-cost:   27
c ---[ 686]---> BDD-cost:   27
c ---[ 685]---> BDD-cost:    5
c ---[ 684]---> BDD-cost:   19
c ---[ 683]---> BDD-cost:    5
c ---[ 682]---> BDD-cost:   27
c ---[ 681]---> BDD-cost:   27
c ---[ 680]---> BDD-cost:   27
c ---[ 679]---> BDD-cost:   27
c ---[ 678]---> BDD-cost:   19
c ---[ 675]---> BDD-cost:   29
c ---[ 674]---> BDD-cost:   19
c ---[ 673]---> BDD-cost:   27
c ---[ 672]---> BDD-cost:   19
c ---[ 671]---> BDD-cost:   27
c ---[ 670]---> BDD-cost:   19
c ---[ 669]---> BDD-cost:    3
c ---[ 668]---> BDD-cost:    3
c ---[ 667]---> BDD-cost:   19
c ---[ 664]---> BDD-cost:   27
c ---[ 663]---> BDD-cost:    3
c ---[ 662]---> BDD-cost:   27
c ---[ 661]---> BDD-cost:   37
c ---[ 660]---> BDD-cost:   27
c ---[ 659]---> BDD-cost:   27
c ---[ 658]---> BDD-cost:   27
c ---[ 657]---> BDD-cost:   27
c ---[ 656]---> BDD-cost:   15
c ---[ 654]---> BDD-cost:   27
c ---[ 653]---> BDD-cost:   27
c ---[ 652]---> BDD-cost:   27
c ---[ 651]---> BDD-cost:   27
c ---[ 650]---> BDD-cost:   25
c ---[ 649]---> BDD-cost:   37
c ---[ 648]---> BDD-cost:   31
c ---[ 647]---> BDD-cost:   37
c ---[ 646]---> BDD-cost:    5
c ---[ 645]---> BDD-cost:   19
c ---[ 643]---> BDD-cost:   27
c ---[ 642]---> BDD-cost:    3
c ---[ 640]---> BDD-cost:   19
c ---[ 638]---> BDD-cost:    3
c ---[ 636]---> BDD-cost:   31
c ---[ 635]---> BDD-cost:   23
c ---[ 634]---> BDD-cost:   25
c ---[ 632]---> BDD-cost:   37
c ---[ 631]---> BDD-cost:   31
c ---[ 630]---> BDD-cost:   27
c ---[ 629]---> BDD-cost:   19
c ---[ 628]---> BDD-cost:   27
c ---[ 627]---> BDD-cost:   19
c ---[ 626]---> BDD-cost:   19
c ---[ 625]---> BDD-cost:   19
c ---[ 624]---> BDD-cost:   37
c ---[ 623]---> BDD-cost:   37
c ---[ 620]---> BDD-cost:   27
c ---[ 619]---> BDD-cost:   27
c ---[ 618]---> BDD-cost:   27
c ---[ 617]---> BDD-cost:   19
c ---[ 616]---> BDD-cost:   27
c ---[ 615]---> BDD-cost:   27
c ---[ 614]---> BDD-cost:   37
c ---[ 613]---> BDD-cost:   25
c ---[ 612]---> BDD-cost:   19
c ---[ 611]---> BDD-cost:   19
c ---[ 609]---> BDD-cost:   13
c ---[ 608]---> BDD-cost:   19
c ---[ 607]---> BDD-cost:   19
c ---[ 606]---> BDD-cost:   19
c ---[ 605]---> BDD-cost:    7
c ---[ 604]---> BDD-cost:    7
c ---[ 603]---> BDD-cost:   27
c ---[ 602]---> BDD-cost:   27
c ---[ 601]---> BDD-cost:    5
c ---[ 600]---> BDD-cost: 8648
c ---[ 599]---> BDD-cost:    7
c ---[ 598]---> BDD-cost:    5
c ---[ 597]---> BDD-cost:    3
c ---[ 596]---> BDD-cost:    7
c ---[ 595]---> BDD-cost:   35
c ---[ 594]---> BDD-cost:   37
c ---[ 593]---> BDD-cost:   19
c ---[ 592]---> BDD-cost:   31
c ---[ 591]---> BDD-cost:   15
c ---[ 589]---> BDD-cost:   25
c ---[ 588]---> BDD-cost:   15
c ---[ 587]---> BDD-cost:   37
c ---[ 586]---> BDD-cost:   37
c ---[ 585]---> BDD-cost:   29
c ---[ 584]---> BDD-cost:    3
c ---[ 583]---> BDD-cost:    7
c ---[ 582]---> BDD-cost:   19
c ---[ 580]---> BDD-cost:    7
c ---[ 578]---> BDD-cost:   37
c ---[ 577]---> BDD-cost:   27
c ---[ 576]---> BDD-cost:   27
c ---[ 575]---> BDD-cost:   25
c ---[ 574]---> BDD-cost:   27
c ---[ 573]---> BDD-cost:   27
c ---[ 572]---> BDD-cost:   27
c ---[ 571]---> BDD-cost:    3
c ---[ 567]---> BDD-cost:   33
c ---[ 566]---> BDD-cost:   29
c ---[ 565]---> BDD-cost:   31
c ---[ 564]---> BDD-cost:   37
c ---[ 563]---> BDD-cost:   31
c ---[ 562]---> BDD-cost:   15
c ---[ 561]---> BDD-cost:   13
c ---[ 560]---> BDD-cost:   29
c ---[ 559]---> BDD-cost:   37
c ---[ 557]---> BDD-cost:   13
c ---[ 556]---> BDD-cost:   37
c ---[ 555]---> BDD-cost:   27
c ---[ 554]---> BDD-cost:   27
c ---[ 553]---> BDD-cost:   19
c ---[ 552]---> BDD-cost:   15
c ---[ 551]---> BDD-cost:   37
c ---[ 550]---> BDD-cost:   15
c ---[ 549]---> BDD-cost:   27
c ---[ 548]---> BDD-cost:   29
c ---[ 546]---> BDD-cost:   29
c ---[ 545]---> BDD-cost:   31
c ---[ 544]---> BDD-cost:   37
c ---[ 543]---> BDD-cost:   37
c ---[ 542]---> BDD-cost:   31
c ---[ 541]---> BDD-cost:   29
c ---[ 540]---> BDD-cost:   31
c ---[ 539]---> BDD-cost:   31
c ---[ 538]---> BDD-cost:   31
c ---[ 537]---> BDD-cost:   37
c ---[ 535]---> BDD-cost:   31
c ---[ 534]---> BDD-cost:   31
c ---[ 533]---> BDD-cost:   31
c ---[ 532]---> BDD-cost:   29
c ---[ 531]---> BDD-cost:   29
c ---[ 530]---> BDD-cost:   29
c ---[ 529]---> BDD-cost:   29
c ---[ 528]---> BDD-cost:   31
c ---[ 527]---> BDD-cost:   37
c ---[ 526]---> BDD-cost:   37
c ---[ 524]---> BDD-cost:   37
c ---[ 523]---> BDD-cost:   37
c ---[ 522]---> BDD-cost:   35
c ---[ 521]---> BDD-cost:   33
c ---[ 520]---> BDD-cost:   37
c ---[ 519]---> BDD-cost:   35
c ---[ 518]---> BDD-cost:   37
c ---[ 517]---> BDD-cost:   31
c ---[ 516]---> BDD-cost:   31
c ---[ 515]---> BDD-cost:   31
c ---[ 512]---> BDD-cost:   33
c ---[ 511]---> BDD-cost:   37
c ---[ 510]---> BDD-cost:   31
c ---[ 509]---> BDD-cost:   31
c ---[ 508]---> BDD-cost:   31
c ---[ 507]---> BDD-cost:   31
c ---[ 506]---> BDD-cost:   29
c ---[ 505]---> BDD-cost:   31
c ---[ 504]---> BDD-cost:   37
c ---[ 503]---> BDD-cost:   29
c ---[ 501]---> BDD-cost:   37
c ---[ 500]---> BDD-cost:   33
c ---[ 499]---> BDD-cost:   31
c ---[ 498]---> BDD-cost:   29
c ---[ 497]---> BDD-cost:   31
c ---[ 496]---> BDD-cost:   29
c ---[ 495]---> BDD-cost:   31
c ---[ 494]---> BDD-cost:   35
c ---[ 493]---> BDD-cost:   37
c ---[ 492]---> BDD-cost:   29
c ---[ 490]---> BDD-cost:   29
c ---[ 489]---> BDD-cost:   31
c ---[ 488]---> BDD-cost:   31
c ---[ 487]---> BDD-cost:   35
c ---[ 485]---> BDD-cost:    5
c ---[ 484]---> BDD-cost:    3
c ---[ 483]---> BDD-cost:    9
c ---[ 482]---> BDD-cost:    9
c ---[ 481]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:   19
c ---[ 478]---> BDD-cost:   19
c ---[ 477]---> BDD-cost:   37
c ---[ 476]---> BDD-cost:   37
c ---[ 475]---> BDD-cost:   29
c ---[ 474]---> BDD-cost:    5
c ---[ 473]---> BDD-cost:   13
c ---[ 472]---> BDD-cost:    9
c ---[ 471]---> BDD-cost:   11
c ---[ 470]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:   31
c ---[ 467]---> BDD-cost:   21
c ---[ 466]---> BDD-cost:   23
c ---[ 465]---> BDD-cost:   19
c ---[ 464]---> BDD-cost:    5
c ---[ 463]---> BDD-cost:    5
c ---[ 462]---> BDD-cost:    7
c ---[ 461]---> BDD-cost:    7
c ---[ 460]---> BDD-cost:   19
c ---[ 459]---> BDD-cost:   19
c ---[ 457]---> BDD-cost:   37
c ---[ 456]---> BDD-cost:    5
c ---[ 455]---> BDD-cost:   11
c ---[ 454]---> BDD-cost:   31
c ---[ 453]---> BDD-cost:   31
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    9
c ---[ 449]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:   19
c ---[ 445]---> BDD-cost:   23
c ---[ 443]---> BDD-cost:   27
c ---[ 442]---> BDD-cost:   27
c ---[ 441]---> BDD-cost:   19
c ---[ 440]---> BDD-cost:    3
c ---[ 439]---> BDD-cost:   37
c ---[ 438]---> BDD-cost:   27
c ---[ 437]---> BDD-cost:   27
c ---[ 435]---> BDD-cost:   27
c ---[ 434]---> BDD-cost:   19
c ---[ 433]---> BDD-cost:   27
c ---[ 432]---> BDD-cost:   27
c ---[ 431]---> BDD-cost:   27
c ---[ 430]---> BDD-cost:   19
c ---[ 428]---> BDD-cost:    3
c ---[ 424]---> BDD-cost:    3
c ---[ 423]---> BDD-cost:    9
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    5
c ---[ 420]---> BDD-cost:   19
c ---[ 419]---> BDD-cost:   19
c ---[ 418]---> BDD-cost:    3
c ---[ 417]---> BDD-cost:    5
c ---[ 416]---> BDD-cost:   27
c ---[ 415]---> BDD-cost:    5
c ---[ 413]---> BDD-cost:   27
c ---[ 412]---> BDD-cost:   27
c ---[ 411]---> BDD-cost:   19
c ---[ 410]---> BDD-cost:    3
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:   37
c ---[ 407]---> BDD-cost:   37
c ---[ 406]---> BDD-cost:   27
c ---[ 405]---> BDD-cost:   27
c ---[ 404]---> BDD-cost:   27
c ---[ 403]---> BDD-cost: 2076
c ---[ 402]---> BDD-cost:  908
c ---[ 401]---> BDD-cost:  282
c ---[ 400]---> BDD-cost:   66
c ---[ 399]---> BDD-cost:   24
c ---[ 398]---> BDD-cost:  458
c ---[ 397]---> BDD-cost:    1
c ---[ 396]---> BDD-cost:  142
c ---[ 395]---> BDD-cost:   69
c ---[ 394]---> BDD-cost:   69
c ---[ 393]---> BDD-cost:  188
c ---[ 392]---> BDD-cost:   60
c ---[ 391]---> BDD-cost:  286
c ---[ 390]---> BDD-cost:   76
c ---[ 389]---> BDD-cost:  136
c ---[ 388]---> BDD-cost:  212
c ---[ 387]---> BDD-cost:  286
c ---[ 386]---> BDD-cost: 1841
c ---[ 385]---> BDD-cost: 2354
c ---[ 384]---> BDD-cost: 3102
c ---[ 383]---> BDD-cost:   62
c ---[ 382]---> BDD-cost:   70
c ---[ 381]---> BDD-cost:   36
c ---[ 380]---> BDD-cost:   22
c ---[ 379]---> BDD-cost:   32
c ---[ 378]---> BDD-cost:   56
c ---[ 377]---> BDD-cost: 1461
c ---[ 376]---> BDD-cost: 1569
c ---[ 375]---> BDD-cost:  846
c ---[ 374]---> BDD-cost:   95
c ---[ 373]---> BDD-cost:  151
c ---[ 372]---> BDD-cost:  371
c ---[ 371]---> BDD-cost:  296
c ---[ 370]---> BDD-cost:  521
c ---[ 369]---> BDD-cost:  151
c ---[ 368]---> BDD-cost:  367
c ---[ 367]---> BDD-cost: 3498
c ---[ 366]---> BDD-cost:  238
c ---[ 365]---> BDD-cost:   72
c ---[ 364]---> BDD-cost:   24
c ---[ 363]---> BDD-cost:   12
c ---[ 362]---> BDD-cost:   70
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:  108
c ---[ 359]---> BDD-cost:   38
c ---[ 358]---> BDD-cost: 3147
c ---[ 357]---> BDD-cost:   56
c ---[ 356]---> BDD-cost:   74
c ---[ 355]---> BDD-cost:  116
c ---[ 354]---> BDD-cost:   28
c ---[ 353]---> BDD-cost:  302
c ---[ 352]---> BDD-cost:   72
c ---[ 351]---> BDD-cost:   78
c ---[ 350]---> BDD-cost:  663
c ---[ 349]---> BDD-cost: 1344
c ---[ 348]---> BDD-cost:  277
c ---[ 347]---> BDD-cost:  114
c ---[ 346]---> BDD-cost:   26
c ---[ 345]---> BDD-cost:  996
c ---[ 344]---> BDD-cost:   14
c ---[ 343]---> BDD-cost:    8
c ---[ 342]---> BDD-cost:  124
c ---[ 341]---> BDD-cost:   28
c ---[ 340]---> BDD-cost:  511
c ---[ 339]---> BDD-cost: 1291
c ---[ 338]---> BDD-cost:  595
c ---[ 337]---> BDD-cost: 1788
c ---[ 336]---> BDD-cost: 2664
c ---[ 335]---> BDD-cost: 2280
c ---[ 334]---> BDD-cost: 3516
c ---[ 333]---> BDD-cost:   38
c ---[ 332]---> BDD-cost: 2211
c ---[ 331]---> BDD-cost: 2709
c ---[ 330]---> BDD-cost:   24
c ---[ 329]---> BDD-cost:   92
c ---[ 328]---> BDD-cost:   46
c ---[ 327]---> BDD-cost:  312
c ---[ 326]---> BDD-cost:   94
c ---[ 325]---> BDD-cost:   44
c ---[ 324]---> BDD-cost:   20
c ---[ 323]---> BDD-cost:   62
c ---[ 322]---> BDD-cost:    8
c ---[ 321]---> BDD-cost:  306
c ---[ 320]---> BDD-cost:  342
c ---[ 319]---> BDD-cost: 4547
c ---[ 318]---> BDD-cost:  548
c ---[ 317]---> BDD-cost:  781
c ---[ 316]---> BDD-cost:  627
c ---[ 315]---> BDD-cost: 1748
c ---[ 314]---> BDD-cost:  720
c ---[ 313]---> BDD-cost:  880
c ---[ 312]---> BDD-cost: 3295
c ---[ 311]---> BDD-cost: 1668
c ---[ 310]---> BDD-cost: 2411
c ---[ 309]---> BDD-cost: 2415
c ---[ 308]---> BDD-cost: 2403
c ---[ 307]---> BDD-cost:  860
c ---[ 306]---> BDD-cost:  462
c ---[ 305]---> BDD-cost:  176
c ---[ 304]---> BDD-cost: 1611
c ---[ 303]---> BDD-cost:  871
c ---[ 302]---> BDD-cost:  949
c ---[ 301]---> BDD-cost:  196
c ---[ 300]---> BDD-cost:  221
c ---[ 299]---> BDD-cost: 2254
c ---[ 298]---> BDD-cost: 2011
c ---[ 297]---> BDD-cost: 3585
c ---[ 296]---> BDD-cost:  277
c ---[ 295]---> BDD-cost:  303
c ---[ 294]---> BDD-cost: 3565
c ---[ 293]---> BDD-cost:  498
c ---[ 292]---> BDD-cost: 2702
c ---[ 291]---> BDD-cost:  954
c ---[ 290]---> BDD-cost: 1050
c ---[ 289]---> BDD-cost:  997
c ---[ 288]---> BDD-cost: 1251
c ---[ 287]---> BDD-cost: 2066
c ---[ 286]---> BDD-cost: 2373
c ---[ 285]---> BDD-cost:  250
c ---[ 284]---> BDD-cost:  280
c ---[ 283]---> BDD-cost:  158
c ---[ 282]---> BDD-cost:  834
c ---[ 281]---> BDD-cost: 3948
c ---[ 280]---> BDD-cost: 4777
c ---[ 279]---> BDD-cost: 4829
c ---[ 278]---> BDD-cost: 2776
c ---[ 277]---> BDD-cost:  178
c ---[ 276]---> BDD-cost:  203
c ---[ 275]---> BDD-cost: 1409
c ---[ 274]---> BDD-cost:  106
c ---[ 273]---> BDD-cost:  121
c ---[ 272]---> BDD-cost:  290
c ---[ 271]---> BDD-cost: 1672
c ---[ 270]---> BDD-cost: 2035
c ---[ 269]---> BDD-cost:  610
c ---[ 268]---> BDD-cost:  675
c ---[ 267]---> BDD-cost: 1359
c ---[ 266]---> BDD-cost: 1630
c ---[ 265]---> BDD-cost:  488
c ---[ 264]---> BDD-cost:  630
c ---[ 263]---> BDD-cost:  689
c ---[ 262]---> BDD-cost:  440
c ---[ 261]---> BDD-cost:   74
c ---[ 260]---> BDD-cost:  485
c ---[ 259]---> BDD-cost: 2754
c ---[ 258]---> BDD-cost: 3636
c ---[ 257]---> BDD-cost: 1450
c ---[ 256]---> BDD-cost: 1830
c ---[ 255]---> BDD-cost:  236
c ---[ 254]---> BDD-cost:  271
c ---[ 253]---> BDD-cost:  832
c ---[ 252]---> BDD-cost:  909
c ---[ 251]---> BDD-cost: 4202
c ---[ 250]---> BDD-cost:  594
c ---[ 249]---> BDD-cost: 5070
c ---[ 248]---> BDD-cost:  958
c ---[ 247]---> BDD-cost: 1096
c ---[ 246]---> BDD-cost:    1
c ---[ 245]---> BDD-cost: 1018
c ---[ 244]---> BDD-cost:  258
c ---[ 243]---> BDD-cost:  288
c ---[ 242]---> BDD-cost: 8250
c ---[ 241]---> BDD-cost: 1066
c ---[ 240]---> BDD-cost: 1860
c ---[ 239]---> BDD-cost: 2798
c ---[ 238]---> BDD-cost:  142
c ---[ 237]---> BDD-cost:  168
c ---[ 236]---> BDD-cost:  192
c ---[ 235]---> BDD-cost: 3957
c ---[ 234]---> BDD-cost:  970
c ---[ 233]---> BDD-cost: 1582
c ---[ 232]---> BDD-cost:  344
c ---[ 231]---> BDD-cost: 1448
c ---[ 230]---> BDD-cost:  100
c ---[ 229]---> BDD-cost:  116
c ---[ 228]---> BDD-cost: 1253
c ---[ 227]---> BDD-cost:  468
c ---[ 226]---> BDD-cost: 1904
c ---[ 225]---> BDD-cost:  419
c ---[ 224]---> BDD-cost:  460
c ---[ 223]---> BDD-cost: 1658
c ---[ 222]---> BDD-cost:  701
c ---[ 221]---> BDD-cost: 2130
c ---[ 220]---> BDD-cost:   80
c ---[ 219]---> BDD-cost:   95
c ---[ 218]---> BDD-cost: 3979
c ---[ 217]---> BDD-cost:  458
c ---[ 216]---> BDD-cost: 5600
c ---[ 215]---> BDD-cost:   90
c ---[ 214]---> BDD-cost:  565
c ---[ 213]---> BDD-cost:  730
c ---[ 212]---> BDD-cost:  441
c ---[ 211]---> BDD-cost:  753
c ---[ 210]---> BDD-cost:  562
c ---[ 209]---> BDD-cost:  617
c ---[ 208]---> BDD-cost:  704
c ---[ 207]---> BDD-cost:  773
c ---[ 206]---> BDD-cost:  457
c ---[ 205]---> BDD-cost:  506
c ---[ 204]---> BDD-cost:  692
c ---[ 203]---> BDD-cost: 5059
c ---[ 202]---> BDD-cost: 5238
c ---[ 201]---> BDD-cost: 3478
c ---[ 200]---> BDD-cost:  897
c ---[ 199]---> BDD-cost: 1064
c ---[ 198]---> BDD-cost:  892
c ---[ 197]---> BDD-cost: 2574
c ---[ 196]---> BDD-cost:  328
c ---[ 195]---> BDD-cost: 3535
c ---[ 194]---> BDD-cost: 2951
c ---[ 193]---> BDD-cost:  321
c ---[ 192]---> BDD-cost:  415
c ---[ 191]---> BDD-cost: 2999
c ---[ 190]---> BDD-cost: 6170
c ---[ 189]---> BDD-cost:  795
c ---[ 188]---> BDD-cost:  181
c ---[ 187]---> BDD-cost:  706
c ---[ 186]---> BDD-cost:  152
c ---[ 185]---> BDD-cost: 1295
c ---[ 184]---> BDD-cost:  873
c ---[ 183]---> BDD-cost: 6611
c ---[ 182]---> BDD-cost: 2264
c ---[ 181]---> BDD-cost: 5238
c ---[ 180]---> BDD-cost:  917
c ---[ 179]---> BDD-cost: 1337
c ---[ 178]---> BDD-cost:33628
c ---[ 177]---> BDD-cost:  148
c ---[ 176]---> BDD-cost:  160
c ---[ 175]---> BDD-cost: 3125
c ---[ 174]---> BDD-cost: 3023
c ---[ 173]---> BDD-cost: 2936
c ---[ 172]---> BDD-cost:  794
c ---[ 171]---> BDD-cost: 5956
c ---[ 170]---> BDD-cost:  896
c ---[ 169]---> BDD-cost:  292
c ---[ 168]---> BDD-cost:  142
c ---[ 167]---> BDD-cost:  186
c ---[ 166]---> BDD-cost:  418
c ---[ 165]---> BDD-cost:  856
c ---[ 164]---> BDD-cost: 1182
c ---[ 163]---> BDD-cost:  178
c ---[ 162]---> BDD-cost:  677
c ---[ 161]---> BDD-cost:    4
c ---[ 160]---> BDD-cost: 1166
c ---[ 159]---> BDD-cost:  526
c ---[ 158]---> BDD-cost:  382
c ---[ 157]---> BDD-cost: 1636
c ---[ 156]---> BDD-cost:  616
c ---[ 155]---> BDD-cost:  392
c ---[ 154]---> BDD-cost:  800
c ---[ 153]---> BDD-cost:   32
c ---[ 152]---> BDD-cost:    8
c ---[ 151]---> BDD-cost:    8
c ---[ 150]---> BDD-cost: 4874
c ---[ 149]---> BDD-cost:   26
c ---[ 148]---> BDD-cost:   22
c ---[ 147]---> BDD-cost:  710
c ---[ 146]---> BDD-cost:  978
c ---[ 145]---> BDD-cost:  452
c ---[ 144]---> BDD-cost: 1682
c ---[ 143]---> BDD-cost:  258
c ---[ 142]---> BDD-cost:  288
c ---[ 141]---> BDD-cost:   86
c ---[ 140]---> BDD-cost:  490
c ---[ 139]---> BDD-cost:  400
c ---[ 138]---> BDD-cost:   28
c ---[ 137]---> BDD-cost: 3675
c ---[ 136]---> BDD-cost:    6
c ---[ 135]---> BDD-cost:  784
c ---[ 134]---> BDD-cost:    2
c ---[ 133]---> BDD-cost:  576
c ---[ 132]---> BDD-cost:  924
c ---[ 131]---> BDD-cost:  398
c ---[ 130]---> BDD-cost:  132
c ---[ 129]---> BDD-cost:  122
c ---[ 128]---> BDD-cost:  334
c ---[ 127]---> BDD-cost:  272
c ---[ 126]---> BDD-cost:  173
c ---[ 125]---> BDD-cost:  475
c ---[ 124]---> BDD-cost: 1894
c ---[ 123]---> BDD-cost: 1520
c ---[ 122]---> BDD-cost:  292
c ---[ 121]---> BDD-cost:   78
c ---[ 120]---> BDD-cost: 1290
c ---[ 119]---> BDD-cost:  350
c ---[ 118]---> BDD-cost:  746
c ---[ 117]---> BDD-cost:  110
c ---[ 116]---> BDD-cost:  942
c ---[ 115]---> BDD-cost:   68
c ---[ 114]---> BDD-cost:  801
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:   38
c ---[ 111]---> BDD-cost: 1109
c ---[ 110]---> BDD-cost:  262
c ---[ 109]---> BDD-cost:  912
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[ 106]---> BDD-cost:    1
c ---[ 105]---> BDD-cost: 1102
c ---[ 104]---> BDD-cost:  197
c ---[ 103]---> BDD-cost:    1
c ---[ 102]---> BDD-cost:   26
c ---[ 101]---> BDD-cost:   90
c ---[ 100]---> BDD-cost:  237
c ---[  99]---> BDD-cost: 5235
c ---[  98]---> BDD-cost:   64
c ---[  97]---> BDD-cost:   70
c ---[  96]---> BDD-cost:  593
c ---[  95]---> BDD-cost:  349
c ---[  94]---> BDD-cost:    1
c ---[  93]---> BDD-cost:  842
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:  903
c ---[  90]---> BDD-cost:  176
c ---[  89]---> BDD-cost:   30
c ---[  88]---> BDD-cost: 2094
c ---[  87]---> BDD-cost: 2881
c ---[  86]---> BDD-cost:  456
c ---[  85]---> BDD-cost:  190
c ---[  84]---> BDD-cost: 1917
c ---[  83]---> BDD-cost:  578
c ---[  82]---> BDD-cost: 1815
c ---[  81]---> BDD-cost:  861
c ---[  80]---> BDD-cost: 1838
c ---[  79]---> BDD-cost:  220
c ---[  78]---> BDD-cost:  229
c ---[  77]---> BDD-cost: 5461
c ---[  76]---> BDD-cost:  299
c ---[  75]---> BDD-cost:   30
c ---[  74]---> BDD-cost:  152
c ---[  73]---> BDD-cost:  750
c ---[  72]---> BDD-cost:  366
c ---[  71]---> BDD-cost: 3010
c ---[  70]---> BDD-cost:  742
c ---[  69]---> BDD-cost: 1038
c ---[  68]---> BDD-cost:  634
c ---[  67]---> BDD-cost:  342
c ---[  66]---> BDD-cost:  102
c ---[  65]---> BDD-cost:  120
c ---[  64]---> BDD-cost:  618
c ---[  63]---> BDD-cost:  164
c ---[  62]---> BDD-cost:   56
c ---[  61]---> BDD-cost:  286
c ---[  60]---> BDD-cost:   18
c ---[  59]---> BDD-cost:  816
c ---[  58]---> BDD-cost:  268
c ---[  57]---> BDD-cost:  186
c ---[  56]---> BDD-cost:   48
c ---[  55]---> BDD-cost:  438
c ---[  54]---> BDD-cost: 1298
c ---[  53]---> BDD-cost: 1097
c ---[  52]---> BDD-cost:  775
c ---[  51]---> BDD-cost:  202
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost: 1035
c ---[  48]---> BDD-cost:  254
c ---[  47]---> BDD-cost: 1285
c ---[  46]---> BDD-cost:  439
c ---[  45]---> BDD-cost:   28
c ---[  44]---> BDD-cost:  870
c ---[  43]---> BDD-cost:  368
c ---[  42]---> BDD-cost:  502
c ---[  41]---> BDD-cost:  355
c ---[  40]---> BDD-cost:  226
c ---[  39]---> BDD-cost:  204
c ---[  38]---> BDD-cost:  188
c ---[  37]---> BDD-cost:   38
c ---[  36]---> BDD-cost: 2379
c ---[  35]---> BDD-cost:  306
c ---[  34]---> BDD-cost:  329
c ---[  33]---> BDD-cost:  128
c ---[  32]---> BDD-cost:   66
c ---[  31]---> BDD-cost:   20
c ---[  30]---> BDD-cost:   18
c ---[  29]---> BDD-cost:    8
c ---[  28]---> BDD-cost:   74
c ---[  27]---> BDD-cost:    6
c ---[  26]---> BDD-cost: 3282
c ---[  25]---> BDD-cost: 2908
c ---[  24]---> BDD-cost:12920
c ---[  23]---> BDD-cost:   18
c ---[  22]---> BDD-cost: 2567
c ---[  21]---> BDD-cost:   58
c ---[  20]---> BDD-cost:   20
c ---[  19]---> BDD-cost: 1689
c ---[  18]---> BDD-cost:11247
c ---[  17]---> BDD-cost:  122
c ---[  16]---> BDD-cost:   54
c ---[  15]---> BDD-cost: 1550
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:   88
c ---[  12]---> BDD-cost:  135
c ---[  11]---> BDD-cost:13798
c ---[  10]---> BDD-cost:    1
c ---[   9]---> BDD-cost: 8984
c ---[   8]---> BDD-cost: 2087
c ---[   7]---> BDD-cost:  552
c ---[   6]---> BDD-cost:    6
c ---[   5]---> BDD-cost:    2
c ---[   4]---> BDD-cost:  974
c ---[   3]---> BDD-cost: 3462
c ---[   2]---> BDD-cost: 4771
c ---[   1]---> BDD-cost:  424
c ---[   0]---> BDD-cost:  118
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1260490  3943518 |  420163       0        0     nan |  0.000 % |
c |       101 | 1260367  3943157 |  462179      71      216     3.0 |  0.286 % |
c |       251 | 1260043  3942227 |  508397     121      349     2.9 |  0.304 % |
c |       476 | 1259573  3940843 |  559236     245      761     3.1 |  0.331 % |
c |       813 | 1258653  3938172 |  615160     446     1457     3.3 |  0.386 % |
c |      1319 | 1258390  3937393 |  676676     800     3045     3.8 |  0.400 % |
c |      2079 | 1258329  3937210 |  744344    1506     7909     5.3 |  0.403 % |
c |      3218 | 1257844  3935759 |  818778    1764     7923     4.5 |  0.431 % |
ERROR! Too large constants encountered in constraint.
c ==============================================================================
c [1mFound solution: 113168195[0m
#### 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.83 0.94 0.91 2/54 18544
Raw data (stat): 18544 (runsolver) R 18543 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 468589785 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.85 0.94 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 41328 0 0 0 901 97 0 0 25 0 1 0 468589785 177106944 39467 4294967295 134512640 134672761 3221224544 3221069896 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43239 39469 603 41 0 43198 0
vsize: 172956
[startup+20.0006 s]
Raw data (loadavg): 0.87 0.94 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 44628 0 0 0 1892 106 0 0 25 0 1 0 468589785 223125504 42767 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54474 42767 603 41 0 54433 0
vsize: 217896
[startup+30.0004 s]
Raw data (loadavg): 0.89 0.94 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 45056 0 0 0 2891 107 0 0 25 0 1 0 468589785 224747520 43195 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54870 43195 603 41 0 54829 0
vsize: 219480
[startup+40.0015 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 45201 0 0 0 3890 108 0 0 25 0 1 0 468589785 225423360 43340 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55035 43340 603 41 0 54994 0
vsize: 220140
[startup+50.002 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 45416 0 0 0 4890 109 0 0 25 0 1 0 468589785 226234368 43555 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55233 43555 603 41 0 55192 0
vsize: 220932
[startup+60.0022 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 45984 0 0 0 5888 111 0 0 25 0 1 0 468589785 228524032 44123 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55792 44123 603 41 0 55751 0
vsize: 223168
[startup+70.003 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 46318 0 0 0 6886 113 0 0 25 0 1 0 468589785 229875712 44457 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56122 44457 603 41 0 56081 0
vsize: 224488
[startup+80.0033 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 46685 0 0 0 7885 114 0 0 25 0 1 0 468589785 231092224 44824 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56419 44824 603 41 0 56378 0
vsize: 225676
[startup+90.0041 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 46967 0 0 0 8884 116 0 0 25 0 1 0 468589785 232292352 45106 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56712 45106 603 41 0 56671 0
vsize: 226848
[startup+100.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 47196 0 0 0 9883 116 0 0 25 0 1 0 468589785 232968192 45335 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56877 45335 603 41 0 56836 0
vsize: 227508
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 47205 0 0 0 10883 116 0 0 25 0 1 0 468589785 233103360 45344 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56910 45344 603 41 0 56869 0
vsize: 227640
[startup+120.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 47217 0 0 0 11883 117 0 0 25 0 1 0 468589785 233103360 45356 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56910 45356 603 41 0 56869 0
vsize: 227640
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 47341 0 0 0 12882 117 0 0 25 0 1 0 468589785 233508864 45480 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57009 45480 603 41 0 56968 0
vsize: 228036
[startup+140.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 47488 0 0 0 13882 118 0 0 25 0 1 0 468589785 234049536 45627 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57141 45627 603 41 0 57100 0
vsize: 228564
[startup+150.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 47654 0 0 0 14881 118 0 0 25 0 1 0 468589785 234319872 45793 4294967295 134512640 134672761 3221224544 3221223712 134564714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57207 45793 603 41 0 57166 0
vsize: 228828
[startup+160.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 47715 0 0 0 15881 118 0 0 25 0 1 0 468589785 234455040 45854 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57240 45854 603 41 0 57199 0
vsize: 228960
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 47813 0 0 0 16881 119 0 0 25 0 1 0 468589785 234590208 45952 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57273 45952 603 41 0 57232 0
vsize: 229092
[startup+180.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 47889 0 0 0 17880 120 0 0 25 0 1 0 468589785 234725376 46028 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57306 46028 603 41 0 57265 0
vsize: 229224
[startup+182.673 s]
Raw data (loadavg): 0.99 0.96 0.91 1/53 18544
Raw data (stat): 18544 (minisat+) R 18543 26667 26666 0 -1 0 47889 0 0 0 17880 120 0 0 25 0 1 0 468589785 234725376 46028 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57306 46028 603 41 0 57265 0
vsize: 0

Child status: 1
Real time (s): 182.672
CPU time (s): 182.665
CPU user time (s): 181.356
CPU system time (s): 1.3088
CPU usage (%): 99.996
Max. virtual memory (Kb): 229224
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####