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 32320

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-05-27 09:08:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=23711 boxname=wulflinc7 idbench=1355 idsolver=16 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  216e30ba4678325d93810a111dd11436  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-liu.opb
REAL COMMAND:  minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-liu.opb
IDLAUNCH: 23711
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        887468 kB
Buffers:          3664 kB
Cached:         123724 kB
SwapCached:        656 kB
Active:          19100 kB
Inactive:       110348 kB
HighTotal:      131008 kB
HighFree:         7196 kB
LowTotal:       903652 kB
LowFree:        880272 kB
SwapTotal:     2097136 kB
SwapFree:      2095552 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5084 kB
Slab:            12196 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 09:29:15 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 23711 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2178 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[2177]---> BDD-cost:  103
c ---[2176]---> BDD-cost:  156
c ---[2175]---> BDD-cost:  155
c ---[2174]---> BDD-cost:  144
c ---[2173]---> BDD-cost:  103
c ---[2172]---> BDD-cost:  134
c ---[2171]---> BDD-cost:  103
c ---[2170]---> BDD-cost:  134
c ---[2169]---> BDD-cost:  103
c ---[2168]---> BDD-cost:  103
c ---[2167]---> BDD-cost:  103
c ---[2166]---> BDD-cost:  103
c ---[2165]---> BDD-cost:   99
c ---[2164]---> BDD-cost:  103
c ---[2163]---> BDD-cost:   99
c ---[2162]---> BDD-cost:   99
c ---[2161]---> BDD-cost:   99
c ---[2160]---> BDD-cost:   99
c ---[2159]---> BDD-cost:  152
c ---[2158]---> BDD-cost:   99
c ---[2157]---> BDD-cost:  152
c ---[2156]---> BDD-cost:   99
c ---[2155]---> BDD-cost:   81
c ---[2154]---> BDD-cost:   99
c ---[2153]---> BDD-cost:  148
c ---[2152]---> BDD-cost:   81
c ---[2151]---> BDD-cost:   99
c ---[2150]---> BDD-cost:   85
c ---[2149]---> BDD-cost:   99
c ---[2148]---> BDD-cost:   85
c ---[2147]---> BDD-cost:   99
c ---[2146]---> BDD-cost:  148
c ---[2145]---> BDD-cost:   99
c ---[2144]---> BDD-cost:  148
c ---[2143]---> BDD-cost:   99
c ---[2142]---> BDD-cost:  103
c ---[2141]---> BDD-cost:  146
c ---[2140]---> BDD-cost:   99
c ---[2139]---> BDD-cost:  146
c ---[2138]---> BDD-cost:   99
c ---[2137]---> BDD-cost:  101
c ---[2136]---> BDD-cost:   99
c ---[2135]---> BDD-cost:  101
c ---[2134]---> BDD-cost:   99
c ---[2133]---> BDD-cost:  137
c ---[2132]---> BDD-cost:   99
c ---[2131]---> BDD-cost:  148
c ---[2130]---> BDD-cost:  137
c ---[2129]---> BDD-cost:   99
c ---[2128]---> BDD-cost:  110
c ---[2127]---> BDD-cost:   99
c ---[2126]---> BDD-cost:  110
c ---[2125]---> BDD-cost:   99
c ---[2124]---> BDD-cost:  154
c ---[2123]---> BDD-cost:   99
c ---[2122]---> BDD-cost:  154
c ---[2121]---> BDD-cost:   99
c ---[2120]---> BDD-cost:  103
c ---[2119]---> BDD-cost:  153
c ---[2118]---> BDD-cost:   99
c ---[2117]---> BDD-cost:  153
c ---[2116]---> BDD-cost:   99
c ---[2115]---> BDD-cost:   99
c ---[2114]---> BDD-cost:   99
c ---[2113]---> BDD-cost:   99
c ---[2112]---> BDD-cost:   99
c ---[2111]---> BDD-cost:  104
c ---[2110]---> BDD-cost:   99
c ---[2109]---> BDD-cost:  152
c ---[2108]---> BDD-cost:  104
c ---[2107]---> BDD-cost:   99
c ---[2106]---> BDD-cost:   87
c ---[2105]---> BDD-cost:   99
c ---[2104]---> BDD-cost:   87
c ---[2103]---> BDD-cost:   99
c ---[2102]---> BDD-cost:   88
c ---[2101]---> BDD-cost:   99
c ---[2100]---> BDD-cost:   88
c ---[2099]---> BDD-cost:   99
c ---[2098]---> BDD-cost:  103
c ---[2097]---> BDD-cost:  155
c ---[2096]---> BDD-cost:   99
c ---[2095]---> BDD-cost:  155
c ---[2094]---> BDD-cost:   99
c ---[2093]---> BDD-cost:  148
c ---[2092]---> BDD-cost:   99
c ---[2091]---> BDD-cost:  148
c ---[2090]---> BDD-cost:   99
c ---[2089]---> BDD-cost:  152
c ---[2088]---> BDD-cost:   99
c ---[2087]---> BDD-cost:  152
c ---[2086]---> BDD-cost:  152
c ---[2085]---> BDD-cost:   99
c ---[2084]---> BDD-cost:  105
c ---[2083]---> BDD-cost:   99
c ---[2082]---> BDD-cost:  105
c ---[2081]---> BDD-cost:   99
c ---[2080]---> BDD-cost:  107
c ---[2079]---> BDD-cost:   99
c ---[2078]---> BDD-cost:  107
c ---[2077]---> BDD-cost:   99
c ---[2076]---> BDD-cost:  103
c ---[2075]---> BDD-cost:  144
c ---[2074]---> BDD-cost:   99
c ---[2073]---> BDD-cost:  144
c ---[2072]---> BDD-cost:   99
c ---[2071]---> BDD-cost:  134
c ---[2070]---> BDD-cost:   99
c ---[2069]---> BDD-cost:  134
c ---[2068]---> BDD-cost:   99
c ---[2067]---> BDD-cost:  103
c ---[2066]---> BDD-cost:   99
c ---[2065]---> BDD-cost:  103
c ---[2064]---> BDD-cost:  105
c ---[2063]---> BDD-cost:  103
c ---[2062]---> BDD-cost:   99
c ---[2061]---> BDD-cost:  152
c ---[2060]---> BDD-cost:   99
c ---[2059]---> BDD-cost:  152
c ---[2058]---> BDD-cost:   99
c ---[2057]---> BDD-cost:   81
c ---[2056]---> BDD-cost:   99
c ---[2055]---> BDD-cost:   81
c ---[2054]---> BDD-cost:   99
c ---[2053]---> BDD-cost:  103
c ---[2052]---> BDD-cost:   85
c ---[2051]---> BDD-cost:   99
c ---[2050]---> BDD-cost:   85
c ---[2049]---> BDD-cost:   99
c ---[2048]---> BDD-cost:  148
c ---[2047]---> BDD-cost:   99
c ---[2046]---> BDD-cost:  148
c ---[2045]---> BDD-cost:   99
c ---[2044]---> BDD-cost:  146
c ---[2043]---> BDD-cost:   99
c ---[2042]---> BDD-cost:  105
c ---[2041]---> BDD-cost:  146
c ---[2040]---> BDD-cost:   99
c ---[2039]---> BDD-cost:  101
c ---[2038]---> BDD-cost:   99
c ---[2037]---> BDD-cost:  101
c ---[2036]---> BDD-cost:   99
c ---[2035]---> BDD-cost:  137
c ---[2034]---> BDD-cost:   99
c ---[2033]---> BDD-cost:  137
c ---[2032]---> BDD-cost:   99
c ---[2031]---> BDD-cost:  103
c ---[2030]---> BDD-cost:  110
c ---[2029]---> BDD-cost:   99
c ---[2028]---> BDD-cost:  110
c ---[2027]---> BDD-cost:   99
c ---[2026]---> BDD-cost:  154
c ---[2025]---> BDD-cost:   99
c ---[2024]---> BDD-cost:  154
c ---[2023]---> BDD-cost:   99
c ---[2022]---> BDD-cost:  153
c ---[2021]---> BDD-cost:   99
c ---[2020]---> BDD-cost:  107
c ---[2019]---> BDD-cost:  153
c ---[2018]---> BDD-cost:   99
c ---[2017]---> BDD-cost:   99
c ---[2016]---> BDD-cost:   99
c ---[2015]---> BDD-cost:   99
c ---[2014]---> BDD-cost:   99
c ---[2013]---> BDD-cost:  104
c ---[2012]---> BDD-cost:   99
c ---[2011]---> BDD-cost:  104
c ---[2010]---> BDD-cost:   99
c ---[2009]---> BDD-cost:  103
c ---[2008]---> BDD-cost:   87
c ---[2007]---> BDD-cost:   99
c ---[2006]---> BDD-cost:   87
c ---[2005]---> BDD-cost:   99
c ---[2004]---> BDD-cost:   88
c ---[2003]---> BDD-cost:   99
c ---[2002]---> BDD-cost:   88
c ---[2001]---> BDD-cost:   99
c ---[2000]---> BDD-cost:  155
c ---[1999]---> BDD-cost:   99
c ---[1998]---> BDD-cost:  107
c ---[1997]---> BDD-cost:  155
c ---[1996]---> BDD-cost:   99
c ---[1995]---> BDD-cost:  148
c ---[1994]---> BDD-cost:   99
c ---[1993]---> BDD-cost:  148
c ---[1992]---> BDD-cost:   99
c ---[1991]---> BDD-cost:  152
c ---[1990]---> BDD-cost:   99
c ---[1989]---> BDD-cost:  152
c ---[1988]---> BDD-cost:   99
c ---[1987]---> BDD-cost:  103
c ---[1986]---> BDD-cost:  105
c ---[1985]---> BDD-cost:   99
c ---[1984]---> BDD-cost:  105
c ---[1983]---> BDD-cost:   99
c ---[1982]---> BDD-cost:  107
c ---[1981]---> BDD-cost:   99
c ---[1980]---> BDD-cost:  107
c ---[1979]---> BDD-cost:   99
c ---[1978]---> BDD-cost:  144
c ---[1977]---> BDD-cost:   99
c ---[1976]---> BDD-cost:  144
c ---[1975]---> BDD-cost:  144
c ---[1974]---> BDD-cost:   99
c ---[1973]---> BDD-cost:  134
c ---[1972]---> BDD-cost:   99
c ---[1971]---> BDD-cost:  134
c ---[1970]---> BDD-cost:   99
c ---[1969]---> BDD-cost:  103
c ---[1968]---> BDD-cost:   99
c ---[1967]---> BDD-cost:  103
c ---[1966]---> BDD-cost:  152
c ---[1965]---> BDD-cost:  103
c ---[1964]---> BDD-cost:   81
c ---[1963]---> BDD-cost:  152
c ---[1962]---> BDD-cost:   81
c ---[1961]---> BDD-cost:  152
c ---[1960]---> BDD-cost:   85
c ---[1959]---> BDD-cost:  152
c ---[1958]---> BDD-cost:   85
c ---[1957]---> BDD-cost:  152
c ---[1956]---> BDD-cost:  148
c ---[1955]---> BDD-cost:  152
c ---[1954]---> BDD-cost:  156
c ---[1953]---> BDD-cost:  144
c ---[1952]---> BDD-cost:  148
c ---[1951]---> BDD-cost:  152
c ---[1950]---> BDD-cost:  146
c ---[1949]---> BDD-cost:  152
c ---[1948]---> BDD-cost:  146
c ---[1947]---> BDD-cost:  152
c ---[1946]---> BDD-cost:  101
c ---[1945]---> BDD-cost:  152
c ---[1944]---> BDD-cost:  101
c ---[1943]---> BDD-cost:  152
c ---[1942]---> BDD-cost:  103
c ---[1941]---> BDD-cost:  137
c ---[1940]---> BDD-cost:  152
c ---[1939]---> BDD-cost:  137
c ---[1938]---> BDD-cost:  152
c ---[1937]---> BDD-cost:  110
c ---[1936]---> BDD-cost:  152
c ---[1935]---> BDD-cost:  110
c ---[1934]---> BDD-cost:  152
c ---[1933]---> BDD-cost:  154
c ---[1932]---> BDD-cost:  152
c ---[1931]---> BDD-cost:  134
c ---[1930]---> BDD-cost:  154
c ---[1929]---> BDD-cost:  152
c ---[1928]---> BDD-cost:  153
c ---[1927]---> BDD-cost:  152
c ---[1926]---> BDD-cost:  153
c ---[1925]---> BDD-cost:  152
c ---[1924]---> BDD-cost:   99
c ---[1923]---> BDD-cost:  152
c ---[1922]---> BDD-cost:   99
c ---[1921]---> BDD-cost:  152
c ---[1920]---> BDD-cost:  103
c ---[1919]---> BDD-cost:  104
c ---[1918]---> BDD-cost:  152
c ---[1917]---> BDD-cost:  104
c ---[1916]---> BDD-cost:  152
c ---[1915]---> BDD-cost:   87
c ---[1914]---> BDD-cost:  152
c ---[1913]---> BDD-cost:   87
c ---[1912]---> BDD-cost:  152
c ---[1911]---> BDD-cost:   88
c ---[1910]---> BDD-cost:  152
c ---[1909]---> BDD-cost:  134
c ---[1908]---> BDD-cost:   88
c ---[1907]---> BDD-cost:  152
c ---[1906]---> BDD-cost:  155
c ---[1905]---> BDD-cost:  152
c ---[1904]---> BDD-cost:  155
c ---[1903]---> BDD-cost:  152
c ---[1902]---> BDD-cost:  148
c ---[1901]---> BDD-cost:  152
c ---[1900]---> BDD-cost:  148
c ---[1899]---> BDD-cost:  152
c ---[1898]---> BDD-cost:  103
c ---[1897]---> BDD-cost:  152
c ---[1896]---> BDD-cost:  152
c ---[1895]---> BDD-cost:  152
c ---[1894]---> BDD-cost:  152
c ---[1893]---> BDD-cost:  105
c ---[1892]---> BDD-cost:  152
c ---[1891]---> BDD-cost:  105
c ---[1890]---> BDD-cost:  152
c ---[1889]---> BDD-cost:  107
c ---[1888]---> BDD-cost:  152
c ---[1887]---> BDD-cost:  103
c ---[1886]---> BDD-cost:  107
c ---[1885]---> BDD-cost:  152
c ---[1884]---> BDD-cost:  144
c ---[1883]---> BDD-cost:  152
c ---[1882]---> BDD-cost:  144
c ---[1881]---> BDD-cost:  152
c ---[1880]---> BDD-cost:  134
c ---[1879]---> BDD-cost:  152
c ---[1878]---> BDD-cost:  134
c ---[1877]---> BDD-cost:  152
c ---[1876]---> BDD-cost:  103
c ---[1875]---> BDD-cost:  103
c ---[1874]---> BDD-cost:  152
c ---[1873]---> BDD-cost:  103
c ---[1872]---> BDD-cost:   81
c ---[1871]---> BDD-cost:   85
c ---[1870]---> BDD-cost:   81
c ---[1869]---> BDD-cost:   85
c ---[1868]---> BDD-cost:   81
c ---[1867]---> BDD-cost:  148
c ---[1866]---> BDD-cost:   81
c ---[1865]---> BDD-cost:  103
c ---[1864]---> BDD-cost:  148
c ---[1863]---> BDD-cost:   81
c ---[1862]---> BDD-cost:  146
c ---[1861]---> BDD-cost:   81
c ---[1860]---> BDD-cost:  146
c ---[1859]---> BDD-cost:   81
c ---[1858]---> BDD-cost:  101
c ---[1857]---> BDD-cost:   81
c ---[1856]---> BDD-cost:  101
c ---[1855]---> BDD-cost:   81
c ---[1854]---> BDD-cost:  137
c ---[1853]---> BDD-cost:  137
c ---[1852]---> BDD-cost:   81
c ---[1851]---> BDD-cost:  137
c ---[1850]---> BDD-cost:   81
c ---[1849]---> BDD-cost:  110
c ---[1848]---> BDD-cost:   81
c ---[1847]---> BDD-cost:  110
c ---[1846]---> BDD-cost:   81
c ---[1845]---> BDD-cost:  154
c ---[1844]---> BDD-cost:   81
c ---[1843]---> BDD-cost:  103
c ---[1842]---> BDD-cost:   83
c ---[1841]---> BDD-cost:  154
c ---[1840]---> BDD-cost:   81
c ---[1839]---> BDD-cost:  153
c ---[1838]---> BDD-cost:   81
c ---[1837]---> BDD-cost:  153
c ---[1836]---> BDD-cost:   81
c ---[1835]---> BDD-cost:   99
c ---[1834]---> BDD-cost:   81
c ---[1833]---> BDD-cost:   99
c ---[1832]---> BDD-cost:   81
c ---[1831]---> BDD-cost:  137
c ---[1830]---> BDD-cost:  104
c ---[1829]---> BDD-cost:   81
c ---[1828]---> BDD-cost:  104
c ---[1827]---> BDD-cost:   81
c ---[1826]---> BDD-cost:   87
c ---[1825]---> BDD-cost:   81
c ---[1824]---> BDD-cost:   87
c ---[1823]---> BDD-cost:   81
c ---[1822]---> BDD-cost:   88
c ---[1821]---> BDD-cost:   81
c ---[1820]---> BDD-cost:   83
c ---[1819]---> BDD-cost:   88
c ---[1818]---> BDD-cost:   81
c ---[1817]---> BDD-cost:  155
c ---[1816]---> BDD-cost:   81
c ---[1815]---> BDD-cost:  155
c ---[1814]---> BDD-cost:   81
c ---[1813]---> BDD-cost:  148
c ---[1812]---> BDD-cost:   81
c ---[1811]---> BDD-cost:  148
c ---[1810]---> BDD-cost:   81
c ---[1809]---> BDD-cost:  137
c ---[1808]---> BDD-cost:  152
c ---[1807]---> BDD-cost:   81
c ---[1806]---> BDD-cost:  152
c ---[1805]---> BDD-cost:   81
c ---[1804]---> BDD-cost:  105
c ---[1803]---> BDD-cost:   81
c ---[1802]---> BDD-cost:  105
c ---[1801]---> BDD-cost:   81
c ---[1800]---> BDD-cost:  107
c ---[1799]---> BDD-cost:   81
c ---[1798]---> BDD-cost:  156
c ---[1797]---> BDD-cost:  107
c ---[1796]---> BDD-cost:   81
c ---[1795]---> BDD-cost:  144
c ---[1794]---> BDD-cost:   81
c ---[1793]---> BDD-cost:  144
c ---[1792]---> BDD-cost:   81
c ---[1791]---> BDD-cost:  134
c ---[1790]---> BDD-cost:   81
c ---[1789]---> BDD-cost:  134
c ---[1788]---> BDD-cost:   81
c ---[1787]---> BDD-cost:  137
c ---[1786]---> BDD-cost:  103
c ---[1785]---> BDD-cost:   81
c ---[1784]---> BDD-cost:  103
c ---[1783]---> BDD-cost:   85
c ---[1782]---> BDD-cost:  148
c ---[1781]---> BDD-cost:   85
c ---[1780]---> BDD-cost:  148
c ---[1779]---> BDD-cost:   85
c ---[1778]---> BDD-cost:  146
c ---[1777]---> BDD-cost:   85
c ---[1776]---> BDD-cost:  156
c ---[1775]---> BDD-cost:  146
c ---[1774]---> BDD-cost:   85
c ---[1773]---> BDD-cost:  101
c ---[1772]---> BDD-cost:   85
c ---[1771]---> BDD-cost:  101
c ---[1770]---> BDD-cost:   85
c ---[1769]---> BDD-cost:  137
c ---[1768]---> BDD-cost:   85
c ---[1767]---> BDD-cost:  137
c ---[1766]---> BDD-cost:   85
c ---[1765]---> BDD-cost:  137
c ---[1764]---> BDD-cost:  110
c ---[1763]---> BDD-cost:   85
c ---[1762]---> BDD-cost:  110
c ---[1761]---> BDD-cost:   85
c ---[1760]---> BDD-cost:  154
c ---[1759]---> BDD-cost:   85
c ---[1758]---> BDD-cost:  154
c ---[1757]---> BDD-cost:   85
c ---[1756]---> BDD-cost:  153
c ---[1755]---> BDD-cost:   85
c ---[1754]---> BDD-cost:  144
c ---[1753]---> BDD-cost:  153
c ---[1752]---> BDD-cost:   85
c ---[1751]---> BDD-cost:   99
c ---[1750]---> BDD-cost:   85
c ---[1749]---> BDD-cost:   99
c ---[1748]---> BDD-cost:   85
c ---[1747]---> BDD-cost:  104
c ---[1746]---> BDD-cost:   85
c ---[1745]---> BDD-cost:  104
c ---[1744]---> BDD-cost:   85
c ---[1743]---> BDD-cost:  137
c ---[1742]---> BDD-cost:   87
c ---[1741]---> BDD-cost:   85
c ---[1740]---> BDD-cost:   87
c ---[1739]---> BDD-cost:   85
c ---[1738]---> BDD-cost:   88
c ---[1737]---> BDD-cost:   85
c ---[1736]---> BDD-cost:   88
c ---[1735]---> BDD-cost:   85
c ---[1734]---> BDD-cost:  155
c ---[1733]---> BDD-cost:   85
c ---[1732]---> BDD-cost:  144
c ---[1731]---> BDD-cost:  144
c ---[1730]---> BDD-cost:  155
c ---[1729]---> BDD-cost:   85
c ---[1728]---> BDD-cost:  148
c ---[1727]---> BDD-cost:   85
c ---[1726]---> BDD-cost:  148
c ---[1725]---> BDD-cost:   85
c ---[1724]---> BDD-cost:  152
c ---[1723]---> BDD-cost:   85
c ---[1722]---> BDD-cost:  152
c ---[1721]---> BDD-cost:   85
c ---[1720]---> BDD-cost:  137
c ---[1719]---> BDD-cost:  105
c ---[1718]---> BDD-cost:   85
c ---[1717]---> BDD-cost:  105
c ---[1716]---> BDD-cost:   85
c ---[1715]---> BDD-cost:  107
c ---[1714]---> BDD-cost:   85
c ---[1713]---> BDD-cost:  107
c ---[1712]---> BDD-cost:   85
c ---[1711]---> BDD-cost:  144
c ---[1710]---> BDD-cost:   85
c ---[1709]---> BDD-cost:  134
c ---[1708]---> BDD-cost:  144
c ---[1707]---> BDD-cost:   85
c ---[1706]---> BDD-cost:  134
c ---[1705]---> BDD-cost:   85
c ---[1704]---> BDD-cost:  134
c ---[1703]---> BDD-cost:   85
c ---[1702]---> BDD-cost:  103
c ---[1701]---> BDD-cost:   85
c ---[1700]---> BDD-cost:  103
c ---[1699]---> BDD-cost:  148
c ---[1698]---> BDD-cost:  137
c ---[1697]---> BDD-cost:  146
c ---[1696]---> BDD-cost:  148
c ---[1695]---> BDD-cost:  146
c ---[1694]---> BDD-cost:  148
c ---[1693]---> BDD-cost:  101
c ---[1692]---> BDD-cost:  148
c ---[1691]---> BDD-cost:  101
c ---[1690]---> BDD-cost:  148
c ---[1689]---> BDD-cost:  137
c ---[1688]---> BDD-cost:  148
c ---[1687]---> BDD-cost:  134
c ---[1686]---> BDD-cost:  137
c ---[1685]---> BDD-cost:  148
c ---[1684]---> BDD-cost:  110
c ---[1683]---> BDD-cost:  148
c ---[1682]---> BDD-cost:  110
c ---[1681]---> BDD-cost:  148
c ---[1680]---> BDD-cost:  154
c ---[1679]---> BDD-cost:  148
c ---[1678]---> BDD-cost:  154
c ---[1677]---> BDD-cost:  148
c ---[1676]---> BDD-cost:  137
c ---[1675]---> BDD-cost:  153
c ---[1674]---> BDD-cost:  148
c ---[1673]---> BDD-cost:  153
c ---[1672]---> BDD-cost:  148
c ---[1671]---> BDD-cost:   99
c ---[1670]---> BDD-cost:  148
c ---[1669]---> BDD-cost:   99
c ---[1668]---> BDD-cost:  148
c ---[1667]---> BDD-cost:  104
c ---[1666]---> BDD-cost:  148
c ---[1665]---> BDD-cost:  143
c ---[1664]---> BDD-cost:  104
c ---[1663]---> BDD-cost:  148
c ---[1662]---> BDD-cost:   87
c ---[1661]---> BDD-cost:  148
c ---[1660]---> BDD-cost:   87
c ---[1659]---> BDD-cost:  148
c ---[1658]---> BDD-cost:   88
c ---[1657]---> BDD-cost:  148
c ---[1656]---> BDD-cost:   88
c ---[1655]---> BDD-cost:  148
c ---[1654]---> BDD-cost:  137
c ---[1653]---> BDD-cost:  155
c ---[1652]---> BDD-cost:  148
c ---[1651]---> BDD-cost:  155
c ---[1650]---> BDD-cost:  148
c ---[1649]---> BDD-cost:  148
c ---[1648]---> BDD-cost:  148
c ---[1647]---> BDD-cost:  148
c ---[1646]---> BDD-cost:  148
c ---[1645]---> BDD-cost:  152
c ---[1644]---> BDD-cost:  148
c ---[1643]---> BDD-cost:  143
c ---[1642]---> BDD-cost:  152
c ---[1641]---> BDD-cost:  148
c ---[1640]---> BDD-cost:  105
c ---[1639]---> BDD-cost:  148
c ---[1638]---> BDD-cost:  105
c ---[1637]---> BDD-cost:  148
c ---[1636]---> BDD-cost:  107
c ---[1635]---> BDD-cost:  148
c ---[1634]---> BDD-cost:  107
c ---[1633]---> BDD-cost:  148
c ---[1632]---> BDD-cost:  137
c ---[1631]---> BDD-cost:  144
c ---[1630]---> BDD-cost:  148
c ---[1629]---> BDD-cost:  144
c ---[1628]---> BDD-cost:  148
c ---[1627]---> BDD-cost:  134
c ---[1626]---> BDD-cost:  148
c ---[1625]---> BDD-cost:  134
c ---[1624]---> BDD-cost:  148
c ---[1623]---> BDD-cost:  103
c ---[1622]---> BDD-cost:  148
c ---[1621]---> BDD-cost:  103
c ---[1620]---> BDD-cost:  147
c ---[1619]---> BDD-cost:  103
c ---[1618]---> BDD-cost:  146
c ---[1617]---> BDD-cost:  101
c ---[1616]---> BDD-cost:  146
c ---[1615]---> BDD-cost:  101
c ---[1614]---> BDD-cost:  146
c ---[1613]---> BDD-cost:  137
c ---[1612]---> BDD-cost:  146
c ---[1611]---> BDD-cost:  137
c ---[1610]---> BDD-cost:  146
c ---[1609]---> BDD-cost:  137
c ---[1608]---> BDD-cost:  110
c ---[1607]---> BDD-cost:  146
c ---[1606]---> BDD-cost:  110
c ---[1605]---> BDD-cost:  146
c ---[1604]---> BDD-cost:  154
c ---[1603]---> BDD-cost:  146
c ---[1602]---> BDD-cost:  154
c ---[1601]---> BDD-cost:  146
c ---[1600]---> BDD-cost:  153
c ---[1599]---> BDD-cost:  146
c ---[1598]---> BDD-cost:  147
c ---[1597]---> BDD-cost:  153
c ---[1596]---> BDD-cost:  146
c ---[1595]---> BDD-cost:   99
c ---[1594]---> BDD-cost:  146
c ---[1593]---> BDD-cost:   99
c ---[1592]---> BDD-cost:  146
c ---[1591]---> BDD-cost:  104
c ---[1590]---> BDD-cost:  146
c ---[1589]---> BDD-cost:  104
c ---[1588]---> BDD-cost:  146
c ---[1587]---> BDD-cost:  137
c ---[1586]---> BDD-cost:   87
c ---[1585]---> BDD-cost:  146
c ---[1584]---> BDD-cost:   87
c ---[1583]---> BDD-cost:  146
c ---[1582]---> BDD-cost:   88
c ---[1581]---> BDD-cost:  146
c ---[1580]---> BDD-cost:   88
c ---[1579]---> BDD-cost:  146
c ---[1578]---> BDD-cost:  155
c ---[1577]---> BDD-cost:  146
c ---[1576]---> BDD-cost:  103
c ---[1575]---> BDD-cost:  155
c ---[1574]---> BDD-cost:  146
c ---[1573]---> BDD-cost:  148
c ---[1572]---> BDD-cost:  146
c ---[1571]---> BDD-cost:  148
c ---[1570]---> BDD-cost:  146
c ---[1569]---> BDD-cost:  152
c ---[1568]---> BDD-cost:  146
c ---[1567]---> BDD-cost:  152
c ---[1566]---> BDD-cost:  146
c ---[1565]---> BDD-cost:  137
c ---[1564]---> BDD-cost:  105
c ---[1563]---> BDD-cost:  146
c ---[1562]---> BDD-cost:  105
c ---[1561]---> BDD-cost:  146
c ---[1560]---> BDD-cost:  107
c ---[1559]---> BDD-cost:  146
c ---[1558]---> BDD-cost:  107
c ---[1557]---> BDD-cost:  146
c ---[1556]---> BDD-cost:  144
c ---[1555]---> BDD-cost:  146
c ---[1554]---> BDD-cost:  103
c ---[1553]---> BDD-cost:  144
c ---[1552]---> BDD-cost:  146
c ---[1551]---> BDD-cost:  134
c ---[1550]---> BDD-cost:  146
c ---[1549]---> BDD-cost:  134
c ---[1548]---> BDD-cost:  146
c ---[1547]---> BDD-cost:  103
c ---[1546]---> BDD-cost:  146
c ---[1545]---> BDD-cost:  103
c ---[1544]---> BDD-cost:  101
c ---[1543]---> BDD-cost:  137
c ---[1542]---> BDD-cost:  137
c ---[1541]---> BDD-cost:  101
c ---[1540]---> BDD-cost:  137
c ---[1539]---> BDD-cost:  101
c ---[1538]---> BDD-cost:  110
c ---[1537]---> BDD-cost:  101
c ---[1536]---> BDD-cost:  110
c ---[1535]---> BDD-cost:  101
c ---[1534]---> BDD-cost:  154
c ---[1533]---> BDD-cost:  101
c ---[1532]---> BDD-cost:   99
c ---[1531]---> BDD-cost:  154
c ---[1530]---> BDD-cost:  101
c ---[1529]---> BDD-cost:  153
c ---[1528]---> BDD-cost:  101
c ---[1527]---> BDD-cost:  153
c ---[1526]---> BDD-cost:  101
c ---[1525]---> BDD-cost:   99
c ---[1524]---> BDD-cost:  101
c ---[1523]---> BDD-cost:   99
c ---[1522]---> BDD-cost:  101
c ---[1521]---> BDD-cost:  137
c ---[1520]---> BDD-cost:  104
c ---[1519]---> BDD-cost:  101
c ---[1518]---> BDD-cost:  104
c ---[1517]---> BDD-cost:  101
c ---[1516]---> BDD-cost:   87
c ---[1515]---> BDD-cost:  101
c ---[1514]---> BDD-cost:   87
c ---[1513]---> BDD-cost:  101
c ---[1512]---> BDD-cost:   88
c ---[1511]---> BDD-cost:  101
c ---[1510]---> BDD-cost:  144
c ---[1509]---> BDD-cost:   99
c ---[1508]---> BDD-cost:   88
c ---[1507]---> BDD-cost:  101
c ---[1506]---> BDD-cost:  155
c ---[1505]---> BDD-cost:  101
c ---[1504]---> BDD-cost:  155
c ---[1503]---> BDD-cost:  101
c ---[1502]---> BDD-cost:  148
c ---[1501]---> BDD-cost:  101
c ---[1500]---> BDD-cost:  148
c ---[1499]---> BDD-cost:  101
c ---[1498]---> BDD-cost:  137
c ---[1497]---> BDD-cost:  152
c ---[1496]---> BDD-cost:  101
c ---[1495]---> BDD-cost:  152
c ---[1494]---> BDD-cost:  101
c ---[1493]---> BDD-cost:  105
c ---[1492]---> BDD-cost:  101
c ---[1491]---> BDD-cost:  105
c ---[1490]---> BDD-cost:  101
c ---[1489]---> BDD-cost:  107
c ---[1488]---> BDD-cost:  101
c ---[1487]---> BDD-cost:   99
c ---[1486]---> BDD-cost:  107
c ---[1485]---> BDD-cost:  101
c ---[1484]---> BDD-cost:  144
c ---[1483]---> BDD-cost:  101
c ---[1482]---> BDD-cost:  144
c ---[1481]---> BDD-cost:  101
c ---[1480]---> BDD-cost:  134
c ---[1479]---> BDD-cost:  101
c ---[1478]---> BDD-cost:  134
c ---[1477]---> BDD-cost:  101
c ---[1476]---> BDD-cost:  137
c ---[1475]---> BDD-cost:  103
c ---[1474]---> BDD-cost:  101
c ---[1473]---> BDD-cost:  103
c ---[1472]---> BDD-cost:  137
c ---[1471]---> BDD-cost:  110
c ---[1470]---> BDD-cost:  137
c ---[1469]---> BDD-cost:  110
c ---[1468]---> BDD-cost:  137
c ---[1467]---> BDD-cost:  154
c ---[1466]---> BDD-cost:  137
c ---[1465]---> BDD-cost:   99
c ---[1464]---> BDD-cost:  154
c ---[1463]---> BDD-cost:  137
c ---[1462]---> BDD-cost:  153
c ---[1461]---> BDD-cost:  137
c ---[1460]---> BDD-cost:  153
c ---[1459]---> BDD-cost:  137
c ---[1458]---> BDD-cost:   99
c ---[1457]---> BDD-cost:  137
c ---[1456]---> BDD-cost:   99
c ---[1455]---> BDD-cost:  137
c ---[1454]---> BDD-cost:  137
c ---[1453]---> BDD-cost:  104
c ---[1452]---> BDD-cost:  137
c ---[1451]---> BDD-cost:  104
c ---[1450]---> BDD-cost:  137
c ---[1449]---> BDD-cost:   87
c ---[1448]---> BDD-cost:  137
c ---[1447]---> BDD-cost:   87
c ---[1446]---> BDD-cost:  137
c ---[1445]---> BDD-cost:   88
c ---[1444]---> BDD-cost:  137
c ---[1443]---> BDD-cost:  152
c ---[1442]---> BDD-cost:   88
c ---[1441]---> BDD-cost:  137
c ---[1440]---> BDD-cost:  155
c ---[1439]---> BDD-cost:  137
c ---[1438]---> BDD-cost:  155
c ---[1437]---> BDD-cost:  137
c ---[1436]---> BDD-cost:  148
c ---[1435]---> BDD-cost:  137
c ---[1434]---> BDD-cost:  148
c ---[1433]---> BDD-cost:  137
c ---[1432]---> BDD-cost:  137
c ---[1431]---> BDD-cost:  152
c ---[1430]---> BDD-cost:  137
c ---[1429]---> BDD-cost:  152
c ---[1428]---> BDD-cost:  137
c ---[1427]---> BDD-cost:  105
c ---[1426]---> BDD-cost:  137
c ---[1425]---> BDD-cost:  105
c ---[1424]---> BDD-cost:  137
c ---[1423]---> BDD-cost:  107
c ---[1422]---> BDD-cost:  137
c ---[1421]---> BDD-cost:  152
c ---[1420]---> BDD-cost:  107
c ---[1419]---> BDD-cost:  137
c ---[1418]---> BDD-cost:  144
c ---[1417]---> BDD-cost:  137
c ---[1416]---> BDD-cost:  144
c ---[1415]---> BDD-cost:  137
c ---[1414]---> BDD-cost:  134
c ---[1413]---> BDD-cost:  137
c ---[1412]---> BDD-cost:  134
c ---[1411]---> BDD-cost:  137
c ---[1410]---> BDD-cost:  137
c ---[1409]---> BDD-cost:  103
c ---[1408]---> BDD-cost:  137
c ---[1407]---> BDD-cost:  103
c ---[1406]---> BDD-cost:  110
c ---[1405]---> BDD-cost:  154
c ---[1404]---> BDD-cost:  110
c ---[1403]---> BDD-cost:  154
c ---[1402]---> BDD-cost:  110
c ---[1401]---> BDD-cost:  153
c ---[1400]---> BDD-cost:  110
c ---[1399]---> BDD-cost:  103
c ---[1398]---> BDD-cost:   81
c ---[1397]---> BDD-cost:  153
c ---[1396]---> BDD-cost:  110
c ---[1395]---> BDD-cost:   99
c ---[1394]---> BDD-cost:  110
c ---[1393]---> BDD-cost:   99
c ---[1392]---> BDD-cost:  110
c ---[1391]---> BDD-cost:  104
c ---[1390]---> BDD-cost:  110
c ---[1389]---> BDD-cost:  104
c ---[1388]---> BDD-cost:  110
c ---[1387]---> BDD-cost:  137
c ---[1386]---> BDD-cost:   87
c ---[1385]---> BDD-cost:  110
c ---[1384]---> BDD-cost:   87
c ---[1383]---> BDD-cost:  110
c ---[1382]---> BDD-cost:   88
c ---[1381]---> BDD-cost:  110
c ---[1380]---> BDD-cost:   88
c ---[1379]---> BDD-cost:  110
c ---[1378]---> BDD-cost:  155
c ---[1377]---> BDD-cost:  110
c ---[1376]---> BDD-cost:   81
c ---[1375]---> BDD-cost:  155
c ---[1374]---> BDD-cost:  110
c ---[1373]---> BDD-cost:  148
c ---[1372]---> BDD-cost:  110
c ---[1371]---> BDD-cost:  148
c ---[1370]---> BDD-cost:  110
c ---[1369]---> BDD-cost:  152
c ---[1368]---> BDD-cost:  110
c ---[1367]---> BDD-cost:  152
c ---[1366]---> BDD-cost:  110
c ---[1365]---> BDD-cost:  137
c ---[1364]---> BDD-cost:  105
c ---[1363]---> BDD-cost:  110
c ---[1362]---> BDD-cost:  105
c ---[1361]---> BDD-cost:  110
c ---[1360]---> BDD-cost:  107
c ---[1359]---> BDD-cost:  110
c ---[1358]---> BDD-cost:  107
c ---[1357]---> BDD-cost:  110
c ---[1356]---> BDD-cost:  144
c ---[1355]---> BDD-cost:  110
c ---[1354]---> BDD-cost:   85
c ---[1353]---> BDD-cost:  144
c ---[1352]---> BDD-cost:  110
c ---[1351]---> BDD-cost:  134
c ---[1350]---> BDD-cost:  110
c ---[1349]---> BDD-cost:  134
c ---[1348]---> BDD-cost:  110
c ---[1347]---> BDD-cost:  103
c ---[1346]---> BDD-cost:  110
c ---[1345]---> BDD-cost:  103
c ---[1344]---> BDD-cost:  154
c ---[1343]---> BDD-cost:  137
c ---[1342]---> BDD-cost:  153
c ---[1341]---> BDD-cost:  154
c ---[1340]---> BDD-cost:  153
c ---[1339]---> BDD-cost:  154
c ---[1338]---> BDD-cost:   99
c ---[1337]---> BDD-cost:  154
c ---[1336]---> BDD-cost:   99
c ---[1335]---> BDD-cost:  154
c ---[1334]---> BDD-cost:  104
c ---[1333]---> BDD-cost:  154
c ---[1332]---> BDD-cost:   85
c ---[1331]---> BDD-cost:  104
c ---[1330]---> BDD-cost:  154
c ---[1329]---> BDD-cost:   87
c ---[1328]---> BDD-cost:  154
c ---[1327]---> BDD-cost:   87
c ---[1326]---> BDD-cost:  154
c ---[1325]---> BDD-cost:   88
c ---[1324]---> BDD-cost:  154
c ---[1323]---> BDD-cost:   88
c ---[1322]---> BDD-cost:  154
c ---[1321]---> BDD-cost:  137
c ---[1320]---> BDD-cost:  155
c ---[1319]---> BDD-cost:  154
c ---[1318]---> BDD-cost:  155
c ---[1317]---> BDD-cost:  154
c ---[1316]---> BDD-cost:  148
c ---[1315]---> BDD-cost:  154
c ---[1314]---> BDD-cost:  148
c ---[1313]---> BDD-cost:  154
c ---[1312]---> BDD-cost:  152
c ---[1311]---> BDD-cost:  154
c ---[1310]---> BDD-cost:  148
c ---[1309]---> BDD-cost:  152
c ---[1308]---> BDD-cost:  154
c ---[1307]---> BDD-cost:  105
c ---[1306]---> BDD-cost:  154
c ---[1305]---> BDD-cost:  105
c ---[1304]---> BDD-cost:  154
c ---[1303]---> BDD-cost:  107
c ---[1302]---> BDD-cost:  154
c ---[1301]---> BDD-cost:  107
c ---[1300]---> BDD-cost:  154
c ---[1299]---> BDD-cost:  137
c ---[1298]---> BDD-cost:  144
c ---[1297]---> BDD-cost:  154
c ---[1296]---> BDD-cost:  144
c ---[1295]---> BDD-cost:  154
c ---[1294]---> BDD-cost:  134
c ---[1293]---> BDD-cost:  154
c ---[1292]---> BDD-cost:  134
c ---[1291]---> BDD-cost:  154
c ---[1290]---> BDD-cost:  103
c ---[1289]---> BDD-cost:  154
c ---[1288]---> BDD-cost:  134
c ---[1287]---> BDD-cost:  148
c ---[1286]---> BDD-cost:  103
c ---[1285]---> BDD-cost:  153
c ---[1284]---> BDD-cost:   99
c ---[1283]---> BDD-cost:  153
c ---[1282]---> BDD-cost:   99
c ---[1281]---> BDD-cost:  153
c ---[1280]---> BDD-cost:  104
c ---[1279]---> BDD-cost:  153
c ---[1278]---> BDD-cost:  104
c ---[1277]---> BDD-cost:  153
c ---[1276]---> BDD-cost:  137
c ---[1275]---> BDD-cost:   87
c ---[1274]---> BDD-cost:  153
c ---[1273]---> BDD-cost:   87
c ---[1272]---> BDD-cost:  153
c ---[1271]---> BDD-cost:   88
c ---[1270]---> BDD-cost:  153
c ---[1269]---> BDD-cost:   88
c ---[1268]---> BDD-cost:  153
c ---[1267]---> BDD-cost:  155
c ---[1266]---> BDD-cost:  153
c ---[1265]---> BDD-cost:  146
c ---[1264]---> BDD-cost:  155
c ---[1263]---> BDD-cost:  153
c ---[1262]---> BDD-cost:  148
c ---[1261]---> BDD-cost:  153
c ---[1260]---> BDD-cost:  148
c ---[1259]---> BDD-cost:  153
c ---[1258]---> BDD-cost:  152
c ---[1257]---> BDD-cost:  153
c ---[1256]---> BDD-cost:  152
c ---[1255]---> BDD-cost:  153
c ---[1254]---> BDD-cost:  137
c ---[1253]---> BDD-cost:  105
c ---[1252]---> BDD-cost:  153
c ---[1251]---> BDD-cost:  105
c ---[1250]---> BDD-cost:  153
c ---[1249]---> BDD-cost:  107
c ---[1248]---> BDD-cost:  153
c ---[1247]---> BDD-cost:  107
c ---[1246]---> BDD-cost:  153
c ---[1245]---> BDD-cost:  144
c ---[1244]---> BDD-cost:  153
c ---[1243]---> BDD-cost:  146
c ---[1242]---> BDD-cost:  144
c ---[1241]---> BDD-cost:  153
c ---[1240]---> BDD-cost:  134
c ---[1239]---> BDD-cost:  153
c ---[1238]---> BDD-cost:  134
c ---[1237]---> BDD-cost:  153
c ---[1236]---> BDD-cost:  103
c ---[1235]---> BDD-cost:  153
c ---[1234]---> BDD-cost:  103
c ---[1233]---> BDD-cost:   99
c ---[1232]---> BDD-cost:  137
c ---[1231]---> BDD-cost:  104
c ---[1230]---> BDD-cost:   99
c ---[1229]---> BDD-cost:  104
c ---[1228]---> BDD-cost:   99
c ---[1227]---> BDD-cost:   87
c ---[1226]---> BDD-cost:   99
c ---[1225]---> BDD-cost:   87
c ---[1224]---> BDD-cost:   99
c ---[1223]---> BDD-cost:   88
c ---[1222]---> BDD-cost:   99
c ---[1221]---> BDD-cost:  101
c ---[1220]---> BDD-cost:   88
c ---[1219]---> BDD-cost:   99
c ---[1218]---> BDD-cost:  155
c ---[1217]---> BDD-cost:   99
c ---[1216]---> BDD-cost:  155
c ---[1215]---> BDD-cost:   99
c ---[1214]---> BDD-cost:  148
c ---[1213]---> BDD-cost:   99
c ---[1212]---> BDD-cost:  148
c ---[1211]---> BDD-cost:   99
c ---[1210]---> BDD-cost:  137
c ---[1209]---> BDD-cost:  152
c ---[1208]---> BDD-cost:   99
c ---[1207]---> BDD-cost:  152
c ---[1206]---> BDD-cost:   99
c ---[1205]---> BDD-cost:  105
c ---[1204]---> BDD-cost:   99
c ---[1203]---> BDD-cost:  105
c ---[1202]---> BDD-cost:   99
c ---[1201]---> BDD-cost:  107
c ---[1200]---> BDD-cost:   99
c ---[1199]---> BDD-cost:  101
c ---[1198]---> BDD-cost:  107
c ---[1197]---> BDD-cost:   99
c ---[1196]---> BDD-cost:  144
c ---[1195]---> BDD-cost:   99
c ---[1194]---> BDD-cost:  144
c ---[1193]---> BDD-cost:   99
c ---[1192]---> BDD-cost:  134
c ---[1191]---> BDD-cost:   99
c ---[1190]---> BDD-cost:  134
c ---[1189]---> BDD-cost:   99
c ---[1188]---> BDD-cost:  137
c ---[1187]---> BDD-cost:  103
c ---[1186]---> BDD-cost:   99
c ---[1185]---> BDD-cost:  103
c ---[1184]---> BDD-cost:  104
c ---[1183]---> BDD-cost:   87
c ---[1182]---> BDD-cost:  104
c ---[1181]---> BDD-cost:   87
c ---[1180]---> BDD-cost:  104
c ---[1179]---> BDD-cost:   88
c ---[1178]---> BDD-cost:  104
c ---[1177]---> BDD-cost:  103
c ---[1176]---> BDD-cost:  137
c ---[1175]---> BDD-cost:   88
c ---[1174]---> BDD-cost:  104
c ---[1173]---> BDD-cost:  155
c ---[1172]---> BDD-cost:  104
c ---[1171]---> BDD-cost:  155
c ---[1170]---> BDD-cost:  104
c ---[1169]---> BDD-cost:  148
c ---[1168]---> BDD-cost:  104
c ---[1167]---> BDD-cost:  148
c ---[1166]---> BDD-cost:  104
c ---[1165]---> BDD-cost:  137
c ---[1164]---> BDD-cost:  152
c ---[1163]---> BDD-cost:  104
c ---[1162]---> BDD-cost:  152
c ---[1161]---> BDD-cost:  104
c ---[1160]---> BDD-cost:  105
c ---[1159]---> BDD-cost:  104
c ---[1158]---> BDD-cost:  105
c ---[1157]---> BDD-cost:  104
c ---[1156]---> BDD-cost:  107
c ---[1155]---> BDD-cost:  104
c ---[1154]---> BDD-cost:  137
c ---[1153]---> BDD-cost:  107
c ---[1152]---> BDD-cost:  104
c ---[1151]---> BDD-cost:  144
c ---[1150]---> BDD-cost:  104
c ---[1149]---> BDD-cost:  144
c ---[1148]---> BDD-cost:  104
c ---[1147]---> BDD-cost:  134
c ---[1146]---> BDD-cost:  104
c ---[1145]---> BDD-cost:  134
c ---[1144]---> BDD-cost:  104
c ---[1143]---> BDD-cost:  137
c ---[1142]---> BDD-cost:  103
c ---[1141]---> BDD-cost:  104
c ---[1140]---> BDD-cost:  103
c ---[1139]---> BDD-cost:   87
c ---[1138]---> BDD-cost:   88
c ---[1137]---> BDD-cost:   87
c ---[1136]---> BDD-cost:   88
c ---[1135]---> BDD-cost:   87
c ---[1134]---> BDD-cost:  155
c ---[1133]---> BDD-cost:   87
c ---[1132]---> BDD-cost:  110
c ---[1131]---> BDD-cost:  155
c ---[1130]---> BDD-cost:   87
c ---[1129]---> BDD-cost:  148
c ---[1128]---> BDD-cost:   87
c ---[1127]---> BDD-cost:  148
c ---[1126]---> BDD-cost:   87
c ---[1125]---> BDD-cost:  152
c ---[1124]---> BDD-cost:   87
c ---[1123]---> BDD-cost:  152
c ---[1122]---> BDD-cost:   87
c ---[1121]---> BDD-cost:  137
c ---[1120]---> BDD-cost:  105
c ---[1119]---> BDD-cost:   87
c ---[1118]---> BDD-cost:  105
c ---[1117]---> BDD-cost:   87
c ---[1116]---> BDD-cost:  107
c ---[1115]---> BDD-cost:   87
c ---[1114]---> BDD-cost:  107
c ---[1113]---> BDD-cost:   87
c ---[1112]---> BDD-cost:  144
c ---[1111]---> BDD-cost:   87
c ---[1110]---> BDD-cost:  110
c ---[1109]---> BDD-cost:  144
c ---[1108]---> BDD-cost:   87
c ---[1107]---> BDD-cost:  134
c ---[1106]---> BDD-cost:   87
c ---[1105]---> BDD-cost:  134
c ---[1104]---> BDD-cost:   87
c ---[1103]---> BDD-cost:  103
c ---[1102]---> BDD-cost:   87
c ---[1101]---> BDD-cost:  103
c ---[1100]---> BDD-cost:   88
c ---[1099]---> BDD-cost:  137
c ---[1098]---> BDD-cost:  155
c ---[1097]---> BDD-cost:   88
c ---[1096]---> BDD-cost:  155
c ---[1095]---> BDD-cost:   88
c ---[1094]---> BDD-cost:  148
c ---[1093]---> BDD-cost:   88
c ---[1092]---> BDD-cost:  148
c ---[1091]---> BDD-cost:   88
c ---[1090]---> BDD-cost:  152
c ---[1089]---> BDD-cost:   88
c ---[1088]---> BDD-cost:  154
c ---[1087]---> BDD-cost:  152
c ---[1086]---> BDD-cost:   88
c ---[1085]---> BDD-cost:  105
c ---[1084]---> BDD-cost:   88
c ---[1083]---> BDD-cost:  105
c ---[1082]---> BDD-cost:   88
c ---[1081]---> BDD-cost:  107
c ---[1080]---> BDD-cost:   88
c ---[1079]---> BDD-cost:  107
c ---[1078]---> BDD-cost:   88
c ---[1077]---> BDD-cost:  137
c ---[1076]---> BDD-cost:  144
c ---[1075]---> BDD-cost:   88
c ---[1074]---> BDD-cost:  144
c ---[1073]---> BDD-cost:   88
c ---[1072]---> BDD-cost:  134
c ---[1071]---> BDD-cost:   88
c ---[1070]---> BDD-cost:  134
c ---[1069]---> BDD-cost:   88
c ---[1068]---> BDD-cost:  103
c ---[1067]---> BDD-cost:   88
c ---[1066]---> BDD-cost:  137
c ---[1065]---> BDD-cost:  134
c ---[1064]---> BDD-cost:  154
c ---[1063]---> BDD-cost:  103
c ---[1062]---> BDD-cost:  155
c ---[1061]---> BDD-cost:  148
c ---[1060]---> BDD-cost:  155
c ---[1059]---> BDD-cost:  148
c ---[1058]---> BDD-cost:  155
c ---[1057]---> BDD-cost:  152
c ---[1056]---> BDD-cost:  155
c ---[1055]---> BDD-cost:  152
c ---[1054]---> BDD-cost:  155
c ---[1053]---> BDD-cost:  137
c ---[1052]---> BDD-cost:  105
c ---[1051]---> BDD-cost:  155
c ---[1050]---> BDD-cost:  105
c ---[1049]---> BDD-cost:  155
c ---[1048]---> BDD-cost:  107
c ---[1047]---> BDD-cost:  155
c ---[1046]---> BDD-cost:  107
c ---[1045]---> BDD-cost:  155
c ---[1044]---> BDD-cost:  144
c ---[1043]---> BDD-cost:  155
c ---[1042]---> BDD-cost:  153
c ---[1041]---> BDD-cost:  144
c ---[1040]---> BDD-cost:  155
c ---[1039]---> BDD-cost:  134
c ---[1038]---> BDD-cost:  155
c ---[1037]---> BDD-cost:  134
c ---[1036]---> BDD-cost:  155
c ---[1035]---> BDD-cost:  103
c ---[1034]---> BDD-cost:  155
c ---[1033]---> BDD-cost:  103
c ---[1032]---> BDD-cost:  148
c ---[1031]---> BDD-cost:  137
c ---[1030]---> BDD-cost:  152
c ---[1029]---> BDD-cost:  148
c ---[1028]---> BDD-cost:  152
c ---[1027]---> BDD-cost:  148
c ---[1026]---> BDD-cost:  105
c ---[1025]---> BDD-cost:  148
c ---[1024]---> BDD-cost:  105
c ---[1023]---> BDD-cost:  148
c ---[1022]---> BDD-cost:  107
c ---[1021]---> BDD-cost:  148
c ---[1020]---> BDD-cost:  153
c ---[1019]---> BDD-cost:  107
c ---[1018]---> BDD-cost:  148
c ---[1017]---> BDD-cost:  144
c ---[1016]---> BDD-cost:  148
c ---[1015]---> BDD-cost:  144
c ---[1014]---> BDD-cost:  148
c ---[1013]---> BDD-cost:  134
c ---[1012]---> BDD-cost:  148
c ---[1011]---> BDD-cost:  134
c ---[1010]---> BDD-cost:  148
c ---[1009]---> BDD-cost:  137
c ---[1008]---> BDD-cost:  103
c ---[1007]---> BDD-cost:  148
c ---[1006]---> BDD-cost:  103
c ---[1005]---> BDD-cost:  152
c ---[1004]---> BDD-cost:  105
c ---[1003]---> BDD-cost:  152
c ---[1002]---> BDD-cost:  105
c ---[1001]---> BDD-cost:  152
c ---[1000]---> BDD-cost:  107
c ---[ 999]---> BDD-cost:  152
c ---[ 998]---> BDD-cost:   99
c ---[ 997]---> BDD-cost:  107
c ---[ 996]---> BDD-cost:  152
c ---[ 995]---> BDD-cost:  144
c ---[ 994]---> BDD-cost:  152
c ---[ 993]---> BDD-cost:  144
c ---[ 992]---> BDD-cost:  152
c ---[ 991]---> BDD-cost:  134
c ---[ 990]---> BDD-cost:  152
c ---[ 989]---> BDD-cost:  134
c ---[ 988]---> BDD-cost:  152
c ---[ 987]---> BDD-cost:  137
c ---[ 986]---> BDD-cost:  103
c ---[ 985]---> BDD-cost:  152
c ---[ 984]---> BDD-cost:  103
c ---[ 983]---> BDD-cost:  105
c ---[ 982]---> BDD-cost:  107
c ---[ 981]---> BDD-cost:  105
c ---[ 980]---> BDD-cost:  107
c ---[ 979]---> BDD-cost:  105
c ---[ 978]---> BDD-cost:  144
c ---[ 977]---> BDD-cost:  105
c ---[ 976]---> BDD-cost:   99
c ---[ 975]---> BDD-cost:  144
c ---[ 974]---> BDD-cost:  105
c ---[ 973]---> BDD-cost:  134
c ---[ 972]---> BDD-cost:  105
c ---[ 971]---> BDD-cost:  134
c ---[ 970]---> BDD-cost:  105
c ---[ 969]---> BDD-cost:  103
c ---[ 968]---> BDD-cost:  105
c ---[ 967]---> BDD-cost:  103
c ---[ 966]---> BDD-cost:  107
c ---[ 965]---> BDD-cost:  137
c ---[ 964]---> BDD-cost:  144
c ---[ 963]---> BDD-cost:  107
c ---[ 962]---> BDD-cost:  144
c ---[ 961]---> BDD-cost:  107
c ---[ 960]---> BDD-cost:  134
c ---[ 959]---> BDD-cost:  107
c ---[ 958]---> BDD-cost:  134
c ---[ 957]---> BDD-cost:  107
c ---[ 956]---> BDD-cost:  103
c ---[ 955]---> BDD-cost:  107
c ---[ 954]---> BDD-cost:  103
c ---[ 953]---> BDD-cost:  104
c ---[ 952]---> BDD-cost:  103
c ---[ 951]---> BDD-cost:  144
c ---[ 950]---> BDD-cost:  134
c ---[ 949]---> BDD-cost:  144
c ---[ 948]---> BDD-cost:  134
c ---[ 947]---> BDD-cost:  144
c ---[ 946]---> BDD-cost:  103
c ---[ 945]---> BDD-cost:  144
c ---[ 944]---> BDD-cost:  103
c ---[ 943]---> BDD-cost:  134
c ---[ 942]---> BDD-cost:  137
c ---[ 941]---> BDD-cost:  103
c ---[ 940]---> BDD-cost:  134
c ---[ 939]---> BDD-cost:  103
c ---[ 938]---> BDD-cost:  101
c ---[ 937]---> BDD-cost:  101
c ---[ 936]---> BDD-cost:  113
c ---[ 935]---> BDD-cost:  113
c ---[ 934]---> BDD-cost:   81
c ---[ 933]---> BDD-cost:   81
c ---[ 932]---> BDD-cost:  109
c ---[ 931]---> BDD-cost:  104
c ---[ 930]---> BDD-cost:  109
c ---[ 929]---> BDD-cost:  113
c ---[ 928]---> BDD-cost:  113
c ---[ 927]---> BDD-cost:  113
c ---[ 926]---> BDD-cost:  113
c ---[ 925]---> BDD-cost:  105
c ---[ 924]---> BDD-cost:  105
c ---[ 923]---> BDD-cost:  113
c ---[ 922]---> BDD-cost:  113
c ---[ 921]---> BDD-cost:  101
c ---[ 920]---> BDD-cost:  137
c ---[ 919]---> BDD-cost:  101
c ---[ 918]---> BDD-cost:   97
c ---[ 917]---> BDD-cost:   97
c ---[ 916]---> BDD-cost:   97
c ---[ 915]---> BDD-cost:   97
c ---[ 914]---> BDD-cost:  110
c ---[ 913]---> BDD-cost:  110
c ---[ 912]---> BDD-cost:   79
c ---[ 911]---> BDD-cost:   79
c ---[ 910]---> BDD-cost:   83
c ---[ 909]---> BDD-cost:   87
c ---[ 908]---> BDD-cost:   83
c ---[ 907]---> BDD-cost:  109
c ---[ 906]---> BDD-cost:  109
c ---[ 905]---> BDD-cost:  110
c ---[ 904]---> BDD-cost:  110
c ---[ 903]---> BDD-cost:   99
c ---[ 902]---> BDD-cost:   99
c ---[ 901]---> BDD-cost:  100
c ---[ 900]---> BDD-cost:  100
c ---[ 899]---> BDD-cost:  108
c ---[ 898]---> BDD-cost:  137
c ---[ 897]---> BDD-cost:  108
c ---[ 896]---> BDD-cost:  107
c ---[ 895]---> BDD-cost:  107
c ---[ 894]---> BDD-cost:  116
c ---[ 893]---> BDD-cost:  116
c ---[ 892]---> BDD-cost:   97
c ---[ 891]---> BDD-cost:   97
c ---[ 890]---> BDD-cost:  102
c ---[ 889]---> BDD-cost:  102
c ---[ 888]---> BDD-cost:   85
c ---[ 887]---> BDD-cost:   87
c ---[ 886]---> BDD-cost:   85
c ---[ 885]---> BDD-cost:   86
c ---[ 884]---> BDD-cost:   86
c ---[ 883]---> BDD-cost:  113
c ---[ 882]---> BDD-cost:  113
c ---[ 881]---> BDD-cost:  104
c ---[ 880]---> BDD-cost:  104
c ---[ 879]---> BDD-cost:  110
c ---[ 878]---> BDD-cost:  110
c ---[ 877]---> BDD-cost:   79
c ---[ 876]---> BDD-cost:  137
c ---[ 875]---> BDD-cost:   79
c ---[ 874]---> BDD-cost:  105
c ---[ 873]---> BDD-cost:  105
c ---[ 872]---> BDD-cost:  113
c ---[ 871]---> BDD-cost:  113
c ---[ 870]---> BDD-cost:  106
c ---[ 869]---> BDD-cost:  106
c ---[ 868]---> BDD-cost:  101
c ---[ 867]---> BDD-cost:  101
c ---[ 866]---> BDD-cost:   88
c ---[ 865]---> BDD-cost:  137
c ---[ 864]---> BDD-cost:  143
c ---[ 863]---> BDD-cost:   88
c ---[ 862]---> BDD-cost:  137
c ---[ 861]---> BDD-cost:  155
c ---[ 860]---> BDD-cost:  137
c ---[ 859]---> BDD-cost:  155
c ---[ 858]---> BDD-cost:  137
c ---[ 857]---> BDD-cost:  148
c ---[ 856]---> BDD-cost:  137
c ---[ 855]---> BDD-cost:  148
c ---[ 854]---> BDD-cost:  137
c ---[ 853]---> BDD-cost:  103
c ---[ 852]---> BDD-cost:  152
c ---[ 851]---> BDD-cost:  137
c ---[ 850]---> BDD-cost:  152
c ---[ 849]---> BDD-cost:  137
c ---[ 848]---> BDD-cost:  105
c ---[ 847]---> BDD-cost:  137
c ---[ 846]---> BDD-cost:  105
c ---[ 845]---> BDD-cost:  137
c ---[ 844]---> BDD-cost:  107
c ---[ 843]---> BDD-cost:  137
c ---[ 842]---> BDD-cost:  143
c ---[ 841]---> BDD-cost:  107
c ---[ 840]---> BDD-cost:  137
c ---[ 839]---> BDD-cost:  144
c ---[ 838]---> BDD-cost:  137
c ---[ 837]---> BDD-cost:  144
c ---[ 836]---> BDD-cost:  137
c ---[ 835]---> BDD-cost:  134
c ---[ 834]---> BDD-cost:  137
c ---[ 833]---> BDD-cost:  134
c ---[ 832]---> BDD-cost:  137
c ---[ 831]---> BDD-cost:  103
c ---[ 830]---> BDD-cost:  103
c ---[ 829]---> BDD-cost:  137
c ---[ 828]---> BDD-cost:  103
c ---[ 827]---> BDD-cost:   83
c ---[ 826]---> BDD-cost:  156
c ---[ 825]---> BDD-cost:   83
c ---[ 824]---> BDD-cost:  156
c ---[ 823]---> BDD-cost:   83
c ---[ 822]---> BDD-cost:  144
c ---[ 821]---> BDD-cost:   83
c ---[ 820]---> BDD-cost:  147
c ---[ 819]---> BDD-cost:  144
c ---[ 818]---> BDD-cost:   83
c ---[ 817]---> BDD-cost:  134
c ---[ 816]---> BDD-cost:   83
c ---[ 815]---> BDD-cost:  134
c ---[ 814]---> BDD-cost:   83
c ---[ 813]---> BDD-cost:  143
c ---[ 812]---> BDD-cost:   83
c ---[ 811]---> BDD-cost:  143
c ---[ 810]---> BDD-cost:   83
c ---[ 809]---> BDD-cost:  103
c ---[ 808]---> BDD-cost:  147
c ---[ 807]---> BDD-cost:   83
c ---[ 806]---> BDD-cost:  147
c ---[ 805]---> BDD-cost:   83
c ---[ 804]---> BDD-cost:  103
c ---[ 803]---> BDD-cost:   83
c ---[ 802]---> BDD-cost:  103
c ---[ 801]---> BDD-cost:   83
c ---[ 800]---> BDD-cost:   99
c ---[ 799]---> BDD-cost:   83
c ---[ 798]---> BDD-cost:  147
c ---[ 797]---> BDD-cost:   99
c ---[ 796]---> BDD-cost:   83
c ---[ 795]---> BDD-cost:   99
c ---[ 794]---> BDD-cost:   83
c ---[ 793]---> BDD-cost:   99
c ---[ 792]---> BDD-cost:   83
c ---[ 791]---> BDD-cost:  152
c ---[ 790]---> BDD-cost:   83
c ---[ 789]---> BDD-cost:  152
c ---[ 788]---> BDD-cost:   83
c ---[ 787]---> BDD-cost:  103
c ---[ 786]---> BDD-cost:   81
c ---[ 785]---> BDD-cost:   83
c ---[ 784]---> BDD-cost:   81
c ---[ 783]---> BDD-cost:   83
c ---[ 782]---> BDD-cost:   85
c ---[ 781]---> BDD-cost:   83
c ---[ 780]---> BDD-cost:   85
c ---[ 779]---> BDD-cost:   83
c ---[ 778]---> BDD-cost:  148
c ---[ 777]---> BDD-cost:   83
c ---[ 776]---> BDD-cost:  103
c ---[ 775]---> BDD-cost:  103
c ---[ 774]---> BDD-cost:  148
c ---[ 773]---> BDD-cost:   83
c ---[ 772]---> BDD-cost:  146
c ---[ 771]---> BDD-cost:   83
c ---[ 770]---> BDD-cost:  146
c ---[ 769]---> BDD-cost:   83
c ---[ 768]---> BDD-cost:  101
c ---[ 767]---> BDD-cost:   83
c ---[ 766]---> BDD-cost:  101
c ---[ 765]---> BDD-cost:   83
c ---[ 764]---> BDD-cost:  103
c ---[ 763]---> BDD-cost:  137
c ---[ 762]---> BDD-cost:   83
c ---[ 761]---> BDD-cost:  137
c ---[ 760]---> BDD-cost:   83
c ---[ 759]---> BDD-cost:  110
c ---[ 758]---> BDD-cost:   83
c ---[ 757]---> BDD-cost:  110
c ---[ 756]---> BDD-cost:   83
c ---[ 755]---> BDD-cost:  154
c ---[ 754]---> BDD-cost:   83
c ---[ 753]---> BDD-cost:  103
c ---[ 752]---> BDD-cost:  154
c ---[ 751]---> BDD-cost:   83
c ---[ 750]---> BDD-cost:  153
c ---[ 749]---> BDD-cost:   83
c ---[ 748]---> BDD-cost:  153
c ---[ 747]---> BDD-cost:   83
c ---[ 746]---> BDD-cost:   99
c ---[ 745]---> BDD-cost:   83
c ---[ 744]---> BDD-cost:   99
c ---[ 743]---> BDD-cost:   83
c ---[ 742]---> BDD-cost:  103
c ---[ 741]---> BDD-cost:  104
c ---[ 740]---> BDD-cost:   83
c ---[ 739]---> BDD-cost:  104
c ---[ 738]---> BDD-cost:   83
c ---[ 737]---> BDD-cost:   87
c ---[ 736]---> BDD-cost:   83
c ---[ 735]---> BDD-cost:   87
c ---[ 734]---> BDD-cost:   83
c ---[ 733]---> BDD-cost:   88
c ---[ 732]---> BDD-cost:   83
c ---[ 731]---> BDD-cost:   99
c ---[ 730]---> BDD-cost:   88
c ---[ 729]---> BDD-cost:   83
c ---[ 728]---> BDD-cost:  155
c ---[ 727]---> BDD-cost:   83
c ---[ 726]---> BDD-cost:  155
c ---[ 725]---> BDD-cost:   83
c ---[ 724]---> BDD-cost:  148
c ---[ 723]---> BDD-cost:   83
c ---[ 722]---> BDD-cost:  148
c ---[ 721]---> BDD-cost:   83
c ---[ 720]---> BDD-cost:  103
c ---[ 719]---> BDD-cost:  152
c ---[ 718]---> BDD-cost:   83
c ---[ 717]---> BDD-cost:  152
c ---[ 716]---> BDD-cost:   83
c ---[ 715]---> BDD-cost:  105
c ---[ 714]---> BDD-cost:   83
c ---[ 713]---> BDD-cost:  105
c ---[ 712]---> BDD-cost:   83
c ---[ 711]---> BDD-cost:  107
c ---[ 710]---> BDD-cost:   83
c ---[ 709]---> BDD-cost:   99
c ---[ 708]---> BDD-cost:  107
c ---[ 707]---> BDD-cost:   83
c ---[ 706]---> BDD-cost:  144
c ---[ 705]---> BDD-cost:   83
c ---[ 704]---> BDD-cost:  144
c ---[ 703]---> BDD-cost:   83
c ---[ 702]---> BDD-cost:  134
c ---[ 701]---> BDD-cost:   83
c ---[ 700]---> BDD-cost:  134
c ---[ 699]---> BDD-cost:   83
c ---[ 698]---> BDD-cost:  103
c ---[ 697]---> BDD-cost:  103
c ---[ 696]---> BDD-cost:   83
c ---[ 695]---> BDD-cost:  103
c ---[ 694]---> BDD-cost:  156
c ---[ 693]---> BDD-cost:  144
c ---[ 692]---> BDD-cost:  156
c ---[ 691]---> BDD-cost:  144
c ---[ 690]---> BDD-cost:  156
c ---[ 689]---> BDD-cost:  134
c ---[ 688]---> BDD-cost:  156
c ---[ 687]---> BDD-cost:   99
c ---[ 686]---> BDD-cost:  134
c ---[ 685]---> BDD-cost:  156
c ---[ 684]---> BDD-cost:  143
c ---[ 683]---> BDD-cost:  156
c ---[ 682]---> BDD-cost:  143
c ---[ 681]---> BDD-cost:  156
c ---[ 680]---> BDD-cost:  147
c ---[ 679]---> BDD-cost:  156
c ---[ 678]---> BDD-cost:  147
c ---[ 677]---> BDD-cost:  156
c ---[ 676]---> BDD-cost:  103
c ---[ 675]---> BDD-cost:  103
c ---[ 674]---> BDD-cost:  156
c ---[ 673]---> BDD-cost:  103
c ---[ 672]---> BDD-cost:  156
c ---[ 671]---> BDD-cost:   99
c ---[ 670]---> BDD-cost:  156
c ---[ 669]---> BDD-cost:   99
c ---[ 668]---> BDD-cost:  156
c ---[ 667]---> BDD-cost:   99
c ---[ 666]---> BDD-cost:  156
c ---[ 665]---> BDD-cost:  137
c ---[ 664]---> BDD-cost:   99
c ---[ 663]---> BDD-cost:   99
c ---[ 662]---> BDD-cost:  156
c ---[ 661]---> BDD-cost:  152
c ---[ 660]---> BDD-cost:  156
c ---[ 659]---> BDD-cost:  152
c ---[ 658]---> BDD-cost:  156
c ---[ 657]---> BDD-cost:   81
c ---[ 656]---> BDD-cost:  156
c ---[ 655]---> BDD-cost:   81
c ---[ 654]---> BDD-cost:  156
c ---[ 653]---> BDD-cost:  103
c ---[ 652]---> BDD-cost:   85
c ---[ 651]---> BDD-cost:  156
c ---[ 650]---> BDD-cost:   85
c ---[ 649]---> BDD-cost:  156
c ---[ 648]---> BDD-cost:  148
c ---[ 647]---> BDD-cost:  156
c ---[ 646]---> BDD-cost:  148
c ---[ 645]---> BDD-cost:  156
c ---[ 644]---> BDD-cost:  146
c ---[ 643]---> BDD-cost:  156
c ---[ 642]---> BDD-cost:  152
c ---[ 641]---> BDD-cost:  146
c ---[ 640]---> BDD-cost:  156
c ---[ 639]---> BDD-cost:  101
c ---[ 638]---> BDD-cost:  156
c ---[ 637]---> BDD-cost:  101
c ---[ 636]---> BDD-cost:  156
c ---[ 635]---> BDD-cost:  137
c ---[ 634]---> BDD-cost:  156
c ---[ 633]---> BDD-cost:  137
c ---[ 632]---> BDD-cost:  156
c ---[ 631]---> BDD-cost:  103
c ---[ 630]---> BDD-cost:  110
c ---[ 629]---> BDD-cost:  156
c ---[ 628]---> BDD-cost:  110
c ---[ 627]---> BDD-cost:  156
c ---[ 626]---> BDD-cost:  154
c ---[ 625]---> BDD-cost:  156
c ---[ 624]---> BDD-cost:  154
c ---[ 623]---> BDD-cost:  156
c ---[ 622]---> BDD-cost:  153
c ---[ 621]---> BDD-cost:  156
c ---[ 620]---> BDD-cost:  152
c ---[ 619]---> BDD-cost:  153
c ---[ 618]---> BDD-cost:  156
c ---[ 617]---> BDD-cost:   99
c ---[ 616]---> BDD-cost:  156
c ---[ 615]---> BDD-cost:   99
c ---[ 614]---> BDD-cost:  156
c ---[ 613]---> BDD-cost:  104
c ---[ 612]---> BDD-cost:  156
c ---[ 611]---> BDD-cost:  104
c ---[ 610]---> BDD-cost:  156
c ---[ 609]---> BDD-cost:  103
c ---[ 608]---> BDD-cost:   87
c ---[ 607]---> BDD-cost:  156
c ---[ 606]---> BDD-cost:   87
c ---[ 605]---> BDD-cost:  156
c ---[ 604]---> BDD-cost:   88
c ---[ 603]---> BDD-cost:  156
c ---[ 602]---> BDD-cost:   88
c ---[ 601]---> BDD-cost:  156
c ---[ 600]---> BDD-cost:  155
c ---[ 599]---> BDD-cost:  156
c ---[ 598]---> BDD-cost:   81
c ---[ 597]---> BDD-cost:  155
c ---[ 596]---> BDD-cost:  156
c ---[ 595]---> BDD-cost:  148
c ---[ 594]---> BDD-cost:  156
c ---[ 593]---> BDD-cost:  148
c ---[ 592]---> BDD-cost:  156
c ---[ 591]---> BDD-cost:  152
c ---[ 590]---> BDD-cost:  156
c ---[ 589]---> BDD-cost:  152
c ---[ 588]---> BDD-cost:  156
c ---[ 587]---> BDD-cost:  103
c ---[ 586]---> BDD-cost:  105
c ---[ 585]---> BDD-cost:  156
c ---[ 584]---> BDD-cost:  105
c ---[ 583]---> BDD-cost:  156
c ---[ 582]---> BDD-cost:  107
c ---[ 581]---> BDD-cost:  156
c ---[ 580]---> BDD-cost:  107
c ---[ 579]---> BDD-cost:  156
c ---[ 578]---> BDD-cost:  144
c ---[ 577]---> BDD-cost:  156
c ---[ 576]---> BDD-cost:   81
c ---[ 575]---> BDD-cost:  144
c ---[ 574]---> BDD-cost:  156
c ---[ 573]---> BDD-cost:  134
c ---[ 572]---> BDD-cost:  156
c ---[ 571]---> BDD-cost:  134
c ---[ 570]---> BDD-cost:  156
c ---[ 569]---> BDD-cost:  103
c ---[ 568]---> BDD-cost:  156
c ---[ 567]---> BDD-cost:  103
c ---[ 566]---> BDD-cost:  144
c ---[ 565]---> BDD-cost:  103
c ---[ 564]---> BDD-cost:  134
c ---[ 563]---> BDD-cost:  144
c ---[ 562]---> BDD-cost:  134
c ---[ 561]---> BDD-cost:  144
c ---[ 560]---> BDD-cost:  143
c ---[ 559]---> BDD-cost:  144
c ---[ 558]---> BDD-cost:  143
c ---[ 557]---> BDD-cost:  144
c ---[ 556]---> BDD-cost:  147
c ---[ 555]---> BDD-cost:  144
c ---[ 554]---> BDD-cost:  103
c ---[ 553]---> BDD-cost:   85
c ---[ 552]---> BDD-cost:  147
c ---[ 551]---> BDD-cost:  144
c ---[ 550]---> BDD-cost:  103
c ---[ 549]---> BDD-cost:  144
c ---[ 548]---> BDD-cost:  103
c ---[ 547]---> BDD-cost:  144
c ---[ 546]---> BDD-cost:   99
c ---[ 545]---> BDD-cost:  144
c ---[ 544]---> BDD-cost:   99
c ---[ 543]---> BDD-cost:  144
c ---[ 542]---> BDD-cost:  103
c ---[ 541]---> BDD-cost:   99
c ---[ 540]---> BDD-cost:  144
c ---[ 539]---> BDD-cost:   99
c ---[ 538]---> BDD-cost:  144
c ---[ 537]---> BDD-cost:  152
c ---[ 536]---> BDD-cost:  144
c ---[ 535]---> BDD-cost:  152
c ---[ 534]---> BDD-cost:  144
c ---[ 533]---> BDD-cost:   81
c ---[ 532]---> BDD-cost:  144
c ---[ 531]---> BDD-cost:   85
c ---[ 530]---> BDD-cost:   81
c ---[ 529]---> BDD-cost:  144
c ---[ 528]---> BDD-cost:   85
c ---[ 527]---> BDD-cost:  144
c ---[ 526]---> BDD-cost:   85
c ---[ 525]---> BDD-cost:  144
c ---[ 524]---> BDD-cost:  148
c ---[ 523]---> BDD-cost:  144
c ---[ 522]---> BDD-cost:  148
c ---[ 521]---> BDD-cost:  144
c ---[ 520]---> BDD-cost:  103
c ---[ 519]---> BDD-cost:  146
c ---[ 518]---> BDD-cost:  144
c ---[ 517]---> BDD-cost:  146
c ---[ 516]---> BDD-cost:  144
c ---[ 515]---> BDD-cost:  101
c ---[ 514]---> BDD-cost:  144
c ---[ 513]---> BDD-cost:  101
c ---[ 512]---> BDD-cost:  144
c ---[ 511]---> BDD-cost:  137
c ---[ 510]---> BDD-cost:  144
c ---[ 509]---> BDD-cost:  148
c ---[ 508]---> BDD-cost:  137
c ---[ 507]---> BDD-cost:  144
c ---[ 506]---> BDD-cost:  110
c ---[ 505]---> BDD-cost:  144
c ---[ 504]---> BDD-cost:  110
c ---[ 503]---> BDD-cost:  144
c ---[ 502]---> BDD-cost:  154
c ---[ 501]---> BDD-cost:  144
c ---[ 500]---> BDD-cost:  154
c ---[ 499]---> BDD-cost:  144
c ---[ 498]---> BDD-cost:  103
c ---[ 497]---> BDD-cost:  153
c ---[ 496]---> BDD-cost:  144
c ---[ 495]---> BDD-cost:  153
c ---[ 494]---> BDD-cost:  144
c ---[ 493]---> BDD-cost:   99
c ---[ 492]---> BDD-cost:  144
c ---[ 491]---> BDD-cost:   99
c ---[ 490]---> BDD-cost:  144
c ---[ 489]---> BDD-cost:  104
c ---[ 488]---> BDD-cost:  144
c ---[ 487]---> BDD-cost:  148
c ---[ 486]---> BDD-cost:  104
c ---[ 485]---> BDD-cost:  144
c ---[ 484]---> BDD-cost:   87
c ---[ 483]---> BDD-cost:  144
c ---[ 482]---> BDD-cost:   87
c ---[ 481]---> BDD-cost:  144
c ---[ 480]---> BDD-cost:   88
c ---[ 479]---> BDD-cost:  144
c ---[ 478]---> BDD-cost:   88
c ---[ 477]---> BDD-cost:  144
c ---[ 476]---> BDD-cost:  103
c ---[ 475]---> BDD-cost:  155
c ---[ 474]---> BDD-cost:  144
c ---[ 473]---> BDD-cost:  155
c ---[ 472]---> BDD-cost:  144
c ---[ 471]---> BDD-cost:  148
c ---[ 470]---> BDD-cost:  144
c ---[ 469]---> BDD-cost:  148
c ---[ 468]---> BDD-cost:  144
c ---[ 467]---> BDD-cost:  152
c ---[ 466]---> BDD-cost:  144
c ---[ 465]---> BDD-cost:  146
c ---[ 464]---> BDD-cost:  152
c ---[ 463]---> BDD-cost:  144
c ---[ 462]---> BDD-cost:  105
c ---[ 461]---> BDD-cost:  144
c ---[ 460]---> BDD-cost:  105
c ---[ 459]---> BDD-cost:  144
c ---[ 458]---> BDD-cost:  107
c ---[ 457]---> BDD-cost:  144
c ---[ 456]---> BDD-cost:  107
c ---[ 455]---> BDD-cost:  144
c ---[ 454]---> BDD-cost:  103
c ---[ 453]---> BDD-cost:  144
c ---[ 452]---> BDD-cost:  144
c ---[ 451]---> BDD-cost:  144
c ---[ 450]---> BDD-cost:  144
c ---[ 449]---> BDD-cost:  134
c ---[ 448]---> BDD-cost:  144
c ---[ 447]---> BDD-cost:  134
c ---[ 446]---> BDD-cost:  144
c ---[ 445]---> BDD-cost:  103
c ---[ 444]---> BDD-cost:  144
c ---[ 443]---> BDD-cost:   83
c ---[ 442]---> BDD-cost:  146
c ---[ 441]---> BDD-cost:  103
c ---[ 440]---> BDD-cost:  134
c ---[ 439]---> BDD-cost:  143
c ---[ 438]---> BDD-cost:  134
c ---[ 437]---> BDD-cost:  143
c ---[ 436]---> BDD-cost:  134
c ---[ 435]---> BDD-cost:  147
c ---[ 434]---> BDD-cost:  134
c ---[ 433]---> BDD-cost:  147
c ---[ 432]---> BDD-cost:  134
c ---[ 431]---> BDD-cost:  103
c ---[ 430]---> BDD-cost:  103
c ---[ 429]---> BDD-cost:  134
c ---[ 428]---> BDD-cost:  103
c ---[ 427]---> BDD-cost:  134
c ---[ 426]---> BDD-cost:   99
c ---[ 425]---> BDD-cost:  134
c ---[ 424]---> BDD-cost:   99
c ---[ 423]---> BDD-cost:  134
c ---[ 422]---> BDD-cost:   99
c ---[ 421]---> BDD-cost:  134
c ---[ 420]---> BDD-cost:  101
c ---[ 419]---> BDD-cost:   99
c ---[ 418]---> BDD-cost:  134
c ---[ 417]---> BDD-cost:  152
c ---[ 416]---> BDD-cost:  134
c ---[ 415]---> BDD-cost:  152
c ---[ 414]---> BDD-cost:  134
c ---[ 413]---> BDD-cost:   81
c ---[ 412]---> BDD-cost:  134
c ---[ 411]---> BDD-cost:   81
c ---[ 410]---> BDD-cost:  134
c ---[ 409]---> BDD-cost:  103
c ---[ 408]---> BDD-cost:   85
c ---[ 407]---> BDD-cost:  134
c ---[ 406]---> BDD-cost:   85
c ---[ 405]---> BDD-cost:  134
c ---[ 404]---> BDD-cost:  148
c ---[ 403]---> BDD-cost:  134
c ---[ 402]---> BDD-cost:  148
c ---[ 401]---> BDD-cost:  134
c ---[ 400]---> BDD-cost:  146
c ---[ 399]---> BDD-cost:  134
c ---[ 398]---> BDD-cost:  101
c ---[ 397]---> BDD-cost:  146
c ---[ 396]---> BDD-cost:  134
c ---[ 395]---> BDD-cost:  101
c ---[ 394]---> BDD-cost:  134
c ---[ 393]---> BDD-cost:  101
c ---[ 392]---> BDD-cost:  134
c ---[ 391]---> BDD-cost:  137
c ---[ 390]---> BDD-cost:  134
c ---[ 389]---> BDD-cost:  137
c ---[ 388]---> BDD-cost:  134
c ---[ 387]---> BDD-cost:  103
c ---[ 386]---> BDD-cost:  110
c ---[ 385]---> BDD-cost:  134
c ---[ 384]---> BDD-cost:  110
c ---[ 383]---> BDD-cost:  134
c ---[ 382]---> BDD-cost:  154
c ---[ 381]---> BDD-cost:  134
c ---[ 380]---> BDD-cost:  154
c ---[ 379]---> BDD-cost:  134
c ---[ 378]---> BDD-cost:  153
c ---[ 377]---> BDD-cost:  134
c ---[ 376]---> BDD-cost:  137
c ---[ 375]---> BDD-cost:  153
c ---[ 374]---> BDD-cost:  134
c ---[ 373]---> BDD-cost:   99
c ---[ 372]---> BDD-cost:  134
c ---[ 371]---> BDD-cost:   99
c ---[ 370]---> BDD-cost:  134
c ---[ 369]---> BDD-cost:  104
c ---[ 368]---> BDD-cost:  134
c ---[ 367]---> BDD-cost:  104
c ---[ 366]---> BDD-cost:  134
c ---[ 365]---> BDD-cost:  103
c ---[ 364]---> BDD-cost:   87
c ---[ 363]---> BDD-cost:  134
c ---[ 362]---> BDD-cost:   87
c ---[ 361]---> BDD-cost:  134
c ---[ 360]---> BDD-cost:   88
c ---[ 359]---> BDD-cost:  134
c ---[ 358]---> BDD-cost:   88
c ---[ 357]---> BDD-cost:  134
c ---[ 356]---> BDD-cost:  155
c ---[ 355]---> BDD-cost:  134
c ---[ 354]---> BDD-cost:  137
c ---[ 353]---> BDD-cost:  155
c ---[ 352]---> BDD-cost:  134
c ---[ 351]---> BDD-cost:  148
c ---[ 350]---> BDD-cost:  134
c ---[ 349]---> BDD-cost:  148
c ---[ 348]---> BDD-cost:  134
c ---[ 347]---> BDD-cost:  152
c ---[ 346]---> BDD-cost:  134
c ---[ 345]---> BDD-cost:  152
c ---[ 344]---> BDD-cost:  134
c ---[ 343]---> BDD-cost:  103
c ---[ 342]---> BDD-cost:  105
c ---[ 341]---> BDD-cost:  134
c ---[ 340]---> BDD-cost:  105
c ---[ 339]---> BDD-cost:  134
c ---[ 338]---> BDD-cost:  107
c ---[ 337]---> BDD-cost:  134
c ---[ 336]---> BDD-cost:  107
c ---[ 335]---> BDD-cost:  134
c ---[ 334]---> BDD-cost:  144
c ---[ 333]---> BDD-cost:  134
c ---[ 332]---> BDD-cost:  103
c ---[ 331]---> BDD-cost:  110
c ---[ 330]---> BDD-cost:  144
c ---[ 329]---> BDD-cost:  134
c ---[ 328]---> BDD-cost:  134
c ---[ 327]---> BDD-cost:  134
c ---[ 326]---> BDD-cost:  134
c ---[ 325]---> BDD-cost:  134
c ---[ 324]---> BDD-cost:  103
c ---[ 323]---> BDD-cost:  134
c ---[ 322]---> BDD-cost:  103
c ---[ 321]---> BDD-cost:  143
c ---[ 320]---> BDD-cost:  103
c ---[ 319]---> BDD-cost:  147
c ---[ 318]---> BDD-cost:  143
c ---[ 317]---> BDD-cost:  147
c ---[ 316]---> BDD-cost:  143
c ---[ 315]---> BDD-cost:  103
c ---[ 314]---> BDD-cost:  143
c ---[ 313]---> BDD-cost:  103
c ---[ 312]---> BDD-cost:  143
c ---[ 311]---> BDD-cost:   99
c ---[ 310]---> BDD-cost:  143
c ---[ 309]---> BDD-cost:  110
c ---[ 308]---> BDD-cost:   99
c ---[ 307]---> BDD-cost:  143
c ---[ 306]---> BDD-cost:   99
c ---[ 305]---> BDD-cost:  143
c ---[ 304]---> BDD-cost:   99
c ---[ 303]---> BDD-cost:  143
c ---[ 302]---> BDD-cost:  152
c ---[ 301]---> BDD-cost:  143
c ---[ 300]---> BDD-cost:  152
c ---[ 299]---> BDD-cost:  143
c ---[ 298]---> BDD-cost:  103
c ---[ 297]---> BDD-cost:   81
c ---[ 296]---> BDD-cost:  143
c ---[ 295]---> BDD-cost:   81
c ---[ 294]---> BDD-cost:  143
c ---[ 293]---> BDD-cost:   85
c ---[ 292]---> BDD-cost:  143
c ---[ 291]---> BDD-cost:   85
c ---[ 290]---> BDD-cost:  143
c ---[ 289]---> BDD-cost:  148
c ---[ 288]---> BDD-cost:  143
c ---[ 287]---> BDD-cost:  154
c ---[ 286]---> BDD-cost:  148
c ---[ 285]---> BDD-cost:  143
c ---[ 284]---> BDD-cost:  146
c ---[ 283]---> BDD-cost:  143
c ---[ 282]---> BDD-cost:  146
c ---[ 281]---> BDD-cost:  143
c ---[ 280]---> BDD-cost:  101
c ---[ 279]---> BDD-cost:  143
c ---[ 278]---> BDD-cost:  101
c ---[ 277]---> BDD-cost:  143
c ---[ 276]---> BDD-cost:  103
c ---[ 275]---> BDD-cost:  137
c ---[ 274]---> BDD-cost:  143
c ---[ 273]---> BDD-cost:  137
c ---[ 272]---> BDD-cost:  143
c ---[ 271]---> BDD-cost:  110
c ---[ 270]---> BDD-cost:  143
c ---[ 269]---> BDD-cost:  110
c ---[ 268]---> BDD-cost:  143
c ---[ 267]---> BDD-cost:  154
c ---[ 266]---> BDD-cost:  143
c ---[ 265]---> BDD-cost:  154
c ---[ 264]---> BDD-cost:  154
c ---[ 263]---> BDD-cost:  143
c ---[ 262]---> BDD-cost:  153
c ---[ 261]---> BDD-cost:  143
c ---[ 260]---> BDD-cost:  153
c ---[ 259]---> BDD-cost:  143
c ---[ 258]---> BDD-cost:   99
c ---[ 257]---> BDD-cost:  143
c ---[ 256]---> BDD-cost:   99
c ---[ 255]---> BDD-cost:  143
c ---[ 254]---> BDD-cost:  103
c ---[ 253]---> BDD-cost:  104
c ---[ 252]---> BDD-cost:  143
c ---[ 251]---> BDD-cost:  104
c ---[ 250]---> BDD-cost:  143
c ---[ 249]---> BDD-cost:   87
c ---[ 248]---> BDD-cost:  143
c ---[ 247]---> BDD-cost:   87
c ---[ 246]---> BDD-cost:  143
c ---[ 245]---> BDD-cost:   88
c ---[ 244]---> BDD-cost:  143
c ---[ 243]---> BDD-cost:  153
c ---[ 242]---> BDD-cost:   88
c ---[ 241]---> BDD-cost:  143
c ---[ 240]---> BDD-cost:  155
c ---[ 239]---> BDD-cost:  143
c ---[ 238]---> BDD-cost:  155
c ---[ 237]---> BDD-cost:  143
c ---[ 236]---> BDD-cost:  148
c ---[ 235]---> BDD-cost:  143
c ---[ 234]---> BDD-cost:  148
c ---[ 233]---> BDD-cost:  143
c ---[ 232]---> BDD-cost:  103
c ---[ 231]---> BDD-cost:  152
c ---[ 230]---> BDD-cost:  143
c ---[ 229]---> BDD-cost:  152
c ---[ 228]---> BDD-cost:  143
c ---[ 227]---> BDD-cost:  105
c ---[ 226]---> BDD-cost:  143
c ---[ 225]---> BDD-cost:  105
c ---[ 224]---> BDD-cost:  143
c ---[ 223]---> BDD-cost:  107
c ---[ 222]---> BDD-cost:  143
c ---[ 221]---> BDD-cost:   83
c ---[ 220]---> BDD-cost:  153
c ---[ 219]---> BDD-cost:  107
c ---[ 218]---> BDD-cost:  143
c ---[ 217]---> BDD-cost:  144
c ---[ 216]---> BDD-cost:  143
c ---[ 215]---> BDD-cost:  144
c ---[ 214]---> BDD-cost:  143
c ---[ 213]---> BDD-cost:  134
c ---[ 212]---> BDD-cost:  143
c ---[ 211]---> BDD-cost:  134
c ---[ 210]---> BDD-cost:  143
c ---[ 209]---> BDD-cost:  103
c ---[ 208]---> BDD-cost:  103
c ---[ 207]---> BDD-cost:  143
c ---[ 206]---> BDD-cost:  103
c ---[ 205]---> BDD-cost:  147
c ---[ 204]---> BDD-cost:  103
c ---[ 203]---> BDD-cost:  147
c ---[ 202]---> BDD-cost:  103
c ---[ 201]---> BDD-cost:  147
c ---[ 200]---> BDD-cost:   99
c ---[ 199]---> BDD-cost:  147
c ---[ 198]---> BDD-cost:   99
c ---[ 197]---> BDD-cost:   99
c ---[ 196]---> BDD-cost:  147
c ---[ 195]---> BDD-cost:   99
c ---[ 194]---> BDD-cost:  147
c ---[ 193]---> BDD-cost:   99
c ---[ 192]---> BDD-cost:  147
c ---[ 191]---> BDD-cost:  152
c ---[ 190]---> BDD-cost:  147
c ---[ 189]---> BDD-cost:  152
c ---[ 188]---> BDD-cost:  147
c ---[ 187]---> BDD-cost:  103
c ---[ 186]---> BDD-cost:   81
c ---[ 185]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:   81
c ---[ 183]---> BDD-cost:  147
c ---[ 182]---> BDD-cost:   85
c ---[ 181]---> BDD-cost:  147
c ---[ 180]---> BDD-cost:   85
c ---[ 179]---> BDD-cost:  147
c ---[ 178]---> BDD-cost:  148
c ---[ 177]---> BDD-cost:  147
c ---[ 176]---> BDD-cost:   99
c ---[ 175]---> BDD-cost:  148
c ---[ 174]---> BDD-cost:  147
c ---[ 173]---> BDD-cost:  146
c ---[ 172]---> BDD-cost:  147
c ---[ 171]---> BDD-cost:  146
c ---[ 170]---> BDD-cost:  147
c ---[ 169]---> BDD-cost:  101
c ---[ 168]---> BDD-cost:  147
c ---[ 167]---> BDD-cost:  101
c ---[ 166]---> BDD-cost:  147
c ---[ 165]---> BDD-cost:  103
c ---[ 164]---> BDD-cost:  137
c ---[ 163]---> BDD-cost:  147
c ---[ 162]---> BDD-cost:  137
c ---[ 161]---> BDD-cost:  147
c ---[ 160]---> BDD-cost:  110
c ---[ 159]---> BDD-cost:  147
c ---[ 158]---> BDD-cost:  110
c ---[ 157]---> BDD-cost:  147
c ---[ 156]---> BDD-cost:  154
c ---[ 155]---> BDD-cost:  147
c ---[ 154]---> BDD-cost:  104
c ---[ 153]---> BDD-cost:  154
c ---[ 152]---> BDD-cost:  147
c ---[ 151]---> BDD-cost:  153
c ---[ 150]---> BDD-cost:  147
c ---[ 149]---> BDD-cost:  153
c ---[ 148]---> BDD-cost:  147
c ---[ 147]---> BDD-cost:   99
c ---[ 146]---> BDD-cost:  147
c ---[ 145]---> BDD-cost:   99
c ---[ 144]---> BDD-cost:  147
c ---[ 143]---> BDD-cost:  103
c ---[ 142]---> BDD-cost:  104
c ---[ 141]---> BDD-cost:  147
c ---[ 140]---> BDD-cost:  104
c ---[ 139]---> BDD-cost:  147
c ---[ 138]---> BDD-cost:   87
c ---[ 137]---> BDD-cost:  147
c ---[ 136]---> BDD-cost:   87
c ---[ 135]---> BDD-cost:  147
c ---[ 134]---> BDD-cost:   88
c ---[ 133]---> BDD-cost:  147
c ---[ 132]---> BDD-cost:  104
c ---[ 131]---> BDD-cost:   88
c ---[ 130]---> BDD-cost:  147
c ---[ 129]---> BDD-cost:  155
c ---[ 128]---> BDD-cost:  147
c ---[ 127]---> BDD-cost:  155
c ---[ 126]---> BDD-cost:  147
c ---[ 125]---> BDD-cost:  148
c ---[ 124]---> BDD-cost:  147
c ---[ 123]---> BDD-cost:  148
c ---[ 122]---> BDD-cost:  147
c ---[ 121]---> BDD-cost:  103
c ---[ 120]---> BDD-cost:  152
c ---[ 119]---> BDD-cost:  147
c ---[ 118]---> BDD-cost:  152
c ---[ 117]---> BDD-cost:  147
c ---[ 116]---> BDD-cost:  105
c ---[ 115]---> BDD-cost:  147
c ---[ 114]---> BDD-cost:  105
c ---[ 113]---> BDD-cost:  147
c ---[ 112]---> BDD-cost:  107
c ---[ 111]---> BDD-cost:  147
c ---[ 110]---> BDD-cost:  103
c ---[ 109]---> BDD-cost:   87
c ---[ 108]---> BDD-cost:  107
c ---[ 107]---> BDD-cost:  147
c ---[ 106]---> BDD-cost:  144
c ---[ 105]---> BDD-cost:  147
c ---[ 104]---> BDD-cost:  144
c ---[ 103]---> BDD-cost:  147
c ---[ 102]---> BDD-cost:  134
c ---[ 101]---> BDD-cost:  147
c ---[ 100]---> BDD-cost:  134
c ---[  99]---> BDD-cost:  147
c ---[  98]---> BDD-cost:  103
c ---[  97]---> BDD-cost:  103
c ---[  96]---> BDD-cost:  147
c ---[  95]---> BDD-cost:  103
c ---[  94]---> BDD-cost:  103
c ---[  93]---> BDD-cost:   99
c ---[  92]---> BDD-cost:  103
c ---[  91]---> BDD-cost:   99
c ---[  90]---> BDD-cost:  103
c ---[  89]---> BDD-cost:   99
c ---[  88]---> BDD-cost:  103
c ---[  87]---> BDD-cost:   87
c ---[  86]---> BDD-cost:   99
c ---[  85]---> BDD-cost:  103
c ---[  84]---> BDD-cost:  152
c ---[  83]---> BDD-cost:  103
c ---[  82]---> BDD-cost:  152
c ---[  81]---> BDD-cost:  103
c ---[  80]---> BDD-cost:   81
c ---[  79]---> BDD-cost:  103
c ---[  78]---> BDD-cost:   81
c ---[  77]---> BDD-cost:  103
c ---[  76]---> BDD-cost:  103
c ---[  75]---> BDD-cost:   85
c ---[  74]---> BDD-cost:  103
c ---[  73]---> BDD-cost:   85
c ---[  72]---> BDD-cost:  103
c ---[  71]---> BDD-cost:  148
c ---[  70]---> BDD-cost:  103
c ---[  69]---> BDD-cost:  148
c ---[  68]---> BDD-cost:  103
c ---[  67]---> BDD-cost:  146
c ---[  66]---> BDD-cost:  103
c ---[  65]---> BDD-cost:   88
c ---[  64]---> BDD-cost:  146
c ---[  63]---> BDD-cost:  103
c ---[  62]---> BDD-cost:  101
c ---[  61]---> BDD-cost:  103
c ---[  60]---> BDD-cost:  101
c ---[  59]---> BDD-cost:  103
c ---[  58]---> BDD-cost:  137
c ---[  57]---> BDD-cost:  103
c ---[  56]---> BDD-cost:  137
c ---[  55]---> BDD-cost:  103
c ---[  54]---> BDD-cost:  103
c ---[  53]---> BDD-cost:  110
c ---[  52]---> BDD-cost:  103
c ---[  51]---> BDD-cost:  110
c ---[  50]---> BDD-cost:  103
c ---[  49]---> BDD-cost:  154
c ---[  48]---> BDD-cost:  103
c ---[  47]---> BDD-cost:  154
c ---[  46]---> BDD-cost:  103
c ---[  45]---> BDD-cost:  153
c ---[  44]---> BDD-cost:  103
c ---[  43]---> BDD-cost:   88
c ---[  42]---> BDD-cost:  153
c ---[  41]---> BDD-cost:  103
c ---[  40]---> BDD-cost:   99
c ---[  39]---> BDD-cost:  103
c ---[  38]---> BDD-cost:   99
c ---[  37]---> BDD-cost:  103
c ---[  36]---> BDD-cost:  104
c ---[  35]---> BDD-cost:  103
c ---[  34]---> BDD-cost:  104
c ---[  33]---> BDD-cost:  103
c ---[  32]---> BDD-cost:  103
c ---[  31]---> BDD-cost:   87
c ---[  30]---> BDD-cost:  103
c ---[  29]---> BDD-cost:   87
c ---[  28]---> BDD-cost:  103
c ---[  27]---> BDD-cost:   88
c ---[  26]---> BDD-cost:  103
c ---[  25]---> BDD-cost:   88
c ---[  24]---> BDD-cost:  103
c ---[  23]---> BDD-cost:  155
c ---[  22]---> BDD-cost:  103
c ---[  21]---> BDD-cost:  155
c ---[  20]---> BDD-cost:  155
c ---[  19]---> BDD-cost:  103
c ---[  18]---> BDD-cost:  148
c ---[  17]---> BDD-cost:  103
c ---[  16]---> BDD-cost:  148
c ---[  15]---> BDD-cost:  103
c ---[  14]---> BDD-cost:  152
c ---[  13]---> BDD-cost:  103
c ---[  12]---> BDD-cost:  152
c ---[  11]---> BDD-cost:  103
c ---[  10]---> BDD-cost:  103
c ---[   9]---> BDD-cost:  105
c ---[   8]---> BDD-cost:  103
c ---[   7]---> BDD-cost:  105
c ---[   6]---> BDD-cost:  103
c ---[   5]---> BDD-cost:  107
c ---[   4]---> BDD-cost:  103
c ---[   3]---> BDD-cost:  107
c ---[   2]---> BDD-cost:  103
c ---[   1]---> BDD-cost:  144
c ---[   0]---> BDD-cost:  103
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  480116  1347916 |  160038       0        0     nan |  0.000 % |
c |       100 |  480116  1347916 |  176041     100      392     3.9 |  0.998 % |
c |       250 |  480116  1347916 |  193645     250     1129     4.5 |  0.998 % |
c |       475 |  480116  1347916 |  213010     475     2220     4.7 |  0.998 % |
c |       813 |  480116  1347916 |  234311     813     3781     4.7 |  0.998 % |
c |      1319 |  480116  1347916 |  257742    1319     8060     6.1 |  0.998 % |
c |      2078 |  480116  1347916 |  283517    2078    19467     9.4 |  0.998 % |
c |      3217 |  480116  1347916 |  311868    3217    36992    11.5 |  0.998 % |
c ==============================================================================
c [1mFound solution: 983036[0m
c ---[   0]---> Sorter-cost:   88     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3989 |  480251  1348247 |  160083    3989    53836    13.5 |  0.998 % |
c |      4090 |  480251  1348247 |  176091    4090    55844    13.7 |  0.998 % |
c ==============================================================================
c [1mFound solution: 644026[0m
c ---[   0]---> Sorter-cost:  103     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4144 |  480444  1348704 |  160148    4144    57052    13.8 |  0.998 % |
c ==============================================================================
c [1mFound solution: 622556[0m
c ---[   0]---> Sorter-cost:   80     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4197 |  480580  1349031 |  160193    4197    58048    13.8 |  0.998 % |
c ==============================================================================
c [1mFound solution: 622124[0m
c ---[   0]---> Sorter-cost:   86     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4260 |  480737  1349403 |  160245    4260    59237    13.9 |  0.998 % |
c ==============================================================================
c [1mFound solution: 619508[0m
c ---[   0]---> Sorter-cost:   83     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4321 |  480880  1349744 |  160293    4321    60494    14.0 |  0.998 % |
c ==============================================================================
c [1mFound solution: 617928[0m
c ---[   0]---> Sorter-cost:   85     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4369 |  481033  1350105 |  160344    4369    61286    14.0 |  0.998 % |
c |      4469 |  481033  1350105 |  176378    4469    63348    14.2 |  0.998 % |
c ==============================================================================
c [1mFound solution: 590298[0m
c ---[   0]---> Sorter-cost:   87     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4569 |  481191  1350476 |  160397    4569    65669    14.4 |  0.998 % |
c |      4669 |  481191  1350476 |  176436    4669    67705    14.5 |  0.999 % |
c ==============================================================================
c [1mFound solution: 582068[0m
c ---[   0]---> Sorter-cost:   77     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4774 |  481329  1350802 |  160443    4774    69904    14.6 |  0.999 % |
c |      4874 |  481329  1350802 |  176487    4874    71757    14.7 |  0.999 % |
c ==============================================================================
c [1mFound solution: 577980[0m
c ---[   0]---> Sorter-cost:   79     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4998 |  481469  1351131 |  160489    4998    75285    15.1 |  0.999 % |
c ==============================================================================
c [1mFound solution: 563546[0m
c ---[   0]---> Sorter-cost:   71     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5078 |  481597  1351431 |  160532    5078    76630    15.1 |  0.999 % |
c |      5178 |  481597  1351431 |  176585    5178    78375    15.1 |  0.999 % |
c ==============================================================================
c [1mFound solution: 539508[0m
c ---[   0]---> Sorter-cost:   68     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5291 |  481716  1351712 |  160572    5291    80785    15.3 |  0.999 % |
c |      5391 |  481716  1351712 |  176629    5391    83098    15.4 |  0.999 % |
c ==============================================================================
c [1mFound solution: 524780[0m
c ---[   0]---> Sorter-cost:   81     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5439 |  481858  1352044 |  160619    5439    83899    15.4 |  0.999 % |
c |      5539 |  481858  1352044 |  176680    5539    85800    15.5 |  0.999 % |
c ==============================================================================
c [1mFound solution: 524732[0m
c ---[   0]---> Sorter-cost:   48     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5681 |  481942  1352239 |  160647    5681    89541    15.8 |  0.999 % |
c |      5781 |  481942  1352239 |  176711    5781    92797    16.1 |  1.000 % |
c ==============================================================================
c [1mFound solution: 524472[0m
c ---[   0]---> Sorter-cost:   95     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5830 |  482114  1352639 |  160704    5830    93891    16.1 |  1.000 % |
c |      5931 |  482114  1352639 |  176774    5931    96488    16.3 |  1.000 % |
c |      6082 |  482114  1352639 |  194451    6082   100732    16.6 |  1.000 % |
c ==============================================================================
c [1mFound solution: 524468[0m
c ---[   0]---> Sorter-cost:   76     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6178 |  482251  1352957 |  160750    6178   102514    16.6 |  1.000 % |
c |      6278 |  482251  1352957 |  176825    6278   104847    16.7 |  1.000 % |
c ==============================================================================
c [1mFound solution: 294364[0m
c ---[   0]---> Sorter-cost:   87     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6372 |  473034  1315431 |  157678    6190   103683    16.8 |  1.000 % |
c |      6472 |  473034  1315431 |  173445    6290   105026    16.7 |  1.610 % |
c ==============================================================================
c [1mFound solution: 294228[0m
c ---[   0]---> Sorter-cost:   84     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6577 |  473186  1315790 |  157728    6395   106795    16.7 |  1.610 % |
c |      6677 |  473186  1315790 |  173500    6495   108595    16.7 |  1.610 % |
c ==============================================================================
c [1mFound solution: 289594[0m
c ---[   0]---> Sorter-cost:   96     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6745 |  473364  1316209 |  157788    6563   109619    16.7 |  1.610 % |
c ==============================================================================
c [1mFound solution: 281478[0m
c ---[   0]---> Sorter-cost:   97     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6789 |  473544  1316630 |  157848    6607   110378    16.7 |  1.610 % |
c |      6889 |  473544  1316630 |  173632    6707   112458    16.8 |  1.609 % |
c |      7039 |  473544  1316630 |  190996    6857   115647    16.9 |  1.609 % |
c ==============================================================================
c [1mFound solution: 278364[0m
c ---[   0]---> Sorter-cost:   60     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7189 |  473647  1316876 |  157882    7007   118065    16.8 |  1.609 % |
c ==============================================================================
c [1mFound solution: 277368[0m
c ---[   0]---> Sorter-cost:   74     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7273 |  473773  1317175 |  157924    7091   119487    16.9 |  1.609 % |
c |      7374 |  473773  1317175 |  173716    7192   121542    16.9 |  1.609 % |
c |      7524 |  473773  1317175 |  191088    7342   125024    17.0 |  1.609 % |
c ==============================================================================
c [1mFound solution: 277340[0m
c ---[   0]---> Sorter-cost:   46     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7667 |  473852  1317363 |  157950    7485   127930    17.1 |  1.609 % |
c |      7767 |  473852  1317363 |  173745    7585   129883    17.1 |  1.610 % |
c |      7918 |  473852  1317363 |  191119    7736   133181    17.2 |  1.610 % |
c ==============================================================================
c [1mFound solution: 277338[0m
c ---[   0]---> Sorter-cost:   72     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8138 |  473979  1317664 |  157993    7956   138864    17.5 |  1.610 % |
c |      8238 |  473979  1317664 |  173792    8056   141277    17.5 |  1.610 % |
c ==============================================================================
c [1mFound solution: 277336[0m
c ---[   0]---> Sorter-cost:   72     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8369 |  474106  1317964 |  158035    8187   144331    17.6 |  1.610 % |
c |      8469 |  474106  1317964 |  173838    8287   146470    17.7 |  1.610 % |
c ==============================================================================
c [1mFound solution: 277274[0m
c ---[   0]---> Sorter-cost:   68     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8560 |  474224  1318242 |  158074    8378   148333    17.7 |  1.610 % |
c |      8660 |  474224  1318242 |  173881    8478   150506    17.8 |  1.610 % |
c |      8810 |  474224  1318242 |  191269    8628   153327    17.8 |  1.610 % |
c ==============================================================================
c [1mFound solution: 277254[0m
c ---[   0]---> Sorter-cost:   61     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8904 |  474329  1318490 |  158109    8722   155165    17.8 |  1.610 % |
c |      9004 |  474329  1318490 |  173919    8822   157347    17.8 |  1.610 % |
c |      9154 |  474329  1318490 |  191311    8972   161622    18.0 |  1.610 % |
c |      9379 |  474329  1318490 |  210443    9197   167788    18.2 |  1.610 % |
c ==============================================================================
c [1mFound solution: 277252[0m
c ---[   0]---> Sorter-cost:   82     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9445 |  474473  1318828 |  158157    9263   169254    18.3 |  1.610 % |
c |      9545 |  474473  1318828 |  173972    9363   170843    18.2 |  1.610 % |
c |      9695 |  474473  1318828 |  191369    9513   173964    18.3 |  1.610 % |
c |      9920 |  474473  1318828 |  210506    9738   178861    18.4 |  1.610 % |
c ==============================================================================
c [1mFound solution: 277250[0m
c ---[   0]---> Sorter-cost:   89     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10076 |  474630  1319196 |  158210    9894   182113    18.4 |  1.610 % |
c |     10176 |  474459  1318721 |  174031    9991   183618    18.4 |  1.621 % |
c |     10329 |  474459  1318721 |  191434   10144   186807    18.4 |  1.621 % |
c ==============================================================================
c [1mFound solution: 277248[0m
c ---[   0]---> Sorter-cost:   53     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10542 |  474550  1318936 |  158183   10357   192343    18.6 |  1.621 % |
c |     10642 |  474550  1318936 |  174001   10457   194438    18.6 |  1.621 % |
c ==============================================================================
c [1mFound solution: 272984[0m
c ---[   0]---> Sorter-cost:   60     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10752 |  474660  1319192 |  158220   10567   196713    18.6 |  1.621 % |
c |     10852 |  474660  1319192 |  174042   10667   198779    18.6 |  1.621 % |
c |     11002 |  474660  1319192 |  191446   10817   201907    18.7 |  1.621 % |
c ==============================================================================
c [1mFound solution: 181326[0m
c ---[   0]---> Sorter-cost:  105     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11202 |  464666  1290293 |  154888   10865   203878    18.8 |  1.621 % |
c |     11303 |  464666  1290293 |  170376   10966   205925    18.8 |  2.217 % |
c |     11453 |  464666  1290293 |  187414   11116   208906    18.8 |  2.217 % |
c |     11678 |  464666  1290293 |  206155   11341   214461    18.9 |  2.217 % |
c |     12015 |  464666  1290293 |  226771   11678   223714    19.2 |  2.217 % |
c |     12522 |  464666  1290293 |  249448   12185   235576    19.3 |  2.217 % |
c ==============================================================================
c [1mFound solution: 180430[0m
c ---[   0]---> Sorter-cost:   62     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13235 |  464777  1290553 |  154925   12898   252427    19.6 |  2.217 % |
c |     13335 |  464777  1290553 |  170417   12998   254098    19.5 |  2.217 % |
c |     13486 |  464777  1290553 |  187459   13149   257999    19.6 |  2.217 % |
c |     13711 |  464777  1290553 |  206205   13374   262921    19.7 |  2.217 % |
c |     14048 |  464777  1290553 |  226825   13711   269866    19.7 |  2.217 % |
c |     14555 |  464777  1290553 |  249508   14218   283333    19.9 |  2.217 % |
c |     15316 |  464777  1290553 |  274459   14979   305340    20.4 |  2.217 % |
c ==============================================================================
c [1mFound solution: 180046[0m
c ---[   0]---> Sorter-cost:   43     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16267 |  464849  1290727 |  154949   15930   332811    20.9 |  2.217 % |
c |     16367 |  464849  1290727 |  170443   16030   335030    20.9 |  2.217 % |
c |     16517 |  464849  1290727 |  187488   16180   338719    20.9 |  2.217 % |
c |     16743 |  464849  1290727 |  206237   16406   343999    21.0 |  2.217 % |
c |     17081 |  464849  1290727 |  226860   16744   352724    21.1 |  2.217 % |
c |     17587 |  464849  1290727 |  249546   17250   365091    21.2 |  2.217 % |
c ==============================================================================
c [1mFound solution: 179790[0m
c ---[   0]---> Sorter-cost:   37     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18325 |  464909  1290872 |  154969   17988   386237    21.5 |  2.217 % |
c |     18425 |  464909  1290872 |  170465   18088   387897    21.4 |  2.217 % |
c |     18575 |  464909  1290872 |  187512   18238   390286    21.4 |  2.217 % |
c |     18801 |  464909  1290872 |  206263   18464   395837    21.4 |  2.217 % |
c |     19139 |  464909  1290872 |  226890   18802   404961    21.5 |  2.217 % |
c |     19645 |  464909  1290872 |  249579   19308   416035    21.5 |  2.217 % |
c ==============================================================================
c [1mFound solution: 179086[0m
c ---[   0]---> Sorter-cost:   57     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19965 |  465008  1291108 |  155002   19628   423244    21.6 |  2.217 % |
c |     20065 |  465008  1291108 |  170502   19728   425575    21.6 |  2.217 % |
c |     20215 |  465008  1291108 |  187552   19878   429558    21.6 |  2.217 % |
c |     20440 |  465008  1291108 |  206307   20103   435238    21.7 |  2.217 % |
c |     20777 |  465008  1291108 |  226938   20440   444103    21.7 |  2.217 % |
c |     21283 |  465008  1291108 |  249632   20946   457871    21.9 |  2.217 % |
c ==============================================================================
c [1mFound solution: 163404[0m
c ---[   0]---> Sorter-cost:   76     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21636 |  465140  1291421 |  155046   21299   466921    21.9 |  2.217 % |
c |     21736 |  465140  1291421 |  170550   21399   468966    21.9 |  2.217 % |
c |     21886 |  465140  1291421 |  187605   21549   472571    21.9 |  2.217 % |
c |     22112 |  465140  1291421 |  206366   21775   477117    21.9 |  2.217 % |
c |     22449 |  465140  1291421 |  227002   22112   488421    22.1 |  2.217 % |
c |     22958 |  465140  1291421 |  249703   22621   501688    22.2 |  2.217 % |
c |     23717 |  465140  1291421 |  274673   23380   527315    22.6 |  2.217 % |
c ==============================================================================
c [1mFound solution: 163150[0m
c ---[   0]---> Sorter-cost:   40     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24301 |  465205  1291578 |  155068   23964   543969    22.7 |  2.217 % |
c |     24401 |  465205  1291578 |  170574   24064   546305    22.7 |  2.217 % |
c |     24551 |  465205  1291578 |  187632   24214   549927    22.7 |  2.217 % |
c |     24776 |  465205  1291578 |  206395   24439   556036    22.8 |  2.217 % |
c |     25114 |  465205  1291578 |  227035   24777   567943    22.9 |  2.217 % |
c |     25620 |  465205  1291578 |  249738   25283   579733    22.9 |  2.217 % |
c ==============================================================================
c [1mFound solution: 163118[0m
c ---[   0]---> Sorter-cost:   62     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25828 |  465312  1291832 |  155104   25491   585199    23.0 |  2.217 % |
c |     25929 |  465312  1291832 |  170614   25592   587925    23.0 |  2.217 % |
c |     26079 |  465312  1291832 |  187675   25742   591692    23.0 |  2.217 % |
c |     26305 |  465312  1291832 |  206443   25968   597204    23.0 |  2.217 % |
c |     26644 |  465312  1291832 |  227087   26307   604406    23.0 |  2.217 % |
c |     27151 |  465312  1291832 |  249796   26814   619340    23.1 |  2.217 % |
c ==============================================================================
c [1mFound solution: 163086[0m
c ---[   0]---> Sorter-cost:   51     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27501 |  465397  1292035 |  155132   27164   629982    23.2 |  2.217 % |
c |     27602 |  465397  1292035 |  170645   27265   632729    23.2 |  2.217 % |
c |     27752 |  465397  1292035 |  187709   27415   636933    23.2 |  2.217 % |
c |     27977 |  465397  1292035 |  206480   27640   641539    23.2 |  2.217 % |
c |     28314 |  465397  1292035 |  227128   27977   649371    23.2 |  2.217 % |
c |     28821 |  465397  1292035 |  249841   28484   662586    23.3 |  2.217 % |
c ==============================================================================
c [1mFound solution: 161986[0m
c ---[   0]---> Sorter-cost:   88     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29346 |  465553  1292402 |  155184   29009   678561    23.4 |  2.217 % |
c |     29447 |  465553  1292402 |  170702   29110   680659    23.4 |  2.217 % |
c |     29598 |  465553  1292402 |  187772   29261   683250    23.4 |  2.217 % |
c |     29823 |  465553  1292402 |  206549   29486   689762    23.4 |  2.217 % |
c |     30160 |  465553  1292402 |  227204   29823   697868    23.4 |  2.217 % |
c |     30667 |  465553  1292402 |  249925   30330   714188    23.5 |  2.217 % |
c ==============================================================================
c [1mFound solution: 159790[0m
c ---[   0]---> Sorter-cost:   53     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31390 |  465644  1292616 |  155214   31053   735283    23.7 |  2.217 % |
c |     31491 |  465644  1292616 |  170735   31154   737351    23.7 |  2.217 % |
c |     31642 |  465644  1292616 |  187808   31305   740749    23.7 |  2.217 % |
c |     31867 |  465644  1292616 |  206589   31530   749707    23.8 |  2.217 % |
c |     32205 |  465644  1292616 |  227248   31868   759228    23.8 |  2.217 % |
c |     32711 |  465644  1292616 |  249973   32374   770908    23.8 |  2.217 % |
c |     33471 |  465644  1292616 |  274971   33134   789858    23.8 |  2.217 % |
c |     34613 |  465644  1292616 |  302468   34276   823325    24.0 |  2.217 % |
c |     36322 |  465644  1292616 |  332714   35985   872219    24.2 |  2.217 % |
c ==============================================================================
c [1mFound solution: 159786[0m
c ---[   0]---> Sorter-cost:   82     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     37322 |  465791  1292960 |  155263   36985   902848    24.4 |  2.217 % |
c |     37422 |  465791  1292960 |  170789   37085   905099    24.4 |  2.217 % |
c |     37572 |  465791  1292960 |  187868   37235   909138    24.4 |  2.217 % |
c |     37799 |  465791  1292960 |  206655   37462   915199    24.4 |  2.217 % |
c |     38137 |  465791  1292960 |  227320   37800   922141    24.4 |  2.217 % |
c |     38644 |  465791  1292960 |  250052   38307   937739    24.5 |  2.217 % |
c |     39403 |  465791  1292960 |  275057   39066   969140    24.8 |  2.217 % |
c ==============================================================================
c [1mFound solution: 158342[0m
c ---[   0]---> Sorter-cost:   82     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     40018 |  465940  1293309 |  155313   39681   987486    24.9 |  2.217 % |
c |     40119 |  465940  1293309 |  170844   39782   990071    24.9 |  2.216 % |
c |     40270 |  465940  1293309 |  187928   39933   993713    24.9 |  2.216 % |
c |     40495 |  465940  1293309 |  206721   40158   998124    24.9 |  2.216 % |
c |     40832 |  465940  1293309 |  227393   40495  1006445    24.9 |  2.216 % |
c |     41338 |  465940  1293309 |  250133   41001  1022161    24.9 |  2.216 % |
c |     42097 |  465940  1293309 |  275146   41760  1051255    25.2 |  2.216 % |
c |     43236 |  465940  1293309 |  302661   42899  1078247    25.1 |  2.216 % |
c ==============================================================================
c [1mFound solution: 157060[0m
c ---[   0]---> Sorter-cost:   82     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     44262 |  466086  1293651 |  155362   43925  1114809    25.4 |  2.216 % |
c |     44362 |  466086  1293651 |  170898   44025  1116311    25.4 |  2.216 % |
c |     44512 |  466086  1293651 |  187988   44175  1119239    25.3 |  2.216 % |
c |     44739 |  466086  1293651 |  206786   44402  1125424    25.3 |  2.216 % |
c |     45078 |  466086  1293651 |  227465   44741  1138059    25.4 |  2.216 % |
c |     45584 |  466086  1293651 |  250212   45247  1152701    25.5 |  2.216 % |
c ==============================================================================
c [1mFound solution: 154886[0m
c ---[   0]---> Sorter-cost:   54     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45960 |  466180  1293873 |  155393   45623  1164754    25.5 |  2.216 % |
c |     46061 |  466180  1293873 |  170932   45724  1167819    25.5 |  2.216 % |
c |     46211 |  466180  1293873 |  188025   45874  1171381    25.5 |  2.216 % |
c |     46437 |  466180  1293873 |  206828   46100  1176267    25.5 |  2.216 % |
c |     46774 |  466180  1293873 |  227510   46437  1184305    25.5 |  2.216 % |
c |     47281 |  466180  1293873 |  250261   46944  1197524    25.5 |  2.216 % |
c |     48040 |  466180  1293873 |  275288   47703  1219393    25.6 |  2.216 % |
c |     49179 |  466180  1293873 |  302816   48842  1251670    25.6 |  2.216 % |
c ==============================================================================
c [1mFound solution: 154884[0m
c ---[   0]---> Sorter-cost:   54     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     50298 |  466274  1294095 |  155424   49961  1287335    25.8 |  2.216 % |
c |     50398 |  466274  1294095 |  170966   50061  1289066    25.7 |  2.216 % |
c |     50548 |  466274  1294095 |  188063   50211  1293729    25.8 |  2.216 % |
c |     50773 |  466274  1294095 |  206869   50436  1300251    25.8 |  2.216 % |
c |     51110 |  466274  1294095 |  227556   50773  1308373    25.8 |  2.216 % |
c |     51616 |  466274  1294095 |  250311   51279  1323987    25.8 |  2.216 % |
c |     52376 |  466274  1294095 |  275343   52039  1346140    25.9 |  2.216 % |
c ==============================================================================
c [1mFound solution: 153546[0m
c ---[   0]---> Sorter-cost:   62     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52987 |  466380  1294347 |  155460   52650  1365296    25.9 |  2.216 % |
c |     53087 |  466380  1294347 |  171006   52750  1367346    25.9 |  2.216 % |
c |     53237 |  466380  1294347 |  188106   52900  1371313    25.9 |  2.216 % |
c |     53462 |  466257  1293968 |  206917   53012  1371371    25.9 |  2.220 % |
c |     53799 |  466257  1293968 |  227608   53349  1384193    25.9 |  2.220 % |
c |     54305 |  466257  1293968 |  250369   53855  1398274    26.0 |  2.220 % |
c |     55065 |  466257  1293968 |  275406   54615  1424786    26.1 |  2.220 % |
c |     56204 |  466257  1293968 |  302947   55754  1464254    26.3 |  2.220 % |
c ==============================================================================
c [1mFound solution: 153412[0m
c ---[   0]---> Sorter-cost:   58     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57419 |  466362  1294215 |  155454   56969  1501652    26.4 |  2.220 % |
c |     57519 |  466362  1294215 |  170999   57069  1503564    26.3 |  2.220 % |
c |     57669 |  466362  1294215 |  188099   57219  1506640    26.3 |  2.220 % |
c |     57894 |  466362  1294215 |  206909   57444  1511325    26.3 |  2.220 % |
c |     58232 |  466362  1294215 |  227600   57782  1520359    26.3 |  2.220 % |
c |     58738 |  466362  1294215 |  250360   58288  1535044    26.3 |  2.220 % |
c |     59497 |  466362  1294215 |  275396   59047  1564519    26.5 |  2.220 % |
c |     60636 |  466362  1294215 |  302935   60186  1601934    26.6 |  2.220 % |
c ==============================================================================
c [1mFound solution: 149284[0m
c ---[   0]---> Sorter-cost:   68     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61307 |  466484  1294501 |  155494   60857  1627349    26.7 |  2.220 % |
c |     61407 |  466484  1294501 |  171043   60957  1629654    26.7 |  2.220 % |
c |     61557 |  466484  1294501 |  188147   61107  1633935    26.7 |  2.220 % |
c |     61782 |  466484  1294501 |  206962   61332  1639462    26.7 |  2.220 % |
c |     62121 |  466484  1294501 |  227658   61671  1648428    26.7 |  2.220 % |
c |     62627 |  466484  1294501 |  250424   62177  1663914    26.8 |  2.220 % |
c |     63387 |  466484  1294501 |  275467   62937  1690027    26.9 |  2.220 % |
c |     64526 |  466484  1294501 |  303013   64076  1732032    27.0 |  2.220 % |
c ==============================================================================
c [1mFound solution: 149264[0m
c ---[   0]---> Sorter-cost:   72     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     65473 |  466610  1294796 |  155536   65023  1772102    27.3 |  2.220 % |
c |     65573 |  466610  1294796 |  171089   65123  1774494    27.2 |  2.220 % |
c |     65723 |  466610  1294796 |  188198   65273  1777475    27.2 |  2.220 % |
c |     65949 |  466610  1294796 |  207018   65499  1784760    27.2 |  2.220 % |
c |     66288 |  466610  1294796 |  227720   65838  1792851    27.2 |  2.220 % |
c |     66795 |  466610  1294796 |  250492   66345  1806056    27.2 |  2.220 % |
c ==============================================================================
c [1mFound solution: 149250[0m
c ---[   0]---> Sorter-cost:   64     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     67275 |  466722  1295059 |  155574   66825  1824756    27.3 |  2.220 % |
c |     67375 |  466722  1295059 |  171131   66925  1826680    27.3 |  2.220 % |
c |     67525 |  466545  1294572 |  188244   66959  1821294    27.2 |  2.233 % |
c |     67750 |  466545  1294572 |  207068   67184  1826196    27.2 |  2.233 % |
c |     68087 |  466545  1294572 |  227775   67521  1836388    27.2 |  2.233 % |
c |     68595 |  466545  1294572 |  250553   68029  1849904    27.2 |  2.233 % |
c |     69354 |  466545  1294572 |  275608   68788  1874292    27.2 |  2.233 % |
c ==============================================================================
c [1mFound solution: 149248[0m
c ---[   0]---> Sorter-cost:   47     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70024 |  466626  1294762 |  155542   69458  1895969    27.3 |  2.233 % |
c |     70124 |  466626  1294762 |  171096   69558  1898079    27.3 |  2.233 % |
c |     70274 |  466626  1294762 |  188205   69708  1901682    27.3 |  2.233 % |
c |     70499 |  466626  1294762 |  207026   69933  1908117    27.3 |  2.233 % |
c |     70836 |  466626  1294762 |  227729   70270  1918687    27.3 |  2.233 % |
c |     71342 |  466626  1294762 |  250501   70776  1930711    27.3 |  2.233 % |
c |     72104 |  466626  1294762 |  275552   71538  1963038    27.4 |  2.233 % |
c |     73243 |  466626  1294762 |  303107   72677  2003043    27.6 |  2.233 % |
c |     74951 |  466626  1294762 |  333418   74385  2067499    27.8 |  2.233 % |
c ==============================================================================
c [1mFound solution: 147444[0m
c ---[   0]---> Sorter-cost:   60     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     76873 |  466721  1294993 |  155573   76307  2137373    28.0 |  2.233 % |
c |     76976 |  466721  1294993 |  171130   76410  2138957    28.0 |  2.233 % |
c |     77126 |  466721  1294993 |  188243   76560  2142491    28.0 |  2.233 % |
c |     77352 |  466721  1294993 |  207067   76786  2147256    28.0 |  2.233 % |
c |     77689 |  466721  1294993 |  227774   77123  2162024    28.0 |  2.233 % |
c |     78195 |  466721  1294993 |  250551   77629  2179017    28.1 |  2.233 % |
c |     78955 |  466721  1294993 |  275607   78389  2199076    28.1 |  2.233 % |
c |     80094 |  466721  1294993 |  303167   79528  2231347    28.1 |  2.233 % |
c |     81803 |  466721  1294993 |  333484   81237  2284606    28.1 |  2.233 % |
c |     84366 |  466721  1294993 |  366832   83800  2367134    28.2 |  2.233 % |
c ==============================================================================
c [1mFound solution: 147438[0m
c ---[   0]---> Sorter-cost:   52     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     88194 |  466802  1295190 |  155600   87628  2507230    28.6 |  2.233 % |
c |     88294 |  466802  1295190 |  171160   87728  2509276    28.6 |  2.233 % |
c |     88444 |  466802  1295190 |  188276   87878  2512746    28.6 |  2.233 % |
c |     88669 |  466442  1294204 |  207103   87831  2501141    28.5 |  2.259 % |
c |     89006 |  466442  1294204 |  227813   88168  2511596    28.5 |  2.259 % |
c |     89513 |  466337  1293861 |  250595   88432  2516858    28.5 |  2.261 % |
c |     90272 |  466337  1293861 |  275654   89191  2556595    28.7 |  2.261 % |
c |     91411 |  466337  1293861 |  303220   90330  2585654    28.6 |  2.261 % |
c |     93119 |  466220  1293494 |  333542   91945  2632394    28.6 |  2.264 % |
c |     95681 |  466220  1293494 |  366896   94507  2783443    29.5 |  2.264 % |
c |     99526 |  466220  1293494 |  403586   98352  2914148    29.6 |  2.264 % |
c ==============================================================================
c [1mFound solution: 147402[0m
c ---[   0]---> Sorter-cost:   32     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    103614 |  465989  1292786 |  155329  102026  3025842    29.7 |  2.264 % |
c |    103716 |  465989  1292786 |  170861  102128  3028397    29.7 |  2.279 % |
c |    103866 |  465989  1292786 |  187948  102278  3031779    29.6 |  2.279 % |
c |    104091 |  465989  1292786 |  206742  102503  3037606    29.6 |  2.279 % |
c |    104428 |  465989  1292786 |  227417  102840  3044972    29.6 |  2.279 % |
c |    104934 |  465989  1292786 |  250158  103346  3058768    29.6 |  2.279 % |
c |    105695 |  465863  1292401 |  275174  103988  3077304    29.6 |  2.284 % |
c |    106835 |  465863  1292401 |  302692  105128  3109515    29.6 |  2.284 % |
c |    108543 |  465716  1291974 |  332961  106603  3149407    29.5 |  2.292 % |
c ==============================================================================
c [1mFound solution: 147360[0m
c ---[   0]---> Sorter-cost:   56     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    111055 |  465806  1292190 |  155268  109115  3281846    30.1 |  2.292 % |
c |    111157 |  465806  1292190 |  170794  109217  3284201    30.1 |  2.292 % |
c |    111307 |  465806  1292190 |  187874  109367  3286733    30.1 |  2.292 % |
c |    111532 |  465806  1292190 |  206661  109592  3293387    30.1 |  2.292 % |
c |    111869 |  465806  1292190 |  227327  109929  3301461    30.0 |  2.292 % |
c |    112375 |  465806  1292190 |  250060  110435  3315736    30.0 |  2.292 % |
c |    113135 |  465806  1292190 |  275066  111195  3340166    30.0 |  2.292 % |
c |    114274 |  465806  1292190 |  302573  112334  3369899    30.0 |  2.292 % |
c |    115982 |  465644  1291733 |  332830  113855  3407168    29.9 |  2.302 % |
c |    118544 |  465644  1291733 |  366113  116417  3495696    30.0 |  2.302 % |
c ==============================================================================
c [1mFound solution: 147342[0m
c ---[   0]---> Sorter-cost:   36     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    122188 |  465521  1291377 |  155173  119942  3653112    30.5 |  2.302 % |
c |    122289 |  465521  1291377 |  170690  120043  3655243    30.4 |  2.315 % |
c |    122439 |  465410  1291022 |  187759  120064  3651953    30.4 |  2.318 % |
c |    122664 |  465410  1291022 |  206535  120289  3657507    30.4 |  2.318 % |
c |    123002 |  465410  1291022 |  227188  120627  3667140    30.4 |  2.318 % |
c |    123508 |  465410  1291022 |  249907  121133  3683326    30.4 |  2.318 % |
c |    124267 |  465308  1290685 |  274898  121786  3696310    30.4 |  2.319 % |
c |    125408 |  465308  1290685 |  302388  122927  3724353    30.3 |  2.319 % |
c |    127116 |  465308  1290685 |  332627  124635  3784367    30.4 |  2.319 % |
c |    129678 |  465308  1290685 |  365889  127197  3907360    30.7 |  2.319 % |
c |    133523 |  465308  1290685 |  402478  131042  4025492    30.7 |  2.319 % |
c |    139289 |  465308  1290685 |  442726  136808  4212317    30.8 |  2.319 % |
c |    147938 |  464852  1289374 |  486999  145090  4559147    31.4 |  2.346 % |
c ==============================================================================
c [1mFound solution: 147326[0m
c ---[   0]---> Sorter-cost:   63     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    150077 |  464771  1289121 |  154923  147084  4650853    31.6 |  2.346 % |
c |    150177 |  464771  1289121 |  170415  147184  4652839    31.6 |  2.360 % |
c |    150327 |  464771  1289121 |  187456  147334  4655543    31.6 |  2.360 % |
c |    150552 |  464771  1289121 |  206202  147559  4662133    31.6 |  2.360 % |
c |    150889 |  464771  1289121 |  226822  147896  4672079    31.6 |  2.360 % |
c |    151396 |  464771  1289121 |  249505  148403  4685080    31.6 |  2.360 % |
c |    152155 |  464771  1289121 |  274455  149162  4713882    31.6 |  2.360 % |
c |    153294 |  464591  1288628 |  301901  150007  4724423    31.5 |  2.373 % |
c |    155002 |  464591  1288628 |  332091  151715  4783782    31.5 |  2.373 % |
c ==============================================================================
c [1mFound solution: 147228[0m
c ---[   0]---> Sorter-cost:   69     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    156874 |  464707  1288904 |  154902  153587  4893726    31.9 |  2.373 % |
c |    156976 |  464707  1288904 |  170392  153689  4895317    31.9 |  2.372 % |
c |    157128 |  464707  1288904 |  187431  153841  4898177    31.8 |  2.372 % |
c |    157353 |  464707  1288904 |  206174  154066  4903675    31.8 |  2.372 % |
c |    157691 |  464707  1288904 |  226792  154404  4911858    31.8 |  2.372 % |
c |    158198 |  464707  1288904 |  249471  154911  4927098    31.8 |  2.372 % |
c |    158958 |  464707  1288904 |  274418  155671  4952672    31.8 |  2.372 % |
c |    160097 |  464707  1288904 |  301860  156810  4991702    31.8 |  2.372 % |
c |    161806 |  464707  1288904 |  332046  158519  5131373    32.4 |  2.372 % |
c |    164368 |  464707  1288904 |  365250  161081  5213307    32.4 |  2.372 % |
c ==============================================================================
c [1mFound solution: 147220[0m
c ---[   0]---> Sorter-cost:   65     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    167558 |  464817  1289166 |  154939  164271  5335108    32.5 |  2.372 % |
c |    167659 |  464817  1289166 |  170432   26484   605881    22.9 |  2.372 % |
c |    167809 |  464817  1289166 |  187476   26634   609058    22.9 |  2.372 % |
c |    168034 |  464817  1289166 |  206223   26859   613928    22.9 |  2.372 % |
c |    168371 |  464817  1289166 |  226846   27196   621711    22.9 |  2.372 % |
c |    168878 |  464817  1289166 |  249530   27703   633969    22.9 |  2.372 % |
c |    169638 |  464817  1289166 |  274483   28463   655368    23.0 |  2.372 % |
c |    170777 |  464709  1288817 |  301932   29599   688176    23.2 |  2.375 % |
c |    172486 |  464709  1288817 |  332125   31308   743843    23.8 |  2.375 % |
c |    175048 |  464709  1288817 |  365338   33870   848990    25.1 |  2.375 % |
c |    178893 |  464535  1288336 |  401871   37714   958354    25.4 |  2.387 % |
c |    184659 |  464430  1287993 |  442059   43477  1133115    26.1 |  2.389 % |
c ==============================================================================
c [1mFound solution: 147134[0m
c ---[   0]---> Sorter-cost:   58     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    191987 |  464352  1287743 |  154784   50802  1432989    28.2 |  2.389 % |
c |    192087 |  464352  1287743 |  170262   50902  1434693    28.2 |  2.401 % |
c |    192238 |  464211  1287328 |  187288   50684  1409856    27.8 |  2.408 % |
c |    192463 |  464211  1287328 |  206017   50909  1414692    27.8 |  2.408 % |
c |    192800 |  464211  1287328 |  226619   51246  1421794    27.7 |  2.408 % |
c |    193306 |  464211  1287328 |  249281   51752  1435772    27.7 |  2.408 % |
c |    194065 |  464211  1287328 |  274209   52511  1462337    27.8 |  2.408 % |
c |    195204 |  464211  1287328 |  301630   53650  1510443    28.2 |  2.408 % |
c |    196913 |  464079  1286931 |  331793   55356  1554407    28.1 |  2.414 % |
c |    199475 |  464079  1286931 |  364972   57918  1623088    28.0 |  2.414 % |
c ==============================================================================
c [1mFound solution: 146980[0m
c ---[   0]---> Sorter-cost:   47     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    203264 |  464156  1287115 |  154718   61707  1777937    28.8 |  2.414 % |
c |    203364 |  464156  1287115 |  170189   61807  1779490    28.8 |  2.414 % |
c |    203515 |  464156  1287115 |  187208   61958  1782149    28.8 |  2.414 % |
c |    203740 |  464156  1287115 |  205929   62183  1786654    28.7 |  2.414 % |
c |    204077 |  464156  1287115 |  226522   62520  1793911    28.7 |  2.414 % |
c |    204583 |  464156  1287115 |  249174   63026  1806480    28.7 |  2.414 % |
c |    205343 |  464156  1287115 |  274092   63786  1828375    28.7 |  2.414 % |
c |    206482 |  464156  1287115 |  301501   64925  1859008    28.6 |  2.414 % |
c |    208190 |  464156  1287115 |  331651   66633  1906173    28.6 |  2.414 % |
c |    210752 |  464156  1287115 |  364816   69195  1994629    28.8 |  2.414 % |
c ==============================================================================
c [1mFound solution: 146978[0m
c ---[   0]---> Sorter-cost:   65     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    214571 |  464269  1287382 |  154756   73014  2130765    29.2 |  2.414 % |
c |    214671 |  464269  1287382 |  170231   73114  2132885    29.2 |  2.414 % |
c |    214821 |  464269  1287382 |  187254   73264  2136422    29.2 |  2.414 % |
c |    215047 |  464269  1287382 |  205980   73490  2140872    29.1 |  2.414 % |
c |    215384 |  464269  1287382 |  226578   73827  2147830    29.1 |  2.414 % |
c |    215890 |  464269  1287382 |  249236   74333  2160341    29.1 |  2.414 % |
c |    216649 |  464269  1287382 |  274159   75092  2179751    29.0 |  2.414 % |
c |    217789 |  464269  1287382 |  301575   76232  2206706    28.9 |  2.414 % |
c |    219497 |  464269  1287382 |  331733   77940  2259383    29.0 |  2.414 % |
c ==============================================================================
c [1mFound solution: 146380[0m
c ---[   0]---> Sorter-cost:   51     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    220837 |  464353  1287583 |  154784   79280  2297368    29.0 |  2.414 % |
c |    220938 |  464353  1287583 |  170262   79381  2299608    29.0 |  2.414 % |
c |    221089 |  464353  1287583 |  187288   79532  2303529    29.0 |  2.414 % |
c |    221315 |  464353  1287583 |  206017   79758  2307437    28.9 |  2.414 % |
c |    221652 |  464353  1287583 |  226619   80095  2316757    28.9 |  2.414 % |
c |    222159 |  464353  1287583 |  249281   80602  2334052    29.0 |  2.414 % |
c |    222919 |  464353  1287583 |  274209   81362  2357434    29.0 |  2.414 % |
c |    224058 |  464353  1287583 |  301630   82501  2393049    29.0 |  2.414 % |
c |    225767 |  464224  1287192 |  331793   84092  2432161    28.9 |  2.419 % |
c ==============================================================================
c [1mFound solution: 146306[0m
c ---[   0]---> Sorter-cost:   51     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    227263 |  464310  1287397 |  154770   85588  2478921    29.0 |  2.419 % |
c |    227363 |  464310  1287397 |  170247   85688  2481299    29.0 |  2.419 % |
c |    227513 |  464310  1287397 |  187271   85838  2484766    28.9 |  2.419 % |
c |    227738 |  464310  1287397 |  205998   86063  2489969    28.9 |  2.419 % |
c |    228075 |  464310  1287397 |  226598   86400  2500545    28.9 |  2.419 % |
c |    228581 |  464310  1287397 |  249258   86906  2515311    28.9 |  2.419 % |
c |    229341 |  464310  1287397 |  274184   87666  2542391    29.0 |  2.419 % |
c |    230481 |  464310  1287397 |  301602   88806  2579673    29.0 |  2.419 % |
c |    232190 |  464310  1287397 |  331763   90515  2651578    29.3 |  2.419 % |
c ==============================================================================
c [1mFound solution: 146304[0m
c ---[   0]---> Sorter-cost:   48     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    234491 |  464390  1287587 |  154796   92816  2766896    29.8 |  2.419 % |
c |    234592 |  464390  1287587 |  170275   92917  2768811    29.8 |  2.419 % |
c |    234743 |  464390  1287587 |  187303   93068  2772158    29.8 |  2.419 % |
c |    234968 |  464390  1287587 |  206033   93293  2777249    29.8 |  2.419 % |
c |    235305 |  464390  1287587 |  226636   93630  2785868    29.8 |  2.419 % |
c |    235811 |  464390  1287587 |  249300   94136  2798699    29.7 |  2.419 % |
c |    236571 |  464390  1287587 |  274230   94896  2817795    29.7 |  2.419 % |
c |    237710 |  464390  1287587 |  301653   96035  2856737    29.7 |  2.419 % |
c |    239418 |  464390  1287587 |  331818   97743  2911029    29.8 |  2.419 % |
c |    241980 |  464390  1287587 |  365000  100305  2992098    29.8 |  2.419 % |
c |    245824 |  464390  1287587 |  401500  104149  3116228    29.9 |  2.419 % |
c ==============================================================================
c [1mFound solution: 146278[0m
c ---[   0]---> Sorter-cost:   62     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    247792 |  464498  1287843 |  154832  106117  3187109    30.0 |  2.419 % |
c |    247892 |  464498  1287843 |  170315  106217  3188942    30.0 |  2.419 % |
c |    248042 |  464498  1287843 |  187346  106367  3191649    30.0 |  2.419 % |
c |    248267 |  464498  1287843 |  206081  106592  3197831    30.0 |  2.419 % |
c |    248604 |  464498  1287843 |  226689  106929  3206615    30.0 |  2.419 % |
c |    249111 |  464498  1287843 |  249358  107436  3221960    30.0 |  2.419 % |
c |    249870 |  464498  1287843 |  274294  108195  3241693    30.0 |  2.419 % |
c |    251010 |  464498  1287843 |  301723  109335  3290682    30.1 |  2.419 % |
c |    252718 |  464498  1287843 |  331896  111043  3345543    30.1 |  2.419 % |
c |    255281 |  464498  1287843 |  365085  113606  3409632    30.0 |  2.419 % |
c |    259126 |  464498  1287843 |  401594  117451  3730233    31.8 |  2.419 % |
c |    264892 |  464498  1287843 |  441753  123217  3917804    31.8 |  2.419 % |
c |    273543 |  464354  1287422 |  485929  131865  4466038    33.9 |  2.427 % |
c ==============================================================================
c [1mFound solution: 146246[0m
c ---[   0]---> Sorter-cost:   58     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    276050 |  464455  1287661 |  154818  134372  4546582    33.8 |  2.427 % |
c |    276150 |  464455  1287661 |  170299  134472  4548327    33.8 |  2.427 % |
c |    276300 |  464455  1287661 |  187329  134622  4552133    33.8 |  2.427 % |
c |    276526 |  464455  1287661 |  206062  134848  4556891    33.8 |  2.427 % |
c |    276863 |  464455  1287661 |  226669  135185  4569004    33.8 |  2.427 % |
c |    277369 |  464455  1287661 |  249335  135691  4582343    33.8 |  2.427 % |
c |    278128 |  464455  1287661 |  274269  136450  4604752    33.7 |  2.427 % |
c |    279267 |  464455  1287661 |  301696  137589  4645116    33.8 |  2.427 % |
c |    280975 |  464455  1287661 |  331866  139297  4697663    33.7 |  2.427 % |
c |    283539 |  464326  1287270 |  365052  141858  4775215    33.7 |  2.432 % |
c |    287383 |  464140  1286765 |  401558  145699  4903741    33.7 |  2.446 % |
c ==============================================================================
c [1mFound solution: 146244[0m
c ---[   0]---> Sorter-cost:   39     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    290243 |  464206  1286923 |  154735  148559  5001580    33.7 |  2.446 % |
c |    290343 |  464206  1286923 |  170208  148659  5003127    33.7 |  2.446 % |
c |    290495 |  464206  1286923 |  187229  148811  5005570    33.6 |  2.446 % |
c |    290721 |  464206  1286923 |  205952  149037  5010575    33.6 |  2.446 % |
c |    291058 |  464206  1286923 |  226547  149374  5017004    33.6 |  2.446 % |
c |    291566 |  464206  1286923 |  249202  149882  5031236    33.6 |  2.446 % |
c |    292325 |  464206  1286923 |  274122  150641  5050362    33.5 |  2.446 % |
c |    293464 |  464206  1286923 |  301534  151780  5082113    33.5 |  2.446 % |
c |    295172 |  464206  1286923 |  331688  153488  5138839    33.5 |  2.446 % |
c ==============================================================================
c [1mFound solution: 146242[0m
c ---[   0]---> Sorter-cost:   54     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    297045 |  464113  1286639 |  154704  155358  5204702    33.5 |  2.446 % |
c |    297145 |  464113  1286639 |  170174  155458  5206396    33.5 |  2.460 % |
c |    297295 |  464113  1286639 |  187191  155608  5209640    33.5 |  2.460 % |
c |    297520 |  464113  1286639 |  205911  155833  5214146    33.5 |  2.460 % |
c |    297858 |  464113  1286639 |  226502  156171  5224369    33.5 |  2.460 % |
c |    298364 |  464113  1286639 |  249152  156677  5235446    33.4 |  2.460 % |
c ==============================================================================
c [1mFound solution: 146240[0m
c ---[   0]---> Sorter-cost:   55     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    299064 |  464206  1286859 |  154735  157377  5267139    33.5 |  2.460 % |
c |    299164 |  464206  1286859 |  170208  157477  5269618    33.5 |  2.460 % |
c |    299314 |  464206  1286859 |  187229  157627  5272869    33.5 |  2.460 % |
c |    299539 |  464206  1286859 |  205952  157852  5277803    33.4 |  2.460 % |
c |    299876 |  464206  1286859 |  226547  158189  5284742    33.4 |  2.460 % |
c |    300382 |  464206  1286859 |  249202  158695  5300169    33.4 |  2.460 % |
c |    301141 |  464206  1286859 |  274122  159454  5319554    33.4 |  2.460 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 25258 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.90 0.95 0.90 2/54 25254
Raw data (stat): 25254 (runsolver) R 25253 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 796751560 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.91 0.96 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0005 s]
Raw data (loadavg): 0.93 0.96 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0011 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0012 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0024 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0025 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0043 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0045 s]
Raw data (loadavg): 0.97 0.96 0.91 5/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.025 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.025 s]
Raw data (loadavg): 1.07 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.024 s]
Raw data (loadavg): 1.06 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.038 s]
Raw data (loadavg): 1.05 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.043 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.043 s]
Raw data (loadavg): 1.04 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.043 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.042 s]
Raw data (loadavg): 1.03 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.043 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.043 s]
Raw data (loadavg): 1.02 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.043 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/55 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.75 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 25258
Raw data (stat): 25254 (minisat+_script) S 25253 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 796751560 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

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