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 18741

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-21 16:17:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17615 boxname=wulflinc26 idbench=1355 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  216e30ba4678325d93810a111dd11436  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-liu.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-liu.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-liu.opb
IDLAUNCH: 17615
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        640216 kB
Buffers:         30948 kB
Cached:         335844 kB
SwapCached:         68 kB
Active:          50580 kB
Inactive:       319088 kB
HighTotal:      131008 kB
HighFree:         5908 kB
LowTotal:       903652 kB
LowFree:        634308 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6876 kB
Slab:            19296 kB
Committed_AS:    63716 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 16:37:06 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 17615 7 1200.3 10
#### 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 |  980472  2705884 |  326824       0        0     nan |  0.000 % |
c |       100 |  980472  2705884 |  359506     100      508     5.1 |  0.998 % |
c |       250 |  980455  2705845 |  395457     249     1283     5.2 |  0.999 % |
c |       475 |  980455  2705845 |  435002     474     2430     5.1 |  0.999 % |
c |       812 |  980434  2705798 |  478503     810     4182     5.2 |  1.000 % |
c |      1318 |  980434  2705798 |  526353    1316     6907     5.2 |  1.000 % |
c |      2077 |  980434  2705798 |  578988    2075    12877     6.2 |  1.000 % |
c |      3216 |  980434  2705798 |  636887    3214    22242     6.9 |  1.000 % |
c |      4924 |  980350  2705610 |  700576    4918    36367     7.4 |  1.003 % |
c |      7486 |  980331  2705567 |  770633    7479    59732     8.0 |  1.004 % |
c |     11330 |  980263  2705416 |  847697   11320   106696     9.4 |  1.007 % |
c |     17096 |  980155  2705175 |  932467   17081   187387    11.0 |  1.012 % |
c ==============================================================================
c [1mFound solution: 788656[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23639 |  980137  2705144 |  326712   23622   301864    12.8 |  1.012 % |
c |     23739 |  980137  2705144 |  359383   23722   303549    12.8 |  1.014 % |
c |     23890 |  980137  2705144 |  395321   23873   305879    12.8 |  1.014 % |
c |     24115 |  980137  2705144 |  434853   24098   309844    12.9 |  1.014 % |
c |     24452 |  980137  2705144 |  478339   24435   314683    12.9 |  1.014 % |
c ==============================================================================
c [1mFound solution: 655528[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24826 |  980167  2705220 |  326722   24809   321258    12.9 |  1.014 % |
c |     24926 |  980167  2705220 |  359394   24909   322870    13.0 |  1.014 % |
c |     25076 |  980167  2705220 |  395333   25059   324895    13.0 |  1.014 % |
c |     25301 |  980167  2705220 |  434866   25284   328893    13.0 |  1.014 % |
c |     25639 |  980167  2705220 |  478353   25622   332792    13.0 |  1.014 % |
c |     26145 |  980167  2705220 |  526189   26128   343056    13.1 |  1.014 % |
c ==============================================================================
c [1mFound solution: 655364[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26671 |  980190  2705283 |  326730   26654   352191    13.2 |  1.014 % |
c |     26771 |  980190  2705283 |  359403   26754   353530    13.2 |  1.015 % |
c |     26922 |  980190  2705283 |  395343   26905   355758    13.2 |  1.015 % |
c ==============================================================================
c [1mFound solution: 552995[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27092 |  980221  2705364 |  326740   27075   358743    13.2 |  1.015 % |
c |     27192 |  980221  2705364 |  359414   27175   359837    13.2 |  1.015 % |
c |     27342 |  980221  2705364 |  395355   27325   361352    13.2 |  1.015 % |
c ==============================================================================
c [1mFound solution: 540881[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   19
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27523 |  980254  2705449 |  326751   27506   363336    13.2 |  1.015 % |
c |     27623 |  980254  2705449 |  359426   27606   364622    13.2 |  1.015 % |
c |     27773 |  980254  2705449 |  395368   27756   366384    13.2 |  1.015 % |
c ==============================================================================
c [1mFound solution: 540234[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27939 |  980286  2705531 |  326762   27922   369073    13.2 |  1.015 % |
c ==============================================================================
c [1mFound solution: 539648[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28028 |  980299  2705566 |  326766   28011   369949    13.2 |  1.015 % |
c |     28128 |  980299  2705566 |  359442   28111   370848    13.2 |  1.016 % |
c |     28278 |  980299  2705566 |  395386   28261   372760    13.2 |  1.016 % |
c ==============================================================================
c [1mFound solution: 539522[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   17
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     28438 |  980326  2705637 |  326775   28421   375189    13.2 |  1.016 % |
c |     28539 |  980326  2705637 |  359452   28522   376966    13.2 |  1.017 % |
c |     28690 |  980326  2705637 |  395397   28673   379456    13.2 |  1.017 % |
c |     28916 |  980326  2705637 |  434937   28899   382426    13.2 |  1.017 % |
c |     29253 |  980326  2705637 |  478431   29236   388194    13.3 |  1.017 % |
c |     29759 |  980326  2705637 |  526274   29742   401782    13.5 |  1.017 % |
c ==============================================================================
c [1mFound solution: 539520[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30231 |  980346  2705689 |  326782   30214   411014    13.6 |  1.017 % |
c |     30331 |  980346  2705689 |  359460   30314   412959    13.6 |  1.017 % |
c |     30481 |  980346  2705689 |  395406   30464   415525    13.6 |  1.017 % |
c |     30706 |  980346  2705689 |  434946   30689   418794    13.6 |  1.017 % |
c ==============================================================================
c [1mFound solution: 393216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    1
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     30835 |  941213  2595921 |  313737   30244   410014    13.6 |  1.017 % |
c |     30935 |  941213  2595921 |  345110   30344   411544    13.6 |  2.662 % |
c |     31085 |  941213  2595921 |  379621   30494   414103    13.6 |  2.662 % |
c |     31310 |  941213  2595921 |  417583   30719   418393    13.6 |  2.662 % |
c ==============================================================================
c [1mFound solution: 327684[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31455 |  941235  2595981 |  313745   30864   420904    13.6 |  2.662 % |
c |     31555 |  941235  2595981 |  345119   30964   422271    13.6 |  2.663 % |
c |     31706 |  941235  2595981 |  379631   31115   424926    13.7 |  2.663 % |
c |     31932 |  941235  2595981 |  417594   31341   428414    13.7 |  2.663 % |
c |     32269 |  941235  2595981 |  459354   31678   432752    13.7 |  2.663 % |
c ==============================================================================
c [1mFound solution: 327683[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     32492 |  941255  2596035 |  313751   31901   436980    13.7 |  2.663 % |
c |     32593 |  941255  2596035 |  345126   32002   438757    13.7 |  2.663 % |
c |     32743 |  941255  2596035 |  379638   32152   440437    13.7 |  2.663 % |
c |     32969 |  941255  2596035 |  417602   32378   444027    13.7 |  2.663 % |
c |     33306 |  941255  2596035 |  459362   32715   449793    13.7 |  2.663 % |
c ==============================================================================
c [1mFound solution: 294912[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     33541 |  941260  2596048 |  313753   32950   453974    13.8 |  2.663 % |
c |     33642 |  941260  2596048 |  345128   33051   456336    13.8 |  2.664 % |
c |     33792 |  941260  2596048 |  379641   33201   459551    13.8 |  2.664 % |
c |     34017 |  941252  2596027 |  417605   33425   464466    13.9 |  2.665 % |
c |     34354 |  941252  2596027 |  459365   33762   469732    13.9 |  2.665 % |
c ==============================================================================
c [1mFound solution: 290848[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   13
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     34730 |  941271  2596078 |  313757   34138   476294    14.0 |  2.665 % |
c |     34830 |  941271  2596078 |  345132   34238   477998    14.0 |  2.665 % |
c |     34981 |  941271  2596078 |  379645   34389   481517    14.0 |  2.665 % |
c |     35207 |  941271  2596078 |  417610   34615   484498    14.0 |  2.665 % |
c |     35545 |  941271  2596078 |  459371   34953   492459    14.1 |  2.665 % |
c ==============================================================================
c [1mFound solution: 278560[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35833 |  941284  2596111 |  313761   35241   497947    14.1 |  2.665 % |
c |     35933 |  941284  2596111 |  345137   35341   499726    14.1 |  2.665 % |
c |     36083 |  941284  2596111 |  379650   35491   503214    14.2 |  2.665 % |
c |     36309 |  941284  2596111 |  417615   35717   509016    14.3 |  2.665 % |
c |     36646 |  941284  2596111 |  459377   36054   517815    14.4 |  2.665 % |
c |     37152 |  941284  2596111 |  505315   36560   527448    14.4 |  2.665 % |
c |     37911 |  941284  2596111 |  555846   37319   542813    14.5 |  2.665 % |
c |     39050 |  941276  2596090 |  611431   38457   569345    14.8 |  2.666 % |
c |     40758 |  940666  2594444 |  672574   40152   607786    15.1 |  2.708 % |
c ==============================================================================
c [1mFound solution: 196672[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     42469 |  911524  2514491 |  303841   41344   637940    15.4 |  2.708 % |
c |     42569 |  911524  2514491 |  334225   41444   639561    15.4 |  4.751 % |
c |     42720 |  911524  2514491 |  367647   41595   642250    15.4 |  4.751 % |
c |     42945 |  911524  2514491 |  404412   41820   647195    15.5 |  4.751 % |
c |     43282 |  911524  2514491 |  444853   42157   653177    15.5 |  4.751 % |
c |     43788 |  911524  2514491 |  489338   42663   662785    15.5 |  4.751 % |
c |     44547 |  911524  2514491 |  538272   43422   696293    16.0 |  4.751 % |
c |     45688 |  911524  2514491 |  592100   44563   720197    16.2 |  4.751 % |
c |     47396 |  911524  2514491 |  651310   46271   750201    16.2 |  4.751 % |
c |     49958 |  911524  2514491 |  716441   48833   800821    16.4 |  4.751 % |
c |     53802 |  911524  2514491 |  788085   52677   877974    16.7 |  4.751 % |
c |     59568 |  911508  2514449 |  866893   58440  1031693    17.7 |  4.753 % |
c |     68217 |  911508  2514449 |  953583   67089  1254254    18.7 |  4.753 % |
c ==============================================================================
c [1mFound solution: 180256[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75343 |  911502  2514430 |  303834   74213  1413084    19.0 |  4.753 % |
c |     75443 |  911502  2514430 |  334217   74313  1414764    19.0 |  4.754 % |
c |     75593 |  911494  2514409 |  367639   74461  1418185    19.0 |  4.755 % |
c |     75818 |  911494  2514409 |  404403   74686  1424084    19.1 |  4.755 % |
c |     76157 |  911494  2514409 |  444843   75025  1431139    19.1 |  4.755 % |
c |     76663 |  911494  2514409 |  489327   75531  1445042    19.1 |  4.755 % |
c |     77423 |  911494  2514409 |  538260   76291  1461338    19.2 |  4.755 % |
c |     78562 |  911494  2514409 |  592086   77430  1481508    19.1 |  4.755 % |
c |     80270 |  911494  2514409 |  651295   79138  1519532    19.2 |  4.755 % |
c |     82832 |  911486  2514388 |  716424   81697  1565551    19.2 |  4.756 % |
c |     86676 |  911478  2514367 |  788067   85540  1638831    19.2 |  4.757 % |
c ==============================================================================
c [1mFound solution: 176256[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90398 |  911490  2514396 |  303830   89260  1732047    19.4 |  4.757 % |
c |     90498 |  911482  2514375 |  334213   89359  1733784    19.4 |  4.759 % |
c |     90648 |  911482  2514375 |  367634   89509  1737668    19.4 |  4.759 % |
c |     90873 |  911482  2514375 |  404397   89734  1742498    19.4 |  4.759 % |
c |     91210 |  911482  2514375 |  444837   90071  1750209    19.4 |  4.759 % |
c |     91717 |  911482  2514375 |  489321   90578  1761994    19.5 |  4.759 % |
c |     92476 |  911482  2514375 |  538253   91337  1783191    19.5 |  4.759 % |
c |     93615 |  911474  2514354 |  592078   92475  1815675    19.6 |  4.760 % |
c |     95325 |  911474  2514354 |  651286   94185  1857776    19.7 |  4.760 % |
c |     97889 |  911474  2514354 |  716415   96749  1908421    19.7 |  4.760 % |
c ==============================================================================
c [1mFound solution: 169553[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98520 |  911502  2514422 |  303834   97380  1926121    19.8 |  4.760 % |
c |     98620 |  911502  2514422 |  334217   97480  1927365    19.8 |  4.761 % |
c |     98770 |  911502  2514422 |  367639   97630  1929702    19.8 |  4.761 % |
c |     98996 |  911502  2514422 |  404403   97856  1932719    19.8 |  4.761 % |
c |     99334 |  911502  2514422 |  444843   98194  1937499    19.7 |  4.761 % |
c |     99840 |  911502  2514422 |  489327   98700  1946525    19.7 |  4.761 % |
c |    100600 |  911502  2514422 |  538260   99460  1959447    19.7 |  4.761 % |
c |    101739 |  911502  2514422 |  592086  100599  1980465    19.7 |  4.761 % |
c |    103448 |  911502  2514422 |  651295  102308  2052759    20.1 |  4.761 % |
c |    106010 |  911502  2514422 |  716424  104870  2127984    20.3 |  4.761 % |
c |    109854 |  911494  2514401 |  788067  108712  2237378    20.6 |  4.761 % |
c |    115620 |  911494  2514401 |  866873  114478  2377735    20.8 |  4.761 % |
c ==============================================================================
c [1mFound solution: 169537[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:   14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    117838 |  911526  2514479 |  303842  116696  2422720    20.8 |  4.761 % |
c |    117939 |  911518  2514458 |  334226  116796  2424780    20.8 |  4.763 % |
c |    118090 |  911518  2514458 |  367648  116947  2428307    20.8 |  4.763 % |
c |    118316 |  911518  2514458 |  404413  117173  2433287    20.8 |  4.763 % |
c |    118653 |  911518  2514458 |  444855  117510  2443971    20.8 |  4.763 % |
c |    119159 |  911518  2514458 |  489340  118016  2456219    20.8 |  4.763 % |
c |    119919 |  911518  2514458 |  538274  118776  2473703    20.8 |  4.763 % |
c |    121059 |  911518  2514458 |  592102  119916  2502581    20.9 |  4.763 % |
c |    122767 |  911518  2514458 |  651312  121624  2564286    21.1 |  4.763 % |
c |    125333 |  911518  2514458 |  716443  124190  2646595    21.3 |  4.763 % |
c |    129178 |  911506  2514428 |  788087  128032  2739618    21.4 |  4.764 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v x1_bit_7 -x1_bit_6 -x1_bit_5 -x1_bit_4 -x1_bit_3 -x1_bit_2 x1_bit_1 -x1_bit0 -x1_bit1 x1_bit2 x1_bit3 -x1_bit4 x1_bit5 -x1_bit6 -x1_bit7 x1_bit8 -x1_bit9 x1_bit10 -x1_bit11 -x1_bit12 -x3_bit0 -x5_bit0 -x6_bit0 x7_bit0 -x11_bit0 x12_bit0 -x13_bit0 -x16_bit0 -x17_bit0 -x18_bit0 x21_bit0 -x22_bit0 -x23_bit0 -x26_bit0 -x27_bit0 -x28_bit0 -x31_bit0 -x32_bit0 -x33_bit0 -x36_bit0 -x37_bit0 x38_bit0 x41_bit0 x42_bit0 x43_bit0 -x46_bit0 -x47_bit0 -x48_bit0 x51_bit0 x52_bit0 x53_bit0 x56_bit0 x57_bit0 -x58_bit0 -x61_bit0 -x62_bit0 -x63_bit0 -x66_bit0 -x67_bit0 x68_bit0 -x71_bit0 -x72_bit0 -x73_bit0 -x76_bit0 -x77_bit0 -x78_bit0 -x81_bit0 -x82_bit0 -x83_bit0 -x86_bit0 -x87_bit0 -x88_bit0 -x91_bit0 -x92_bit0 -x93_bit0 x96_bit0 x97_bit0 -x98_bit0 x101_bit0 x102_bit0 -x103_bit0 -x106_bit0 -x107_bit0 -x108_bit0 -x111_bit0 -x112_bit0 x113_bit0 x116_bit0 -x117_bit0 x118_bit0 -x121_bit0 -x122_bit0 -x123_bit0 -x126_bit0 -x127_bit0 -x128_bit0 -x131_bit0 -x132_bit0 -x133_bit0 -x136_bit0 x137_bit0 x138_bit0 -x141_bit0 -x142_bit0 -x143_bit0 -x146_bit0 -x147_bit0 -x148_bit0 -x151_bit0 -x152_bit0 -x153_bit0 -x156_bit0 -x157_bit0 x158_bit0 -x161_bit0 -x162_bit0 -x163_bit0 -x165_bit0 x166_bit0 -x167_bit0 x168_bit0 x169_bit0 -x170_bit0 x171_bit0 -x172_bit0 -x173_bit0 -x174_bit0 x175_bit0 -x176_bit0 x177_bit0 -x178_bit0 x179_bit0 -x180_bit0 -x181_bit0 x182_bit0 -x183_bit0 x184_bit0 -x185_bit0 x186_bit0 -x187_bit0 x188_bit0 -x189_bit0 x190_bit0 -x191_bit0 x192_bit0 -x193_bit0 -x194_bit0 x195_bit0 -x196_bit0 x197_bit0 -x198_bit0 x199_bit0 -x200_bit0 x201_bit0 -x202_bit0 x203_bit0 -x204_bit0 x205_bit0 -x206_bit0 -x207_bit0 x208_bit0 -x209_bit0 x210_bit0 x211_bit0 -x212_bit0 x213_bit0 -x214_bit0 x215_bit0 -x216_bit0 x217_bit0 -x218_bit0 -x219_bit0 x220_bit0 x221_bit0 -x222_bit0 x223_bit0 -x224_bit0 x225_bit0 -x226_bit0 -x227_bit0 -x228_bit0 x229_bit0 x230_bit0 -x231_bit0 -x232_bit0 -x233_bit0 -x234_bit0 -x235_bit0 -x236_bit0 x237_bit0 x238_bit0 -x239_bit0 -x240_bit0 x241_bit0 x242_bit0 x243_bit0 x244_bit0 -x245_bit0 -x246_bit0 -x247_bit0 -x248_bit0 -x249_bit0 -x250_bit0 -x251_bit0 -x252_bit0 -x253_bit0 -x254_bit0 -x255_bit0 -x256_bit0 -x257_bit0 -x258_bit0 x259_bit0 x260_bit0 x261_bit0 x262_bit0 -x263_bit0 -x264_bit0 -x265_bit0 -x266_bit0 x267_bit0 x268_bit0 -x269_bit0 -x270_bit0 -x271_bit0 -x272_bit0 -x273_bit0 -x274_bit0 x275_bit0 x276_bit0 -x277_bit0 -x278_bit0 -x279_bit0 -x280_bit0 -x281_bit0 -x282_bit0 -x283_bit0 -x284_bit0 -x285_bit0 -x286_bit0 x287_bit0 -x288_bit0 x289_bit0 x290_bit0 -x291_bit0 -x292_bit0 x293_bit0 x294_bit0 x295_bit0 -x296_bit0 x297_bit0 x298_bit0 x299_bit0 -x300_bit0 x301_bit0 x302_bit0 -x303_bit0 -x304_bit0 x305_bit0 x306_bit0 -x307_bit0 -x308_bit0 -x309_bit0 -x310_bit0 -x311_bit0 -x312_bit0 x313_bit0 x314_bit0 x315_bit0 x316_bit0 x317_bit0 -x318_bit0 x319_bit0 -x320_bit0 x321_bit0 x322_bit0 x323_bit0 x324_bit0 x325_bit0 -x326_bit0 x327_bit0 x328_bit0 -x329_bit0 x330_bit0 x331_bit0 x332_bit0 x333_bit0 -x334_bit0 x335_bit0 x336_bit0 x337_bit0 x338_bit0 x339_bit0 x340_bit0 x341_bit0 x342_bit0 x343_bit0 x344_bit0 -x345_bit0 -x346_bit0 -x347_bit0 -x348_bit0 -x349_bit0 -x350_bit0 x351_bit0 x352_bit0 -x353_bit0 -x354_bit0 x355_bit0 x356_bit0 -x357_bit0 -x358_bit0 -x359_bit0 -x360_bit0 -x361_bit0 -x362_bit0 -x363_bit0 -x364_bit0 -x365_bit0 -x366_bit0 -x367_bit0 -x368_bit0 -x369_bit0 -x370_bit0 -x371_bit0 -x372_bit0 x373_bit0 x374_bit0 -x375_bit0 -x376_bit0 -x377_bit0 -x378_bit0 x379_bit0 x380_bit0 x381_bit0 x382_bit0 -x383_bit0 -x384_bit0 -x385_bit0 -x386_bit0 -x387_bit0 -x388_bit0 -x389_bit0 x390_bit0 -x391_bit0 -x392_bit0 -x393_bit0 -x394_bit0 -x395_bit0 -x396_bit0 -x397_bit0 -x398_bit0 -x399_bit0 -x400_bit0 -x401_bit0 -x402_bit0 x403_bit0 x404_bit0 x405_bit0 -x406_bit0 x407_bit0 -x408_bit0 x409_bit0 -x410_bit0 -x411_bit0 x412_bit0 -x413_bit0 -x414_bit0 -x415_bit0 x416_bit0 -x417_bit0 -x418_bit0 -x419_bit0 -x420_bit0 -x421_bit0 -x422_bit0 x423_bit0 x424_bit0 x425_bit0 x426_bit0 x427_bit0 -x428_bit0 x429_bit0 -x430_bit0 x431_bit0 x432_bit0 -x433_bit0 -x434_bit0 x435_bit0 -x436_bit0 -x437_bit0 x438_bit0 -x439_bit0 x440_bit0 x441_bit0 x442_bit0 x443_bit0 -x444_bit0 x445_bit0 -x446_bit0 -x447_bit0 x448_bit0 -x449_bit0 -x450_bit0 -x451_bit0 x452_bit0 x453_bit0 -x454_bit0 x455_bit0 -x456_bit0 x457_bit0 -x458_bit0 x459_bit0 -x460_bit0 -x461_bit0 x462_bit0 -x463_bit0 x464_bit0 -x465_bit0 x466_bit0 x467_bit0 -x468_bit0 -x469_bit0 x470_bit0 x471_bit0 -x472_bit0 -x473_bit0 x474_bit0 x475_bit0 -x476_bit0 x477_bit0 -x478_bit0 x479_bit0 -x480_bit0 x481_bit0 -x482_bit0 x483_bit0 -x484_bit0 x485_bit0 -x486_bit0 -x487_bit0 x488_bit0 -x489_bit0 x490_bit0 -x491_bit0 x492_bit0 x493_bit0 -x494_bit0 -x495_bit0 x496_bit0 x497_bit0 -x498_bit0 -x499_bit0 x500_bit0 x501_bit0 -x502_bit0 -x503_bit0 x504_bit0 x505_bit0 -x506_bit0 x507_bit0 -x508_bit0 -x509_bit0 x510_bit0 -x511_bit0 x512_bit0 -x513_bit0 x514_bit0 -x515_bit0 -x516_bit0 -x517_bit0 x518_bit0 -x519_bit0 -x520_bit0 -x521_bit0 -x522_bit0 -x523_bit0 -x524_bit0 -x525_bit0 x526_bit0 -x527_bit0 x528_bit0 x529_bit0 -x530_bit0 x531_bit0 -x532_bit0 -x533_bit0 -x534_bit0 -x535_bit0 -x536_bit0 -x537_bit0 x538_bit0 -x539_bit0 x540_bit0 -x541_bit0 x542_bit0 -x543_bit0 x544_bit0 -x545_bit0 x546_bit0 x547_bit0 -x548_bit0 -x549_bit0 x550_bit0 -x551_bit0 -x552_bit0 -x553_bit0 x554_bit0 -x555_bit0 x556_bit0 -x557_bit0 -x558_bit0 -x559_bit0 x560_bit0 -x561_bit0 x562_bit0 -x563_bit0 -x564_bit0 -x565_bit0 -x566_bit0 -x567_bit0 -x568_bit0 -x569_bit0 -x570_bit0 -x571_bit0 -x572_bit0 -x573_bit0 -x574_bit0 -x575_bit0 -x576_bit0 x577_bit0 -x578_bit0 -x579_bit0 x580_bit0 -x581_bit0 -x582_bit0 -x583_bit0 -x584_bit0 x585_bit0 -x586_bit0 -x587_bit0 -x588_bit0 -x589_bit0 -x590_bit0 -x591_bit0 -x592_bit0 -x593_bit0 x594_bit0 -x595_bit0 -x596_bit0 -x597_bit0 -x598_bit0 -x599_bit0 -x600_bit0 -x601_bit0 -x602_bit0 -x603_bit0 -x604_bit0 x605_bit0 -x606_bit0 -x607_bit0 x608_bit0 -x609_bit0 -x610_bit0 -x611_bit0 x612_bit0 -x613_bit0 -x614_bit0 -x615_bit0 -x616_bit0 -x617_bit0 -x618_bit0 -x619_bit0 -x620_bit0 x621_bit0 x622_bit0 x623_bit0 -x624_bit0 x625_bit0 -x626_bit0 -x627_bit0 -x628_bit0 -x629_bit0 -x630_bit0 x631_bit0 -x632_bit0 -x633_bit0 -x634_bit0 -x635_bit0 -x636_bit0 -x637_bit0 -x638_bit0 -x639_bit0 x640_bit0 x641_bit0 x642_bit0 -x643_bit0 -x644_bit0 -x645_bit0 -x646_bit0 -x647_bit0 x648_bit0 x649_bit0 x650_bit0 -x651_bit0 x652_bit0 -x653_bit0 -x654_bit0 -x655_bit0 -x656_bit0 -x657_bit0 -x658_bit0 -x659_bit0 -x660_bit0 -x661_bit0 -x662_bit0 -x663_bit0 -x664_bit0 -x665_bit0 -x666_bit0 x667_bit0 x668_bit0 x669_bit0 x670_bit0 -x671_bit0 -x672_bit0 -x673_bit0 -x674_bit0 x675_bit0 -x676_bit0 -x677_bit0 -x678_bit0 -x679_bit0 -x680_bit0 -x681_bit0 -x682_bit0 -x683_bit0 x684_bit0 x685_bit0 x686_bit0 -x687_bit0 -x688_bit0 -x689_bit0 -x690_bit0 -x691_bit0 -x692_bit0 x693_bit0 x694_bit0 -x695_bit0 -x696_bit0 x697_bit0 x698_bit0 -x699_bit0 -x700_bit0 -x701_bit0 -x702_bit0 -x703_bit0 -x704_bit0 -x705_bit0 -x706_bit0 -x707_bit0 -x708_bit0 x709_bit0 x710_bit0 x711_bit0 x712_bit0 -x713_bit0 -x714_bit0 -x715_bit0 -x716_bit0 x717_bit0 -x718_bit0 -x719_bit0 -x720_bit0 -x721_bit0 -x722_bit0 -x723_bit0 -x724_bit0 -x725_bit0 x726_bit0 x727_bit0 x728_bit0 -x729_bit0 -x730_bit0 -x731_bit0 -x732_bit0 -x733_bit0 -x734_bit0 x735_bit0 x736_bit0 x737_bit0 -x738_bit0 -x739_bit0 x740_bit0 x741_bit0 x742_bit0 x743_bit0 x744_bit0 x745_bit0 -x746_bit0 x747_bit0 -x748_bit0 x749_bit0 -x750_bit0 x751_bit0 -x752_bit0 x753_bit0 -x754_bit0 x755_bit0 -x756_bit0 x757_bit0 -x758_bit0 x759_bit0 -x760_bit0 -x761_bit0 x762_bit0 x763_bit0 -x764_bit0 x765_bit0 -x766_bit0 x767_bit0 -x768_bit0 x769_bit0 -x770_bit0 x771_bit0 -x772_bit0 x773_bit0 -x774_bit0 x775_bit0 -x776_bit0 -x777_bit0 -x778_bit0 -x779_bit0 -x780_bit0 -x781_bit0 -x782_bit0 -x783_bit0 -x784_bit0 x785_bit0 x786_bit0 x787_bit0 -x788_bit0 x789_bit0 -x790_bit0 -x791_bit0 -x792_bit0 -x793_bit0 -x794_bit0 x795_bit0 -x796_bit0 -x797_bit0 -x798_bit0 -x799_bit0 -x800_bit0 x801_bit0 x802_bit0 -x803_bit0 x804_bit0 x805_bit0 x806_bit0 -x807_bit0 -x808_bit0 -x809_bit0 -x810_bit0 -x811_bit0 x812_bit0 x813_bit0 x814_bit0 x815_bit0 x816_bit0 x817_bit0 x818_bit0 x819_bit0 -x820_bit0 x821_bit0 -x822_bit0 x823_bit0 -x824_bit0 x825_bit0 -x826_bit0 x827_bit0 -x828_bit0 x829_bit0 -x830_bit0 x831_bit0 -x832_bit0 x833_bit0 -x834_bit0 x835_bit0 -x836_bit0 x837_bit0 -x838_bit0 x839_bit0 -x840_bit0 x841_bit0 -x842_bit0 x843_bit0 -x844_bit0 x845_bit0 -x846_bit0 x847_bit0 -x848_bit0 x849_bit0 -x850_bit0 -x851_bit0 -x852_bit0 x853_bit0 x854_bit0 x855_bit0 -x856_bit0 x857_bit0 -x858_bit0 x859_bit0 -x860_bit0 x861_bit0 -x862_bit0 x863_bit0 -x864_bit0 x865_bit0 -x866_bit0 x867_bit0 -x868_bit0 -x869_bit0 x870_bit0 x871_bit0 -x872_bit0 -x873_bit0 x874_bit0 x875_bit0 -x876_bit0 x877_bit0 -x878_bit0 x879_bit0 -x880_bit0 -x881_bit0 x882_bit0 x883_bit0 -x884_bit0 x885_bit0 -x886_bit0 x887_bit0 -x888_bit0 x889_bit0 -x890_bit0 x891_bit0 -x892_bit0 x893_bit0 -x894_bit0 x895_bit0 -x896_bit0 x897_bit0 -x898_bit0 x899_bit0 -x900_bit0 -x901_bit0 x902_bit0 x903_bit0 -x904_bit0 x905_bit0 -x906_bit0 x907_bit0 -x908_bit0 x909_bit0 -x910_bit0 x911_bit0 -x912_bit0 x913_bit0 -x914_bit0 x915_bit0 -x916_bit0 x917_bit0 -x918_bit0 x919_bit0 -x920_bit0 x921_bit0 -x922_bit0 x923_bit0 x924_bit0 -x925_bit0 x926_bit0 -x927_bit0 x928_bit0 -x929_bit0 x930_bit0 -x931_bit0 x932_bit0 -x933_bit0 x934_bit0 x935_bit0 -x936_bit0 x937_bit0 -x938_bit0 -x939_bit0 x940_bit0 -x941_bit0 x942_bit0 -x943_bit0 x944_bit0 x945_bit0 -x946_bit0 x947_bit0 -x948_bit0 x949_bit0 -x950_bit0 -x951_bit0 -x952_bit0 -x953_bit0 -x954_bit0 x955_bit0 -x956_bit0 -x957_bit0 x958_bit0 -x959_bit0 x960_bit0 -x961_bit0 x962_bit0 x963_bit0 -x964_bit0 x965_bit0 -x966_bit0 -x967_bit0 -x968_bit0 -x969_bit0 -x970_bit0 -x971_bit0 x972_bit0 x973_bit0 -x974_bit0 -x975_bit0 -x976_bit0 -x977_bit0 -x978_bit0 -x979_bit0 -x980_bit0 -x981_bit0 x982_bit0 -x983_bit0 -x984_bit0 -x985_bit0 -x986_bit0 -x987_bit0 -x988_bit0 -x989_bit0 x990_bit0 -x991_bit0 -x992_bit0 -x993_bit0 -x994_bit0 -x995_bit0 -x996_bit0 -x997_bit0 -x998_bit0 -x999_bit0 -x1000_bit0 -x1001_bit0 -x1002_bit0 -x1003_bit0 -x1004_bit0 -x1005_bit0 x1006_bit0 -x1007_bit0 -x1008_bit0 -x1009_bit0 -x1010_bit0 -x1011_bit0 -x1012_bit0 -x1013_bit0 x1014_bit0 -x1015_bit0 -x1016_bit0 -x1017_bit0 -x1018_bit0 -x1019_bit0 -x1020_bit0 -x1021_bit0 -x1022_bit0 -x1023_bit0 -x1024_bit0 -x1025_bit0 x1026_bit0 -x1027_bit0 x1028_bit0 x1029_bit0 -x1030_bit0 -x1031_bit0 x1032_bit0 -x1033_bit0 x1034_bit0 x1035_bit0 -x1036_bit0 x1037_bit0 -x1038_bit0 -x1039_bit0 x1040_bit0 -x1041_bit0 x1042_bit0 x1043_bit0 -x1044_bit0 x1045_bit0 -x1046_bit0 -x1047_bit0 x1048_bit0 x1049_bit0 -x1050_bit0 -x1051_bit0 x1052_bit0 x1053_bit0 x1054_bit0 -x1055_bit0 x1056_bit0 x1057_bit0 -x1058_bit0 -x1059_bit0 x1060_bit0 -x1061_bit0 -x1062_bit0 x1063_bit0 -x1064_bit0 x1065_bit0 -x1066_bit0 -x1067_bit0 -x1068_bit0 -x1069_bit0 -x1070_bit0 -x1071_bit0 -x1072_bit0 -x1073_bit0 x1074_bit0 -x1075_bit0 -x1076_bit0 -x1077_bit0 -x1078_bit0 -x1079_bit0 -x1080_bit0 -x1081_bit0 -x1082_bit0 -x1083_bit0 -x1084_bit0 -x1085_bit0 x1086_bit0 x1087_bit0 x1088_bit0 x1089_bit0 -x1090_bit0 x1091_bit0 -x1092_bit0 -x1093_bit0 -x1094_bit0 -x1095_bit0 -x1096_bit0 -x1097_bit0 x1098_bit0 x1099_bit0 -x1100_bit0 x1101_bit0 x1102_bit0 x1103_bit0 -x1104_bit0 x1105_bit0 -x1106_bit0 x1107_bit0 x1108_bit0 x1109_bit0 x1110_bit0 x1111_bit0 x1112_bit0 x1113_bit0 -x1114_bit0 x1115_bit0 -x1116_bit0 x1117_bit0 -x1118_bit0 -x1119_bit0 x1120_bit0 -x1121_bit0 -x1122_bit0 -x1123_bit0 x1124_bit0 x1125_bit0 -x1126_bit0 x1127_bit0 x1128_bit0 -x1129_bit0 -x1130_bit0 -x1131_bit0 -x1132_bit0 -x1133_bit0 -x1134_bit0 x1135_bit0 x1136_bit0 -x1137_bit0 -x1138_bit0 -x1139_bit0 -x1140_bit0 -x1141_bit0 x1142_bit0 -x1143_bit0 x1144_bit0 x1145_bit0 x1146_bit0 x1147_bit0 -x1148_bit0 x1149_bit0 -x1150_bit0 -x1151_bit0 x1152_bit0 x1153_bit0 -x1154_bit0 x1155_bit0 -x1156_bit0 x2_bit_7 x2_bit_6 -x2_bit_5 -x2_bit_4 -x2_bit_3 -x2_bit_2 -x2_bit_1 -x2_bit0 -x2_bit1 x2_bit2 x2_bit3 -x2_bit4 -x2_bit5 -x2_bit6 x2_bit7 -x2_bit8 -x2_bit9 -x2_bit10 -x2_bit11 -x2_bit12 x4_bit_7 -x4_bit_6 -x4_bit_5 -x4_bit_4 -x4_bit_3 -x4_bit_2 -x4_bit_1 -x4_bit0 -x4_bit1 -x4_bit2 -x4_bit3 -x4_bit4 -x4_bit5 -x4_bit6 -x4_bit7 -x4_bit8 -x4_bit9 x4_bit10 -x4_bit11 -x4_bit12 -x15_bit_7 -x15_bit_6 -x15_bit_5 -x15_bit_4 -x15_bit_3 x15_bit_2 -x15_bit_1 -x15_bit0 -x15_bit1 -x15_bit2 x15_bit3 -x15_bit4 -x15_bit5 -x15_bit6 x15_bit7 x15_bit8 -x15_bit9 -x15_bit10 -x15_bit11 -x15_bit12 x8_bit_7 -x8_bit_6 -x8_bit_5 -x8_bit_4 -x8_bit_3 -x8_bit_2 -x8_bit_1 -x8_bit0 -x8_bit1 -x8_bit2 x8_bit3 x8_bit4 -x8_bit5 -x8_bit6 x8_bit7 x8_bit8 x8_bit9 -x8_bit10 -x8_bit11 -x8_bit12 -x129_bit_7 -x129_bit_6 -x129_bit_5 -x129_bit_4 -x129_bit_3 -x129_bit_2 -x129_bit_1 -x129_bit0 -x129_bit1 -x129_bit2 x129_bit3 x129_bit4 -x129_bit5 -x129_bit6 -x129_bit7 -x129_bit8 -x129_bit9 x129_bit10 -x129_bit11 -x129_bit12 -x44_bit_7 -x44_bit_6 -x44_bit_5 -x44_bit_4 -x44_bit_3 -x44_bit_2 -x44_bit_1 -x44_bit0 -x44_bit1 -x44_bit2 x44_bit3 -x44_bit4 -x44_bit5 -x44_bit6 -x44_bit7 -x44_bit8 -x44_bit9 -x44_bit10 -x44_bit11 -x44_bit12 -x154_bit_7 -x154_bit_6 -x154_bit_5 -x154_bit_4 -x154_bit_3 -x154_bit_2 -x154_bit_1 -x154_bit0 -x154_bit1 x154_bit2 x154_bit3 x154_bit4 x154_bit5 x154_bit6 x154_bit7 -x154_bit8 -x154_bit9 -x154_bit10 -x154_bit11 -x154_bit12 -x40_bit_7 -x40_bit_6 -x40_bit_5 -x40_bit_4 -x40_bit_3 -x40_bit_2 -x40_bit_1 x40_bit0 -x40_bit1 -x40_bit2 -x40_bit3 -x40_bit4 x40_bit5 -x40_bit6 x40_bit7 -x40_bit8 -x40_bit9 -x40_bit10 -x40_bit11 -x40_bit12 -x155_bit_7 -x155_bit_6 -x155_bit_5 -x155_bit_4 -x155_bit_3 -x155_bit_2 x155_bit_1 -x155_bit0 x155_bit1 x155_bit2 x155_bit3 x155_bit4 x155_bit5 x155_bit6 x155_bit7 x155_bit8 -x155_bit9 -x155_bit10 -x155_bit11 -x155_bit12 x159_bit_7 -x159_bit_6 -x159_bit_5 -x159_bit_4 -x159_bit_3 -x159_bit_2 x159_bit_1 x159_bit0 x159_bit1 -x159_bit2 x159_bit3 -x159_bit4 -x159_bit5 x159_bit6 x159_bit7 -x159_bit8 x159_bit9 -x159_bit10 -x159_bit11 -x159_bit12 -x160_bit_7 -x160_bit_6 -x160_bit_5 -x160_bit_4 -x160_bit_3 -x160_bit_2 x160_bit_1 -x160_bit0 -x160_bit1 x160_bit2 x160_bit3 -x160_bit4 x160_bit5 -x160_bit6 -x160_bit7 x160_bit8 -x160_bit9 -x160_bit10 -x160_bit11 -x160_bit12 -x164_bit_7 -x164_bit_6 -x164_bit_5 -x164_bit_4 -x164_bit_3 -x164_bit_2 -x164_bit_1 x164_bit0 -x164_bit1 x164_bit2 -x164_bit3 x164_bit4 -x164_bit5 x164_bit6 x164_bit7 -x164_bit8 -x164_bit9 -x164_bit10 -x164_bit11 -x164_bit12 x45_bit_7 -x45_bit_6 -x45_bit_5 -x45_bit_4 -x45_bit_3 -x45_bit_2 x45_bit_1 x45_bit0 -x45_bit1 -x45_bit2 x45_bit3 -x45_bit4 -x45_bit5 x45_bit6 -x45_bit7 x45_bit8 -x45_bit9 -x45_bit10 -x45_bit11 -x45_bit12 -x50_bit_7 -x50_bit_6 x50_bit_5 -x50_bit_4 -x50_bit_3 -x50_bit_2 x50_bit_1 x50_bit0 x50_bit1 x50_bit2 -x50_bit3 x50_bit4 x50_bit5 x50_bit6 -x50_bit7 -x50_bit8 -x50_bit9 -x50_bit10 -x50_bit11 -x50_bit12 x130_bit_7 -x130_bit_6 -x130_bit_5 -x130_bit_4 -x130_bit_3 -x130_bit_2 x130_bit_1 x130_bit0 x130_bit1 x130_bit2 x130_bit3 x130_bit4 x130_bit5 x130_bit6 x130_bit7 x130_bit8 -x130_bit9 -x130_bit10 -x130_bit11 -x130_bit12 -x49_bit_7 -x49_bit_6 -x49_bit_5 -x49_bit_4 -x49_bit_3 -x49_bit_2 -x49_bit_1 x49_bit0 -x49_bit1 -x49_bit2 x49_bit3 x49_bit4 -x49_bit5 x49_bit6 -x49_bit7 x49_bit8 -x49_bit9 -x49_bit10 -x49_bit11 -x49_bit12 -x54_bit_7 -x54_bit_6 x54_bit_5 -x54_bit_4 -x54_bit_3 -x54_bit_2 x54_bit_1 x54_bit0 -x54_bit1 x54_bit2 x54_bit3 x54_bit4 x54_bit5 x54_bit6 x54_bit7 x54_bit8 -x54_bit9 -x54_bit10 -x54_bit11 -x54_bit12 -x55_bit_7 -x55_bit_6 -x55_bit_5 x55_bit_4 -x55_bit_3 -x55_bit_2 -x55_bit_1 -x55_bit0 -x55_bit1 x55_bit2 x55_bit3 -x55_bit4 -x55_bit5 -x55_bit6 x55_bit7 -x55_bit8 -x55_bit9 -x55_bit10 -x55_bit11 -x55_bit12 -x59_bit_7 -x59_bit_6 -x59_bit_5 -x59_bit_4 -x59_bit_3 x59_bit_2 x59_bit_1 -x59_bit0 x59_bit1 x59_bit2 -x59_bit3 x59_bit4 -x59_bit5 x59_bit6 x59_bit7 -x59_bit8 x59_bit9 -x59_bit10 -x59_bit11 -x59_bit12 -x60_bit_7 x60_bit_6 -x60_bit_5 -x60_bit_4 x60_bit_3 -x60_bit_2 -x60_bit_1 -x60_bit0 x60_bit1 -x60_bit2 x60_bit3 x60_bit4 x60_bit5 -x60_bit6 -x60_bit7 -x60_bit8 -x60_bit9 x60_bit10 -x60_bit11 -x60_bit12 -x64_bit_7 x64_bit_6 -x64_bit_5 -x64_bit_4 -x64_bit_3 x64_bit_2 -x64_bit_1 x64_bit0 x64_bit1 x64_bit2 x64_bit3 x64_bit4 x64_bit5 x64_bit6 -x64_bit7 -x64_bit8 x64_bit9 -x64_bit10 -x64_bit11 -x64_bit12 -x65_bit_7 -x65_bit_6 x65_bit_5 -x65_bit_4 -x65_bit_3 -x65_bit_2 -x65_bit_1 x65_bit0 x65_bit1 -x65_bit2 -x65_bit3 -x65_bit4 -x65_bit5 -x65_bit6 x65_bit7 x65_bit8 -x65_bit9 -x65_bit10 -x65_bit11 -x65_bit12 -x69_bit_7 -x69_bit_6 -x69_bit_5 x69_bit_4 -x69_bit_3 -x69_bit_2 -x69_bit_1 -x69_bit0 x69_bit1 x69_bit2 x69_bit3 x69_bit4 x69_bit5 -x69_bit6 -x69_bit7 -x69_bit8 x69_bit9 -x69_bit10 -x69_bit11 -x69_bit12 -x70_bit_7 -x70_bit_6 -x70_bit_5 -x70_bit_4 x70_bit_3 -x70_bit_2 -x70_bit_1 -x70_bit0 -x70_bit1 -x70_bit2 x70_bit3 -x70_bit4 -x70_bit5 -x70_bit6 -x70_bit7 -x70_bit8 -x70_bit9 x70_bit10 -x70_bit11 -x70_bit12 -x74_bit_7 -x74_bit_6 x74_bit_5 -x74_bit_4 x74_bit_3 x74_bit_2 -x74_bit_1 -x74_bit0 -x74_bit1 -x74_bit2 -x74_bit3 x74_bit4 x74_bit5 -x74_bit6 -x74_bit7 x74_bit8 x74_bit9 -x74_bit10 -x74_bit11 -x74_bit12 -x75_bit_7 -x75_bit_6 -x75_bit_5 -x75_bit_4 -x75_bit_3 -x75_bit_2 x75_bit_1 x75_bit0 x75_bit1 x75_bit2 x75_bit3 x75_bit4 x75_bit5 x75_bit6 x75_bit7 x75_bit8 x75_bit9 -x75_bit10 -x75_bit11 -x75_bit12 -x134_bit_7 -x134_bit_6 -x134_bit_5 -x134_bit_4 -x134_bit_3 -x134_bit_2 -x134_bit_1 x134_bit0 x134_bit1 -x134_bit2 x134_bit3 x134_bit4 x134_bit5 x134_bit6 x134_bit7 -x134_bit8 -x134_bit9 -x134_bit10 -x134_bit11 -x134_bit12 -x79_bit_7 -x79_bit_6 -x79_bit_5 -x79_bit_4 -x79_bit_3 -x79_bit_2 -x79_bit_1 x79_bit0 -x79_bit1 x79_bit2 -x79_bit3 x79_bit4 x79_bit5 x79_bit6 -x79_bit7 x79_bit8 -x79_bit9 -x79_bit10 -x79_bit11 -x79_bit12 -x80_bit_7 -x80_bit_6 -x80_bit_5 -x80_bit_4 -x80_bit_3 -x80_bit_2 x80_bit_1 x80_bit0 x80_bit1 x80_bit2 -x80_bit3 x80_bit4 x80_bit5 x80_bit6 -x80_bit7 -x80_bit8 -x80_bit9 x80_bit10 -x80_bit11 -x80_bit12 -x84_bit_7 -x84_bit_6 -x84_bit_5 -x84_bit_4 -x84_bit_3 -x84_bit_2 -x84_bit_1 -x84_bit0 x84_bit1 x84_bit2 x84_bit3 -x84_bit4 -x84_bit5 x84_bit6 x84_bit7 x84_bit8 -x84_bit9 -x84_bit10 -x84_bit11 -x84_bit12 x85_bit_7 -x85_bit_6 -x85_bit_5 -x85_bit_4 -x85_bit_3 -x85_bit_2 x85_bit_1 x85_bit0 -x85_bit1 -x85_bit2 x85_bit3 x85_bit4 -x85_bit5 x85_bit6 x85_bit7 -x85_bit8 x85_bit9 -x85_bit10 -x85_bit11 -x85_bit12 -x89_bit_7 x89_bit_6 -x89_bit_5 -x89_bit_4 -x89_bit_3 -x89_bit_2 -x89_bit_1 -x89_bit0 -x89_bit1 x89_bit2 -x89_bit3 -x89_bit4 -x89_bit5 -x89_bit6 x89_bit7 -x89_bit8 -x89_bit9 -x89_bit10 -x89_bit11 -x89_bit12 -x90_bit_7 -x90_bit_6 -x90_bit_5 -x90_bit_4 -x90_bit_3 x90_bit_2 -x90_bit_1 x90_bit0 x90_bit1 x90_bit2 x90_bit3 x90_bit4 x90_bit5 x90_bit6 x90_bit7 x90_bit8 -x90_bit9 -x90_bit10 -x90_bit11 -x90_bit12 -x94_bit_7 x94_bit_6 -x94_bit_5 -x94_bit_4 -x94_bit_3 -x94_bit_2 -x94_bit_1 -x94_bit0 -x94_bit1 x94_bit2 -x94_bit3 -x94_bit4 -x94_bit5 -x94_bit6 x94_bit7 -x94_bit8 -x94_bit9 -x94_bit10 -x94_bit11 -x94_bit12 x95_bit_7 -x95_bit_6 -x95_bit_5 -x95_bit_4 x95_bit_3 -x95_bit_2 x95_bit_1 -x95_bit0 -x95_bit1 -x95_bit2 -x95_bit3 -x95_bit4 -x95_bit5 -x95_bit6 -x95_bit7 -x95_bit8 -x95_bit9 -x95_bit10 -x95_bit11 -x95_bit12 x99_bit_7 -x99_bit_6 -x99_bit_5 -x99_bit_4 -x99_bit_3 -x99_bit_2 x99_bit_1 x99_bit0 -x99_bit1 x99_bit2 x99_bit3 -x99_bit4 -x99_bit5 -x99_bit6 -x99_bit7 -x99_bit8 -x99_bit9 -x99_bit10 -x99_bit11 -x99_bit12 x100_bit_7 -x100_bit_6 x100_bit_5 -x100_bit_4 -x100_bit_3 -x100_bit_2 -x100_bit_1 -x100_bit0 -x100_bit1 -x100_bit2 -x100_bit3 -x100_bit4 x100_bit5 -x100_bit6 x100_bit7 -x100_bit8 -x100_bit9 -x100_bit10 -x100_bit11 -x100_bit12 x135_bit_7 -x135_bit_6 -x135_bit_5 -x135_bit_4 x135_bit_3 -x135_bit_2 -x135_bit_1 -x135_bit0 -x135_bit1 x135_bit2 x135_bit3 -x135_bit4 -x135_bit5 -x135_bit6 -x135_bit7 -x135_bit8 -x135_bit9 -x135_bit10 -x135_bit11 -x135_bit12 -x104_bit_7 x104_bit_6 -x104_bit_5 x104_bit_4 x104_bit_3 x104_bit_2 -x104_bit_1 -x104_bit0 x104_bit1 -x104_bit2 -x104_bit3 -x104_bit4 x104_bit5 x104_bit6 -x104_bit7 -x104_bit8 -x104_bit9 -x104_bit10 -x104_bit11 -x104_bit12 -x105_bit_7 -x105_bit_6 -x105_bit_5 -x105_bit_4 -x105_bit_3 x105_bit_2 x105_bit_1 x105_bit0 -x105_bit1 -x105_bit2 x105_bit3 -x105_bit4 x105_bit5 -x105_bit6 -x105_bit7 x105_bit8 x105_bit9 -x105_bit10 -x105_bit11 -x105_bit12 -x109_bit_7 -x109_bit_6 -x109_bit_5 -x109_bit_4 -x109_bit_3 x109_bit_2 -x109_bit_1 -x109_bit0 -x109_bit1 -x109_bit2 x109_bit3 -x109_bit4 -x109_bit5 -x109_bit6 -x109_bit7 -x109_bit8 -x109_bit9 -x109_bit10 -x109_bit11 -x109_bit12 -x110_bit_7 -x110_bit_6 -x110_bit_5 x110_bit_4 -x110_bit_3 x110_bit_2 x110_bit_1 x110_bit0 x110_bit1 x110_bit2 x110_bit3 x110_bit4 x110_bit5 -x110_bit6 -x110_bit7 x110_bit8 x110_bit9 -x110_bit10 -x110_bit11 -x110_bit12 -x114_bit_7 x114_bit_6 -x114_bit_5 -x114_bit_4 x114_bit_3 -x114_bit_2 -x114_bit_1 x114_bit0 x114_bit1 x114_bit2 x114_bit3 x114_bit4 x114_bit5 x114_bit6 -x114_bit7 x114_bit8 -x114_bit9 -x114_bit10 -x114_bit11 -x114_bit12 -x115_bit_7 x115_bit_6 -x115_bit_5 -x115_bit_4 -x115_bit_3 -x115_bit_2 -x115_bit_1 x115_bit0 -x115_bit1 -x115_bit2 -x115_bit3 -x115_bit4 -x115_bit5 -x115_bit6 -x115_bit7 -x115_bit8 -x115_bit9 -x115_bit10 -x115_bit11 -x115_bit12 x119_bit_7 -x119_bit_6 -x119_bit_5 -x119_bit_4 -x119_bit_3 -x119_bit_2 x119_bit_1 x119_bit0 -x119_bit1 x119_bit2 x119_bit3 x119_bit4 x119_bit5 x119_bit6 x119_bit7 x119_bit8 -x119_bit9 -x119_bit10 -x119_bit11 -x119_bit12 -x120_bit_7 -x120_bit_6 -x120_bit_5 -x120_bit_4 -x120_bit_3 -x120_bit_2 -x120_bit_1 -x120_bit0 -x120_bit1 x120_bit2 -x120_bit3 -x120_bit4 -x120_bit5 -x120_bit6 -x120_bit7 -x120_bit8 x120_bit9 -x120_bit10 -x120_bit11 -x120_bit12 -x124_bit_7 x124_bit_6 -x124_bit_5 -x124_bit_4 x124_bit_3 -x124_bit_2 -x124_bit_1 x124_bit0 x124_bit1 -x124_bit2 x124_bit3 -x124_bit4 -x124_bit5 -x124_bit6 -x124_bit7 -x124_bit8 x124_bit9 -x124_bit10 -x124_bit11 -x124_bit12 -x125_bit_7 x125_bit_6 -x125_bit_5 -x125_bit_4 -x125_bit_3 -x125_bit_2 -x125_bit_1 -x125_bit0 x125_bit1 -x125_bit2 x125_bit3 x125_bit4 x125_bit5 -x125_bit6 -x125_bit7 -x125_bit8 x125_bit9 -x125_bit10 -x125_bit11 -x125_bit12 x139_bit_7 -x139_bit_6 -x139_bit_5 -x139_bit_4 x139_bit_3 -x139_bit_2 -x139_bit_1 x139_bit0 -x139_bit1 x139_bit2 x139_bit3 x139_bit4 x139_bit5 x139_bit6 x139_bit7 x139_bit8 x139_bit9 -x139_bit10 -x139_bit11 -x139_bit12 -x140_bit_7 x140_bit_6 x140_bit_5 -x140_bit_4 -x140_bit_3 -x140_bit_2 -x140_bit_1 x140_bit0 -x140_bit1 x140_bit2 x140_bit3 -x140_bit4 x140_bit5 -x140_bit6 -x140_bit7 x140_bit8 -x140_bit9 -x140_bit10 -x140_bit11 -x140_bit12 x144_bit_7 -x144_bit_6 -x144_bit_5 -x144_bit_4 -x144_bit_3 -x144_bit_2 -x144_bit_1 x144_bit0 -x144_bit1 -x144_bit2 -x144_bit3 -x144_bit4 -x144_bit5 -x144_bit6 -x144_bit7 -x144_bit8 -x144_bit9 -x144_bit10 -x144_bit11 -x144_bit12 -x145_bit_7 -x145_bit_6 -x145_bit_5 -x145_bit_4 -x145_bit_3 -x145_bit_2 x145_bit_1 -x145_bit0 -x145_bit1 -x145_bit2 -x145_bit3 x145_bit4 x145_bit5 x145_bit6 x145_bit7 -x145_bit8 x145_bit9 -x145_bit10 -x145_bit11 -x145_bit12 -x149_bit_7 x149_bit_6 -x149_bit_5 -x149_bit_4 -x149_bit_3 -x149_bit_2 x149_bit_1 x149_bit0 x149_bit1 x149_bit2 -x149_bit3 x149_bit4 x149_bit5 x149_bit6 -x149_bit7 -x149_bit8 x149_bit9 -x149_bit10 -x149_bit11 -x149_bit12 -x150_bit_7 x150_bit_6 -x150_bit_5 -x150_bit_4 -x150_bit_3 x150_bit_2 -x150_bit_1 x150_bit0 x150_bit1 -x150_bit2 x150_bit3 x150_bit4 x150_bit5 x150_bit6 -x150_bit7 x150_bit8 x150_bit9 -x150_bit10 -x150_bit11 -x150_bit12 -x19_bit_7 -x19_bit_6 -x19_bit_5 -x19_bit_4 -x19_bit_3 -x19_bit_2 -x19_bit_1 x19_bit0 -x19_bit1 x19_bit2 x19_bit3 -x19_bit4 -x19_bit5 -x19_bit6 x19_bit7 x19_bit8 x19_bit9 -x19_bit10 -x19_bit11 -x19_bit12 x10_bit_7 x10_bit_6 x10_bit_5 -x10_bit_4 -x10_bit_3 -x10_bit_2 -x10_bit_1 x10_bit0 -x10_bit1 -x10_bit2 -x10_bit3 -x10_bit4 x10_bit5 x10_bit6 -x10_bit7 -x10_bit8 -x10_bit9 -x10_bit10 -x10_bit11 -x10_bit12 -x20_bit_7 x20_bit_6 -x20_bit_5 -x20_bit_4 x20_bit_3 -x20_bit_2 -x20_bit_1 -x20_bit0 x20_bit1 x20_bit2 -x20_bit3 -x20_bit4 -x20_bit5 -x20_bit6 -x20_bit7 -x20_bit8 -x20_bit9 -x20_bit10 -x20_bit11 -x20_bit12 x9_bit_7 -x9_bit_6 -x9_bit_5 -x9_bit_4 -x9_bit_3 -x9_bit_2 -x9_bit_1 x9_bit0 x9_bit1 x9_bit2 x9_bit3 -x9_bit4 -x9_bit5 -x9_bit6 -x9_bit7 -x9_bit8 -x9_bit9 -x9_bit10 -x9_bit11 -x9_bit12 -x14_bit_7 -x14_bit_6 -x14_bit_5 -x14_bit_4 x14_bit_3 -x14_bit_2 x14_bit_1 x14_bit0 x14_bit1 -x14_bit2 x14_bit3 x14_bit4 x14_bit5 x14_bit6 -x14_bit7 -x14_bit8 -x14_bit9 x14_bit10 -x14_bit11 -x14_bit12 -x24_bit_7 -x24_bit_6 x24_bit_5 -x24_bit_4 x24_bit_3 -x24_bit_2 -x24_bit_1 x24_bit0 -x24_bit1 -x24_bit2 -x24_bit3 -x24_bit4 -x24_bit5 x24_bit6 x24_bit7 -x24_bit8 x24_bit9 -x24_bit10 -x24_bit11 -x24_bit12 x25_bit_7 -x25_b#### 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.93 0.97 0.91 2/54 2064
Raw data (stat): 2064 (runsolver) R 2063 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546458016 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0002 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22237 0 0 0 944 53 0 0 25 0 1 0 546458016 98017280 21580 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23930 21580 603 41 0 23889 0
vsize: 95720
[startup+20.0008 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22271 0 0 0 1943 54 0 0 25 0 1 0 546458016 98152448 21614 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23963 21614 603 41 0 23922 0
vsize: 95852
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22287 0 0 0 2943 54 0 0 25 0 1 0 546458016 98152448 21630 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23963 21630 603 41 0 23922 0
vsize: 95852
[startup+40.0016 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22298 0 0 0 3943 54 0 0 25 0 1 0 546458016 98152448 21641 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23963 21641 603 41 0 23922 0
vsize: 95852
[startup+50.0016 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22305 0 0 0 4943 54 0 0 25 0 1 0 546458016 98152448 21648 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23963 21648 603 41 0 23922 0
vsize: 95852
[startup+60.0013 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22313 0 0 0 5943 54 0 0 25 0 1 0 546458016 98152448 21656 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23963 21656 603 41 0 23922 0
vsize: 95852
[startup+70.0022 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22321 0 0 0 6943 55 0 0 25 0 1 0 546458016 98152448 21664 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23963 21664 603 41 0 23922 0
vsize: 95852
[startup+80.0026 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22325 0 0 0 7943 55 0 0 25 0 1 0 546458016 98287616 21668 4294967295 134512640 134672761 3221224544 3221223744 134557885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23996 21668 603 41 0 23955 0
vsize: 95984
[startup+90.0023 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22329 0 0 0 8943 55 0 0 25 0 1 0 546458016 98287616 21672 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23996 21672 603 41 0 23955 0
vsize: 95984
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22334 0 0 0 9942 55 0 0 25 0 1 0 546458016 98287616 21677 4294967295 134512640 134672761 3221224544 3221223716 134556615 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23996 21677 603 41 0 23955 0
vsize: 95984
[startup+110.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22340 0 0 0 10942 55 0 0 25 0 1 0 546458016 98287616 21683 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23996 21683 603 41 0 23955 0
vsize: 95984
[startup+120.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22344 0 0 0 11942 55 0 0 25 0 1 0 546458016 98287616 21687 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23996 21687 603 41 0 23955 0
vsize: 95984
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22351 0 0 0 12942 55 0 0 25 0 1 0 546458016 98287616 21694 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23996 21694 603 41 0 23955 0
vsize: 95984
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22356 0 0 0 13942 55 0 0 25 0 1 0 546458016 98287616 21699 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23996 21699 603 41 0 23955 0
vsize: 95984
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22363 0 0 0 14942 55 0 0 25 0 1 0 546458016 98418688 21706 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24028 21706 603 41 0 23987 0
vsize: 96112
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22369 0 0 0 15942 55 0 0 25 0 1 0 546458016 98418688 21712 4294967295 134512640 134672761 3221224544 3221223688 134560555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24028 21712 603 41 0 23987 0
vsize: 96112
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22378 0 0 0 16943 55 0 0 25 0 1 0 546458016 98418688 21721 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24028 21721 603 41 0 23987 0
vsize: 96112
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22383 0 0 0 17943 55 0 0 25 0 1 0 546458016 98418688 21726 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24028 21726 603 41 0 23987 0
vsize: 96112
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22386 0 0 0 18943 55 0 0 25 0 1 0 546458016 98418688 21729 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24028 21729 603 41 0 23987 0
vsize: 96112
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22391 0 0 0 19943 55 0 0 25 0 1 0 546458016 98418688 21734 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24028 21734 603 41 0 23987 0
vsize: 96112
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22396 0 0 0 20943 56 0 0 25 0 1 0 546458016 98418688 21739 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24028 21739 603 41 0 23987 0
vsize: 96112
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22414 0 0 0 21943 56 0 0 25 0 1 0 546458016 98549760 21757 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24060 21757 603 41 0 24019 0
vsize: 96240
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22418 0 0 0 22944 56 0 0 25 0 1 0 546458016 98549760 21761 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24060 21761 603 41 0 24019 0
vsize: 96240
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22434 0 0 0 23944 56 0 0 25 0 1 0 546458016 98684928 21777 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24093 21777 603 41 0 24052 0
vsize: 96372
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22444 0 0 0 24944 56 0 0 25 0 1 0 546458016 98684928 21787 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24093 21787 603 41 0 24052 0
vsize: 96372
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22455 0 0 0 25944 56 0 0 25 0 1 0 546458016 98684928 21798 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24093 21798 603 41 0 24052 0
vsize: 96372
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22470 0 0 0 26944 56 0 0 25 0 1 0 546458016 98816000 21813 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24125 21813 603 41 0 24084 0
vsize: 96500
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22480 0 0 0 27944 56 0 0 25 0 1 0 546458016 98816000 21823 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24125 21823 603 41 0 24084 0
vsize: 96500
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22487 0 0 0 28944 56 0 0 25 0 1 0 546458016 98816000 21830 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24125 21830 603 41 0 24084 0
vsize: 96500
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22502 0 0 0 29945 56 0 0 25 0 1 0 546458016 98951168 21845 4294967295 134512640 134672761 3221224544 3221223680 134560640 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24158 21845 603 41 0 24117 0
vsize: 96632
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22512 0 0 0 30945 56 0 0 25 0 1 0 546458016 98951168 21855 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24158 21855 603 41 0 24117 0
vsize: 96632
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22521 0 0 0 31945 56 0 0 25 0 1 0 546458016 98951168 21864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24158 21864 603 41 0 24117 0
vsize: 96632
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22536 0 0 0 32945 56 0 0 25 0 1 0 546458016 99086336 21879 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24191 21879 603 41 0 24150 0
vsize: 96764
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22547 0 0 0 33945 56 0 0 25 0 1 0 546458016 99086336 21890 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24191 21890 603 41 0 24150 0
vsize: 96764
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22568 0 0 0 34945 56 0 0 25 0 1 0 546458016 99307520 21911 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24245 21911 603 41 0 24204 0
vsize: 96980
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22575 0 0 0 35946 56 0 0 25 0 1 0 546458016 99307520 21918 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24245 21918 603 41 0 24204 0
vsize: 96980
[startup+370.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22587 0 0 0 36946 56 0 0 25 0 1 0 546458016 99307520 21930 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24245 21930 603 41 0 24204 0
vsize: 96980
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22597 0 0 0 37946 56 0 0 25 0 1 0 546458016 99307520 21940 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24245 21940 603 41 0 24204 0
vsize: 96980
[startup+390.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22614 0 0 0 38946 56 0 0 25 0 1 0 546458016 99442688 21957 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24278 21957 603 41 0 24237 0
vsize: 97112
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22634 0 0 0 39946 56 0 0 25 0 1 0 546458016 99442688 21977 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24278 21977 603 41 0 24237 0
vsize: 97112
[startup+410.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22645 0 0 0 40946 56 0 0 25 0 1 0 546458016 99577856 21988 4294967295 134512640 134672761 3221224544 3221223728 134557999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 21988 603 41 0 24270 0
vsize: 97244
[startup+420.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22666 0 0 0 41947 56 0 0 25 0 1 0 546458016 99577856 22009 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24311 22009 603 41 0 24270 0
vsize: 97244
[startup+430.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22687 0 0 0 42947 57 0 0 25 0 1 0 546458016 99708928 22030 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24343 22030 603 41 0 24302 0
vsize: 97372
[startup+440.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22696 0 0 0 43947 57 0 0 25 0 1 0 546458016 99708928 22039 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24343 22039 603 41 0 24302 0
vsize: 97372
[startup+450.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22717 0 0 0 44947 57 0 0 25 0 1 0 546458016 99840000 22060 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24375 22060 603 41 0 24334 0
vsize: 97500
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22942 0 0 0 45947 57 0 0 25 0 1 0 546458016 100716544 22285 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24589 22285 603 41 0 24548 0
vsize: 98356
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22959 0 0 0 46947 57 0 0 25 0 1 0 546458016 100847616 22302 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24621 22302 603 41 0 24580 0
vsize: 98484
[startup+480.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 22981 0 0 0 47946 57 0 0 25 0 1 0 546458016 101720064 22324 4294967295 134512640 134672761 3221224544 3221223712 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24834 22324 603 41 0 24793 0
vsize: 99336
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23006 0 0 0 48946 58 0 0 25 0 1 0 546458016 101855232 22349 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24867 22349 603 41 0 24826 0
vsize: 99468
[startup+500.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23020 0 0 0 49947 58 0 0 25 0 1 0 546458016 101855232 22363 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24867 22363 603 41 0 24826 0
vsize: 99468
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23032 0 0 0 50947 58 0 0 25 0 1 0 546458016 101990400 22375 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24900 22375 603 41 0 24859 0
vsize: 99600
[startup+520.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23048 0 0 0 51947 58 0 0 25 0 1 0 546458016 101990400 22391 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24900 22391 603 41 0 24859 0
vsize: 99600
[startup+530.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23083 0 0 0 52947 58 0 0 25 0 1 0 546458016 102125568 22426 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24933 22426 603 41 0 24892 0
vsize: 99732
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23099 0 0 0 53947 58 0 0 25 0 1 0 546458016 102260736 22442 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24966 22442 603 41 0 24925 0
vsize: 99864
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23101 0 0 0 54947 58 0 0 25 0 1 0 546458016 102260736 22444 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24966 22444 603 41 0 24925 0
vsize: 99864
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23102 0 0 0 55947 58 0 0 25 0 1 0 546458016 102260736 22445 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24966 22445 603 41 0 24925 0
vsize: 99864
[startup+570.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23136 0 0 0 56948 58 0 0 25 0 1 0 546458016 102522880 22479 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25030 22479 603 41 0 24989 0
vsize: 100120
[startup+580.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23137 0 0 0 57948 58 0 0 25 0 1 0 546458016 102522880 22480 4294967295 134512640 134672761 3221224544 3221223712 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25030 22480 603 41 0 24989 0
vsize: 100120
[startup+590.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23138 0 0 0 58948 58 0 0 25 0 1 0 546458016 102522880 22481 4294967295 134512640 134672761 3221224544 3221223688 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25030 22481 603 41 0 24989 0
vsize: 100120
[startup+600.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23162 0 0 0 59948 58 0 0 25 0 1 0 546458016 102653952 22505 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25062 22505 603 41 0 25021 0
vsize: 100248
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23203 0 0 0 60949 59 0 0 25 0 1 0 546458016 102789120 22546 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25095 22546 603 41 0 25054 0
vsize: 100380
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23243 0 0 0 61949 59 0 0 25 0 1 0 546458016 102924288 22586 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25128 22586 603 41 0 25087 0
vsize: 100512
[startup+630.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23276 0 0 0 62949 59 0 0 25 0 1 0 546458016 103059456 22619 4294967295 134512640 134672761 3221224544 3221223704 134561240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25161 22619 603 41 0 25120 0
vsize: 100644
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23305 0 0 0 63949 59 0 0 25 0 1 0 546458016 103194624 22648 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25194 22648 603 41 0 25153 0
vsize: 100776
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23350 0 0 0 64949 59 0 0 25 0 1 0 546458016 103329792 22693 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25227 22693 603 41 0 25186 0
vsize: 100908
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23377 0 0 0 65949 59 0 0 25 0 1 0 546458016 103464960 22720 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25260 22720 603 41 0 25219 0
vsize: 101040
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23414 0 0 0 66949 60 0 0 25 0 1 0 546458016 103600128 22757 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25293 22757 603 41 0 25252 0
vsize: 101172
[startup+680.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23441 0 0 0 67949 60 0 0 25 0 1 0 546458016 103735296 22784 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25326 22784 603 41 0 25285 0
vsize: 101304
[startup+690.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23480 0 0 0 68949 60 0 0 25 0 1 0 546458016 103870464 22823 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25359 22823 603 41 0 25318 0
vsize: 101436
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23521 0 0 0 69949 60 0 0 25 0 1 0 546458016 104001536 22864 4294967295 134512640 134672761 3221224544 3221223680 134560673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25391 22864 603 41 0 25350 0
vsize: 101564
[startup+710.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23563 0 0 0 70949 60 0 0 25 0 1 0 546458016 104136704 22906 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25424 22906 603 41 0 25383 0
vsize: 101696
[startup+720.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23612 0 0 0 71949 61 0 0 25 0 1 0 546458016 104407040 22955 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25490 22955 603 41 0 25449 0
vsize: 101960
[startup+730.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23663 0 0 0 72949 61 0 0 25 0 1 0 546458016 104542208 23006 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25523 23006 603 41 0 25482 0
vsize: 102092
[startup+740.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23704 0 0 0 73949 61 0 0 25 0 1 0 546458016 104673280 23047 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25555 23047 603 41 0 25514 0
vsize: 102220
[startup+750.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23759 0 0 0 74949 61 0 0 25 0 1 0 546458016 104947712 23102 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25622 23102 603 41 0 25581 0
vsize: 102488
[startup+760.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23808 0 0 0 75949 62 0 0 25 0 1 0 546458016 105082880 23151 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25655 23151 603 41 0 25614 0
vsize: 102620
[startup+770.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23852 0 0 0 76949 62 0 0 25 0 1 0 546458016 105345024 23195 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25719 23195 603 41 0 25678 0
vsize: 102876
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23900 0 0 0 77949 62 0 0 25 0 1 0 546458016 105742336 23243 4294967295 134512640 134672761 3221224544 3221223744 134557919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25816 23243 603 41 0 25775 0
vsize: 103264
[startup+790.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23949 0 0 0 78949 62 0 0 25 0 1 0 546458016 106008576 23292 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25881 23292 603 41 0 25840 0
vsize: 103524
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 23986 0 0 0 79949 62 0 0 25 0 1 0 546458016 106143744 23329 4294967295 134512640 134672761 3221224544 3221223744 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25914 23329 603 41 0 25873 0
vsize: 103656
[startup+810.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24031 0 0 0 80949 63 0 0 25 0 1 0 546458016 106278912 23374 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25947 23374 603 41 0 25906 0
vsize: 103788
[startup+820.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24065 0 0 0 81949 63 0 0 25 0 1 0 546458016 106414080 23408 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25980 23408 603 41 0 25939 0
vsize: 103920
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24116 0 0 0 82949 63 0 0 25 0 1 0 546458016 106684416 23459 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26046 23459 603 41 0 26005 0
vsize: 104184
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24157 0 0 0 83949 64 0 0 25 0 1 0 546458016 106819584 23500 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26079 23500 603 41 0 26038 0
vsize: 104316
[startup+850.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24202 0 0 0 84949 64 0 0 25 0 1 0 546458016 106950656 23545 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26111 23545 603 41 0 26070 0
vsize: 104444
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24242 0 0 0 85948 64 0 0 25 0 1 0 546458016 107085824 23585 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26144 23585 603 41 0 26103 0
vsize: 104576
[startup+870.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24294 0 0 0 86948 65 0 0 25 0 1 0 546458016 107360256 23637 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26211 23637 603 41 0 26170 0
vsize: 104844
[startup+880.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24335 0 0 0 87948 65 0 0 25 0 1 0 546458016 107495424 23678 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26244 23678 603 41 0 26203 0
vsize: 104976
[startup+890.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24375 0 0 0 88948 65 0 0 25 0 1 0 546458016 107630592 23718 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26277 23718 603 41 0 26236 0
vsize: 105108
[startup+900.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24416 0 0 0 89948 65 0 0 25 0 1 0 546458016 107765760 23759 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26310 23759 603 41 0 26269 0
vsize: 105240
[startup+910.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24466 0 0 0 90948 65 0 0 25 0 1 0 546458016 108027904 23809 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26374 23809 603 41 0 26333 0
vsize: 105496
[startup+920.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24518 0 0 0 91948 66 0 0 25 0 1 0 546458016 108163072 23861 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26407 23861 603 41 0 26366 0
vsize: 105628
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24567 0 0 0 92948 66 0 0 25 0 1 0 546458016 108433408 23910 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26473 23910 603 41 0 26432 0
vsize: 105892
[startup+940.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24619 0 0 0 93948 66 0 0 25 0 1 0 546458016 108568576 23962 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26506 23962 603 41 0 26465 0
vsize: 106024
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24686 0 0 0 94948 67 0 0 25 0 1 0 546458016 108843008 24029 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26573 24029 603 41 0 26532 0
vsize: 106292
[startup+960.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24740 0 0 0 95948 67 0 0 25 0 1 0 546458016 109113344 24083 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26639 24083 603 41 0 26598 0
vsize: 106556
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24791 0 0 0 96948 67 0 0 25 0 1 0 546458016 109248512 24134 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26672 24134 603 41 0 26631 0
vsize: 106688
[startup+980.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24844 0 0 0 97948 67 0 0 25 0 1 0 546458016 109518848 24187 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26738 24187 603 41 0 26697 0
vsize: 106952
[startup+990.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24880 0 0 0 98948 67 0 0 25 0 1 0 546458016 109649920 24223 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26770 24223 603 41 0 26729 0
vsize: 107080
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 24923 0 0 0 99948 67 0 0 25 0 1 0 546458016 109785088 24266 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26803 24266 603 41 0 26762 0
vsize: 107212
[startup+1010.03 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25008 0 0 0 100948 68 0 0 25 0 1 0 546458016 110186496 24351 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26901 24351 603 41 0 26860 0
vsize: 107604
[startup+1020.03 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25080 0 0 0 101948 68 0 0 25 0 1 0 546458016 110456832 24423 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26967 24423 603 41 0 26926 0
vsize: 107868
[startup+1030.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25136 0 0 0 102947 68 0 0 25 0 1 0 546458016 110727168 24479 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27033 24479 603 41 0 26992 0
vsize: 108132
[startup+1040.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25196 0 0 0 103947 69 0 0 25 0 1 0 546458016 110862336 24539 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27066 24539 603 41 0 27025 0
vsize: 108264
[startup+1050.03 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25257 0 0 0 104947 69 0 0 25 0 1 0 546458016 111132672 24600 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27132 24600 603 41 0 27091 0
vsize: 108528
[startup+1060.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25310 0 0 0 105947 69 0 0 25 0 1 0 546458016 111403008 24653 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27198 24653 603 41 0 27157 0
vsize: 108792
[startup+1070.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25352 0 0 0 106947 69 0 0 25 0 1 0 546458016 111538176 24695 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27231 24695 603 41 0 27190 0
vsize: 108924
[startup+1080.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25394 0 0 0 107947 69 0 0 25 0 1 0 546458016 111673344 24737 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27264 24737 603 41 0 27223 0
vsize: 109056
[startup+1090.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25437 0 0 0 108947 70 0 0 25 0 1 0 546458016 111808512 24780 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27297 24780 603 41 0 27256 0
vsize: 109188
[startup+1100.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25473 0 0 0 109947 70 0 0 25 0 1 0 546458016 112078848 24816 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27363 24816 603 41 0 27322 0
vsize: 109452
[startup+1110.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25522 0 0 0 110947 70 0 0 25 0 1 0 546458016 112209920 24865 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27395 24865 603 41 0 27354 0
vsize: 109580
[startup+1120.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25567 0 0 0 111947 70 0 0 25 0 1 0 546458016 112349184 24910 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27429 24910 603 41 0 27388 0
vsize: 109716
[startup+1130.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25616 0 0 0 112947 71 0 0 25 0 1 0 546458016 112615424 24959 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27494 24959 603 41 0 27453 0
vsize: 109976
[startup+1140.05 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25693 0 0 0 113948 71 0 0 25 0 1 0 546458016 112877568 25036 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27558 25036 603 41 0 27517 0
vsize: 110232
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25760 0 0 0 114950 71 0 0 25 0 1 0 546458016 113143808 25103 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27623 25103 603 41 0 27582 0
vsize: 110492
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25807 0 0 0 115950 72 0 0 25 0 1 0 546458016 113410048 25150 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27688 25150 603 41 0 27647 0
vsize: 110752
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25849 0 0 0 116951 72 0 0 25 0 1 0 546458016 113545216 25192 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27721 25192 603 41 0 27680 0
vsize: 110884
[startup+1180.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25897 0 0 0 117952 72 0 0 25 0 1 0 546458016 113680384 25240 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27754 25240 603 41 0 27713 0
vsize: 111016
[startup+1190.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 25945 0 0 0 118951 72 0 0 25 0 1 0 546458016 113946624 25288 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27819 25288 603 41 0 27778 0
vsize: 111276
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2064
Raw data (stat): 2064 (minisat+) R 2063 22612 22611 0 -1 0 26002 0 0 0 119951 72 0 0 25 0 1 0 546458016 114606080 25345 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27980 25345 603 41 0 27939 0
vsize: 111920
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 2064
Raw data (stat): 2064 (minisat+) Z 2063 22612 22611 0 -1 12 26005 0 0 0 119952 77 0 0 24 0 1 0 546458016 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.16
CPU time (s): 1200.3
CPU user time (s): 1199.52
CPU system time (s): 0.779881
CPU usage (%): 100.012
Max. virtual memory (Kb): 111920
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####