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/MIPLIB/miplib2003/normalized-mps-v2-13-7-liu.opb
MD5SUM	216e30ba4678325d93810a111dd11436
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	451651
Optimality of the best value was proved	NO
Number of terms in the objective function	20
Biggest coefficient in the objective function	524288
Number of bits for the biggest coefficient in the objective function	20
Sum of the numbers in the objective function	1048575
Number of bits of the sum of numbers in the objective function	20
Biggest number in a constraint	2143744
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	6434814
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.05
Number of variables	2429
Total number of constraints	3267
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	1089
Number of constraints which are nor clauses,nor cardinality constraints	2178
Minimum length of a constraint	1
Maximum length of a constraint	43
Trace number 31138

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-05-25 22:22:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22539 boxname=wulflinc6 idbench=1355 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  216e30ba4678325d93810a111dd11436  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-liu.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-liu.opb
IDLAUNCH: 22539
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        850724 kB
Buffers:         30668 kB
Cached:         128720 kB
SwapCached:        412 kB
Active:          29572 kB
Inactive:       132184 kB
HighTotal:      131008 kB
HighFree:        11788 kB
LowTotal:       903652 kB
LowFree:        838936 kB
SwapTotal:     2097136 kB
SwapFree:      2096036 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5696 kB
Slab:            16520 kB
Committed_AS:    63700 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 22:43:17 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22539 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2178 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[2177]---> BDD-cost:  103
c ---[2176]---> BDD-cost:  156
c ---[2175]---> BDD-cost:  155
c ---[2174]---> BDD-cost:  144
c ---[2173]---> BDD-cost:  103
c ---[2172]---> BDD-cost:  134
c ---[2171]---> BDD-cost:  103
c ---[2170]---> BDD-cost:  134
c ---[2169]---> BDD-cost:  103
c ---[2168]---> BDD-cost:  103
c ---[2167]---> BDD-cost:  103
c ---[2166]---> BDD-cost:  103
c ---[2165]---> BDD-cost:   99
c ---[2164]---> BDD-cost:  103
c ---[2163]---> BDD-cost:   99
c ---[2162]---> BDD-cost:   99
c ---[2161]---> BDD-cost:   99
c ---[2160]---> BDD-cost:   99
c ---[2159]---> BDD-cost:  152
c ---[2158]---> BDD-cost:   99
c ---[2157]---> BDD-cost:  152
c ---[2156]---> BDD-cost:   99
c ---[2155]---> BDD-cost:   81
c ---[2154]---> BDD-cost:   99
c ---[2153]---> BDD-cost:  148
c ---[2152]---> BDD-cost:   81
c ---[2151]---> BDD-cost:   99
c ---[2150]---> BDD-cost:   85
c ---[2149]---> BDD-cost:   99
c ---[2148]---> BDD-cost:   85
c ---[2147]---> BDD-cost:   99
c ---[2146]---> BDD-cost:  148
c ---[2145]---> BDD-cost:   99
c ---[2144]---> BDD-cost:  148
c ---[2143]---> BDD-cost:   99
c ---[2142]---> BDD-cost:  103
c ---[2141]---> BDD-cost:  146
c ---[2140]---> BDD-cost:   99
c ---[2139]---> BDD-cost:  146
c ---[2138]---> BDD-cost:   99
c ---[2137]---> BDD-cost:  101
c ---[2136]---> BDD-cost:   99
c ---[2135]---> BDD-cost:  101
c ---[2134]---> BDD-cost:   99
c ---[2133]---> BDD-cost:  137
c ---[2132]---> BDD-cost:   99
c ---[2131]---> BDD-cost:  148
c ---[2130]---> BDD-cost:  137
c ---[2129]---> BDD-cost:   99
c ---[2128]---> BDD-cost:  110
c ---[2127]---> BDD-cost:   99
c ---[2126]---> BDD-cost:  110
c ---[2125]---> BDD-cost:   99
c ---[2124]---> BDD-cost:  154
c ---[2123]---> BDD-cost:   99
c ---[2122]---> BDD-cost:  154
c ---[2121]---> BDD-cost:   99
c ---[2120]---> BDD-cost:  103
c ---[2119]---> BDD-cost:  153
c ---[2118]---> BDD-cost:   99
c ---[2117]---> BDD-cost:  153
c ---[2116]---> BDD-cost:   99
c ---[2115]---> BDD-cost:   99
c ---[2114]---> BDD-cost:   99
c ---[2113]---> BDD-cost:   99
c ---[2112]---> BDD-cost:   99
c ---[2111]---> BDD-cost:  104
c ---[2110]---> BDD-cost:   99
c ---[2109]---> BDD-cost:  152
c ---[2108]---> BDD-cost:  104
c ---[2107]---> BDD-cost:   99
c ---[2106]---> BDD-cost:   87
c ---[2105]---> BDD-cost:   99
c ---[2104]---> BDD-cost:   87
c ---[2103]---> BDD-cost:   99
c ---[2102]---> BDD-cost:   88
c ---[2101]---> BDD-cost:   99
c ---[2100]---> BDD-cost:   88
c ---[2099]---> BDD-cost:   99
c ---[2098]---> BDD-cost:  103
c ---[2097]---> BDD-cost:  155
c ---[2096]---> BDD-cost:   99
c ---[2095]---> BDD-cost:  155
c ---[2094]---> BDD-cost:   99
c ---[2093]---> BDD-cost:  148
c ---[2092]---> BDD-cost:   99
c ---[2091]---> BDD-cost:  148
c ---[2090]---> BDD-cost:   99
c ---[2089]---> BDD-cost:  152
c ---[2088]---> BDD-cost:   99
c ---[2087]---> BDD-cost:  152
c ---[2086]---> BDD-cost:  152
c ---[2085]---> BDD-cost:   99
c ---[2084]---> BDD-cost:  105
c ---[2083]---> BDD-cost:   99
c ---[2082]---> BDD-cost:  105
c ---[2081]---> BDD-cost:   99
c ---[2080]---> BDD-cost:  107
c ---[2079]---> BDD-cost:   99
c ---[2078]---> BDD-cost:  107
c ---[2077]---> BDD-cost:   99
c ---[2076]---> BDD-cost:  103
c ---[2075]---> BDD-cost:  144
c ---[2074]---> BDD-cost:   99
c ---[2073]---> BDD-cost:  144
c ---[2072]---> BDD-cost:   99
c ---[2071]---> BDD-cost:  134
c ---[2070]---> BDD-cost:   99
c ---[2069]---> BDD-cost:  134
c ---[2068]---> BDD-cost:   99
c ---[2067]---> BDD-cost:  103
c ---[2066]---> BDD-cost:   99
c ---[2065]---> BDD-cost:  103
c ---[2064]---> BDD-cost:  105
c ---[2063]---> BDD-cost:  103
c ---[2062]---> BDD-cost:   99
c ---[2061]---> BDD-cost:  152
c ---[2060]---> BDD-cost:   99
c ---[2059]---> BDD-cost:  152
c ---[2058]---> BDD-cost:   99
c ---[2057]---> BDD-cost:   81
c ---[2056]---> BDD-cost:   99
c ---[2055]---> BDD-cost:   81
c ---[2054]---> BDD-cost:   99
c ---[2053]---> BDD-cost:  103
c ---[2052]---> BDD-cost:   85
c ---[2051]---> BDD-cost:   99
c ---[2050]---> BDD-cost:   85
c ---[2049]---> BDD-cost:   99
c ---[2048]---> BDD-cost:  148
c ---[2047]---> BDD-cost:   99
c ---[2046]---> BDD-cost:  148
c ---[2045]---> BDD-cost:   99
c ---[2044]---> BDD-cost:  146
c ---[2043]---> BDD-cost:   99
c ---[2042]---> BDD-cost:  105
c ---[2041]---> BDD-cost:  146
c ---[2040]---> BDD-cost:   99
c ---[2039]---> BDD-cost:  101
c ---[2038]---> BDD-cost:   99
c ---[2037]---> BDD-cost:  101
c ---[2036]---> BDD-cost:   99
c ---[2035]---> BDD-cost:  137
c ---[2034]---> BDD-cost:   99
c ---[2033]---> BDD-cost:  137
c ---[2032]---> BDD-cost:   99
c ---[2031]---> BDD-cost:  103
c ---[2030]---> BDD-cost:  110
c ---[2029]---> BDD-cost:   99
c ---[2028]---> BDD-cost:  110
c ---[2027]---> BDD-cost:   99
c ---[2026]---> BDD-cost:  154
c ---[2025]---> BDD-cost:   99
c ---[2024]---> BDD-cost:  154
c ---[2023]---> BDD-cost:   99
c ---[2022]---> BDD-cost:  153
c ---[2021]---> BDD-cost:   99
c ---[2020]---> BDD-cost:  107
c ---[2019]---> BDD-cost:  153
c ---[2018]---> BDD-cost:   99
c ---[2017]---> BDD-cost:   99
c ---[2016]---> BDD-cost:   99
c ---[2015]---> BDD-cost:   99
c ---[2014]---> BDD-cost:   99
c ---[2013]---> BDD-cost:  104
c ---[2012]---> BDD-cost:   99
c ---[2011]---> BDD-cost:  104
c ---[2010]---> BDD-cost:   99
c ---[2009]---> BDD-cost:  103
c ---[2008]---> BDD-cost:   87
c ---[2007]---> BDD-cost:   99
c ---[2006]---> BDD-cost:   87
c ---[2005]---> BDD-cost:   99
c ---[2004]---> BDD-cost:   88
c ---[2003]---> BDD-cost:   99
c ---[2002]---> BDD-cost:   88
c ---[2001]---> BDD-cost:   99
c ---[2000]---> BDD-cost:  155
c ---[1999]---> BDD-cost:   99
c ---[1998]---> BDD-cost:  107
c ---[1997]---> BDD-cost:  155
c ---[1996]---> BDD-cost:   99
c ---[1995]---> BDD-cost:  148
c ---[1994]---> BDD-cost:   99
c ---[1993]---> BDD-cost:  148
c ---[1992]---> BDD-cost:   99
c ---[1991]---> BDD-cost:  152
c ---[1990]---> BDD-cost:   99
c ---[1989]---> BDD-cost:  152
c ---[1988]---> BDD-cost:   99
c ---[1987]---> BDD-cost:  103
c ---[1986]---> BDD-cost:  105
c ---[1985]---> BDD-cost:   99
c ---[1984]---> BDD-cost:  105
c ---[1983]---> BDD-cost:   99
c ---[1982]---> BDD-cost:  107
c ---[1981]---> BDD-cost:   99
c ---[1980]---> BDD-cost:  107
c ---[1979]---> BDD-cost:   99
c ---[1978]---> BDD-cost:  144
c ---[1977]---> BDD-cost:   99
c ---[1976]---> BDD-cost:  144
c ---[1975]---> BDD-cost:  144
c ---[1974]---> BDD-cost:   99
c ---[1973]---> BDD-cost:  134
c ---[1972]---> BDD-cost:   99
c ---[1971]---> BDD-cost:  134
c ---[1970]---> BDD-cost:   99
c ---[1969]---> BDD-cost:  103
c ---[1968]---> BDD-cost:   99
c ---[1967]---> BDD-cost:  103
c ---[1966]---> BDD-cost:  152
c ---[1965]---> BDD-cost:  103
c ---[1964]---> BDD-cost:   81
c ---[1963]---> BDD-cost:  152
c ---[1962]---> BDD-cost:   81
c ---[1961]---> BDD-cost:  152
c ---[1960]---> BDD-cost:   85
c ---[1959]---> BDD-cost:  152
c ---[1958]---> BDD-cost:   85
c ---[1957]---> BDD-cost:  152
c ---[1956]---> BDD-cost:  148
c ---[1955]---> BDD-cost:  152
c ---[1954]---> BDD-cost:  156
c ---[1953]---> BDD-cost:  144
c ---[1952]---> BDD-cost:  148
c ---[1951]---> BDD-cost:  152
c ---[1950]---> BDD-cost:  146
c ---[1949]---> BDD-cost:  152
c ---[1948]---> BDD-cost:  146
c ---[1947]---> BDD-cost:  152
c ---[1946]---> BDD-cost:  101
c ---[1945]---> BDD-cost:  152
c ---[1944]---> BDD-cost:  101
c ---[1943]---> BDD-cost:  152
c ---[1942]---> BDD-cost:  103
c ---[1941]---> BDD-cost:  137
c ---[1940]---> BDD-cost:  152
c ---[1939]---> BDD-cost:  137
c ---[1938]---> BDD-cost:  152
c ---[1937]---> BDD-cost:  110
c ---[1936]---> BDD-cost:  152
c ---[1935]---> BDD-cost:  110
c ---[1934]---> BDD-cost:  152
c ---[1933]---> BDD-cost:  154
c ---[1932]---> BDD-cost:  152
c ---[1931]---> BDD-cost:  134
c ---[1930]---> BDD-cost:  154
c ---[1929]---> BDD-cost:  152
c ---[1928]---> BDD-cost:  153
c ---[1927]---> BDD-cost:  152
c ---[1926]---> BDD-cost:  153
c ---[1925]---> BDD-cost:  152
c ---[1924]---> BDD-cost:   99
c ---[1923]---> BDD-cost:  152
c ---[1922]---> BDD-cost:   99
c ---[1921]---> BDD-cost:  152
c ---[1920]---> BDD-cost:  103
c ---[1919]---> BDD-cost:  104
c ---[1918]---> BDD-cost:  152
c ---[1917]---> BDD-cost:  104
c ---[1916]---> BDD-cost:  152
c ---[1915]---> BDD-cost:   87
c ---[1914]---> BDD-cost:  152
c ---[1913]---> BDD-cost:   87
c ---[1912]---> BDD-cost:  152
c ---[1911]---> BDD-cost:   88
c ---[1910]---> BDD-cost:  152
c ---[1909]---> BDD-cost:  134
c ---[1908]---> BDD-cost:   88
c ---[1907]---> BDD-cost:  152
c ---[1906]---> BDD-cost:  155
c ---[1905]---> BDD-cost:  152
c ---[1904]---> BDD-cost:  155
c ---[1903]---> BDD-cost:  152
c ---[1902]---> BDD-cost:  148
c ---[1901]---> BDD-cost:  152
c ---[1900]---> BDD-cost:  148
c ---[1899]---> BDD-cost:  152
c ---[1898]---> BDD-cost:  103
c ---[1897]---> BDD-cost:  152
c ---[1896]---> BDD-cost:  152
c ---[1895]---> BDD-cost:  152
c ---[1894]---> BDD-cost:  152
c ---[1893]---> BDD-cost:  105
c ---[1892]---> BDD-cost:  152
c ---[1891]---> BDD-cost:  105
c ---[1890]---> BDD-cost:  152
c ---[1889]---> BDD-cost:  107
c ---[1888]---> BDD-cost:  152
c ---[1887]---> BDD-cost:  103
c ---[1886]---> BDD-cost:  107
c ---[1885]---> BDD-cost:  152
c ---[1884]---> BDD-cost:  144
c ---[1883]---> BDD-cost:  152
c ---[1882]---> BDD-cost:  144
c ---[1881]---> BDD-cost:  152
c ---[1880]---> BDD-cost:  134
c ---[1879]---> BDD-cost:  152
c ---[1878]---> BDD-cost:  134
c ---[1877]---> BDD-cost:  152
c ---[1876]---> BDD-cost:  103
c ---[1875]---> BDD-cost:  103
c ---[1874]---> BDD-cost:  152
c ---[1873]---> BDD-cost:  103
c ---[1872]---> BDD-cost:   81
c ---[1871]---> BDD-cost:   85
c ---[1870]---> BDD-cost:   81
c ---[1869]---> BDD-cost:   85
c ---[1868]---> BDD-cost:   81
c ---[1867]---> BDD-cost:  148
c ---[1866]---> BDD-cost:   81
c ---[1865]---> BDD-cost:  103
c ---[1864]---> BDD-cost:  148
c ---[1863]---> BDD-cost:   81
c ---[1862]---> BDD-cost:  146
c ---[1861]---> BDD-cost:   81
c ---[1860]---> BDD-cost:  146
c ---[1859]---> BDD-cost:   81
c ---[1858]---> BDD-cost:  101
c ---[1857]---> BDD-cost:   81
c ---[1856]---> BDD-cost:  101
c ---[1855]---> BDD-cost:   81
c ---[1854]---> BDD-cost:  137
c ---[1853]---> BDD-cost:  137
c ---[1852]---> BDD-cost:   81
c ---[1851]---> BDD-cost:  137
c ---[1850]---> BDD-cost:   81
c ---[1849]---> BDD-cost:  110
c ---[1848]---> BDD-cost:   81
c ---[1847]---> BDD-cost:  110
c ---[1846]---> BDD-cost:   81
c ---[1845]---> BDD-cost:  154
c ---[1844]---> BDD-cost:   81
c ---[1843]---> BDD-cost:  103
c ---[1842]---> BDD-cost:   83
c ---[1841]---> BDD-cost:  154
c ---[1840]---> BDD-cost:   81
c ---[1839]---> BDD-cost:  153
c ---[1838]---> BDD-cost:   81
c ---[1837]---> BDD-cost:  153
c ---[1836]---> BDD-cost:   81
c ---[1835]---> BDD-cost:   99
c ---[1834]---> BDD-cost:   81
c ---[1833]---> BDD-cost:   99
c ---[1832]---> BDD-cost:   81
c ---[1831]---> BDD-cost:  137
c ---[1830]---> BDD-cost:  104
c ---[1829]---> BDD-cost:   81
c ---[1828]---> BDD-cost:  104
c ---[1827]---> BDD-cost:   81
c ---[1826]---> BDD-cost:   87
c ---[1825]---> BDD-cost:   81
c ---[1824]---> BDD-cost:   87
c ---[1823]---> BDD-cost:   81
c ---[1822]---> BDD-cost:   88
c ---[1821]---> BDD-cost:   81
c ---[1820]---> BDD-cost:   83
c ---[1819]---> BDD-cost:   88
c ---[1818]---> BDD-cost:   81
c ---[1817]---> BDD-cost:  155
c ---[1816]---> BDD-cost:   81
c ---[1815]---> BDD-cost:  155
c ---[1814]---> BDD-cost:   81
c ---[1813]---> BDD-cost:  148
c ---[1812]---> BDD-cost:   81
c ---[1811]---> BDD-cost:  148
c ---[1810]---> BDD-cost:   81
c ---[1809]---> BDD-cost:  137
c ---[1808]---> BDD-cost:  152
c ---[1807]---> BDD-cost:   81
c ---[1806]---> BDD-cost:  152
c ---[1805]---> BDD-cost:   81
c ---[1804]---> BDD-cost:  105
c ---[1803]---> BDD-cost:   81
c ---[1802]---> BDD-cost:  105
c ---[1801]---> BDD-cost:   81
c ---[1800]---> BDD-cost:  107
c ---[1799]---> BDD-cost:   81
c ---[1798]---> BDD-cost:  156
c ---[1797]---> BDD-cost:  107
c ---[1796]---> BDD-cost:   81
c ---[1795]---> BDD-cost:  144
c ---[1794]---> BDD-cost:   81
c ---[1793]---> BDD-cost:  144
c ---[1792]---> BDD-cost:   81
c ---[1791]---> BDD-cost:  134
c ---[1790]---> BDD-cost:   81
c ---[1789]---> BDD-cost:  134
c ---[1788]---> BDD-cost:   81
c ---[1787]---> BDD-cost:  137
c ---[1786]---> BDD-cost:  103
c ---[1785]---> BDD-cost:   81
c ---[1784]---> BDD-cost:  103
c ---[1783]---> BDD-cost:   85
c ---[1782]---> BDD-cost:  148
c ---[1781]---> BDD-cost:   85
c ---[1780]---> BDD-cost:  148
c ---[1779]---> BDD-cost:   85
c ---[1778]---> BDD-cost:  146
c ---[1777]---> BDD-cost:   85
c ---[1776]---> BDD-cost:  156
c ---[1775]---> BDD-cost:  146
c ---[1774]---> BDD-cost:   85
c ---[1773]---> BDD-cost:  101
c ---[1772]---> BDD-cost:   85
c ---[1771]---> BDD-cost:  101
c ---[1770]---> BDD-cost:   85
c ---[1769]---> BDD-cost:  137
c ---[1768]---> BDD-cost:   85
c ---[1767]---> BDD-cost:  137
c ---[1766]---> BDD-cost:   85
c ---[1765]---> BDD-cost:  137
c ---[1764]---> BDD-cost:  110
c ---[1763]---> BDD-cost:   85
c ---[1762]---> BDD-cost:  110
c ---[1761]---> BDD-cost:   85
c ---[1760]---> BDD-cost:  154
c ---[1759]---> BDD-cost:   85
c ---[1758]---> BDD-cost:  154
c ---[1757]---> BDD-cost:   85
c ---[1756]---> BDD-cost:  153
c ---[1755]---> BDD-cost:   85
c ---[1754]---> BDD-cost:  144
c ---[1753]---> BDD-cost:  153
c ---[1752]---> BDD-cost:   85
c ---[1751]---> BDD-cost:   99
c ---[1750]---> BDD-cost:   85
c ---[1749]---> BDD-cost:   99
c ---[1748]---> BDD-cost:   85
c ---[1747]---> BDD-cost:  104
c ---[1746]---> BDD-cost:   85
c ---[1745]---> BDD-cost:  104
c ---[1744]---> BDD-cost:   85
c ---[1743]---> BDD-cost:  137
c ---[1742]---> BDD-cost:   87
c ---[1741]---> BDD-cost:   85
c ---[1740]---> BDD-cost:   87
c ---[1739]---> BDD-cost:   85
c ---[1738]---> BDD-cost:   88
c ---[1737]---> BDD-cost:   85
c ---[1736]---> BDD-cost:   88
c ---[1735]---> BDD-cost:   85
c ---[1734]---> BDD-cost:  155
c ---[1733]---> BDD-cost:   85
c ---[1732]---> BDD-cost:  144
c ---[1731]---> BDD-cost:  144
c ---[1730]---> BDD-cost:  155
c ---[1729]---> BDD-cost:   85
c ---[1728]---> BDD-cost:  148
c ---[1727]---> BDD-cost:   85
c ---[1726]---> BDD-cost:  148
c ---[1725]---> BDD-cost:   85
c ---[1724]---> BDD-cost:  152
c ---[1723]---> BDD-cost:   85
c ---[1722]---> BDD-cost:  152
c ---[1721]---> BDD-cost:   85
c ---[1720]---> BDD-cost:  137
c ---[1719]---> BDD-cost:  105
c ---[1718]---> BDD-cost:   85
c ---[1717]---> BDD-cost:  105
c ---[1716]---> BDD-cost:   85
c ---[1715]---> BDD-cost:  107
c ---[1714]---> BDD-cost:   85
c ---[1713]---> BDD-cost:  107
c ---[1712]---> BDD-cost:   85
c ---[1711]---> BDD-cost:  144
c ---[1710]---> BDD-cost:   85
c ---[1709]---> BDD-cost:  134
c ---[1708]---> BDD-cost:  144
c ---[1707]---> BDD-cost:   85
c ---[1706]---> BDD-cost:  134
c ---[1705]---> BDD-cost:   85
c ---[1704]---> BDD-cost:  134
c ---[1703]---> BDD-cost:   85
c ---[1702]---> BDD-cost:  103
c ---[1701]---> BDD-cost:   85
c ---[1700]---> BDD-cost:  103
c ---[1699]---> BDD-cost:  148
c ---[1698]---> BDD-cost:  137
c ---[1697]---> BDD-cost:  146
c ---[1696]---> BDD-cost:  148
c ---[1695]---> BDD-cost:  146
c ---[1694]---> BDD-cost:  148
c ---[1693]---> BDD-cost:  101
c ---[1692]---> BDD-cost:  148
c ---[1691]---> BDD-cost:  101
c ---[1690]---> BDD-cost:  148
c ---[1689]---> BDD-cost:  137
c ---[1688]---> BDD-cost:  148
c ---[1687]---> BDD-cost:  134
c ---[1686]---> BDD-cost:  137
c ---[1685]---> BDD-cost:  148
c ---[1684]---> BDD-cost:  110
c ---[1683]---> BDD-cost:  148
c ---[1682]---> BDD-cost:  110
c ---[1681]---> BDD-cost:  148
c ---[1680]---> BDD-cost:  154
c ---[1679]---> BDD-cost:  148
c ---[1678]---> BDD-cost:  154
c ---[1677]---> BDD-cost:  148
c ---[1676]---> BDD-cost:  137
c ---[1675]---> BDD-cost:  153
c ---[1674]---> BDD-cost:  148
c ---[1673]---> BDD-cost:  153
c ---[1672]---> BDD-cost:  148
c ---[1671]---> BDD-cost:   99
c ---[1670]---> BDD-cost:  148
c ---[1669]---> BDD-cost:   99
c ---[1668]---> BDD-cost:  148
c ---[1667]---> BDD-cost:  104
c ---[1666]---> BDD-cost:  148
c ---[1665]---> BDD-cost:  143
c ---[1664]---> BDD-cost:  104
c ---[1663]---> BDD-cost:  148
c ---[1662]---> BDD-cost:   87
c ---[1661]---> BDD-cost:  148
c ---[1660]---> BDD-cost:   87
c ---[1659]---> BDD-cost:  148
c ---[1658]---> BDD-cost:   88
c ---[1657]---> BDD-cost:  148
c ---[1656]---> BDD-cost:   88
c ---[1655]---> BDD-cost:  148
c ---[1654]---> BDD-cost:  137
c ---[1653]---> BDD-cost:  155
c ---[1652]---> BDD-cost:  148
c ---[1651]---> BDD-cost:  155
c ---[1650]---> BDD-cost:  148
c ---[1649]---> BDD-cost:  148
c ---[1648]---> BDD-cost:  148
c ---[1647]---> BDD-cost:  148
c ---[1646]---> BDD-cost:  148
c ---[1645]---> BDD-cost:  152
c ---[1644]---> BDD-cost:  148
c ---[1643]---> BDD-cost:  143
c ---[1642]---> BDD-cost:  152
c ---[1641]---> BDD-cost:  148
c ---[1640]---> BDD-cost:  105
c ---[1639]---> BDD-cost:  148
c ---[1638]---> BDD-cost:  105
c ---[1637]---> BDD-cost:  148
c ---[1636]---> BDD-cost:  107
c ---[1635]---> BDD-cost:  148
c ---[1634]---> BDD-cost:  107
c ---[1633]---> BDD-cost:  148
c ---[1632]---> BDD-cost:  137
c ---[1631]---> BDD-cost:  144
c ---[1630]---> BDD-cost:  148
c ---[1629]---> BDD-cost:  144
c ---[1628]---> BDD-cost:  148
c ---[1627]---> BDD-cost:  134
c ---[1626]---> BDD-cost:  148
c ---[1625]---> BDD-cost:  134
c ---[1624]---> BDD-cost:  148
c ---[1623]---> BDD-cost:  103
c ---[1622]---> BDD-cost:  148
c ---[1621]---> BDD-cost:  103
c ---[1620]---> BDD-cost:  147
c ---[1619]---> BDD-cost:  103
c ---[1618]---> BDD-cost:  146
c ---[1617]---> BDD-cost:  101
c ---[1616]---> BDD-cost:  146
c ---[1615]---> BDD-cost:  101
c ---[1614]---> BDD-cost:  146
c ---[1613]---> BDD-cost:  137
c ---[1612]---> BDD-cost:  146
c ---[1611]---> BDD-cost:  137
c ---[1610]---> BDD-cost:  146
c ---[1609]---> BDD-cost:  137
c ---[1608]---> BDD-cost:  110
c ---[1607]---> BDD-cost:  146
c ---[1606]---> BDD-cost:  110
c ---[1605]---> BDD-cost:  146
c ---[1604]---> BDD-cost:  154
c ---[1603]---> BDD-cost:  146
c ---[1602]---> BDD-cost:  154
c ---[1601]---> BDD-cost:  146
c ---[1600]---> BDD-cost:  153
c ---[1599]---> BDD-cost:  146
c ---[1598]---> BDD-cost:  147
c ---[1597]---> BDD-cost:  153
c ---[1596]---> BDD-cost:  146
c ---[1595]---> BDD-cost:   99
c ---[1594]---> BDD-cost:  146
c ---[1593]---> BDD-cost:   99
c ---[1592]---> BDD-cost:  146
c ---[1591]---> BDD-cost:  104
c ---[1590]---> BDD-cost:  146
c ---[1589]---> BDD-cost:  104
c ---[1588]---> BDD-cost:  146
c ---[1587]---> BDD-cost:  137
c ---[1586]---> BDD-cost:   87
c ---[1585]---> BDD-cost:  146
c ---[1584]---> BDD-cost:   87
c ---[1583]---> BDD-cost:  146
c ---[1582]---> BDD-cost:   88
c ---[1581]---> BDD-cost:  146
c ---[1580]---> BDD-cost:   88
c ---[1579]---> BDD-cost:  146
c ---[1578]---> BDD-cost:  155
c ---[1577]---> BDD-cost:  146
c ---[1576]---> BDD-cost:  103
c ---[1575]---> BDD-cost:  155
c ---[1574]---> BDD-cost:  146
c ---[1573]---> BDD-cost:  148
c ---[1572]---> BDD-cost:  146
c ---[1571]---> BDD-cost:  148
c ---[1570]---> BDD-cost:  146
c ---[1569]---> BDD-cost:  152
c ---[1568]---> BDD-cost:  146
c ---[1567]---> BDD-cost:  152
c ---[1566]---> BDD-cost:  146
c ---[1565]---> BDD-cost:  137
c ---[1564]---> BDD-cost:  105
c ---[1563]---> BDD-cost:  146
c ---[1562]---> BDD-cost:  105
c ---[1561]---> BDD-cost:  146
c ---[1560]---> BDD-cost:  107
c ---[1559]---> BDD-cost:  146
c ---[1558]---> BDD-cost:  107
c ---[1557]---> BDD-cost:  146
c ---[1556]---> BDD-cost:  144
c ---[1555]---> BDD-cost:  146
c ---[1554]---> BDD-cost:  103
c ---[1553]---> BDD-cost:  144
c ---[1552]---> BDD-cost:  146
c ---[1551]---> BDD-cost:  134
c ---[1550]---> BDD-cost:  146
c ---[1549]---> BDD-cost:  134
c ---[1548]---> BDD-cost:  146
c ---[1547]---> BDD-cost:  103
c ---[1546]---> BDD-cost:  146
c ---[1545]---> BDD-cost:  103
c ---[1544]---> BDD-cost:  101
c ---[1543]---> BDD-cost:  137
c ---[1542]---> BDD-cost:  137
c ---[1541]---> BDD-cost:  101
c ---[1540]---> BDD-cost:  137
c ---[1539]---> BDD-cost:  101
c ---[1538]---> BDD-cost:  110
c ---[1537]---> BDD-cost:  101
c ---[1536]---> BDD-cost:  110
c ---[1535]---> BDD-cost:  101
c ---[1534]---> BDD-cost:  154
c ---[1533]---> BDD-cost:  101
c ---[1532]---> BDD-cost:   99
c ---[1531]---> BDD-cost:  154
c ---[1530]---> BDD-cost:  101
c ---[1529]---> BDD-cost:  153
c ---[1528]---> BDD-cost:  101
c ---[1527]---> BDD-cost:  153
c ---[1526]---> BDD-cost:  101
c ---[1525]---> BDD-cost:   99
c ---[1524]---> BDD-cost:  101
c ---[1523]---> BDD-cost:   99
c ---[1522]---> BDD-cost:  101
c ---[1521]---> BDD-cost:  137
c ---[1520]---> BDD-cost:  104
c ---[1519]---> BDD-cost:  101
c ---[1518]---> BDD-cost:  104
c ---[1517]---> BDD-cost:  101
c ---[1516]---> BDD-cost:   87
c ---[1515]---> BDD-cost:  101
c ---[1514]---> BDD-cost:   87
c ---[1513]---> BDD-cost:  101
c ---[1512]---> BDD-cost:   88
c ---[1511]---> BDD-cost:  101
c ---[1510]---> BDD-cost:  144
c ---[1509]---> BDD-cost:   99
c ---[1508]---> BDD-cost:   88
c ---[1507]---> BDD-cost:  101
c ---[1506]---> BDD-cost:  155
c ---[1505]---> BDD-cost:  101
c ---[1504]---> BDD-cost:  155
c ---[1503]---> BDD-cost:  101
c ---[1502]---> BDD-cost:  148
c ---[1501]---> BDD-cost:  101
c ---[1500]---> BDD-cost:  148
c ---[1499]---> BDD-cost:  101
c ---[1498]---> BDD-cost:  137
c ---[1497]---> BDD-cost:  152
c ---[1496]---> BDD-cost:  101
c ---[1495]---> BDD-cost:  152
c ---[1494]---> BDD-cost:  101
c ---[1493]---> BDD-cost:  105
c ---[1492]---> BDD-cost:  101
c ---[1491]---> BDD-cost:  105
c ---[1490]---> BDD-cost:  101
c ---[1489]---> BDD-cost:  107
c ---[1488]---> BDD-cost:  101
c ---[1487]---> BDD-cost:   99
c ---[1486]---> BDD-cost:  107
c ---[1485]---> BDD-cost:  101
c ---[1484]---> BDD-cost:  144
c ---[1483]---> BDD-cost:  101
c ---[1482]---> BDD-cost:  144
c ---[1481]---> BDD-cost:  101
c ---[1480]---> BDD-cost:  134
c ---[1479]---> BDD-cost:  101
c ---[1478]---> BDD-cost:  134
c ---[1477]---> BDD-cost:  101
c ---[1476]---> BDD-cost:  137
c ---[1475]---> BDD-cost:  103
c ---[1474]---> BDD-cost:  101
c ---[1473]---> BDD-cost:  103
c ---[1472]---> BDD-cost:  137
c ---[1471]---> BDD-cost:  110
c ---[1470]---> BDD-cost:  137
c ---[1469]---> BDD-cost:  110
c ---[1468]---> BDD-cost:  137
c ---[1467]---> BDD-cost:  154
c ---[1466]---> BDD-cost:  137
c ---[1465]---> BDD-cost:   99
c ---[1464]---> BDD-cost:  154
c ---[1463]---> BDD-cost:  137
c ---[1462]---> BDD-cost:  153
c ---[1461]---> BDD-cost:  137
c ---[1460]---> BDD-cost:  153
c ---[1459]---> BDD-cost:  137
c ---[1458]---> BDD-cost:   99
c ---[1457]---> BDD-cost:  137
c ---[1456]---> BDD-cost:   99
c ---[1455]---> BDD-cost:  137
c ---[1454]---> BDD-cost:  137
c ---[1453]---> BDD-cost:  104
c ---[1452]---> BDD-cost:  137
c ---[1451]---> BDD-cost:  104
c ---[1450]---> BDD-cost:  137
c ---[1449]---> BDD-cost:   87
c ---[1448]---> BDD-cost:  137
c ---[1447]---> BDD-cost:   87
c ---[1446]---> BDD-cost:  137
c ---[1445]---> BDD-cost:   88
c ---[1444]---> BDD-cost:  137
c ---[1443]---> BDD-cost:  152
c ---[1442]---> BDD-cost:   88
c ---[1441]---> BDD-cost:  137
c ---[1440]---> BDD-cost:  155
c ---[1439]---> BDD-cost:  137
c ---[1438]---> BDD-cost:  155
c ---[1437]---> BDD-cost:  137
c ---[1436]---> BDD-cost:  148
c ---[1435]---> BDD-cost:  137
c ---[1434]---> BDD-cost:  148
c ---[1433]---> BDD-cost:  137
c ---[1432]---> BDD-cost:  137
c ---[1431]---> BDD-cost:  152
c ---[1430]---> BDD-cost:  137
c ---[1429]---> BDD-cost:  152
c ---[1428]---> BDD-cost:  137
c ---[1427]---> BDD-cost:  105
c ---[1426]---> BDD-cost:  137
c ---[1425]---> BDD-cost:  105
c ---[1424]---> BDD-cost:  137
c ---[1423]---> BDD-cost:  107
c ---[1422]---> BDD-cost:  137
c ---[1421]---> BDD-cost:  152
c ---[1420]---> BDD-cost:  107
c ---[1419]---> BDD-cost:  137
c ---[1418]---> BDD-cost:  144
c ---[1417]---> BDD-cost:  137
c ---[1416]---> BDD-cost:  144
c ---[1415]---> BDD-cost:  137
c ---[1414]---> BDD-cost:  134
c ---[1413]---> BDD-cost:  137
c ---[1412]---> BDD-cost:  134
c ---[1411]---> BDD-cost:  137
c ---[1410]---> BDD-cost:  137
c ---[1409]---> BDD-cost:  103
c ---[1408]---> BDD-cost:  137
c ---[1407]---> BDD-cost:  103
c ---[1406]---> BDD-cost:  110
c ---[1405]---> BDD-cost:  154
c ---[1404]---> BDD-cost:  110
c ---[1403]---> BDD-cost:  154
c ---[1402]---> BDD-cost:  110
c ---[1401]---> BDD-cost:  153
c ---[1400]---> BDD-cost:  110
c ---[1399]---> BDD-cost:  103
c ---[1398]---> BDD-cost:   81
c ---[1397]---> BDD-cost:  153
c ---[1396]---> BDD-cost:  110
c ---[1395]---> BDD-cost:   99
c ---[1394]---> BDD-cost:  110
c ---[1393]---> BDD-cost:   99
c ---[1392]---> BDD-cost:  110
c ---[1391]---> BDD-cost:  104
c ---[1390]---> BDD-cost:  110
c ---[1389]---> BDD-cost:  104
c ---[1388]---> BDD-cost:  110
c ---[1387]---> BDD-cost:  137
c ---[1386]---> BDD-cost:   87
c ---[1385]---> BDD-cost:  110
c ---[1384]---> BDD-cost:   87
c ---[1383]---> BDD-cost:  110
c ---[1382]---> BDD-cost:   88
c ---[1381]---> BDD-cost:  110
c ---[1380]---> BDD-cost:   88
c ---[1379]---> BDD-cost:  110
c ---[1378]---> BDD-cost:  155
c ---[1377]---> BDD-cost:  110
c ---[1376]---> BDD-cost:   81
c ---[1375]---> BDD-cost:  155
c ---[1374]---> BDD-cost:  110
c ---[1373]---> BDD-cost:  148
c ---[1372]---> BDD-cost:  110
c ---[1371]---> BDD-cost:  148
c ---[1370]---> BDD-cost:  110
c ---[1369]---> BDD-cost:  152
c ---[1368]---> BDD-cost:  110
c ---[1367]---> BDD-cost:  152
c ---[1366]---> BDD-cost:  110
c ---[1365]---> BDD-cost:  137
c ---[1364]---> BDD-cost:  105
c ---[1363]---> BDD-cost:  110
c ---[1362]---> BDD-cost:  105
c ---[1361]---> BDD-cost:  110
c ---[1360]---> BDD-cost:  107
c ---[1359]---> BDD-cost:  110
c ---[1358]---> BDD-cost:  107
c ---[1357]---> BDD-cost:  110
c ---[1356]---> BDD-cost:  144
c ---[1355]---> BDD-cost:  110
c ---[1354]---> BDD-cost:   85
c ---[1353]---> BDD-cost:  144
c ---[1352]---> BDD-cost:  110
c ---[1351]---> BDD-cost:  134
c ---[1350]---> BDD-cost:  110
c ---[1349]---> BDD-cost:  134
c ---[1348]---> BDD-cost:  110
c ---[1347]---> BDD-cost:  103
c ---[1346]---> BDD-cost:  110
c ---[1345]---> BDD-cost:  103
c ---[1344]---> BDD-cost:  154
c ---[1343]---> BDD-cost:  137
c ---[1342]---> BDD-cost:  153
c ---[1341]---> BDD-cost:  154
c ---[1340]---> BDD-cost:  153
c ---[1339]---> BDD-cost:  154
c ---[1338]---> BDD-cost:   99
c ---[1337]---> BDD-cost:  154
c ---[1336]---> BDD-cost:   99
c ---[1335]---> BDD-cost:  154
c ---[1334]---> BDD-cost:  104
c ---[1333]---> BDD-cost:  154
c ---[1332]---> BDD-cost:   85
c ---[1331]---> BDD-cost:  104
c ---[1330]---> BDD-cost:  154
c ---[1329]---> BDD-cost:   87
c ---[1328]---> BDD-cost:  154
c ---[1327]---> BDD-cost:   87
c ---[1326]---> BDD-cost:  154
c ---[1325]---> BDD-cost:   88
c ---[1324]---> BDD-cost:  154
c ---[1323]---> BDD-cost:   88
c ---[1322]---> BDD-cost:  154
c ---[1321]---> BDD-cost:  137
c ---[1320]---> BDD-cost:  155
c ---[1319]---> BDD-cost:  154
c ---[1318]---> BDD-cost:  155
c ---[1317]---> BDD-cost:  154
c ---[1316]---> BDD-cost:  148
c ---[1315]---> BDD-cost:  154
c ---[1314]---> BDD-cost:  148
c ---[1313]---> BDD-cost:  154
c ---[1312]---> BDD-cost:  152
c ---[1311]---> BDD-cost:  154
c ---[1310]---> BDD-cost:  148
c ---[1309]---> BDD-cost:  152
c ---[1308]---> BDD-cost:  154
c ---[1307]---> BDD-cost:  105
c ---[1306]---> BDD-cost:  154
c ---[1305]---> BDD-cost:  105
c ---[1304]---> BDD-cost:  154
c ---[1303]---> BDD-cost:  107
c ---[1302]---> BDD-cost:  154
c ---[1301]---> BDD-cost:  107
c ---[1300]---> BDD-cost:  154
c ---[1299]---> BDD-cost:  137
c ---[1298]---> BDD-cost:  144
c ---[1297]---> BDD-cost:  154
c ---[1296]---> BDD-cost:  144
c ---[1295]---> BDD-cost:  154
c ---[1294]---> BDD-cost:  134
c ---[1293]---> BDD-cost:  154
c ---[1292]---> BDD-cost:  134
c ---[1291]---> BDD-cost:  154
c ---[1290]---> BDD-cost:  103
c ---[1289]---> BDD-cost:  154
c ---[1288]---> BDD-cost:  134
c ---[1287]---> BDD-cost:  148
c ---[1286]---> BDD-cost:  103
c ---[1285]---> BDD-cost:  153
c ---[1284]---> BDD-cost:   99
c ---[1283]---> BDD-cost:  153
c ---[1282]---> BDD-cost:   99
c ---[1281]---> BDD-cost:  153
c ---[1280]---> BDD-cost:  104
c ---[1279]---> BDD-cost:  153
c ---[1278]---> BDD-cost:  104
c ---[1277]---> BDD-cost:  153
c ---[1276]---> BDD-cost:  137
c ---[1275]---> BDD-cost:   87
c ---[1274]---> BDD-cost:  153
c ---[1273]---> BDD-cost:   87
c ---[1272]---> BDD-cost:  153
c ---[1271]---> BDD-cost:   88
c ---[1270]---> BDD-cost:  153
c ---[1269]---> BDD-cost:   88
c ---[1268]---> BDD-cost:  153
c ---[1267]---> BDD-cost:  155
c ---[1266]---> BDD-cost:  153
c ---[1265]---> BDD-cost:  146
c ---[1264]---> BDD-cost:  155
c ---[1263]---> BDD-cost:  153
c ---[1262]---> BDD-cost:  148
c ---[1261]---> BDD-cost:  153
c ---[1260]---> BDD-cost:  148
c ---[1259]---> BDD-cost:  153
c ---[1258]---> BDD-cost:  152
c ---[1257]---> BDD-cost:  153
c ---[1256]---> BDD-cost:  152
c ---[1255]---> BDD-cost:  153
c ---[1254]---> BDD-cost:  137
c ---[1253]---> BDD-cost:  105
c ---[1252]---> BDD-cost:  153
c ---[1251]---> BDD-cost:  105
c ---[1250]---> BDD-cost:  153
c ---[1249]---> BDD-cost:  107
c ---[1248]---> BDD-cost:  153
c ---[1247]---> BDD-cost:  107
c ---[1246]---> BDD-cost:  153
c ---[1245]---> BDD-cost:  144
c ---[1244]---> BDD-cost:  153
c ---[1243]---> BDD-cost:  146
c ---[1242]---> BDD-cost:  144
c ---[1241]---> BDD-cost:  153
c ---[1240]---> BDD-cost:  134
c ---[1239]---> BDD-cost:  153
c ---[1238]---> BDD-cost:  134
c ---[1237]---> BDD-cost:  153
c ---[1236]---> BDD-cost:  103
c ---[1235]---> BDD-cost:  153
c ---[1234]---> BDD-cost:  103
c ---[1233]---> BDD-cost:   99
c ---[1232]---> BDD-cost:  137
c ---[1231]---> BDD-cost:  104
c ---[1230]---> BDD-cost:   99
c ---[1229]---> BDD-cost:  104
c ---[1228]---> BDD-cost:   99
c ---[1227]---> BDD-cost:   87
c ---[1226]---> BDD-cost:   99
c ---[1225]---> BDD-cost:   87
c ---[1224]---> BDD-cost:   99
c ---[1223]---> BDD-cost:   88
c ---[1222]---> BDD-cost:   99
c ---[1221]---> BDD-cost:  101
c ---[1220]---> BDD-cost:   88
c ---[1219]---> BDD-cost:   99
c ---[1218]---> BDD-cost:  155
c ---[1217]---> BDD-cost:   99
c ---[1216]---> BDD-cost:  155
c ---[1215]---> BDD-cost:   99
c ---[1214]---> BDD-cost:  148
c ---[1213]---> BDD-cost:   99
c ---[1212]---> BDD-cost:  148
c ---[1211]---> BDD-cost:   99
c ---[1210]---> BDD-cost:  137
c ---[1209]---> BDD-cost:  152
c ---[1208]---> BDD-cost:   99
c ---[1207]---> BDD-cost:  152
c ---[1206]---> BDD-cost:   99
c ---[1205]---> BDD-cost:  105
c ---[1204]---> BDD-cost:   99
c ---[1203]---> BDD-cost:  105
c ---[1202]---> BDD-cost:   99
c ---[1201]---> BDD-cost:  107
c ---[1200]---> BDD-cost:   99
c ---[1199]---> BDD-cost:  101
c ---[1198]---> BDD-cost:  107
c ---[1197]---> BDD-cost:   99
c ---[1196]---> BDD-cost:  144
c ---[1195]---> BDD-cost:   99
c ---[1194]---> BDD-cost:  144
c ---[1193]---> BDD-cost:   99
c ---[1192]---> BDD-cost:  134
c ---[1191]---> BDD-cost:   99
c ---[1190]---> BDD-cost:  134
c ---[1189]---> BDD-cost:   99
c ---[1188]---> BDD-cost:  137
c ---[1187]---> BDD-cost:  103
c ---[1186]---> BDD-cost:   99
c ---[1185]---> BDD-cost:  103
c ---[1184]---> BDD-cost:  104
c ---[1183]---> BDD-cost:   87
c ---[1182]---> BDD-cost:  104
c ---[1181]---> BDD-cost:   87
c ---[1180]---> BDD-cost:  104
c ---[1179]---> BDD-cost:   88
c ---[1178]---> BDD-cost:  104
c ---[1177]---> BDD-cost:  103
c ---[1176]---> BDD-cost:  137
c ---[1175]---> BDD-cost:   88
c ---[1174]---> BDD-cost:  104
c ---[1173]---> BDD-cost:  155
c ---[1172]---> BDD-cost:  104
c ---[1171]---> BDD-cost:  155
c ---[1170]---> BDD-cost:  104
c ---[1169]---> BDD-cost:  148
c ---[1168]---> BDD-cost:  104
c ---[1167]---> BDD-cost:  148
c ---[1166]---> BDD-cost:  104
c ---[1165]---> BDD-cost:  137
c ---[1164]---> BDD-cost:  152
c ---[1163]---> BDD-cost:  104
c ---[1162]---> BDD-cost:  152
c ---[1161]---> BDD-cost:  104
c ---[1160]---> BDD-cost:  105
c ---[1159]---> BDD-cost:  104
c ---[1158]---> BDD-cost:  105
c ---[1157]---> BDD-cost:  104
c ---[1156]---> BDD-cost:  107
c ---[1155]---> BDD-cost:  104
c ---[1154]---> BDD-cost:  137
c ---[1153]---> BDD-cost:  107
c ---[1152]---> BDD-cost:  104
c ---[1151]---> BDD-cost:  144
c ---[1150]---> BDD-cost:  104
c ---[1149]---> BDD-cost:  144
c ---[1148]---> BDD-cost:  104
c ---[1147]---> BDD-cost:  134
c ---[1146]---> BDD-cost:  104
c ---[1145]---> BDD-cost:  134
c ---[1144]---> BDD-cost:  104
c ---[1143]---> BDD-cost:  137
c ---[1142]---> BDD-cost:  103
c ---[1141]---> BDD-cost:  104
c ---[1140]---> BDD-cost:  103
c ---[1139]---> BDD-cost:   87
c ---[1138]---> BDD-cost:   88
c ---[1137]---> BDD-cost:   87
c ---[1136]---> BDD-cost:   88
c ---[1135]---> BDD-cost:   87
c ---[1134]---> BDD-cost:  155
c ---[1133]---> BDD-cost:   87
c ---[1132]---> BDD-cost:  110
c ---[1131]---> BDD-cost:  155
c ---[1130]---> BDD-cost:   87
c ---[1129]---> BDD-cost:  148
c ---[1128]---> BDD-cost:   87
c ---[1127]---> BDD-cost:  148
c ---[1126]---> BDD-cost:   87
c ---[1125]---> BDD-cost:  152
c ---[1124]---> BDD-cost:   87
c ---[1123]---> BDD-cost:  152
c ---[1122]---> BDD-cost:   87
c ---[1121]---> BDD-cost:  137
c ---[1120]---> BDD-cost:  105
c ---[1119]---> BDD-cost:   87
c ---[1118]---> BDD-cost:  105
c ---[1117]---> BDD-cost:   87
c ---[1116]---> BDD-cost:  107
c ---[1115]---> BDD-cost:   87
c ---[1114]---> BDD-cost:  107
c ---[1113]---> BDD-cost:   87
c ---[1112]---> BDD-cost:  144
c ---[1111]---> BDD-cost:   87
c ---[1110]---> BDD-cost:  110
c ---[1109]---> BDD-cost:  144
c ---[1108]---> BDD-cost:   87
c ---[1107]---> BDD-cost:  134
c ---[1106]---> BDD-cost:   87
c ---[1105]---> BDD-cost:  134
c ---[1104]---> BDD-cost:   87
c ---[1103]---> BDD-cost:  103
c ---[1102]---> BDD-cost:   87
c ---[1101]---> BDD-cost:  103
c ---[1100]---> BDD-cost:   88
c ---[1099]---> BDD-cost:  137
c ---[1098]---> BDD-cost:  155
c ---[1097]---> BDD-cost:   88
c ---[1096]---> BDD-cost:  155
c ---[1095]---> BDD-cost:   88
c ---[1094]---> BDD-cost:  148
c ---[1093]---> BDD-cost:   88
c ---[1092]---> BDD-cost:  148
c ---[1091]---> BDD-cost:   88
c ---[1090]---> BDD-cost:  152
c ---[1089]---> BDD-cost:   88
c ---[1088]---> BDD-cost:  154
c ---[1087]---> BDD-cost:  152
c ---[1086]---> BDD-cost:   88
c ---[1085]---> BDD-cost:  105
c ---[1084]---> BDD-cost:   88
c ---[1083]---> BDD-cost:  105
c ---[1082]---> BDD-cost:   88
c ---[1081]---> BDD-cost:  107
c ---[1080]---> BDD-cost:   88
c ---[1079]---> BDD-cost:  107
c ---[1078]---> BDD-cost:   88
c ---[1077]---> BDD-cost:  137
c ---[1076]---> BDD-cost:  144
c ---[1075]---> BDD-cost:   88
c ---[1074]---> BDD-cost:  144
c ---[1073]---> BDD-cost:   88
c ---[1072]---> BDD-cost:  134
c ---[1071]---> BDD-cost:   88
c ---[1070]---> BDD-cost:  134
c ---[1069]---> BDD-cost:   88
c ---[1068]---> BDD-cost:  103
c ---[1067]---> BDD-cost:   88
c ---[1066]---> BDD-cost:  137
c ---[1065]---> BDD-cost:  134
c ---[1064]---> BDD-cost:  154
c ---[1063]---> BDD-cost:  103
c ---[1062]---> BDD-cost:  155
c ---[1061]---> BDD-cost:  148
c ---[1060]---> BDD-cost:  155
c ---[1059]---> BDD-cost:  148
c ---[1058]---> BDD-cost:  155
c ---[1057]---> BDD-cost:  152
c ---[1056]---> BDD-cost:  155
c ---[1055]---> BDD-cost:  152
c ---[1054]---> BDD-cost:  155
c ---[1053]---> BDD-cost:  137
c ---[1052]---> BDD-cost:  105
c ---[1051]---> BDD-cost:  155
c ---[1050]---> BDD-cost:  105
c ---[1049]---> BDD-cost:  155
c ---[1048]---> BDD-cost:  107
c ---[1047]---> BDD-cost:  155
c ---[1046]---> BDD-cost:  107
c ---[1045]---> BDD-cost:  155
c ---[1044]---> BDD-cost:  144
c ---[1043]---> BDD-cost:  155
c ---[1042]---> BDD-cost:  153
c ---[1041]---> BDD-cost:  144
c ---[1040]---> BDD-cost:  155
c ---[1039]---> BDD-cost:  134
c ---[1038]---> BDD-cost:  155
c ---[1037]---> BDD-cost:  134
c ---[1036]---> BDD-cost:  155
c ---[1035]---> BDD-cost:  103
c ---[1034]---> BDD-cost:  155
c ---[1033]---> BDD-cost:  103
c ---[1032]---> BDD-cost:  148
c ---[1031]---> BDD-cost:  137
c ---[1030]---> BDD-cost:  152
c ---[1029]---> BDD-cost:  148
c ---[1028]---> BDD-cost:  152
c ---[1027]---> BDD-cost:  148
c ---[1026]---> BDD-cost:  105
c ---[1025]---> BDD-cost:  148
c ---[1024]---> BDD-cost:  105
c ---[1023]---> BDD-cost:  148
c ---[1022]---> BDD-cost:  107
c ---[1021]---> BDD-cost:  148
c ---[1020]---> BDD-cost:  153
c ---[1019]---> BDD-cost:  107
c ---[1018]---> BDD-cost:  148
c ---[1017]---> BDD-cost:  144
c ---[1016]---> BDD-cost:  148
c ---[1015]---> BDD-cost:  144
c ---[1014]---> BDD-cost:  148
c ---[1013]---> BDD-cost:  134
c ---[1012]---> BDD-cost:  148
c ---[1011]---> BDD-cost:  134
c ---[1010]---> BDD-cost:  148
c ---[1009]---> BDD-cost:  137
c ---[1008]---> BDD-cost:  103
c ---[1007]---> BDD-cost:  148
c ---[1006]---> BDD-cost:  103
c ---[1005]---> BDD-cost:  152
c ---[1004]---> BDD-cost:  105
c ---[1003]---> BDD-cost:  152
c ---[1002]---> BDD-cost:  105
c ---[1001]---> BDD-cost:  152
c ---[1000]---> BDD-cost:  107
c ---[ 999]---> BDD-cost:  152
c ---[ 998]---> BDD-cost:   99
c ---[ 997]---> BDD-cost:  107
c ---[ 996]---> BDD-cost:  152
c ---[ 995]---> BDD-cost:  144
c ---[ 994]---> BDD-cost:  152
c ---[ 993]---> BDD-cost:  144
c ---[ 992]---> BDD-cost:  152
c ---[ 991]---> BDD-cost:  134
c ---[ 990]---> BDD-cost:  152
c ---[ 989]---> BDD-cost:  134
c ---[ 988]---> BDD-cost:  152
c ---[ 987]---> BDD-cost:  137
c ---[ 986]---> BDD-cost:  103
c ---[ 985]---> BDD-cost:  152
c ---[ 984]---> BDD-cost:  103
c ---[ 983]---> BDD-cost:  105
c ---[ 982]---> BDD-cost:  107
c ---[ 981]---> BDD-cost:  105
c ---[ 980]---> BDD-cost:  107
c ---[ 979]---> BDD-cost:  105
c ---[ 978]---> BDD-cost:  144
c ---[ 977]---> BDD-cost:  105
c ---[ 976]---> BDD-cost:   99
c ---[ 975]---> BDD-cost:  144
c ---[ 974]---> BDD-cost:  105
c ---[ 973]---> BDD-cost:  134
c ---[ 972]---> BDD-cost:  105
c ---[ 971]---> BDD-cost:  134
c ---[ 970]---> BDD-cost:  105
c ---[ 969]---> BDD-cost:  103
c ---[ 968]---> BDD-cost:  105
c ---[ 967]---> BDD-cost:  103
c ---[ 966]---> BDD-cost:  107
c ---[ 965]---> BDD-cost:  137
c ---[ 964]---> BDD-cost:  144
c ---[ 963]---> BDD-cost:  107
c ---[ 962]---> BDD-cost:  144
c ---[ 961]---> BDD-cost:  107
c ---[ 960]---> BDD-cost:  134
c ---[ 959]---> BDD-cost:  107
c ---[ 958]---> BDD-cost:  134
c ---[ 957]---> BDD-cost:  107
c ---[ 956]---> BDD-cost:  103
c ---[ 955]---> BDD-cost:  107
c ---[ 954]---> BDD-cost:  103
c ---[ 953]---> BDD-cost:  104
c ---[ 952]---> BDD-cost:  103
c ---[ 951]---> BDD-cost:  144
c ---[ 950]---> BDD-cost:  134
c ---[ 949]---> BDD-cost:  144
c ---[ 948]---> BDD-cost:  134
c ---[ 947]---> BDD-cost:  144
c ---[ 946]---> BDD-cost:  103
c ---[ 945]---> BDD-cost:  144
c ---[ 944]---> BDD-cost:  103
c ---[ 943]---> BDD-cost:  134
c ---[ 942]---> BDD-cost:  137
c ---[ 941]---> BDD-cost:  103
c ---[ 940]---> BDD-cost:  134
c ---[ 939]---> BDD-cost:  103
c ---[ 938]---> BDD-cost:  101
c ---[ 937]---> BDD-cost:  101
c ---[ 936]---> BDD-cost:  113
c ---[ 935]---> BDD-cost:  113
c ---[ 934]---> BDD-cost:   81
c ---[ 933]---> BDD-cost:   81
c ---[ 932]---> BDD-cost:  109
c ---[ 931]---> BDD-cost:  104
c ---[ 930]---> BDD-cost:  109
c ---[ 929]---> BDD-cost:  113
c ---[ 928]---> BDD-cost:  113
c ---[ 927]---> BDD-cost:  113
c ---[ 926]---> BDD-cost:  113
c ---[ 925]---> BDD-cost:  105
c ---[ 924]---> BDD-cost:  105
c ---[ 923]---> BDD-cost:  113
c ---[ 922]---> BDD-cost:  113
c ---[ 921]---> BDD-cost:  101
c ---[ 920]---> BDD-cost:  137
c ---[ 919]---> BDD-cost:  101
c ---[ 918]---> BDD-cost:   97
c ---[ 917]---> BDD-cost:   97
c ---[ 916]---> BDD-cost:   97
c ---[ 915]---> BDD-cost:   97
c ---[ 914]---> BDD-cost:  110
c ---[ 913]---> BDD-cost:  110
c ---[ 912]---> BDD-cost:   79
c ---[ 911]---> BDD-cost:   79
c ---[ 910]---> BDD-cost:   83
c ---[ 909]---> BDD-cost:   87
c ---[ 908]---> BDD-cost:   83
c ---[ 907]---> BDD-cost:  109
c ---[ 906]---> BDD-cost:  109
c ---[ 905]---> BDD-cost:  110
c ---[ 904]---> BDD-cost:  110
c ---[ 903]---> BDD-cost:   99
c ---[ 902]---> BDD-cost:   99
c ---[ 901]---> BDD-cost:  100
c ---[ 900]---> BDD-cost:  100
c ---[ 899]---> BDD-cost:  108
c ---[ 898]---> BDD-cost:  137
c ---[ 897]---> BDD-cost:  108
c ---[ 896]---> BDD-cost:  107
c ---[ 895]---> BDD-cost:  107
c ---[ 894]---> BDD-cost:  116
c ---[ 893]---> BDD-cost:  116
c ---[ 892]---> BDD-cost:   97
c ---[ 891]---> BDD-cost:   97
c ---[ 890]---> BDD-cost:  102
c ---[ 889]---> BDD-cost:  102
c ---[ 888]---> BDD-cost:   85
c ---[ 887]---> BDD-cost:   87
c ---[ 886]---> BDD-cost:   85
c ---[ 885]---> BDD-cost:   86
c ---[ 884]---> BDD-cost:   86
c ---[ 883]---> BDD-cost:  113
c ---[ 882]---> BDD-cost:  113
c ---[ 881]---> BDD-cost:  104
c ---[ 880]---> BDD-cost:  104
c ---[ 879]---> BDD-cost:  110
c ---[ 878]---> BDD-cost:  110
c ---[ 877]---> BDD-cost:   79
c ---[ 876]---> BDD-cost:  137
c ---[ 875]---> BDD-cost:   79
c ---[ 874]---> BDD-cost:  105
c ---[ 873]---> BDD-cost:  105
c ---[ 872]---> BDD-cost:  113
c ---[ 871]---> BDD-cost:  113
c ---[ 870]---> BDD-cost:  106
c ---[ 869]---> BDD-cost:  106
c ---[ 868]---> BDD-cost:  101
c ---[ 867]---> BDD-cost:  101
c ---[ 866]---> BDD-cost:   88
c ---[ 865]---> BDD-cost:  137
c ---[ 864]---> BDD-cost:  143
c ---[ 863]---> BDD-cost:   88
c ---[ 862]---> BDD-cost:  137
c ---[ 861]---> BDD-cost:  155
c ---[ 860]---> BDD-cost:  137
c ---[ 859]---> BDD-cost:  155
c ---[ 858]---> BDD-cost:  137
c ---[ 857]---> BDD-cost:  148
c ---[ 856]---> BDD-cost:  137
c ---[ 855]---> BDD-cost:  148
c ---[ 854]---> BDD-cost:  137
c ---[ 853]---> BDD-cost:  103
c ---[ 852]---> BDD-cost:  152
c ---[ 851]---> BDD-cost:  137
c ---[ 850]---> BDD-cost:  152
c ---[ 849]---> BDD-cost:  137
c ---[ 848]---> BDD-cost:  105
c ---[ 847]---> BDD-cost:  137
c ---[ 846]---> BDD-cost:  105
c ---[ 845]---> BDD-cost:  137
c ---[ 844]---> BDD-cost:  107
c ---[ 843]---> BDD-cost:  137
c ---[ 842]---> BDD-cost:  143
c ---[ 841]---> BDD-cost:  107
c ---[ 840]---> BDD-cost:  137
c ---[ 839]---> BDD-cost:  144
c ---[ 838]---> BDD-cost:  137
c ---[ 837]---> BDD-cost:  144
c ---[ 836]---> BDD-cost:  137
c ---[ 835]---> BDD-cost:  134
c ---[ 834]---> BDD-cost:  137
c ---[ 833]---> BDD-cost:  134
c ---[ 832]---> BDD-cost:  137
c ---[ 831]---> BDD-cost:  103
c ---[ 830]---> BDD-cost:  103
c ---[ 829]---> BDD-cost:  137
c ---[ 828]---> BDD-cost:  103
c ---[ 827]---> BDD-cost:   83
c ---[ 826]---> BDD-cost:  156
c ---[ 825]---> BDD-cost:   83
c ---[ 824]---> BDD-cost:  156
c ---[ 823]---> BDD-cost:   83
c ---[ 822]---> BDD-cost:  144
c ---[ 821]---> BDD-cost:   83
c ---[ 820]---> BDD-cost:  147
c ---[ 819]---> BDD-cost:  144
c ---[ 818]---> BDD-cost:   83
c ---[ 817]---> BDD-cost:  134
c ---[ 816]---> BDD-cost:   83
c ---[ 815]---> BDD-cost:  134
c ---[ 814]---> BDD-cost:   83
c ---[ 813]---> BDD-cost:  143
c ---[ 812]---> BDD-cost:   83
c ---[ 811]---> BDD-cost:  143
c ---[ 810]---> BDD-cost:   83
c ---[ 809]---> BDD-cost:  103
c ---[ 808]---> BDD-cost:  147
c ---[ 807]---> BDD-cost:   83
c ---[ 806]---> BDD-cost:  147
c ---[ 805]---> BDD-cost:   83
c ---[ 804]---> BDD-cost:  103
c ---[ 803]---> BDD-cost:   83
c ---[ 802]---> BDD-cost:  103
c ---[ 801]---> BDD-cost:   83
c ---[ 800]---> BDD-cost:   99
c ---[ 799]---> BDD-cost:   83
c ---[ 798]---> BDD-cost:  147
c ---[ 797]---> BDD-cost:   99
c ---[ 796]---> BDD-cost:   83
c ---[ 795]---> BDD-cost:   99
c ---[ 794]---> BDD-cost:   83
c ---[ 793]---> BDD-cost:   99
c ---[ 792]---> BDD-cost:   83
c ---[ 791]---> BDD-cost:  152
c ---[ 790]---> BDD-cost:   83
c ---[ 789]---> BDD-cost:  152
c ---[ 788]---> BDD-cost:   83
c ---[ 787]---> BDD-cost:  103
c ---[ 786]---> BDD-cost:   81
c ---[ 785]---> BDD-cost:   83
c ---[ 784]---> BDD-cost:   81
c ---[ 783]---> BDD-cost:   83
c ---[ 782]---> BDD-cost:   85
c ---[ 781]---> BDD-cost:   83
c ---[ 780]---> BDD-cost:   85
c ---[ 779]---> BDD-cost:   83
c ---[ 778]---> BDD-cost:  148
c ---[ 777]---> BDD-cost:   83
c ---[ 776]---> BDD-cost:  103
c ---[ 775]---> BDD-cost:  103
c ---[ 774]---> BDD-cost:  148
c ---[ 773]---> BDD-cost:   83
c ---[ 772]---> BDD-cost:  146
c ---[ 771]---> BDD-cost:   83
c ---[ 770]---> BDD-cost:  146
c ---[ 769]---> BDD-cost:   83
c ---[ 768]---> BDD-cost:  101
c ---[ 767]---> BDD-cost:   83
c ---[ 766]---> BDD-cost:  101
c ---[ 765]---> BDD-cost:   83
c ---[ 764]---> BDD-cost:  103
c ---[ 763]---> BDD-cost:  137
c ---[ 762]---> BDD-cost:   83
c ---[ 761]---> BDD-cost:  137
c ---[ 760]---> BDD-cost:   83
c ---[ 759]---> BDD-cost:  110
c ---[ 758]---> BDD-cost:   83
c ---[ 757]---> BDD-cost:  110
c ---[ 756]---> BDD-cost:   83
c ---[ 755]---> BDD-cost:  154
c ---[ 754]---> BDD-cost:   83
c ---[ 753]---> BDD-cost:  103
c ---[ 752]---> BDD-cost:  154
c ---[ 751]---> BDD-cost:   83
c ---[ 750]---> BDD-cost:  153
c ---[ 749]---> BDD-cost:   83
c ---[ 748]---> BDD-cost:  153
c ---[ 747]---> BDD-cost:   83
c ---[ 746]---> BDD-cost:   99
c ---[ 745]---> BDD-cost:   83
c ---[ 744]---> BDD-cost:   99
c ---[ 743]---> BDD-cost:   83
c ---[ 742]---> BDD-cost:  103
c ---[ 741]---> BDD-cost:  104
c ---[ 740]---> BDD-cost:   83
c ---[ 739]---> BDD-cost:  104
c ---[ 738]---> BDD-cost:   83
c ---[ 737]---> BDD-cost:   87
c ---[ 736]---> BDD-cost:   83
c ---[ 735]---> BDD-cost:   87
c ---[ 734]---> BDD-cost:   83
c ---[ 733]---> BDD-cost:   88
c ---[ 732]---> BDD-cost:   83
c ---[ 731]---> BDD-cost:   99
c ---[ 730]---> BDD-cost:   88
c ---[ 729]---> BDD-cost:   83
c ---[ 728]---> BDD-cost:  155
c ---[ 727]---> BDD-cost:   83
c ---[ 726]---> BDD-cost:  155
c ---[ 725]---> BDD-cost:   83
c ---[ 724]---> BDD-cost:  148
c ---[ 723]---> BDD-cost:   83
c ---[ 722]---> BDD-cost:  148
c ---[ 721]---> BDD-cost:   83
c ---[ 720]---> BDD-cost:  103
c ---[ 719]---> BDD-cost:  152
c ---[ 718]---> BDD-cost:   83
c ---[ 717]---> BDD-cost:  152
c ---[ 716]---> BDD-cost:   83
c ---[ 715]---> BDD-cost:  105
c ---[ 714]---> BDD-cost:   83
c ---[ 713]---> BDD-cost:  105
c ---[ 712]---> BDD-cost:   83
c ---[ 711]---> BDD-cost:  107
c ---[ 710]---> BDD-cost:   83
c ---[ 709]---> BDD-cost:   99
c ---[ 708]---> BDD-cost:  107
c ---[ 707]---> BDD-cost:   83
c ---[ 706]---> BDD-cost:  144
c ---[ 705]---> BDD-cost:   83
c ---[ 704]---> BDD-cost:  144
c ---[ 703]---> BDD-cost:   83
c ---[ 702]---> BDD-cost:  134
c ---[ 701]---> BDD-cost:   83
c ---[ 700]---> BDD-cost:  134
c ---[ 699]---> BDD-cost:   83
c ---[ 698]---> BDD-cost:  103
c ---[ 697]---> BDD-cost:  103
c ---[ 696]---> BDD-cost:   83
c ---[ 695]---> BDD-cost:  103
c ---[ 694]---> BDD-cost:  156
c ---[ 693]---> BDD-cost:  144
c ---[ 692]---> BDD-cost:  156
c ---[ 691]---> BDD-cost:  144
c ---[ 690]---> BDD-cost:  156
c ---[ 689]---> BDD-cost:  134
c ---[ 688]---> BDD-cost:  156
c ---[ 687]---> BDD-cost:   99
c ---[ 686]---> BDD-cost:  134
c ---[ 685]---> BDD-cost:  156
c ---[ 684]---> BDD-cost:  143
c ---[ 683]---> BDD-cost:  156
c ---[ 682]---> BDD-cost:  143
c ---[ 681]---> BDD-cost:  156
c ---[ 680]---> BDD-cost:  147
c ---[ 679]---> BDD-cost:  156
c ---[ 678]---> BDD-cost:  147
c ---[ 677]---> BDD-cost:  156
c ---[ 676]---> BDD-cost:  103
c ---[ 675]---> BDD-cost:  103
c ---[ 674]---> BDD-cost:  156
c ---[ 673]---> BDD-cost:  103
c ---[ 672]---> BDD-cost:  156
c ---[ 671]---> BDD-cost:   99
c ---[ 670]---> BDD-cost:  156
c ---[ 669]---> BDD-cost:   99
c ---[ 668]---> BDD-cost:  156
c ---[ 667]---> BDD-cost:   99
c ---[ 666]---> BDD-cost:  156
c ---[ 665]---> BDD-cost:  137
c ---[ 664]---> BDD-cost:   99
c ---[ 663]---> BDD-cost:   99
c ---[ 662]---> BDD-cost:  156
c ---[ 661]---> BDD-cost:  152
c ---[ 660]---> BDD-cost:  156
c ---[ 659]---> BDD-cost:  152
c ---[ 658]---> BDD-cost:  156
c ---[ 657]---> BDD-cost:   81
c ---[ 656]---> BDD-cost:  156
c ---[ 655]---> BDD-cost:   81
c ---[ 654]---> BDD-cost:  156
c ---[ 653]---> BDD-cost:  103
c ---[ 652]---> BDD-cost:   85
c ---[ 651]---> BDD-cost:  156
c ---[ 650]---> BDD-cost:   85
c ---[ 649]---> BDD-cost:  156
c ---[ 648]---> BDD-cost:  148
c ---[ 647]---> BDD-cost:  156
c ---[ 646]---> BDD-cost:  148
c ---[ 645]---> BDD-cost:  156
c ---[ 644]---> BDD-cost:  146
c ---[ 643]---> BDD-cost:  156
c ---[ 642]---> BDD-cost:  152
c ---[ 641]---> BDD-cost:  146
c ---[ 640]---> BDD-cost:  156
c ---[ 639]---> BDD-cost:  101
c ---[ 638]---> BDD-cost:  156
c ---[ 637]---> BDD-cost:  101
c ---[ 636]---> BDD-cost:  156
c ---[ 635]---> BDD-cost:  137
c ---[ 634]---> BDD-cost:  156
c ---[ 633]---> BDD-cost:  137
c ---[ 632]---> BDD-cost:  156
c ---[ 631]---> BDD-cost:  103
c ---[ 630]---> BDD-cost:  110
c ---[ 629]---> BDD-cost:  156
c ---[ 628]---> BDD-cost:  110
c ---[ 627]---> BDD-cost:  156
c ---[ 626]---> BDD-cost:  154
c ---[ 625]---> BDD-cost:  156
c ---[ 624]---> BDD-cost:  154
c ---[ 623]---> BDD-cost:  156
c ---[ 622]---> BDD-cost:  153
c ---[ 621]---> BDD-cost:  156
c ---[ 620]---> BDD-cost:  152
c ---[ 619]---> BDD-cost:  153
c ---[ 618]---> BDD-cost:  156
c ---[ 617]---> BDD-cost:   99
c ---[ 616]---> BDD-cost:  156
c ---[ 615]---> BDD-cost:   99
c ---[ 614]---> BDD-cost:  156
c ---[ 613]---> BDD-cost:  104
c ---[ 612]---> BDD-cost:  156
c ---[ 611]---> BDD-cost:  104
c ---[ 610]---> BDD-cost:  156
c ---[ 609]---> BDD-cost:  103
c ---[ 608]---> BDD-cost:   87
c ---[ 607]---> BDD-cost:  156
c ---[ 606]---> BDD-cost:   87
c ---[ 605]---> BDD-cost:  156
c ---[ 604]---> BDD-cost:   88
c ---[ 603]---> BDD-cost:  156
c ---[ 602]---> BDD-cost:   88
c ---[ 601]---> BDD-cost:  156
c ---[ 600]---> BDD-cost:  155
c ---[ 599]---> BDD-cost:  156
c ---[ 598]---> BDD-cost:   81
c ---[ 597]---> BDD-cost:  155
c ---[ 596]---> BDD-cost:  156
c ---[ 595]---> BDD-cost:  148
c ---[ 594]---> BDD-cost:  156
c ---[ 593]---> BDD-cost:  148
c ---[ 592]---> BDD-cost:  156
c ---[ 591]---> BDD-cost:  152
c ---[ 590]---> BDD-cost:  156
c ---[ 589]---> BDD-cost:  152
c ---[ 588]---> BDD-cost:  156
c ---[ 587]---> BDD-cost:  103
c ---[ 586]---> BDD-cost:  105
c ---[ 585]---> BDD-cost:  156
c ---[ 584]---> BDD-cost:  105
c ---[ 583]---> BDD-cost:  156
c ---[ 582]---> BDD-cost:  107
c ---[ 581]---> BDD-cost:  156
c ---[ 580]---> BDD-cost:  107
c ---[ 579]---> BDD-cost:  156
c ---[ 578]---> BDD-cost:  144
c ---[ 577]---> BDD-cost:  156
c ---[ 576]---> BDD-cost:   81
c ---[ 575]---> BDD-cost:  144
c ---[ 574]---> BDD-cost:  156
c ---[ 573]---> BDD-cost:  134
c ---[ 572]---> BDD-cost:  156
c ---[ 571]---> BDD-cost:  134
c ---[ 570]---> BDD-cost:  156
c ---[ 569]---> BDD-cost:  103
c ---[ 568]---> BDD-cost:  156
c ---[ 567]---> BDD-cost:  103
c ---[ 566]---> BDD-cost:  144
c ---[ 565]---> BDD-cost:  103
c ---[ 564]---> BDD-cost:  134
c ---[ 563]---> BDD-cost:  144
c ---[ 562]---> BDD-cost:  134
c ---[ 561]---> BDD-cost:  144
c ---[ 560]---> BDD-cost:  143
c ---[ 559]---> BDD-cost:  144
c ---[ 558]---> BDD-cost:  143
c ---[ 557]---> BDD-cost:  144
c ---[ 556]---> BDD-cost:  147
c ---[ 555]---> BDD-cost:  144
c ---[ 554]---> BDD-cost:  103
c ---[ 553]---> BDD-cost:   85
c ---[ 552]---> BDD-cost:  147
c ---[ 551]---> BDD-cost:  144
c ---[ 550]---> BDD-cost:  103
c ---[ 549]---> BDD-cost:  144
c ---[ 548]---> BDD-cost:  103
c ---[ 547]---> BDD-cost:  144
c ---[ 546]---> BDD-cost:   99
c ---[ 545]---> BDD-cost:  144
c ---[ 544]---> BDD-cost:   99
c ---[ 543]---> BDD-cost:  144
c ---[ 542]---> BDD-cost:  103
c ---[ 541]---> BDD-cost:   99
c ---[ 540]---> BDD-cost:  144
c ---[ 539]---> BDD-cost:   99
c ---[ 538]---> BDD-cost:  144
c ---[ 537]---> BDD-cost:  152
c ---[ 536]---> BDD-cost:  144
c ---[ 535]---> BDD-cost:  152
c ---[ 534]---> BDD-cost:  144
c ---[ 533]---> BDD-cost:   81
c ---[ 532]---> BDD-cost:  144
c ---[ 531]---> BDD-cost:   85
c ---[ 530]---> BDD-cost:   81
c ---[ 529]---> BDD-cost:  144
c ---[ 528]---> BDD-cost:   85
c ---[ 527]---> BDD-cost:  144
c ---[ 526]---> BDD-cost:   85
c ---[ 525]---> BDD-cost:  144
c ---[ 524]---> BDD-cost:  148
c ---[ 523]---> BDD-cost:  144
c ---[ 522]---> BDD-cost:  148
c ---[ 521]---> BDD-cost:  144
c ---[ 520]---> BDD-cost:  103
c ---[ 519]---> BDD-cost:  146
c ---[ 518]---> BDD-cost:  144
c ---[ 517]---> BDD-cost:  146
c ---[ 516]---> BDD-cost:  144
c ---[ 515]---> BDD-cost:  101
c ---[ 514]---> BDD-cost:  144
c ---[ 513]---> BDD-cost:  101
c ---[ 512]---> BDD-cost:  144
c ---[ 511]---> BDD-cost:  137
c ---[ 510]---> BDD-cost:  144
c ---[ 509]---> BDD-cost:  148
c ---[ 508]---> BDD-cost:  137
c ---[ 507]---> BDD-cost:  144
c ---[ 506]---> BDD-cost:  110
c ---[ 505]---> BDD-cost:  144
c ---[ 504]---> BDD-cost:  110
c ---[ 503]---> BDD-cost:  144
c ---[ 502]---> BDD-cost:  154
c ---[ 501]---> BDD-cost:  144
c ---[ 500]---> BDD-cost:  154
c ---[ 499]---> BDD-cost:  144
c ---[ 498]---> BDD-cost:  103
c ---[ 497]---> BDD-cost:  153
c ---[ 496]---> BDD-cost:  144
c ---[ 495]---> BDD-cost:  153
c ---[ 494]---> BDD-cost:  144
c ---[ 493]---> BDD-cost:   99
c ---[ 492]---> BDD-cost:  144
c ---[ 491]---> BDD-cost:   99
c ---[ 490]---> BDD-cost:  144
c ---[ 489]---> BDD-cost:  104
c ---[ 488]---> BDD-cost:  144
c ---[ 487]---> BDD-cost:  148
c ---[ 486]---> BDD-cost:  104
c ---[ 485]---> BDD-cost:  144
c ---[ 484]---> BDD-cost:   87
c ---[ 483]---> BDD-cost:  144
c ---[ 482]---> BDD-cost:   87
c ---[ 481]---> BDD-cost:  144
c ---[ 480]---> BDD-cost:   88
c ---[ 479]---> BDD-cost:  144
c ---[ 478]---> BDD-cost:   88
c ---[ 477]---> BDD-cost:  144
c ---[ 476]---> BDD-cost:  103
c ---[ 475]---> BDD-cost:  155
c ---[ 474]---> BDD-cost:  144
c ---[ 473]---> BDD-cost:  155
c ---[ 472]---> BDD-cost:  144
c ---[ 471]---> BDD-cost:  148
c ---[ 470]---> BDD-cost:  144
c ---[ 469]---> BDD-cost:  148
c ---[ 468]---> BDD-cost:  144
c ---[ 467]---> BDD-cost:  152
c ---[ 466]---> BDD-cost:  144
c ---[ 465]---> BDD-cost:  146
c ---[ 464]---> BDD-cost:  152
c ---[ 463]---> BDD-cost:  144
c ---[ 462]---> BDD-cost:  105
c ---[ 461]---> BDD-cost:  144
c ---[ 460]---> BDD-cost:  105
c ---[ 459]---> BDD-cost:  144
c ---[ 458]---> BDD-cost:  107
c ---[ 457]---> BDD-cost:  144
c ---[ 456]---> BDD-cost:  107
c ---[ 455]---> BDD-cost:  144
c ---[ 454]---> BDD-cost:  103
c ---[ 453]---> BDD-cost:  144
c ---[ 452]---> BDD-cost:  144
c ---[ 451]---> BDD-cost:  144
c ---[ 450]---> BDD-cost:  144
c ---[ 449]---> BDD-cost:  134
c ---[ 448]---> BDD-cost:  144
c ---[ 447]---> BDD-cost:  134
c ---[ 446]---> BDD-cost:  144
c ---[ 445]---> BDD-cost:  103
c ---[ 444]---> BDD-cost:  144
c ---[ 443]---> BDD-cost:   83
c ---[ 442]---> BDD-cost:  146
c ---[ 441]---> BDD-cost:  103
c ---[ 440]---> BDD-cost:  134
c ---[ 439]---> BDD-cost:  143
c ---[ 438]---> BDD-cost:  134
c ---[ 437]---> BDD-cost:  143
c ---[ 436]---> BDD-cost:  134
c ---[ 435]---> BDD-cost:  147
c ---[ 434]---> BDD-cost:  134
c ---[ 433]---> BDD-cost:  147
c ---[ 432]---> BDD-cost:  134
c ---[ 431]---> BDD-cost:  103
c ---[ 430]---> BDD-cost:  103
c ---[ 429]---> BDD-cost:  134
c ---[ 428]---> BDD-cost:  103
c ---[ 427]---> BDD-cost:  134
c ---[ 426]---> BDD-cost:   99
c ---[ 425]---> BDD-cost:  134
c ---[ 424]---> BDD-cost:   99
c ---[ 423]---> BDD-cost:  134
c ---[ 422]---> BDD-cost:   99
c ---[ 421]---> BDD-cost:  134
c ---[ 420]---> BDD-cost:  101
c ---[ 419]---> BDD-cost:   99
c ---[ 418]---> BDD-cost:  134
c ---[ 417]---> BDD-cost:  152
c ---[ 416]---> BDD-cost:  134
c ---[ 415]---> BDD-cost:  152
c ---[ 414]---> BDD-cost:  134
c ---[ 413]---> BDD-cost:   81
c ---[ 412]---> BDD-cost:  134
c ---[ 411]---> BDD-cost:   81
c ---[ 410]---> BDD-cost:  134
c ---[ 409]---> BDD-cost:  103
c ---[ 408]---> BDD-cost:   85
c ---[ 407]---> BDD-cost:  134
c ---[ 406]---> BDD-cost:   85
c ---[ 405]---> BDD-cost:  134
c ---[ 404]---> BDD-cost:  148
c ---[ 403]---> BDD-cost:  134
c ---[ 402]---> BDD-cost:  148
c ---[ 401]---> BDD-cost:  134
c ---[ 400]---> BDD-cost:  146
c ---[ 399]---> BDD-cost:  134
c ---[ 398]---> BDD-cost:  101
c ---[ 397]---> BDD-cost:  146
c ---[ 396]---> BDD-cost:  134
c ---[ 395]---> BDD-cost:  101
c ---[ 394]---> BDD-cost:  134
c ---[ 393]---> BDD-cost:  101
c ---[ 392]---> BDD-cost:  134
c ---[ 391]---> BDD-cost:  137
c ---[ 390]---> BDD-cost:  134
c ---[ 389]---> BDD-cost:  137
c ---[ 388]---> BDD-cost:  134
c ---[ 387]---> BDD-cost:  103
c ---[ 386]---> BDD-cost:  110
c ---[ 385]---> BDD-cost:  134
c ---[ 384]---> BDD-cost:  110
c ---[ 383]---> BDD-cost:  134
c ---[ 382]---> BDD-cost:  154
c ---[ 381]---> BDD-cost:  134
c ---[ 380]---> BDD-cost:  154
c ---[ 379]---> BDD-cost:  134
c ---[ 378]---> BDD-cost:  153
c ---[ 377]---> BDD-cost:  134
c ---[ 376]---> BDD-cost:  137
c ---[ 375]---> BDD-cost:  153
c ---[ 374]---> BDD-cost:  134
c ---[ 373]---> BDD-cost:   99
c ---[ 372]---> BDD-cost:  134
c ---[ 371]---> BDD-cost:   99
c ---[ 370]---> BDD-cost:  134
c ---[ 369]---> BDD-cost:  104
c ---[ 368]---> BDD-cost:  134
c ---[ 367]---> BDD-cost:  104
c ---[ 366]---> BDD-cost:  134
c ---[ 365]---> BDD-cost:  103
c ---[ 364]---> BDD-cost:   87
c ---[ 363]---> BDD-cost:  134
c ---[ 362]---> BDD-cost:   87
c ---[ 361]---> BDD-cost:  134
c ---[ 360]---> BDD-cost:   88
c ---[ 359]---> BDD-cost:  134
c ---[ 358]---> BDD-cost:   88
c ---[ 357]---> BDD-cost:  134
c ---[ 356]---> BDD-cost:  155
c ---[ 355]---> BDD-cost:  134
c ---[ 354]---> BDD-cost:  137
c ---[ 353]---> BDD-cost:  155
c ---[ 352]---> BDD-cost:  134
c ---[ 351]---> BDD-cost:  148
c ---[ 350]---> BDD-cost:  134
c ---[ 349]---> BDD-cost:  148
c ---[ 348]---> BDD-cost:  134
c ---[ 347]---> BDD-cost:  152
c ---[ 346]---> BDD-cost:  134
c ---[ 345]---> BDD-cost:  152
c ---[ 344]---> BDD-cost:  134
c ---[ 343]---> BDD-cost:  103
c ---[ 342]---> BDD-cost:  105
c ---[ 341]---> BDD-cost:  134
c ---[ 340]---> BDD-cost:  105
c ---[ 339]---> BDD-cost:  134
c ---[ 338]---> BDD-cost:  107
c ---[ 337]---> BDD-cost:  134
c ---[ 336]---> BDD-cost:  107
c ---[ 335]---> BDD-cost:  134
c ---[ 334]---> BDD-cost:  144
c ---[ 333]---> BDD-cost:  134
c ---[ 332]---> BDD-cost:  103
c ---[ 331]---> BDD-cost:  110
c ---[ 330]---> BDD-cost:  144
c ---[ 329]---> BDD-cost:  134
c ---[ 328]---> BDD-cost:  134
c ---[ 327]---> BDD-cost:  134
c ---[ 326]---> BDD-cost:  134
c ---[ 325]---> BDD-cost:  134
c ---[ 324]---> BDD-cost:  103
c ---[ 323]---> BDD-cost:  134
c ---[ 322]---> BDD-cost:  103
c ---[ 321]---> BDD-cost:  143
c ---[ 320]---> BDD-cost:  103
c ---[ 319]---> BDD-cost:  147
c ---[ 318]---> BDD-cost:  143
c ---[ 317]---> BDD-cost:  147
c ---[ 316]---> BDD-cost:  143
c ---[ 315]---> BDD-cost:  103
c ---[ 314]---> BDD-cost:  143
c ---[ 313]---> BDD-cost:  103
c ---[ 312]---> BDD-cost:  143
c ---[ 311]---> BDD-cost:   99
c ---[ 310]---> BDD-cost:  143
c ---[ 309]---> BDD-cost:  110
c ---[ 308]---> BDD-cost:   99
c ---[ 307]---> BDD-cost:  143
c ---[ 306]---> BDD-cost:   99
c ---[ 305]---> BDD-cost:  143
c ---[ 304]---> BDD-cost:   99
c ---[ 303]---> BDD-cost:  143
c ---[ 302]---> BDD-cost:  152
c ---[ 301]---> BDD-cost:  143
c ---[ 300]---> BDD-cost:  152
c ---[ 299]---> BDD-cost:  143
c ---[ 298]---> BDD-cost:  103
c ---[ 297]---> BDD-cost:   81
c ---[ 296]---> BDD-cost:  143
c ---[ 295]---> BDD-cost:   81
c ---[ 294]---> BDD-cost:  143
c ---[ 293]---> BDD-cost:   85
c ---[ 292]---> BDD-cost:  143
c ---[ 291]---> BDD-cost:   85
c ---[ 290]---> BDD-cost:  143
c ---[ 289]---> BDD-cost:  148
c ---[ 288]---> BDD-cost:  143
c ---[ 287]---> BDD-cost:  154
c ---[ 286]---> BDD-cost:  148
c ---[ 285]---> BDD-cost:  143
c ---[ 284]---> BDD-cost:  146
c ---[ 283]---> BDD-cost:  143
c ---[ 282]---> BDD-cost:  146
c ---[ 281]---> BDD-cost:  143
c ---[ 280]---> BDD-cost:  101
c ---[ 279]---> BDD-cost:  143
c ---[ 278]---> BDD-cost:  101
c ---[ 277]---> BDD-cost:  143
c ---[ 276]---> BDD-cost:  103
c ---[ 275]---> BDD-cost:  137
c ---[ 274]---> BDD-cost:  143
c ---[ 273]---> BDD-cost:  137
c ---[ 272]---> BDD-cost:  143
c ---[ 271]---> BDD-cost:  110
c ---[ 270]---> BDD-cost:  143
c ---[ 269]---> BDD-cost:  110
c ---[ 268]---> BDD-cost:  143
c ---[ 267]---> BDD-cost:  154
c ---[ 266]---> BDD-cost:  143
c ---[ 265]---> BDD-cost:  154
c ---[ 264]---> BDD-cost:  154
c ---[ 263]---> BDD-cost:  143
c ---[ 262]---> BDD-cost:  153
c ---[ 261]---> BDD-cost:  143
c ---[ 260]---> BDD-cost:  153
c ---[ 259]---> BDD-cost:  143
c ---[ 258]---> BDD-cost:   99
c ---[ 257]---> BDD-cost:  143
c ---[ 256]---> BDD-cost:   99
c ---[ 255]---> BDD-cost:  143
c ---[ 254]---> BDD-cost:  103
c ---[ 253]---> BDD-cost:  104
c ---[ 252]---> BDD-cost:  143
c ---[ 251]---> BDD-cost:  104
c ---[ 250]---> BDD-cost:  143
c ---[ 249]---> BDD-cost:   87
c ---[ 248]---> BDD-cost:  143
c ---[ 247]---> BDD-cost:   87
c ---[ 246]---> BDD-cost:  143
c ---[ 245]---> BDD-cost:   88
c ---[ 244]---> BDD-cost:  143
c ---[ 243]---> BDD-cost:  153
c ---[ 242]---> BDD-cost:   88
c ---[ 241]---> BDD-cost:  143
c ---[ 240]---> BDD-cost:  155
c ---[ 239]---> BDD-cost:  143
c ---[ 238]---> BDD-cost:  155
c ---[ 237]---> BDD-cost:  143
c ---[ 236]---> BDD-cost:  148
c ---[ 235]---> BDD-cost:  143
c ---[ 234]---> BDD-cost:  148
c ---[ 233]---> BDD-cost:  143
c ---[ 232]---> BDD-cost:  103
c ---[ 231]---> BDD-cost:  152
c ---[ 230]---> BDD-cost:  143
c ---[ 229]---> BDD-cost:  152
c ---[ 228]---> BDD-cost:  143
c ---[ 227]---> BDD-cost:  105
c ---[ 226]---> BDD-cost:  143
c ---[ 225]---> BDD-cost:  105
c ---[ 224]---> BDD-cost:  143
c ---[ 223]---> BDD-cost:  107
c ---[ 222]---> BDD-cost:  143
c ---[ 221]---> BDD-cost:   83
c ---[ 220]---> BDD-cost:  153
c ---[ 219]---> BDD-cost:  107
c ---[ 218]---> BDD-cost:  143
c ---[ 217]---> BDD-cost:  144
c ---[ 216]---> BDD-cost:  143
c ---[ 215]---> BDD-cost:  144
c ---[ 214]---> BDD-cost:  143
c ---[ 213]---> BDD-cost:  134
c ---[ 212]---> BDD-cost:  143
c ---[ 211]---> BDD-cost:  134
c ---[ 210]---> BDD-cost:  143
c ---[ 209]---> BDD-cost:  103
c ---[ 208]---> BDD-cost:  103
c ---[ 207]---> BDD-cost:  143
c ---[ 206]---> BDD-cost:  103
c ---[ 205]---> BDD-cost:  147
c ---[ 204]---> BDD-cost:  103
c ---[ 203]---> BDD-cost:  147
c ---[ 202]---> BDD-cost:  103
c ---[ 201]---> BDD-cost:  147
c ---[ 200]---> BDD-cost:   99
c ---[ 199]---> BDD-cost:  147
c ---[ 198]---> BDD-cost:   99
c ---[ 197]---> BDD-cost:   99
c ---[ 196]---> BDD-cost:  147
c ---[ 195]---> BDD-cost:   99
c ---[ 194]---> BDD-cost:  147
c ---[ 193]---> BDD-cost:   99
c ---[ 192]---> BDD-cost:  147
c ---[ 191]---> BDD-cost:  152
c ---[ 190]---> BDD-cost:  147
c ---[ 189]---> BDD-cost:  152
c ---[ 188]---> BDD-cost:  147
c ---[ 187]---> BDD-cost:  103
c ---[ 186]---> BDD-cost:   81
c ---[ 185]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:   81
c ---[ 183]---> BDD-cost:  147
c ---[ 182]---> BDD-cost:   85
c ---[ 181]---> BDD-cost:  147
c ---[ 180]---> BDD-cost:   85
c ---[ 179]---> BDD-cost:  147
c ---[ 178]---> BDD-cost:  148
c ---[ 177]---> BDD-cost:  147
c ---[ 176]---> BDD-cost:   99
c ---[ 175]---> BDD-cost:  148
c ---[ 174]---> BDD-cost:  147
c ---[ 173]---> BDD-cost:  146
c ---[ 172]---> BDD-cost:  147
c ---[ 171]---> BDD-cost:  146
c ---[ 170]---> BDD-cost:  147
c ---[ 169]---> BDD-cost:  101
c ---[ 168]---> BDD-cost:  147
c ---[ 167]---> BDD-cost:  101
c ---[ 166]---> BDD-cost:  147
c ---[ 165]---> BDD-cost:  103
c ---[ 164]---> BDD-cost:  137
c ---[ 163]---> BDD-cost:  147
c ---[ 162]---> BDD-cost:  137
c ---[ 161]---> BDD-cost:  147
c ---[ 160]---> BDD-cost:  110
c ---[ 159]---> BDD-cost:  147
c ---[ 158]---> BDD-cost:  110
c ---[ 157]---> BDD-cost:  147
c ---[ 156]---> BDD-cost:  154
c ---[ 155]---> BDD-cost:  147
c ---[ 154]---> BDD-cost:  104
c ---[ 153]---> BDD-cost:  154
c ---[ 152]---> BDD-cost:  147
c ---[ 151]---> BDD-cost:  153
c ---[ 150]---> BDD-cost:  147
c ---[ 149]---> BDD-cost:  153
c ---[ 148]---> BDD-cost:  147
c ---[ 147]---> BDD-cost:   99
c ---[ 146]---> BDD-cost:  147
c ---[ 145]---> BDD-cost:   99
c ---[ 144]---> BDD-cost:  147
c ---[ 143]---> BDD-cost:  103
c ---[ 142]---> BDD-cost:  104
c ---[ 141]---> BDD-cost:  147
c ---[ 140]---> BDD-cost:  104
c ---[ 139]---> BDD-cost:  147
c ---[ 138]---> BDD-cost:   87
c ---[ 137]---> BDD-cost:  147
c ---[ 136]---> BDD-cost:   87
c ---[ 135]---> BDD-cost:  147
c ---[ 134]---> BDD-cost:   88
c ---[ 133]---> BDD-cost:  147
c ---[ 132]---> BDD-cost:  104
c ---[ 131]---> BDD-cost:   88
c ---[ 130]---> BDD-cost:  147
c ---[ 129]---> BDD-cost:  155
c ---[ 128]---> BDD-cost:  147
c ---[ 127]---> BDD-cost:  155
c ---[ 126]---> BDD-cost:  147
c ---[ 125]---> BDD-cost:  148
c ---[ 124]---> BDD-cost:  147
c ---[ 123]---> BDD-cost:  148
c ---[ 122]---> BDD-cost:  147
c ---[ 121]---> BDD-cost:  103
c ---[ 120]---> BDD-cost:  152
c ---[ 119]---> BDD-cost:  147
c ---[ 118]---> BDD-cost:  152
c ---[ 117]---> BDD-cost:  147
c ---[ 116]---> BDD-cost:  105
c ---[ 115]---> BDD-cost:  147
c ---[ 114]---> BDD-cost:  105
c ---[ 113]---> BDD-cost:  147
c ---[ 112]---> BDD-cost:  107
c ---[ 111]---> BDD-cost:  147
c ---[ 110]---> BDD-cost:  103
c ---[ 109]---> BDD-cost:   87
c ---[ 108]---> BDD-cost:  107
c ---[ 107]---> BDD-cost:  147
c ---[ 106]---> BDD-cost:  144
c ---[ 105]---> BDD-cost:  147
c ---[ 104]---> BDD-cost:  144
c ---[ 103]---> BDD-cost:  147
c ---[ 102]---> BDD-cost:  134
c ---[ 101]---> BDD-cost:  147
c ---[ 100]---> BDD-cost:  134
c ---[  99]---> BDD-cost:  147
c ---[  98]---> BDD-cost:  103
c ---[  97]---> BDD-cost:  103
c ---[  96]---> BDD-cost:  147
c ---[  95]---> BDD-cost:  103
c ---[  94]---> BDD-cost:  103
c ---[  93]---> BDD-cost:   99
c ---[  92]---> BDD-cost:  103
c ---[  91]---> BDD-cost:   99
c ---[  90]---> BDD-cost:  103
c ---[  89]---> BDD-cost:   99
c ---[  88]---> BDD-cost:  103
c ---[  87]---> BDD-cost:   87
c ---[  86]---> BDD-cost:   99
c ---[  85]---> BDD-cost:  103
c ---[  84]---> BDD-cost:  152
c ---[  83]---> BDD-cost:  103
c ---[  82]---> BDD-cost:  152
c ---[  81]---> BDD-cost:  103
c ---[  80]---> BDD-cost:   81
c ---[  79]---> BDD-cost:  103
c ---[  78]---> BDD-cost:   81
c ---[  77]---> BDD-cost:  103
c ---[  76]---> BDD-cost:  103
c ---[  75]---> BDD-cost:   85
c ---[  74]---> BDD-cost:  103
c ---[  73]---> BDD-cost:   85
c ---[  72]---> BDD-cost:  103
c ---[  71]---> BDD-cost:  148
c ---[  70]---> BDD-cost:  103
c ---[  69]---> BDD-cost:  148
c ---[  68]---> BDD-cost:  103
c ---[  67]---> BDD-cost:  146
c ---[  66]---> BDD-cost:  103
c ---[  65]---> BDD-cost:   88
c ---[  64]---> BDD-cost:  146
c ---[  63]---> BDD-cost:  103
c ---[  62]---> BDD-cost:  101
c ---[  61]---> BDD-cost:  103
c ---[  60]---> BDD-cost:  101
c ---[  59]---> BDD-cost:  103
c ---[  58]---> BDD-cost:  137
c ---[  57]---> BDD-cost:  103
c ---[  56]---> BDD-cost:  137
c ---[  55]---> BDD-cost:  103
c ---[  54]---> BDD-cost:  103
c ---[  53]---> BDD-cost:  110
c ---[  52]---> BDD-cost:  103
c ---[  51]---> BDD-cost:  110
c ---[  50]---> BDD-cost:  103
c ---[  49]---> BDD-cost:  154
c ---[  48]---> BDD-cost:  103
c ---[  47]---> BDD-cost:  154
c ---[  46]---> BDD-cost:  103
c ---[  45]---> BDD-cost:  153
c ---[  44]---> BDD-cost:  103
c ---[  43]---> BDD-cost:   88
c ---[  42]---> BDD-cost:  153
c ---[  41]---> BDD-cost:  103
c ---[  40]---> BDD-cost:   99
c ---[  39]---> BDD-cost:  103
c ---[  38]---> BDD-cost:   99
c ---[  37]---> BDD-cost:  103
c ---[  36]---> BDD-cost:  104
c ---[  35]---> BDD-cost:  103
c ---[  34]---> BDD-cost:  104
c ---[  33]---> BDD-cost:  103
c ---[  32]---> BDD-cost:  103
c ---[  31]---> BDD-cost:   87
c ---[  30]---> BDD-cost:  103
c ---[  29]---> BDD-cost:   87
c ---[  28]---> BDD-cost:  103
c ---[  27]---> BDD-cost:   88
c ---[  26]---> BDD-cost:  103
c ---[  25]---> BDD-cost:   88
c ---[  24]---> BDD-cost:  103
c ---[  23]---> BDD-cost:  155
c ---[  22]---> BDD-cost:  103
c ---[  21]---> BDD-cost:  155
c ---[  20]---> BDD-cost:  155
c ---[  19]---> BDD-cost:  103
c ---[  18]---> BDD-cost:  148
c ---[  17]---> BDD-cost:  103
c ---[  16]---> BDD-cost:  148
c ---[  15]---> BDD-cost:  103
c ---[  14]---> BDD-cost:  152
c ---[  13]---> BDD-cost:  103
c ---[  12]---> BDD-cost:  152
c ---[  11]---> BDD-cost:  103
c ---[  10]---> BDD-cost:  103
c ---[   9]---> BDD-cost:  105
c ---[   8]---> BDD-cost:  103
c ---[   7]---> BDD-cost:  105
c ---[   6]---> BDD-cost:  103
c ---[   5]---> BDD-cost:  107
c ---[   4]---> BDD-cost:  103
c ---[   3]---> BDD-cost:  107
c ---[   2]---> BDD-cost:  103
c ---[   1]---> BDD-cost:  144
c ---[   0]---> BDD-cost:  103
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  480116  1347916 |  160038       0        0     nan |  0.000 % |
c |       100 |  480116  1347916 |  176041     100      392     3.9 |  0.998 % |
c |       250 |  480116  1347916 |  193645     250     1129     4.5 |  0.998 % |
c |       475 |  480116  1347916 |  213010     475     2220     4.7 |  0.998 % |
c |       813 |  480116  1347916 |  234311     813     3781     4.7 |  0.998 % |
c |      1319 |  480116  1347916 |  257742    1319     8060     6.1 |  0.998 % |
c |      2078 |  480116  1347916 |  283517    2078    19467     9.4 |  0.998 % |
c |      3217 |  480116  1347916 |  311868    3217    36992    11.5 |  0.998 % |
c ==============================================================================
c [1mFound solution: 983036[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3989 |  480120  1347940 |  160040    3989    53836    13.5 |  0.998 % |
c ==============================================================================
c [1mFound solution: 784316[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4051 |  480130  1347974 |  160043    4051    55099    13.6 |  0.998 % |
c ==============================================================================
c [1mFound solution: 747516[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4134 |  480141  1348006 |  160047    4134    56679    13.7 |  0.998 % |
c ==============================================================================
c [1mFound solution: 711644[0m
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4185 |  480157  1348050 |  160052    4185    57704    13.8 |  0.998 % |
c ==============================================================================
c [1mFound solution: 702392[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4215 |  480173  1348093 |  160057    4215    58101    13.8 |  0.998 % |
c ==============================================================================
c [1mFound solution: 701932[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4269 |  480192  1348142 |  160064    4269    58945    13.8 |  0.998 % |
c ==============================================================================
c [1mFound solution: 686966[0m
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4365 |  480209  1348188 |  160069    4365    60683    13.9 |  0.998 % |
c ==============================================================================
c [1mFound solution: 683958[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4437 |  480223  1348227 |  160074    4437    62180    14.0 |  0.998 % |
c ==============================================================================
c [1mFound solution: 683516[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4499 |  480237  1348264 |  160079    4499    63323    14.1 |  0.998 % |
c |      4599 |  480237  1348264 |  176086    4599    66113    14.4 |  1.002 % |
c ==============================================================================
c [1mFound solution: 677740[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4672 |  480254  1348307 |  160084    4672    67722    14.5 |  1.002 % |
c |      4772 |  480254  1348307 |  176092    4772    70644    14.8 |  1.002 % |
c ==============================================================================
c [1mFound solution: 638680[0m
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4909 |  480268  1348346 |  160089    4909    74431    15.2 |  1.002 % |
c |      5009 |  480268  1348346 |  176097    5009    76827    15.3 |  1.002 % |
c ==============================================================================
c [1mFound solution: 617436[0m
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5071 |  480279  1348373 |  160093    5071    78304    15.4 |  1.002 % |
c ==============================================================================
c [1mFound solution: 612212[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5158 |  480298  1348421 |  160099    5158    80318    15.6 |  1.002 % |
c ==============================================================================
c [1mFound solution: 581092[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5200 |  480312  1348459 |  160104    5200    81089    15.6 |  1.002 % |
c ==============================================================================
c [1mFound solution: 531192[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5256 |  480327  1348495 |  160109    5256    81997    15.6 |  1.002 % |
c |      5356 |  480327  1348495 |  176119    5356    83944    15.7 |  1.004 % |
c ==============================================================================
c [1mFound solution: 530356[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5429 |  480342  1348533 |  160114    5429    85417    15.7 |  1.004 % |
c |      5529 |  480342  1348533 |  176125    5529    88120    15.9 |  1.004 % |
c ==============================================================================
c [1mFound solution: 283100[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5660 |  471268  1311353 |  157089    5481    87529    16.0 |  1.004 % |
c |      5760 |  471268  1311353 |  172797    5581    90134    16.2 |  1.610 % |
c |      5910 |  471268  1311353 |  190077    5731    93733    16.4 |  1.610 % |
c |      6136 |  471268  1311353 |  209085    5957    99059    16.6 |  1.610 % |
c ==============================================================================
c [1mFound solution: 263032[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6244 |  471282  1311385 |  157094    6065   101651    16.8 |  1.610 % |
c |      6344 |  471282  1311385 |  172803    6165   104110    16.9 |  1.610 % |
c ==============================================================================
c [1mFound solution: 262572[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6462 |  471297  1311419 |  157099    6283   106859    17.0 |  1.610 % |
c |      6562 |  471297  1311419 |  172808    6383   109240    17.1 |  1.610 % |
c |      6712 |  471297  1311419 |  190089    6533   112381    17.2 |  1.610 % |
c |      6937 |  471297  1311419 |  209098    6758   118139    17.5 |  1.610 % |
c ==============================================================================
c [1mFound solution: 262324[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7132 |  471310  1311447 |  157103    6953   122715    17.6 |  1.610 % |
c |      7232 |  471310  1311447 |  172813    7053   124564    17.7 |  1.611 % |
c |      7383 |  471310  1311447 |  190094    7204   128291    17.8 |  1.611 % |
c |      7609 |  471310  1311447 |  209104    7430   133540    18.0 |  1.611 % |
c |      7946 |  470935  1310431 |  230014    7761   142076    18.3 |  1.640 % |
c ==============================================================================
c [1mFound solution: 262268[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8076 |  470949  1310461 |  156983    7891   145250    18.4 |  1.640 % |
c |      8176 |  470949  1310461 |  172681    7991   146974    18.4 |  1.640 % |
c |      8326 |  470949  1310461 |  189949    8141   150268    18.5 |  1.640 % |
c |      8551 |  470787  1310004 |  208944    8365   154947    18.5 |  1.651 % |
c |      8888 |  470787  1310004 |  229838    8702   163689    18.8 |  1.651 % |
c ==============================================================================
c [1mFound solution: 262266[0m
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9112 |  470803  1310041 |  156934    8926   168699    18.9 |  1.651 % |
c |      9212 |  470803  1310041 |  172627    9026   171407    19.0 |  1.651 % |
c |      9364 |  470803  1310041 |  189890    9178   174953    19.1 |  1.651 % |
c |      9589 |  470803  1310041 |  208879    9403   179574    19.1 |  1.651 % |
c |      9927 |  470803  1310041 |  229767    9741   191731    19.7 |  1.651 % |
c ==============================================================================
c [1mFound solution: 262252[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10147 |  470815  1310066 |  156938    9961   197139    19.8 |  1.651 % |
c |     10249 |  470647  1309597 |  172631   10059   199214    19.8 |  1.663 % |
c |     10399 |  470647  1309597 |  189894   10209   202536    19.8 |  1.663 % |
c |     10624 |  470647  1309597 |  208884   10434   207306    19.9 |  1.663 % |
c ==============================================================================
c [1mFound solution: 262250[0m
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10774 |  470664  1309635 |  156888   10584   211215    20.0 |  1.663 % |
c |     10875 |  470526  1309226 |  172576   10683   213312    20.0 |  1.670 % |
c |     11025 |  470526  1309226 |  189834   10833   216822    20.0 |  1.670 % |
c ==============================================================================
c [1mFound solution: 262244[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11188 |  470540  1309257 |  156846   10996   220546    20.1 |  1.670 % |
c |     11288 |  470381  1308806 |  172530   11088   222797    20.1 |  1.681 % |
c |     11438 |  470381  1308806 |  189783   11238   226115    20.1 |  1.681 % |
c |     11663 |  470381  1308806 |  208762   11463   232149    20.3 |  1.681 % |
c ==============================================================================
c [1mFound solution: 262236[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11832 |  470395  1308836 |  156798   11632   236219    20.3 |  1.681 % |
c |     11932 |  470395  1308836 |  172477   11732   238019    20.3 |  1.681 % |
c |     12084 |  470395  1308836 |  189725   11884   241597    20.3 |  1.681 % |
c ==============================================================================
c [1mFound solution: 262234[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12226 |  470412  1308873 |  156804   12026   244975    20.4 |  1.681 % |
c |     12326 |  470412  1308873 |  172484   12126   247126    20.4 |  1.682 % |
c |     12476 |  470412  1308873 |  189732   12276   250273    20.4 |  1.682 % |
c |     12702 |  470412  1308873 |  208706   12502   256913    20.5 |  1.682 % |
c ==============================================================================
c [1mFound solution: 262228[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12903 |  470429  1308910 |  156809   12703   262018    20.6 |  1.682 % |
c |     13003 |  470429  1308910 |  172489   12803   264282    20.6 |  1.682 % |
c |     13153 |  470429  1308910 |  189738   12953   268264    20.7 |  1.682 % |
c |     13378 |  470429  1308910 |  208712   13178   274640    20.8 |  1.682 % |
c |     13715 |  470429  1308910 |  229584   13515   283231    21.0 |  1.682 % |
c ==============================================================================
c [1mFound solution: 262222[0m
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13810 |  470447  1308949 |  156815   13610   285100    20.9 |  1.682 % |
c |     13910 |  470447  1308949 |  172496   13710   287128    20.9 |  1.683 % |
c |     14060 |  470447  1308949 |  189746   13860   291045    21.0 |  1.683 % |
c |     14285 |  470447  1308949 |  208720   14085   296150    21.0 |  1.683 % |
c ==============================================================================
c [1mFound solution: 262220[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14484 |  470463  1308983 |  156821   14284   300963    21.1 |  1.683 % |
c |     14585 |  470316  1308556 |  172503   14382   302950    21.1 |  1.691 % |
c ==============================================================================
c [1mFound solution: 230388[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14722 |  461346  1282563 |  153782   14435   305716    21.2 |  1.691 % |
c |     14822 |  461346  1282563 |  169160   14535   308034    21.2 |  2.220 % |
c |     14972 |  461346  1282563 |  186076   14685   311408    21.2 |  2.220 % |
c |     15197 |  461346  1282563 |  204683   14910   317528    21.3 |  2.220 % |
c |     15534 |  461346  1282563 |  225152   15247   326436    21.4 |  2.220 % |
c |     16042 |  461346  1282563 |  247667   15755   336901    21.4 |  2.220 % |
c ==============================================================================
c [1mFound solution: 200636[0m
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16712 |  461353  1282580 |  153784   16425   353886    21.5 |  2.220 % |
c |     16812 |  461353  1282580 |  169162   16525   355854    21.5 |  2.221 % |
c |     16962 |  461353  1282580 |  186078   16675   359133    21.5 |  2.221 % |
c |     17188 |  461353  1282580 |  204686   16901   363461    21.5 |  2.221 % |
c ==============================================================================
c [1mFound solution: 189260[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17399 |  461364  1282608 |  153788   17112   368698    21.5 |  2.221 % |
c |     17501 |  461364  1282608 |  169166   17214   370834    21.5 |  2.221 % |
c |     17651 |  461364  1282608 |  186083   17364   374020    21.5 |  2.221 % |
c |     17877 |  461364  1282608 |  204691   17590   378297    21.5 |  2.221 % |
c |     18215 |  461364  1282608 |  225161   17928   387082    21.6 |  2.221 % |
c |     18722 |  461364  1282608 |  247677   18435   401021    21.8 |  2.221 % |
c ==============================================================================
c [1mFound solution: 186298[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19442 |  461377  1282643 |  153792   19155   417300    21.8 |  2.221 % |
c |     19543 |  461377  1282643 |  169171   19256   419092    21.8 |  2.221 % |
c |     19695 |  461377  1282643 |  186088   19408   422111    21.7 |  2.221 % |
c |     19923 |  461377  1282643 |  204697   19636   427055    21.7 |  2.221 % |
c |     20261 |  461377  1282643 |  225166   19974   435060    21.8 |  2.221 % |
c |     20767 |  461377  1282643 |  247683   20480   449229    21.9 |  2.221 % |
c |     21526 |  461377  1282643 |  272451   21239   467288    22.0 |  2.221 % |
c ==============================================================================
c [1mFound solution: 186284[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22300 |  461387  1282669 |  153795   22013   485877    22.1 |  2.221 % |
c |     22400 |  461387  1282669 |  169174   22113   487885    22.1 |  2.222 % |
c |     22550 |  461387  1282669 |  186091   22263   490764    22.0 |  2.222 % |
c |     22775 |  461387  1282669 |  204701   22488   496993    22.1 |  2.222 % |
c ==============================================================================
c [1mFound solution: 180182[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23064 |  461397  1282700 |  153799   22777   505373    22.2 |  2.222 % |
c |     23165 |  461397  1282700 |  169178   22878   507976    22.2 |  2.222 % |
c |     23315 |  461397  1282700 |  186096   23028   511571    22.2 |  2.222 % |
c |     23541 |  461397  1282700 |  204706   23254   518141    22.3 |  2.222 % |
c |     23879 |  461397  1282700 |  225177   23592   527487    22.4 |  2.222 % |
c ==============================================================================
c [1mFound solution: 179908[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24293 |  461409  1282733 |  153803   24006   537504    22.4 |  2.222 % |
c |     24396 |  461409  1282733 |  169183   24109   539504    22.4 |  2.223 % |
c |     24546 |  461409  1282733 |  186101   24259   543323    22.4 |  2.223 % |
c |     24771 |  461409  1282733 |  204711   24484   548132    22.4 |  2.223 % |
c |     25108 |  461409  1282733 |  225182   24821   558010    22.5 |  2.223 % |
c |     25615 |  461409  1282733 |  247701   25328   574024    22.7 |  2.223 % |
c ==============================================================================
c [1mFound solution: 176034[0m
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26247 |  461425  1282774 |  153808   25960   589585    22.7 |  2.223 % |
c |     26347 |  461425  1282774 |  169188   26060   591314    22.7 |  2.223 % |
c |     26499 |  461425  1282774 |  186107   26212   594062    22.7 |  2.223 % |
c |     26724 |  461425  1282774 |  204718   26437   599149    22.7 |  2.223 % |
c |     27061 |  461425  1282774 |  225190   26774   605915    22.6 |  2.223 % |
c ==============================================================================
c [1mFound solution: 163234[0m
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27386 |  461433  1282798 |  153811   27099   614570    22.7 |  2.223 % |
c |     27488 |  461433  1282798 |  169192   27201   617168    22.7 |  2.223 % |
c |     27638 |  461433  1282798 |  186111   27351   621517    22.7 |  2.223 % |
c |     27864 |  461433  1282798 |  204722   27577   627230    22.7 |  2.223 % |
c |     28203 |  461433  1282798 |  225194   27916   636579    22.8 |  2.223 % |
c ==============================================================================
c [1mFound solution: 163232[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28705 |  461443  1282826 |  153814   28418   653214    23.0 |  2.223 % |
c |     28805 |  461443  1282826 |  169195   28518   655624    23.0 |  2.224 % |
c |     28958 |  461443  1282826 |  186114   28671   659447    23.0 |  2.224 % |
c |     29183 |  461443  1282826 |  204726   28896   664459    23.0 |  2.224 % |
c |     29520 |  461443  1282826 |  225199   29233   676060    23.1 |  2.224 % |
c ==============================================================================
c [1mFound solution: 162276[0m
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30024 |  461450  1282845 |  153816   29737   691675    23.3 |  2.224 % |
c |     30124 |  461450  1282845 |  169197   29837   693697    23.2 |  2.224 % |
c |     30274 |  461450  1282845 |  186117   29987   697650    23.3 |  2.224 % |
c |     30499 |  461450  1282845 |  204729   30212   703232    23.3 |  2.224 % |
c |     30837 |  461450  1282845 |  225202   30550   712960    23.3 |  2.224 % |
c |     31343 |  461450  1282845 |  247722   31056   731657    23.6 |  2.224 % |
c |     32103 |  461450  1282845 |  272494   31816   754532    23.7 |  2.224 % |
c ==============================================================================
c [1mFound solution: 156390[0m
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32913 |  461465  1282882 |  153821   32626   781545    24.0 |  2.224 % |
c |     33013 |  461465  1282882 |  169203   32726   783230    23.9 |  2.225 % |
c |     33163 |  461465  1282882 |  186123   32876   786189    23.9 |  2.225 % |
c |     33388 |  461465  1282882 |  204735   33101   792967    24.0 |  2.225 % |
c |     33725 |  461465  1282882 |  225209   33438   803198    24.0 |  2.225 % |
c |     34231 |  461465  1282882 |  247730   33944   817209    24.1 |  2.225 % |
c |     34991 |  461465  1282882 |  272503   34704   846170    24.4 |  2.225 % |
c |     36130 |  461465  1282882 |  299753   35843   877662    24.5 |  2.225 % |
c |     37838 |  461339  1282497 |  329728   37465   981620    26.2 |  2.230 % |
c ==============================================================================
c [1mFound solution: 154594[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     39610 |  461350  1282527 |  153783   39237  1035174    26.4 |  2.230 % |
c |     39710 |  461350  1282527 |  169161   39337  1037072    26.4 |  2.230 % |
c |     39862 |  461350  1282527 |  186077   39489  1041602    26.4 |  2.230 % |
c |     40089 |  461350  1282527 |  204685   39716  1046526    26.4 |  2.230 % |
c |     40426 |  461227  1282148 |  225153   40008  1052614    26.3 |  2.235 % |
c |     40933 |  461227  1282148 |  247669   40515  1068939    26.4 |  2.235 % |
c |     41693 |  461227  1282148 |  272435   41275  1092477    26.5 |  2.235 % |
c |     42832 |  461227  1282148 |  299679   42414  1134796    26.8 |  2.235 % |
c |     44540 |  461227  1282148 |  329647   44122  1195740    27.1 |  2.235 % |
c ==============================================================================
c [1mFound solution: 147452[0m
c ---[   0]---> BDD-cost:    4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45299 |  461233  1282164 |  153744   44881  1220481    27.2 |  2.235 % |
c |     45399 |  461233  1282164 |  169118   44981  1222621    27.2 |  2.235 % |
c |     45549 |  461233  1282164 |  186030   45131  1225657    27.2 |  2.235 % |
c |     45774 |  461233  1282164 |  204633   45356  1230865    27.1 |  2.235 % |
c |     46111 |  461131  1281827 |  225096   45552  1230824    27.0 |  2.236 % |
c |     46617 |  461023  1281478 |  247606   45888  1234180    26.9 |  2.239 % |
c |     47377 |  461023  1281478 |  272366   46648  1266138    27.1 |  2.239 % |
c |     48517 |  461023  1281478 |  299603   47788  1302175    27.2 |  2.239 % |
c ==============================================================================
c [1mFound solution: 147420[0m
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49674 |  461029  1281495 |  153676   48945  1350161    27.6 |  2.239 % |
c |     49774 |  461029  1281495 |  169043   49045  1352265    27.6 |  2.239 % |
c |     49924 |  461029  1281495 |  185947   49195  1356025    27.6 |  2.239 % |
c |     50149 |  460867  1281038 |  204542   49323  1355993    27.5 |  2.250 % |
c |     50486 |  460867  1281038 |  224997   49660  1364668    27.5 |  2.250 % |
c |     50992 |  460867  1281038 |  247496   50166  1378861    27.5 |  2.250 % |
c |     51751 |  460867  1281038 |  272246   50925  1403760    27.6 |  2.250 % |
c |     52890 |  460867  1281038 |  299471   52064  1436687    27.6 |  2.250 % |
c |     54598 |  460867  1281038 |  329418   53772  1484098    27.6 |  2.250 % |
c |     57160 |  460867  1281038 |  362359   56334  1613533    28.6 |  2.250 % |
c |     61005 |  460693  1280557 |  398595   60115  1765982    29.4 |  2.262 % |
c |     66773 |  460693  1280557 |  438455   65883  2044526    31.0 |  2.262 % |
c ==============================================================================
c [1mFound solution: 147292[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68675 |  460590  1280225 |  153530   67714  2109743    31.2 |  2.262 % |
c |     68775 |  460590  1280225 |  168883   67814  2111322    31.1 |  2.265 % |
c |     68927 |  460590  1280225 |  185771   67966  2115070    31.1 |  2.265 % |
c |     69152 |  460590  1280225 |  204348   68191  2122103    31.1 |  2.265 % |
c |     69490 |  460590  1280225 |  224783   68529  2129828    31.1 |  2.265 % |
c |     69996 |  460590  1280225 |  247261   69035  2145911    31.1 |  2.265 % |
c |     70757 |  460590  1280225 |  271987   69796  2166192    31.0 |  2.265 % |
c |     71896 |  460590  1280225 |  299186   70935  2202699    31.1 |  2.265 % |
c |     73604 |  460590  1280225 |  329105   72643  2260472    31.1 |  2.265 % |
c |     76166 |  460590  1280225 |  362015   75205  2419634    32.2 |  2.265 % |
c ==============================================================================
c [1mFound solution: 147280[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     77569 |  460601  1280255 |  153533   76608  2462171    32.1 |  2.265 % |
c |     77669 |  460601  1280255 |  168886   76708  2464180    32.1 |  2.266 % |
c |     77821 |  460601  1280255 |  185774   76860  2467197    32.1 |  2.266 % |
c |     78047 |  460601  1280255 |  204352   77086  2472901    32.1 |  2.266 % |
c |     78384 |  460601  1280255 |  224787   77423  2480441    32.0 |  2.266 % |
c |     78892 |  460418  1279756 |  247266   77848  2485571    31.9 |  2.279 % |
c |     79651 |  460418  1279756 |  271993   78607  2511060    31.9 |  2.279 % |
c |     80790 |  460418  1279756 |  299192   79746  2542488    31.9 |  2.279 % |
c |     82498 |  460418  1279756 |  329111   81454  2593581    31.8 |  2.279 % |
c |     85060 |  460418  1279756 |  362022   84016  2723913    32.4 |  2.279 % |
c |     88904 |  460418  1279756 |  398225   87860  2845139    32.4 |  2.279 % |
c |     94670 |  460304  1279395 |  438047   93565  3092108    33.0 |  2.282 % |
c ==============================================================================
c [1mFound solution: 147278[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     99764 |  460060  1278648 |  153353   98484  3647228    37.0 |  2.282 % |
c |     99864 |  459913  1278221 |  168688   98467  3642499    37.0 |  2.301 % |
c |    100014 |  459913  1278221 |  185557   98617  3646485    37.0 |  2.301 % |
c |    100239 |  459913  1278221 |  204112   98842  3652369    37.0 |  2.301 % |
c |    100576 |  459727  1277716 |  224524   99130  3657357    36.9 |  2.315 % |
c |    101082 |  459727  1277716 |  246976   99636  3669952    36.8 |  2.315 % |
c |    101841 |  459727  1277716 |  271674  100395  3696542    36.8 |  2.315 % |
c ==============================================================================
c [1mFound solution: 147276[0m
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    102487 |  459733  1277733 |  153244  101041  3728134    36.9 |  2.315 % |
c |    102588 |  459733  1277733 |  168568  101142  3729979    36.9 |  2.316 % |
c |    102738 |  459733  1277733 |  185425  101292  3733474    36.9 |  2.316 % |
c |    102964 |  459733  1277733 |  203967  101518  3738086    36.8 |  2.316 % |
c |    103301 |  459733  1277733 |  224364  101855  3748610    36.8 |  2.316 % |
c |    103807 |  459733  1277733 |  246800  102361  3761437    36.7 |  2.316 % |
c ==============================================================================
c [1mFound solution: 146844[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    104289 |  459744  1277762 |  153248  102843  3778675    36.7 |  2.316 % |
c |    104389 |  459744  1277762 |  168572  102943  3781519    36.7 |  2.316 % |
c |    104539 |  459744  1277762 |  185430  103093  3784049    36.7 |  2.316 % |
c |    104764 |  459744  1277762 |  203973  103318  3788807    36.7 |  2.316 % |
c |    105102 |  459744  1277762 |  224370  103656  3797483    36.6 |  2.316 % |
c |    105608 |  459744  1277762 |  246807  104162  3813338    36.6 |  2.316 % |
c |    106368 |  459744  1277762 |  271488  104922  3834235    36.5 |  2.316 % |
c |    107508 |  459744  1277762 |  298636  106062  3866039    36.5 |  2.316 % |
c |    109216 |  459744  1277762 |  328500  107770  4005961    37.2 |  2.316 % |
c |    111778 |  459744  1277762 |  361350  110332  4102960    37.2 |  2.316 % |
c |    115623 |  459456  1276920 |  397485  114026  4231048    37.1 |  2.332 % |
c |    121389 |  459336  1276547 |  437234  119736  4693320    39.2 |  2.336 % |
c |    130038 |  459336  1276547 |  480957  128385  4982585    38.8 |  2.336 % |
c ==============================================================================
c [1mFound solution: 146722[0m
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    132746 |  459140  1275895 |  153046  130809  5034050    38.5 |  2.336 % |
c |    132846 |  459140  1275895 |  168350  130909  5036132    38.5 |  2.339 % |
c |    132996 |  459140  1275895 |  185185  131059  5039068    38.4 |  2.339 % |
c |    133221 |  459140  1275895 |  203704  131284  5045050    38.4 |  2.339 % |
c |    133559 |  459140  1275895 |  224074  131622  5054062    38.4 |  2.339 % |
c |    134065 |  459140  1275895 |  246482  132128  5071858    38.4 |  2.339 % |
c |    134824 |  459140  1275895 |  271130  132887  5096267    38.4 |  2.339 % |
c |    135966 |  459140  1275895 |  298243  134029  5132257    38.3 |  2.339 % |
c |    137674 |  459140  1275895 |  328067  135737  5185804    38.2 |  2.339 % |
c |    140236 |  459140  1275895 |  360874  138299  5300100    38.3 |  2.339 % |
c |    144080 |  459140  1275895 |  396961  142143  5424193    38.2 |  2.339 % |
c ==============================================================================
c [1mFound solution: 146684[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    146231 |  459150  1275921 |  153050  144294  5506670    38.2 |  2.339 % |
c |    146331 |  459150  1275921 |  168355  144394  5508489    38.1 |  2.340 % |
c |    146481 |  459150  1275921 |  185190  144544  5511551    38.1 |  2.340 % |
c |    146706 |  459150  1275921 |  203709  144769  5518919    38.1 |  2.340 % |
c |    147043 |  459150  1275921 |  224080  145106  5529032    38.1 |  2.340 % |
c |    147549 |  459150  1275921 |  246488  145612  5544117    38.1 |  2.340 % |
c |    148308 |  459150  1275921 |  271137  146371  5566292    38.0 |  2.340 % |
c |    149447 |  459150  1275921 |  298251  147510  5593641    37.9 |  2.340 % |
c |    151156 |  458958  1275404 |  328076  149186  5643489    37.8 |  2.355 % |
c |    153718 |  458958  1275404 |  360883  151748  5735135    37.8 |  2.355 % |
c |    157562 |  458469  1274027 |  396972  154657  5749310    37.2 |  2.387 % |
c ==============================================================================
c [1mFound solution: 146656[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    161701 |  458299  1273561 |  152766  158777  5875117    37.0 |  2.387 % |
c |    161801 |  458299  1273561 |  168042   25209   446861    17.7 |  2.401 % |
c |    161951 |  458299  1273561 |  184846   25359   449463    17.7 |  2.401 % |
c |    162176 |  458299  1273561 |  203331   25584   455406    17.8 |  2.401 % |
c |    162514 |  458155  1273140 |  223664   25919   461805    17.8 |  2.408 % |
c |    163020 |  458155  1273140 |  246031   26425   473756    17.9 |  2.408 % |
c |    163780 |  457975  1272647 |  270634   27182   491125    18.1 |  2.422 % |
c |    164919 |  457975  1272647 |  297697   28321   520806    18.4 |  2.422 % |
c |    166627 |  457975  1272647 |  327467   30029   622715    20.7 |  2.422 % |
c |    169189 |  457975  1272647 |  360214   32591   716100    22.0 |  2.422 % |
c |    173033 |  457975  1272647 |  396235   36435   851299    23.4 |  2.422 % |
c |    178799 |  457975  1272647 |  435859   42201  1059644    25.1 |  2.422 % |
c ==============================================================================
c [1mFound solution: 146300[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    180078 |  457986  1272675 |  152662   43480  1120551    25.8 |  2.422 % |
c |    180178 |  457986  1272675 |  167928   43580  1122227    25.8 |  2.422 % |
c |    180328 |  457986  1272675 |  184721   43730  1125850    25.7 |  2.422 % |
c |    180553 |  457986  1272675 |  203193   43955  1129646    25.7 |  2.422 % |
c |    180890 |  457986  1272675 |  223512   44292  1136101    25.7 |  2.422 % |
c |    181396 |  457986  1272675 |  245863   44798  1149961    25.7 |  2.422 % |
c |    182155 |  457986  1272675 |  270450   45557  1166369    25.6 |  2.422 % |
c |    183294 |  457986  1272675 |  297495   46696  1195422    25.6 |  2.422 % |
c |    185002 |  457986  1272675 |  327244   48404  1252286    25.9 |  2.422 % |
c ==============================================================================
c [1mFound solution: 146298[0m
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    186035 |  457997  1272703 |  152665   49437  1288923    26.1 |  2.422 % |
c |    186137 |  457997  1272703 |  167931   49539  1290731    26.1 |  2.422 % |
c |    186288 |  457997  1272703 |  184724   49690  1293608    26.0 |  2.422 % |
c |    186513 |  457997  1272703 |  203197   49915  1297385    26.0 |  2.422 % |
c |    186850 |  457820  1272216 |  223516   50249  1303662    25.9 |  2.435 % |
c |    187356 |  457820  1272216 |  245868   50755  1316816    25.9 |  2.435 % |
c |    188116 |  457820  1272216 |  270455   51515  1342240    26.1 |  2.435 % |
c |    189255 |  457820  1272216 |  297500   52654  1378396    26.2 |  2.435 % |
c |    190963 |  457820  1272216 |  327250   54362  1435834    26.4 |  2.435 % |
c |    193526 |  457820  1272216 |  359976   56925  1552628    27.3 |  2.435 % |
c ==============================================================================
c [1mFound solution: 146286[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    195620 |  457834  1272252 |  152611   59019  1626633    27.6 |  2.435 % |
c |    195721 |  457834  1272252 |  167872   59120  1628356    27.5 |  2.436 % |
c |    195871 |  457834  1272252 |  184659   59270  1631787    27.5 |  2.436 % |
c |    196097 |  457834  1272252 |  203125   59496  1636717    27.5 |  2.436 % |
c |    196435 |  457834  1272252 |  223437   59834  1645003    27.5 |  2.436 % |
c |    196942 |  457834  1272252 |  245781   60341  1657003    27.5 |  2.436 % |
c |    197701 |  457834  1272252 |  270359   61100  1676558    27.4 |  2.436 % |
c |    198840 |  457834  1272252 |  297395   62239  1716720    27.6 |  2.436 % |
c |    200548 |  457834  1272252 |  327135   63947  1775441    27.8 |  2.436 % |
c |    203110 |  457834  1272252 |  359848   66509  1858359    27.9 |  2.436 % |
c ==============================================================================
c [1mFound solution: 146284[0m
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    206372 |  457843  1272276 |  152614   69771  1983595    28.4 |  2.436 % |
c |    206472 |  457843  1272276 |  167875   69871  1985163    28.4 |  2.436 % |
c |    206622 |  457843  1272276 |  184662   70021  1989030    28.4 |  2.436 % |
c |    206849 |  457843  1272276 |  203129   70248  1993589    28.4 |  2.436 % |
c |    207186 |  457843  1272276 |  223442   70585  2000278    28.3 |  2.436 % |
c |    207692 |  457843  1272276 |  245786   71091  2015916    28.4 |  2.436 % |
c |    208451 |  457711  1271879 |  270365   71847  2031956    28.3 |  2.442 % |
c |    209590 |  457711  1271879 |  297401   72986  2070676    28.4 |  2.442 % |
c |    211298 |  457711  1271879 |  327141   74694  2131147    28.5 |  2.442 % |
c |    213861 |  457711  1271879 |  359855   77257  2206132    28.6 |  2.442 % |
c |    217705 |  457603  1271530 |  395841   81098  2392018    29.5 |  2.444 % |
c |    223471 |  457603  1271530 |  435425   86864  2592520    29.8 |  2.444 % |
c |    232122 |  457474  1271139 |  478968   95512  3219488    33.7 |  2.450 % |
c |    245096 |  457474  1271139 |  526864  108486  3691867    34.0 |  2.450 % |
c ==============================================================================
c [1mFound solution: 146252[0m
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    246615 |  457482  1271159 |  152494  110005  3805248    34.6 |  2.450 % |
c |    246715 |  457482  1271159 |  167743  110105  3807125    34.6 |  2.450 % |
c |    246865 |  457365  1270792 |  184517  110252  3810147    34.6 |  2.454 % |
c |    247090 |  457365  1270792 |  202969  110477  3814133    34.5 |  2.454 % |
c |    247428 |  457365  1270792 |  223266  110815  3825251    34.5 |  2.454 % |
c |    247934 |  457365  1270792 |  245593  111321  3838236    34.5 |  2.454 % |
c |    248693 |  457365  1270792 |  270152  112080  3859205    34.4 |  2.454 % |
c ==============================================================================
c [1mFound solution: 146250[0m
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    249376 |  457379  1270827 |  152459  112763  3880525    34.4 |  2.454 % |
c |    249476 |  457379  1270827 |  167704  112863  3882560    34.4 |  2.454 % |
c |    249626 |  457379  1270827 |  184475  113013  3885424    34.4 |  2.454 % |
c |    249851 |  457379  1270827 |  202922  113238  3892064    34.4 |  2.454 % |
c |    250188 |  457379  1270827 |  223215  113575  3899111    34.3 |  2.454 % |
c |    250694 |  457379  1270827 |  245536  114081  3913585    34.3 |  2.454 % |
c |    251453 |  457196  1270328 |  270090  114836  3935986    34.3 |  2.468 % |
c |    252593 |  457196  1270328 |  297099  115976  3966935    34.2 |  2.468 % |
c ==============================================================================
c [1mFound solution: 146190[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    254214 |  457208  1270358 |  152402  117597  4020785    34.2 |  2.468 % |
c |    254315 |  457208  1270358 |  167642  117698  4022353    34.2 |  2.468 % |
c |    254465 |  457208  1270358 |  184406  117848  4025620    34.2 |  2.468 % |
c |    254691 |  457208  1270358 |  202847  118074  4030477    34.1 |  2.468 % |
c |    255028 |  457208  1270358 |  223131  118411  4037626    34.1 |  2.468 % |
c |    255534 |  457208  1270358 |  245444  118917  4047422    34.0 |  2.468 % |
c |    256293 |  457208  1270358 |  269989  119676  4065658    34.0 |  2.468 % |
c ==============================================================================
c [1mFound solution: 146188[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    257342 |  457220  1270388 |  152406  120725  4099538    34.0 |  2.468 % |
c |    257442 |  457220  1270388 |  167646  120825  4101024    33.9 |  2.469 % |
c |    257592 |  457220  1270388 |  184411  120975  4104029    33.9 |  2.469 % |
c |    257817 |  457220  1270388 |  202852  121200  4109913    33.9 |  2.469 % |
c |    258154 |  457220  1270388 |  223137  121537  4118032    33.9 |  2.469 % |
c |    258661 |  457220  1270388 |  245451  122044  4130776    33.8 |  2.469 % |
c |    259421 |  457220  1270388 |  269996  122804  4151646    33.8 |  2.469 % |
c |    260560 |  457220  1270388 |  296996  123943  4179712    33.7 |  2.469 % |
c |    262270 |  457220  1270388 |  326695  125653  4240056    33.7 |  2.469 % |
c |    264832 |  457220  1270388 |  359365  128215  4342930    33.9 |  2.469 % |
c |    268677 |  457220  1270388 |  395301  132060  4517621    34.2 |  2.469 % |
c |    274443 |  457220  1270388 |  434832  137826  4792476    34.8 |  2.469 % |
c |    283092 |  457220  1270388 |  478315  146475  5267045    36.0 |  2.469 % |
c |    296067 |  457220  1270388 |  526146  159450  5756756    36.1 |  2.469 % |
c ==============================================================================
c [1mFound solution: 146186[0m
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    300296 |  457232  1270418 |  152410  163679  6047821    36.9 |  2.469 % |
c |    300396 |  457232  1270418 |  167651   31291   697773    22.3 |  2.469 % |
c |    300548 |  457232  1270418 |  184416   31443   700793    22.3 |  2.469 % |
c |    300773 |  457232  1270418 |  202857   31668   705724    22.3 |  2.469 % |
c |    301110 |  457232  1270418 |  223143   32005   712422    22.3 |  2.469 % |
c |    301616 |  457232  1270418 |  245457   32511   729673    22.4 |  2.469 % |
c |    302376 |  457232  1270418 |  270003   33271   746421    22.4 |  2.469 % |
c |    303515 |  457058  1269937 |  297003   34407   775983    22.6 |  2.481 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 11987 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### 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.84 0.94 0.91 2/54 11983
Raw data (stat): 11983 (runsolver) R 11982 25568 25567 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784224923 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.87 0.94 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0023 s]
Raw data (loadavg): 0.89 0.94 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0029 s]
Raw data (loadavg): 0.90 0.94 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.003 s]
Raw data (loadavg): 0.92 0.94 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0034 s]
Raw data (loadavg): 0.93 0.94 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0033 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0035 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0039 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0037 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.057 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.52 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 11987
Raw data (stat): 11983 (minisat+_script) S 11982 25568 25567 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784224923 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.52
CPU time (s): 1229.88
CPU user time (s): 1229.05
CPU system time (s): 0.826874
CPU usage (%): 100.03
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####