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-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-liu.opb
MD5SUM	7c5b217de8d505f751f776306b4ebb3a
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	3145687
Optimality of the best value was proved	NO
Number of terms in the objective function	30
Biggest coefficient in the objective function	536870912
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	1073741823
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	536870912
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	2182184958
Number of bits of the biggest sum of numbers	32
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	3785.95
Number of variables	3099
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	63
Trace number 31939

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        818892 kB
Buffers:         32888 kB
Cached:         162264 kB
SwapCached:       1028 kB
Active:          25724 kB
Inactive:       171604 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        818640 kB
SwapTotal:     2097892 kB
SwapFree:      2096024 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5036 kB
Slab:            12748 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-27 07:21:47 (client local time) WITH STATUS 152 IN 1229.94 SECONDS
stats: 23327 7 1229.94 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:  298
c ---[2176]---> BDD-cost:  367
c ---[2175]---> BDD-cost:  351
c ---[2174]---> BDD-cost:  352
c ---[2173]---> BDD-cost:  298
c ---[2172]---> BDD-cost:  329
c ---[2171]---> BDD-cost:  298
c ---[2170]---> BDD-cost:  329
c ---[2169]---> BDD-cost:  298
c ---[2168]---> BDD-cost:  310
c ---[2167]---> BDD-cost:  298
c ---[2166]---> BDD-cost:  310
c ---[2165]---> BDD-cost:  292
c ---[2164]---> BDD-cost:  298
c ---[2163]---> BDD-cost:  292
c ---[2162]---> BDD-cost:  292
c ---[2161]---> BDD-cost:  292
c ---[2160]---> BDD-cost:  292
c ---[2159]---> BDD-cost:  340
c ---[2158]---> BDD-cost:  292
c ---[2157]---> BDD-cost:  340
c ---[2156]---> BDD-cost:  292
c ---[2155]---> BDD-cost:  259
c ---[2154]---> BDD-cost:  292
c ---[2153]---> BDD-cost:  345
c ---[2152]---> BDD-cost:  259
c ---[2151]---> BDD-cost:  292
c ---[2150]---> BDD-cost:  274
c ---[2149]---> BDD-cost:  292
c ---[2148]---> BDD-cost:  274
c ---[2147]---> BDD-cost:  292
c ---[2146]---> BDD-cost:  350
c ---[2145]---> BDD-cost:  292
c ---[2144]---> BDD-cost:  350
c ---[2143]---> BDD-cost:  292
c ---[2142]---> BDD-cost:  298
c ---[2141]---> BDD-cost:  347
c ---[2140]---> BDD-cost:  292
c ---[2139]---> BDD-cost:  347
c ---[2138]---> BDD-cost:  292
c ---[2137]---> BDD-cost:  314
c ---[2136]---> BDD-cost:  292
c ---[2135]---> BDD-cost:  314
c ---[2134]---> BDD-cost:  292
c ---[2133]---> BDD-cost:  332
c ---[2132]---> BDD-cost:  292
c ---[2131]---> BDD-cost:  345
c ---[2130]---> BDD-cost:  332
c ---[2129]---> BDD-cost:  292
c ---[2128]---> BDD-cost:  293
c ---[2127]---> BDD-cost:  292
c ---[2126]---> BDD-cost:  293
c ---[2125]---> BDD-cost:  292
c ---[2124]---> BDD-cost:  345
c ---[2123]---> BDD-cost:  292
c ---[2122]---> BDD-cost:  345
c ---[2121]---> BDD-cost:  292
c ---[2120]---> BDD-cost:  298
c ---[2119]---> BDD-cost:  359
c ---[2118]---> BDD-cost:  292
c ---[2117]---> BDD-cost:  359
c ---[2116]---> BDD-cost:  292
c ---[2115]---> BDD-cost:  309
c ---[2114]---> BDD-cost:  292
c ---[2113]---> BDD-cost:  309
c ---[2112]---> BDD-cost:  292
c ---[2111]---> BDD-cost:  321
c ---[2110]---> BDD-cost:  292
c ---[2109]---> BDD-cost:  340
c ---[2108]---> BDD-cost:  321
c ---[2107]---> BDD-cost:  292
c ---[2106]---> BDD-cost:  277
c ---[2105]---> BDD-cost:  292
c ---[2104]---> BDD-cost:  277
c ---[2103]---> BDD-cost:  292
c ---[2102]---> BDD-cost:  295
c ---[2101]---> BDD-cost:  292
c ---[2100]---> BDD-cost:  295
c ---[2099]---> BDD-cost:  292
c ---[2098]---> BDD-cost:  298
c ---[2097]---> BDD-cost:  351
c ---[2096]---> BDD-cost:  292
c ---[2095]---> BDD-cost:  351
c ---[2094]---> BDD-cost:  292
c ---[2093]---> BDD-cost:  345
c ---[2092]---> BDD-cost:  292
c ---[2091]---> BDD-cost:  345
c ---[2090]---> BDD-cost:  292
c ---[2089]---> BDD-cost:  340
c ---[2088]---> BDD-cost:  292
c ---[2087]---> BDD-cost:  340
c ---[2086]---> BDD-cost:  340
c ---[2085]---> BDD-cost:  292
c ---[2084]---> BDD-cost:  261
c ---[2083]---> BDD-cost:  292
c ---[2082]---> BDD-cost:  261
c ---[2081]---> BDD-cost:  292
c ---[2080]---> BDD-cost:  322
c ---[2079]---> BDD-cost:  292
c ---[2078]---> BDD-cost:  322
c ---[2077]---> BDD-cost:  292
c ---[2076]---> BDD-cost:  298
c ---[2075]---> BDD-cost:  352
c ---[2074]---> BDD-cost:  292
c ---[2073]---> BDD-cost:  352
c ---[2072]---> BDD-cost:  292
c ---[2071]---> BDD-cost:  329
c ---[2070]---> BDD-cost:  292
c ---[2069]---> BDD-cost:  329
c ---[2068]---> BDD-cost:  292
c ---[2067]---> BDD-cost:  310
c ---[2066]---> BDD-cost:  292
c ---[2065]---> BDD-cost:  298
c ---[2064]---> BDD-cost:  261
c ---[2063]---> BDD-cost:  310
c ---[2062]---> BDD-cost:  292
c ---[2061]---> BDD-cost:  340
c ---[2060]---> BDD-cost:  292
c ---[2059]---> BDD-cost:  340
c ---[2058]---> BDD-cost:  292
c ---[2057]---> BDD-cost:  259
c ---[2056]---> BDD-cost:  292
c ---[2055]---> BDD-cost:  259
c ---[2054]---> BDD-cost:  292
c ---[2053]---> BDD-cost:  298
c ---[2052]---> BDD-cost:  274
c ---[2051]---> BDD-cost:  292
c ---[2050]---> BDD-cost:  274
c ---[2049]---> BDD-cost:  292
c ---[2048]---> BDD-cost:  350
c ---[2047]---> BDD-cost:  292
c ---[2046]---> BDD-cost:  350
c ---[2045]---> BDD-cost:  292
c ---[2044]---> BDD-cost:  347
c ---[2043]---> BDD-cost:  292
c ---[2042]---> BDD-cost:  261
c ---[2041]---> BDD-cost:  347
c ---[2040]---> BDD-cost:  292
c ---[2039]---> BDD-cost:  314
c ---[2038]---> BDD-cost:  292
c ---[2037]---> BDD-cost:  314
c ---[2036]---> BDD-cost:  292
c ---[2035]---> BDD-cost:  332
c ---[2034]---> BDD-cost:  292
c ---[2033]---> BDD-cost:  332
c ---[2032]---> BDD-cost:  292
c ---[2031]---> BDD-cost:  298
c ---[2030]---> BDD-cost:  293
c ---[2029]---> BDD-cost:  292
c ---[2028]---> BDD-cost:  293
c ---[2027]---> BDD-cost:  292
c ---[2026]---> BDD-cost:  345
c ---[2025]---> BDD-cost:  292
c ---[2024]---> BDD-cost:  345
c ---[2023]---> BDD-cost:  292
c ---[2022]---> BDD-cost:  359
c ---[2021]---> BDD-cost:  292
c ---[2020]---> BDD-cost:  322
c ---[2019]---> BDD-cost:  359
c ---[2018]---> BDD-cost:  292
c ---[2017]---> BDD-cost:  309
c ---[2016]---> BDD-cost:  292
c ---[2015]---> BDD-cost:  309
c ---[2014]---> BDD-cost:  292
c ---[2013]---> BDD-cost:  321
c ---[2012]---> BDD-cost:  292
c ---[2011]---> BDD-cost:  321
c ---[2010]---> BDD-cost:  292
c ---[2009]---> BDD-cost:  298
c ---[2008]---> BDD-cost:  277
c ---[2007]---> BDD-cost:  292
c ---[2006]---> BDD-cost:  277
c ---[2005]---> BDD-cost:  292
c ---[2004]---> BDD-cost:  295
c ---[2003]---> BDD-cost:  292
c ---[2002]---> BDD-cost:  295
c ---[2001]---> BDD-cost:  292
c ---[2000]---> BDD-cost:  351
c ---[1999]---> BDD-cost:  292
c ---[1998]---> BDD-cost:  322
c ---[1997]---> BDD-cost:  351
c ---[1996]---> BDD-cost:  292
c ---[1995]---> BDD-cost:  345
c ---[1994]---> BDD-cost:  292
c ---[1993]---> BDD-cost:  345
c ---[1992]---> BDD-cost:  292
c ---[1991]---> BDD-cost:  340
c ---[1990]---> BDD-cost:  292
c ---[1989]---> BDD-cost:  340
c ---[1988]---> BDD-cost:  292
c ---[1987]---> BDD-cost:  298
c ---[1986]---> BDD-cost:  261
c ---[1985]---> BDD-cost:  292
c ---[1984]---> BDD-cost:  261
c ---[1983]---> BDD-cost:  292
c ---[1982]---> BDD-cost:  322
c ---[1981]---> BDD-cost:  292
c ---[1980]---> BDD-cost:  322
c ---[1979]---> BDD-cost:  292
c ---[1978]---> BDD-cost:  352
c ---[1977]---> BDD-cost:  292
c ---[1976]---> BDD-cost:  352
c ---[1975]---> BDD-cost:  352
c ---[1974]---> BDD-cost:  292
c ---[1973]---> BDD-cost:  329
c ---[1972]---> BDD-cost:  292
c ---[1971]---> BDD-cost:  329
c ---[1970]---> BDD-cost:  292
c ---[1969]---> BDD-cost:  310
c ---[1968]---> BDD-cost:  292
c ---[1967]---> BDD-cost:  310
c ---[1966]---> BDD-cost:  340
c ---[1965]---> BDD-cost:  298
c ---[1964]---> BDD-cost:  259
c ---[1963]---> BDD-cost:  340
c ---[1962]---> BDD-cost:  259
c ---[1961]---> BDD-cost:  340
c ---[1960]---> BDD-cost:  274
c ---[1959]---> BDD-cost:  340
c ---[1958]---> BDD-cost:  274
c ---[1957]---> BDD-cost:  340
c ---[1956]---> BDD-cost:  350
c ---[1955]---> BDD-cost:  340
c ---[1954]---> BDD-cost:  367
c ---[1953]---> BDD-cost:  352
c ---[1952]---> BDD-cost:  350
c ---[1951]---> BDD-cost:  340
c ---[1950]---> BDD-cost:  347
c ---[1949]---> BDD-cost:  340
c ---[1948]---> BDD-cost:  347
c ---[1947]---> BDD-cost:  340
c ---[1946]---> BDD-cost:  314
c ---[1945]---> BDD-cost:  340
c ---[1944]---> BDD-cost:  314
c ---[1943]---> BDD-cost:  340
c ---[1942]---> BDD-cost:  298
c ---[1941]---> BDD-cost:  332
c ---[1940]---> BDD-cost:  340
c ---[1939]---> BDD-cost:  332
c ---[1938]---> BDD-cost:  340
c ---[1937]---> BDD-cost:  293
c ---[1936]---> BDD-cost:  340
c ---[1935]---> BDD-cost:  293
c ---[1934]---> BDD-cost:  340
c ---[1933]---> BDD-cost:  345
c ---[1932]---> BDD-cost:  340
c ---[1931]---> BDD-cost:  329
c ---[1930]---> BDD-cost:  345
c ---[1929]---> BDD-cost:  340
c ---[1928]---> BDD-cost:  359
c ---[1927]---> BDD-cost:  340
c ---[1926]---> BDD-cost:  359
c ---[1925]---> BDD-cost:  340
c ---[1924]---> BDD-cost:  309
c ---[1923]---> BDD-cost:  340
c ---[1922]---> BDD-cost:  309
c ---[1921]---> BDD-cost:  340
c ---[1920]---> BDD-cost:  298
c ---[1919]---> BDD-cost:  321
c ---[1918]---> BDD-cost:  340
c ---[1917]---> BDD-cost:  321
c ---[1916]---> BDD-cost:  340
c ---[1915]---> BDD-cost:  277
c ---[1914]---> BDD-cost:  340
c ---[1913]---> BDD-cost:  277
c ---[1912]---> BDD-cost:  340
c ---[1911]---> BDD-cost:  295
c ---[1910]---> BDD-cost:  340
c ---[1909]---> BDD-cost:  329
c ---[1908]---> BDD-cost:  295
c ---[1907]---> BDD-cost:  340
c ---[1906]---> BDD-cost:  351
c ---[1905]---> BDD-cost:  340
c ---[1904]---> BDD-cost:  351
c ---[1903]---> BDD-cost:  340
c ---[1902]---> BDD-cost:  345
c ---[1901]---> BDD-cost:  340
c ---[1900]---> BDD-cost:  345
c ---[1899]---> BDD-cost:  340
c ---[1898]---> BDD-cost:  298
c ---[1897]---> BDD-cost:  340
c ---[1896]---> BDD-cost:  340
c ---[1895]---> BDD-cost:  340
c ---[1894]---> BDD-cost:  340
c ---[1893]---> BDD-cost:  261
c ---[1892]---> BDD-cost:  340
c ---[1891]---> BDD-cost:  261
c ---[1890]---> BDD-cost:  340
c ---[1889]---> BDD-cost:  322
c ---[1888]---> BDD-cost:  340
c ---[1887]---> BDD-cost:  310
c ---[1886]---> BDD-cost:  322
c ---[1885]---> BDD-cost:  340
c ---[1884]---> BDD-cost:  352
c ---[1883]---> BDD-cost:  340
c ---[1882]---> BDD-cost:  352
c ---[1881]---> BDD-cost:  340
c ---[1880]---> BDD-cost:  329
c ---[1879]---> BDD-cost:  340
c ---[1878]---> BDD-cost:  329
c ---[1877]---> BDD-cost:  340
c ---[1876]---> BDD-cost:  298
c ---[1875]---> BDD-cost:  310
c ---[1874]---> BDD-cost:  340
c ---[1873]---> BDD-cost:  310
c ---[1872]---> BDD-cost:  259
c ---[1871]---> BDD-cost:  274
c ---[1870]---> BDD-cost:  259
c ---[1869]---> BDD-cost:  274
c ---[1868]---> BDD-cost:  259
c ---[1867]---> BDD-cost:  350
c ---[1866]---> BDD-cost:  259
c ---[1865]---> BDD-cost:  310
c ---[1864]---> BDD-cost:  350
c ---[1863]---> BDD-cost:  259
c ---[1862]---> BDD-cost:  347
c ---[1861]---> BDD-cost:  259
c ---[1860]---> BDD-cost:  347
c ---[1859]---> BDD-cost:  259
c ---[1858]---> BDD-cost:  314
c ---[1857]---> BDD-cost:  259
c ---[1856]---> BDD-cost:  314
c ---[1855]---> BDD-cost:  259
c ---[1854]---> BDD-cost:  332
c ---[1853]---> BDD-cost:  332
c ---[1852]---> BDD-cost:  259
c ---[1851]---> BDD-cost:  332
c ---[1850]---> BDD-cost:  259
c ---[1849]---> BDD-cost:  293
c ---[1848]---> BDD-cost:  259
c ---[1847]---> BDD-cost:  293
c ---[1846]---> BDD-cost:  259
c ---[1845]---> BDD-cost:  345
c ---[1844]---> BDD-cost:  259
c ---[1843]---> BDD-cost:  298
c ---[1842]---> BDD-cost:  270
c ---[1841]---> BDD-cost:  345
c ---[1840]---> BDD-cost:  259
c ---[1839]---> BDD-cost:  359
c ---[1838]---> BDD-cost:  259
c ---[1837]---> BDD-cost:  359
c ---[1836]---> BDD-cost:  259
c ---[1835]---> BDD-cost:  309
c ---[1834]---> BDD-cost:  259
c ---[1833]---> BDD-cost:  309
c ---[1832]---> BDD-cost:  259
c ---[1831]---> BDD-cost:  332
c ---[1830]---> BDD-cost:  321
c ---[1829]---> BDD-cost:  259
c ---[1828]---> BDD-cost:  321
c ---[1827]---> BDD-cost:  259
c ---[1826]---> BDD-cost:  277
c ---[1825]---> BDD-cost:  259
c ---[1824]---> BDD-cost:  277
c ---[1823]---> BDD-cost:  259
c ---[1822]---> BDD-cost:  295
c ---[1821]---> BDD-cost:  259
c ---[1820]---> BDD-cost:  270
c ---[1819]---> BDD-cost:  295
c ---[1818]---> BDD-cost:  259
c ---[1817]---> BDD-cost:  351
c ---[1816]---> BDD-cost:  259
c ---[1815]---> BDD-cost:  351
c ---[1814]---> BDD-cost:  259
c ---[1813]---> BDD-cost:  345
c ---[1812]---> BDD-cost:  259
c ---[1811]---> BDD-cost:  345
c ---[1810]---> BDD-cost:  259
c ---[1809]---> BDD-cost:  332
c ---[1808]---> BDD-cost:  340
c ---[1807]---> BDD-cost:  259
c ---[1806]---> BDD-cost:  340
c ---[1805]---> BDD-cost:  259
c ---[1804]---> BDD-cost:  261
c ---[1803]---> BDD-cost:  259
c ---[1802]---> BDD-cost:  261
c ---[1801]---> BDD-cost:  259
c ---[1800]---> BDD-cost:  322
c ---[1799]---> BDD-cost:  259
c ---[1798]---> BDD-cost:  367
c ---[1797]---> BDD-cost:  322
c ---[1796]---> BDD-cost:  259
c ---[1795]---> BDD-cost:  352
c ---[1794]---> BDD-cost:  259
c ---[1793]---> BDD-cost:  352
c ---[1792]---> BDD-cost:  259
c ---[1791]---> BDD-cost:  329
c ---[1790]---> BDD-cost:  259
c ---[1789]---> BDD-cost:  329
c ---[1788]---> BDD-cost:  259
c ---[1787]---> BDD-cost:  332
c ---[1786]---> BDD-cost:  310
c ---[1785]---> BDD-cost:  259
c ---[1784]---> BDD-cost:  310
c ---[1783]---> BDD-cost:  274
c ---[1782]---> BDD-cost:  350
c ---[1781]---> BDD-cost:  274
c ---[1780]---> BDD-cost:  350
c ---[1779]---> BDD-cost:  274
c ---[1778]---> BDD-cost:  347
c ---[1777]---> BDD-cost:  274
c ---[1776]---> BDD-cost:  367
c ---[1775]---> BDD-cost:  347
c ---[1774]---> BDD-cost:  274
c ---[1773]---> BDD-cost:  314
c ---[1772]---> BDD-cost:  274
c ---[1771]---> BDD-cost:  314
c ---[1770]---> BDD-cost:  274
c ---[1769]---> BDD-cost:  332
c ---[1768]---> BDD-cost:  274
c ---[1767]---> BDD-cost:  332
c ---[1766]---> BDD-cost:  274
c ---[1765]---> BDD-cost:  332
c ---[1764]---> BDD-cost:  293
c ---[1763]---> BDD-cost:  274
c ---[1762]---> BDD-cost:  293
c ---[1761]---> BDD-cost:  274
c ---[1760]---> BDD-cost:  345
c ---[1759]---> BDD-cost:  274
c ---[1758]---> BDD-cost:  345
c ---[1757]---> BDD-cost:  274
c ---[1756]---> BDD-cost:  359
c ---[1755]---> BDD-cost:  274
c ---[1754]---> BDD-cost:  352
c ---[1753]---> BDD-cost:  359
c ---[1752]---> BDD-cost:  274
c ---[1751]---> BDD-cost:  309
c ---[1750]---> BDD-cost:  274
c ---[1749]---> BDD-cost:  309
c ---[1748]---> BDD-cost:  274
c ---[1747]---> BDD-cost:  321
c ---[1746]---> BDD-cost:  274
c ---[1745]---> BDD-cost:  321
c ---[1744]---> BDD-cost:  274
c ---[1743]---> BDD-cost:  332
c ---[1742]---> BDD-cost:  277
c ---[1741]---> BDD-cost:  274
c ---[1740]---> BDD-cost:  277
c ---[1739]---> BDD-cost:  274
c ---[1738]---> BDD-cost:  295
c ---[1737]---> BDD-cost:  274
c ---[1736]---> BDD-cost:  295
c ---[1735]---> BDD-cost:  274
c ---[1734]---> BDD-cost:  351
c ---[1733]---> BDD-cost:  274
c ---[1732]---> BDD-cost:  352
c ---[1731]---> BDD-cost:  352
c ---[1730]---> BDD-cost:  351
c ---[1729]---> BDD-cost:  274
c ---[1728]---> BDD-cost:  345
c ---[1727]---> BDD-cost:  274
c ---[1726]---> BDD-cost:  345
c ---[1725]---> BDD-cost:  274
c ---[1724]---> BDD-cost:  340
c ---[1723]---> BDD-cost:  274
c ---[1722]---> BDD-cost:  340
c ---[1721]---> BDD-cost:  274
c ---[1720]---> BDD-cost:  332
c ---[1719]---> BDD-cost:  261
c ---[1718]---> BDD-cost:  274
c ---[1717]---> BDD-cost:  261
c ---[1716]---> BDD-cost:  274
c ---[1715]---> BDD-cost:  322
c ---[1714]---> BDD-cost:  274
c ---[1713]---> BDD-cost:  322
c ---[1712]---> BDD-cost:  274
c ---[1711]---> BDD-cost:  352
c ---[1710]---> BDD-cost:  274
c ---[1709]---> BDD-cost:  330
c ---[1708]---> BDD-cost:  352
c ---[1707]---> BDD-cost:  274
c ---[1706]---> BDD-cost:  329
c ---[1705]---> BDD-cost:  274
c ---[1704]---> BDD-cost:  329
c ---[1703]---> BDD-cost:  274
c ---[1702]---> BDD-cost:  310
c ---[1701]---> BDD-cost:  274
c ---[1700]---> BDD-cost:  310
c ---[1699]---> BDD-cost:  350
c ---[1698]---> BDD-cost:  332
c ---[1697]---> BDD-cost:  347
c ---[1696]---> BDD-cost:  350
c ---[1695]---> BDD-cost:  347
c ---[1694]---> BDD-cost:  350
c ---[1693]---> BDD-cost:  314
c ---[1692]---> BDD-cost:  350
c ---[1691]---> BDD-cost:  314
c ---[1690]---> BDD-cost:  350
c ---[1689]---> BDD-cost:  332
c ---[1688]---> BDD-cost:  350
c ---[1687]---> BDD-cost:  330
c ---[1686]---> BDD-cost:  332
c ---[1685]---> BDD-cost:  350
c ---[1684]---> BDD-cost:  293
c ---[1683]---> BDD-cost:  350
c ---[1682]---> BDD-cost:  293
c ---[1681]---> BDD-cost:  350
c ---[1680]---> BDD-cost:  345
c ---[1679]---> BDD-cost:  350
c ---[1678]---> BDD-cost:  345
c ---[1677]---> BDD-cost:  350
c ---[1676]---> BDD-cost:  332
c ---[1675]---> BDD-cost:  359
c ---[1674]---> BDD-cost:  350
c ---[1673]---> BDD-cost:  359
c ---[1672]---> BDD-cost:  350
c ---[1671]---> BDD-cost:  309
c ---[1670]---> BDD-cost:  350
c ---[1669]---> BDD-cost:  309
c ---[1668]---> BDD-cost:  350
c ---[1667]---> BDD-cost:  321
c ---[1666]---> BDD-cost:  350
c ---[1665]---> BDD-cost:  343
c ---[1664]---> BDD-cost:  321
c ---[1663]---> BDD-cost:  350
c ---[1662]---> BDD-cost:  277
c ---[1661]---> BDD-cost:  350
c ---[1660]---> BDD-cost:  277
c ---[1659]---> BDD-cost:  350
c ---[1658]---> BDD-cost:  295
c ---[1657]---> BDD-cost:  350
c ---[1656]---> BDD-cost:  295
c ---[1655]---> BDD-cost:  350
c ---[1654]---> BDD-cost:  332
c ---[1653]---> BDD-cost:  351
c ---[1652]---> BDD-cost:  350
c ---[1651]---> BDD-cost:  351
c ---[1650]---> BDD-cost:  350
c ---[1649]---> BDD-cost:  345
c ---[1648]---> BDD-cost:  350
c ---[1647]---> BDD-cost:  345
c ---[1646]---> BDD-cost:  350
c ---[1645]---> BDD-cost:  340
c ---[1644]---> BDD-cost:  350
c ---[1643]---> BDD-cost:  343
c ---[1642]---> BDD-cost:  340
c ---[1641]---> BDD-cost:  350
c ---[1640]---> BDD-cost:  261
c ---[1639]---> BDD-cost:  350
c ---[1638]---> BDD-cost:  261
c ---[1637]---> BDD-cost:  350
c ---[1636]---> BDD-cost:  322
c ---[1635]---> BDD-cost:  350
c ---[1634]---> BDD-cost:  322
c ---[1633]---> BDD-cost:  350
c ---[1632]---> BDD-cost:  332
c ---[1631]---> BDD-cost:  352
c ---[1630]---> BDD-cost:  350
c ---[1629]---> BDD-cost:  352
c ---[1628]---> BDD-cost:  350
c ---[1627]---> BDD-cost:  329
c ---[1626]---> BDD-cost:  350
c ---[1625]---> BDD-cost:  329
c ---[1624]---> BDD-cost:  350
c ---[1623]---> BDD-cost:  310
c ---[1622]---> BDD-cost:  350
c ---[1621]---> BDD-cost:  298
c ---[1620]---> BDD-cost:  342
c ---[1619]---> BDD-cost:  310
c ---[1618]---> BDD-cost:  347
c ---[1617]---> BDD-cost:  314
c ---[1616]---> BDD-cost:  347
c ---[1615]---> BDD-cost:  314
c ---[1614]---> BDD-cost:  347
c ---[1613]---> BDD-cost:  332
c ---[1612]---> BDD-cost:  347
c ---[1611]---> BDD-cost:  332
c ---[1610]---> BDD-cost:  347
c ---[1609]---> BDD-cost:  332
c ---[1608]---> BDD-cost:  293
c ---[1607]---> BDD-cost:  347
c ---[1606]---> BDD-cost:  293
c ---[1605]---> BDD-cost:  347
c ---[1604]---> BDD-cost:  345
c ---[1603]---> BDD-cost:  347
c ---[1602]---> BDD-cost:  345
c ---[1601]---> BDD-cost:  347
c ---[1600]---> BDD-cost:  359
c ---[1599]---> BDD-cost:  347
c ---[1598]---> BDD-cost:  342
c ---[1597]---> BDD-cost:  359
c ---[1596]---> BDD-cost:  347
c ---[1595]---> BDD-cost:  309
c ---[1594]---> BDD-cost:  347
c ---[1593]---> BDD-cost:  309
c ---[1592]---> BDD-cost:  347
c ---[1591]---> BDD-cost:  321
c ---[1590]---> BDD-cost:  347
c ---[1589]---> BDD-cost:  321
c ---[1588]---> BDD-cost:  347
c ---[1587]---> BDD-cost:  332
c ---[1586]---> BDD-cost:  277
c ---[1585]---> BDD-cost:  347
c ---[1584]---> BDD-cost:  277
c ---[1583]---> BDD-cost:  347
c ---[1582]---> BDD-cost:  295
c ---[1581]---> BDD-cost:  347
c ---[1580]---> BDD-cost:  295
c ---[1579]---> BDD-cost:  347
c ---[1578]---> BDD-cost:  351
c ---[1577]---> BDD-cost:  347
c ---[1576]---> BDD-cost:  298
c ---[1575]---> BDD-cost:  351
c ---[1574]---> BDD-cost:  347
c ---[1573]---> BDD-cost:  345
c ---[1572]---> BDD-cost:  347
c ---[1571]---> BDD-cost:  345
c ---[1570]---> BDD-cost:  347
c ---[1569]---> BDD-cost:  340
c ---[1568]---> BDD-cost:  347
c ---[1567]---> BDD-cost:  340
c ---[1566]---> BDD-cost:  347
c ---[1565]---> BDD-cost:  332
c ---[1564]---> BDD-cost:  261
c ---[1563]---> BDD-cost:  347
c ---[1562]---> BDD-cost:  261
c ---[1561]---> BDD-cost:  347
c ---[1560]---> BDD-cost:  322
c ---[1559]---> BDD-cost:  347
c ---[1558]---> BDD-cost:  322
c ---[1557]---> BDD-cost:  347
c ---[1556]---> BDD-cost:  352
c ---[1555]---> BDD-cost:  347
c ---[1554]---> BDD-cost:  298
c ---[1553]---> BDD-cost:  352
c ---[1552]---> BDD-cost:  347
c ---[1551]---> BDD-cost:  329
c ---[1550]---> BDD-cost:  347
c ---[1549]---> BDD-cost:  329
c ---[1548]---> BDD-cost:  347
c ---[1547]---> BDD-cost:  310
c ---[1546]---> BDD-cost:  347
c ---[1545]---> BDD-cost:  310
c ---[1544]---> BDD-cost:  314
c ---[1543]---> BDD-cost:  332
c ---[1542]---> BDD-cost:  332
c ---[1541]---> BDD-cost:  314
c ---[1540]---> BDD-cost:  332
c ---[1539]---> BDD-cost:  314
c ---[1538]---> BDD-cost:  293
c ---[1537]---> BDD-cost:  314
c ---[1536]---> BDD-cost:  293
c ---[1535]---> BDD-cost:  314
c ---[1534]---> BDD-cost:  345
c ---[1533]---> BDD-cost:  314
c ---[1532]---> BDD-cost:  292
c ---[1531]---> BDD-cost:  345
c ---[1530]---> BDD-cost:  314
c ---[1529]---> BDD-cost:  359
c ---[1528]---> BDD-cost:  314
c ---[1527]---> BDD-cost:  359
c ---[1526]---> BDD-cost:  314
c ---[1525]---> BDD-cost:  309
c ---[1524]---> BDD-cost:  314
c ---[1523]---> BDD-cost:  309
c ---[1522]---> BDD-cost:  314
c ---[1521]---> BDD-cost:  332
c ---[1520]---> BDD-cost:  321
c ---[1519]---> BDD-cost:  314
c ---[1518]---> BDD-cost:  321
c ---[1517]---> BDD-cost:  314
c ---[1516]---> BDD-cost:  277
c ---[1515]---> BDD-cost:  314
c ---[1514]---> BDD-cost:  277
c ---[1513]---> BDD-cost:  314
c ---[1512]---> BDD-cost:  295
c ---[1511]---> BDD-cost:  314
c ---[1510]---> BDD-cost:  352
c ---[1509]---> BDD-cost:  292
c ---[1508]---> BDD-cost:  295
c ---[1507]---> BDD-cost:  314
c ---[1506]---> BDD-cost:  351
c ---[1505]---> BDD-cost:  314
c ---[1504]---> BDD-cost:  351
c ---[1503]---> BDD-cost:  314
c ---[1502]---> BDD-cost:  345
c ---[1501]---> BDD-cost:  314
c ---[1500]---> BDD-cost:  345
c ---[1499]---> BDD-cost:  314
c ---[1498]---> BDD-cost:  332
c ---[1497]---> BDD-cost:  340
c ---[1496]---> BDD-cost:  314
c ---[1495]---> BDD-cost:  340
c ---[1494]---> BDD-cost:  314
c ---[1493]---> BDD-cost:  261
c ---[1492]---> BDD-cost:  314
c ---[1491]---> BDD-cost:  261
c ---[1490]---> BDD-cost:  314
c ---[1489]---> BDD-cost:  322
c ---[1488]---> BDD-cost:  314
c ---[1487]---> BDD-cost:  292
c ---[1486]---> BDD-cost:  322
c ---[1485]---> BDD-cost:  314
c ---[1484]---> BDD-cost:  352
c ---[1483]---> BDD-cost:  314
c ---[1482]---> BDD-cost:  352
c ---[1481]---> BDD-cost:  314
c ---[1480]---> BDD-cost:  329
c ---[1479]---> BDD-cost:  314
c ---[1478]---> BDD-cost:  329
c ---[1477]---> BDD-cost:  314
c ---[1476]---> BDD-cost:  332
c ---[1475]---> BDD-cost:  310
c ---[1474]---> BDD-cost:  314
c ---[1473]---> BDD-cost:  310
c ---[1472]---> BDD-cost:  332
c ---[1471]---> BDD-cost:  293
c ---[1470]---> BDD-cost:  332
c ---[1469]---> BDD-cost:  293
c ---[1468]---> BDD-cost:  332
c ---[1467]---> BDD-cost:  345
c ---[1466]---> BDD-cost:  332
c ---[1465]---> BDD-cost:  292
c ---[1464]---> BDD-cost:  345
c ---[1463]---> BDD-cost:  332
c ---[1462]---> BDD-cost:  359
c ---[1461]---> BDD-cost:  332
c ---[1460]---> BDD-cost:  359
c ---[1459]---> BDD-cost:  332
c ---[1458]---> BDD-cost:  309
c ---[1457]---> BDD-cost:  332
c ---[1456]---> BDD-cost:  309
c ---[1455]---> BDD-cost:  332
c ---[1454]---> BDD-cost:  332
c ---[1453]---> BDD-cost:  321
c ---[1452]---> BDD-cost:  332
c ---[1451]---> BDD-cost:  321
c ---[1450]---> BDD-cost:  332
c ---[1449]---> BDD-cost:  277
c ---[1448]---> BDD-cost:  332
c ---[1447]---> BDD-cost:  277
c ---[1446]---> BDD-cost:  332
c ---[1445]---> BDD-cost:  295
c ---[1444]---> BDD-cost:  332
c ---[1443]---> BDD-cost:  340
c ---[1442]---> BDD-cost:  295
c ---[1441]---> BDD-cost:  332
c ---[1440]---> BDD-cost:  351
c ---[1439]---> BDD-cost:  332
c ---[1438]---> BDD-cost:  351
c ---[1437]---> BDD-cost:  332
c ---[1436]---> BDD-cost:  345
c ---[1435]---> BDD-cost:  332
c ---[1434]---> BDD-cost:  345
c ---[1433]---> BDD-cost:  332
c ---[1432]---> BDD-cost:  332
c ---[1431]---> BDD-cost:  340
c ---[1430]---> BDD-cost:  332
c ---[1429]---> BDD-cost:  340
c ---[1428]---> BDD-cost:  332
c ---[1427]---> BDD-cost:  261
c ---[1426]---> BDD-cost:  332
c ---[1425]---> BDD-cost:  261
c ---[1424]---> BDD-cost:  332
c ---[1423]---> BDD-cost:  322
c ---[1422]---> BDD-cost:  332
c ---[1421]---> BDD-cost:  340
c ---[1420]---> BDD-cost:  322
c ---[1419]---> BDD-cost:  332
c ---[1418]---> BDD-cost:  352
c ---[1417]---> BDD-cost:  332
c ---[1416]---> BDD-cost:  352
c ---[1415]---> BDD-cost:  332
c ---[1414]---> BDD-cost:  329
c ---[1413]---> BDD-cost:  332
c ---[1412]---> BDD-cost:  329
c ---[1411]---> BDD-cost:  332
c ---[1410]---> BDD-cost:  332
c ---[1409]---> BDD-cost:  310
c ---[1408]---> BDD-cost:  332
c ---[1407]---> BDD-cost:  310
c ---[1406]---> BDD-cost:  293
c ---[1405]---> BDD-cost:  345
c ---[1404]---> BDD-cost:  293
c ---[1403]---> BDD-cost:  345
c ---[1402]---> BDD-cost:  293
c ---[1401]---> BDD-cost:  359
c ---[1400]---> BDD-cost:  293
c ---[1399]---> BDD-cost:  298
c ---[1398]---> BDD-cost:  259
c ---[1397]---> BDD-cost:  359
c ---[1396]---> BDD-cost:  293
c ---[1395]---> BDD-cost:  309
c ---[1394]---> BDD-cost:  293
c ---[1393]---> BDD-cost:  309
c ---[1392]---> BDD-cost:  293
c ---[1391]---> BDD-cost:  321
c ---[1390]---> BDD-cost:  293
c ---[1389]---> BDD-cost:  321
c ---[1388]---> BDD-cost:  293
c ---[1387]---> BDD-cost:  332
c ---[1386]---> BDD-cost:  277
c ---[1385]---> BDD-cost:  293
c ---[1384]---> BDD-cost:  277
c ---[1383]---> BDD-cost:  293
c ---[1382]---> BDD-cost:  295
c ---[1381]---> BDD-cost:  293
c ---[1380]---> BDD-cost:  295
c ---[1379]---> BDD-cost:  293
c ---[1378]---> BDD-cost:  351
c ---[1377]---> BDD-cost:  293
c ---[1376]---> BDD-cost:  259
c ---[1375]---> BDD-cost:  351
c ---[1374]---> BDD-cost:  293
c ---[1373]---> BDD-cost:  345
c ---[1372]---> BDD-cost:  293
c ---[1371]---> BDD-cost:  345
c ---[1370]---> BDD-cost:  293
c ---[1369]---> BDD-cost:  340
c ---[1368]---> BDD-cost:  293
c ---[1367]---> BDD-cost:  340
c ---[1366]---> BDD-cost:  293
c ---[1365]---> BDD-cost:  332
c ---[1364]---> BDD-cost:  261
c ---[1363]---> BDD-cost:  293
c ---[1362]---> BDD-cost:  261
c ---[1361]---> BDD-cost:  293
c ---[1360]---> BDD-cost:  322
c ---[1359]---> BDD-cost:  293
c ---[1358]---> BDD-cost:  322
c ---[1357]---> BDD-cost:  293
c ---[1356]---> BDD-cost:  352
c ---[1355]---> BDD-cost:  293
c ---[1354]---> BDD-cost:  274
c ---[1353]---> BDD-cost:  352
c ---[1352]---> BDD-cost:  293
c ---[1351]---> BDD-cost:  329
c ---[1350]---> BDD-cost:  293
c ---[1349]---> BDD-cost:  329
c ---[1348]---> BDD-cost:  293
c ---[1347]---> BDD-cost:  310
c ---[1346]---> BDD-cost:  293
c ---[1345]---> BDD-cost:  310
c ---[1344]---> BDD-cost:  345
c ---[1343]---> BDD-cost:  332
c ---[1342]---> BDD-cost:  359
c ---[1341]---> BDD-cost:  345
c ---[1340]---> BDD-cost:  359
c ---[1339]---> BDD-cost:  345
c ---[1338]---> BDD-cost:  309
c ---[1337]---> BDD-cost:  345
c ---[1336]---> BDD-cost:  309
c ---[1335]---> BDD-cost:  345
c ---[1334]---> BDD-cost:  321
c ---[1333]---> BDD-cost:  345
c ---[1332]---> BDD-cost:  274
c ---[1331]---> BDD-cost:  321
c ---[1330]---> BDD-cost:  345
c ---[1329]---> BDD-cost:  277
c ---[1328]---> BDD-cost:  345
c ---[1327]---> BDD-cost:  277
c ---[1326]---> BDD-cost:  345
c ---[1325]---> BDD-cost:  295
c ---[1324]---> BDD-cost:  345
c ---[1323]---> BDD-cost:  295
c ---[1322]---> BDD-cost:  345
c ---[1321]---> BDD-cost:  332
c ---[1320]---> BDD-cost:  351
c ---[1319]---> BDD-cost:  345
c ---[1318]---> BDD-cost:  351
c ---[1317]---> BDD-cost:  345
c ---[1316]---> BDD-cost:  345
c ---[1315]---> BDD-cost:  345
c ---[1314]---> BDD-cost:  345
c ---[1313]---> BDD-cost:  345
c ---[1312]---> BDD-cost:  340
c ---[1311]---> BDD-cost:  345
c ---[1310]---> BDD-cost:  350
c ---[1309]---> BDD-cost:  340
c ---[1308]---> BDD-cost:  345
c ---[1307]---> BDD-cost:  261
c ---[1306]---> BDD-cost:  345
c ---[1305]---> BDD-cost:  261
c ---[1304]---> BDD-cost:  345
c ---[1303]---> BDD-cost:  322
c ---[1302]---> BDD-cost:  345
c ---[1301]---> BDD-cost:  322
c ---[1300]---> BDD-cost:  345
c ---[1299]---> BDD-cost:  332
c ---[1298]---> BDD-cost:  352
c ---[1297]---> BDD-cost:  345
c ---[1296]---> BDD-cost:  352
c ---[1295]---> BDD-cost:  345
c ---[1294]---> BDD-cost:  329
c ---[1293]---> BDD-cost:  345
c ---[1292]---> BDD-cost:  329
c ---[1291]---> BDD-cost:  345
c ---[1290]---> BDD-cost:  310
c ---[1289]---> BDD-cost:  345
c ---[1288]---> BDD-cost:  330
c ---[1287]---> BDD-cost:  350
c ---[1286]---> BDD-cost:  310
c ---[1285]---> BDD-cost:  359
c ---[1284]---> BDD-cost:  309
c ---[1283]---> BDD-cost:  359
c ---[1282]---> BDD-cost:  309
c ---[1281]---> BDD-cost:  359
c ---[1280]---> BDD-cost:  321
c ---[1279]---> BDD-cost:  359
c ---[1278]---> BDD-cost:  321
c ---[1277]---> BDD-cost:  359
c ---[1276]---> BDD-cost:  332
c ---[1275]---> BDD-cost:  277
c ---[1274]---> BDD-cost:  359
c ---[1273]---> BDD-cost:  277
c ---[1272]---> BDD-cost:  359
c ---[1271]---> BDD-cost:  295
c ---[1270]---> BDD-cost:  359
c ---[1269]---> BDD-cost:  295
c ---[1268]---> BDD-cost:  359
c ---[1267]---> BDD-cost:  351
c ---[1266]---> BDD-cost:  359
c ---[1265]---> BDD-cost:  347
c ---[1264]---> BDD-cost:  351
c ---[1263]---> BDD-cost:  359
c ---[1262]---> BDD-cost:  345
c ---[1261]---> BDD-cost:  359
c ---[1260]---> BDD-cost:  345
c ---[1259]---> BDD-cost:  359
c ---[1258]---> BDD-cost:  340
c ---[1257]---> BDD-cost:  359
c ---[1256]---> BDD-cost:  340
c ---[1255]---> BDD-cost:  359
c ---[1254]---> BDD-cost:  332
c ---[1253]---> BDD-cost:  261
c ---[1252]---> BDD-cost:  359
c ---[1251]---> BDD-cost:  261
c ---[1250]---> BDD-cost:  359
c ---[1249]---> BDD-cost:  322
c ---[1248]---> BDD-cost:  359
c ---[1247]---> BDD-cost:  322
c ---[1246]---> BDD-cost:  359
c ---[1245]---> BDD-cost:  352
c ---[1244]---> BDD-cost:  359
c ---[1243]---> BDD-cost:  347
c ---[1242]---> BDD-cost:  352
c ---[1241]---> BDD-cost:  359
c ---[1240]---> BDD-cost:  329
c ---[1239]---> BDD-cost:  359
c ---[1238]---> BDD-cost:  329
c ---[1237]---> BDD-cost:  359
c ---[1236]---> BDD-cost:  310
c ---[1235]---> BDD-cost:  359
c ---[1234]---> BDD-cost:  310
c ---[1233]---> BDD-cost:  309
c ---[1232]---> BDD-cost:  332
c ---[1231]---> BDD-cost:  321
c ---[1230]---> BDD-cost:  309
c ---[1229]---> BDD-cost:  321
c ---[1228]---> BDD-cost:  309
c ---[1227]---> BDD-cost:  277
c ---[1226]---> BDD-cost:  309
c ---[1225]---> BDD-cost:  277
c ---[1224]---> BDD-cost:  309
c ---[1223]---> BDD-cost:  295
c ---[1222]---> BDD-cost:  309
c ---[1221]---> BDD-cost:  314
c ---[1220]---> BDD-cost:  295
c ---[1219]---> BDD-cost:  309
c ---[1218]---> BDD-cost:  351
c ---[1217]---> BDD-cost:  309
c ---[1216]---> BDD-cost:  351
c ---[1215]---> BDD-cost:  309
c ---[1214]---> BDD-cost:  345
c ---[1213]---> BDD-cost:  309
c ---[1212]---> BDD-cost:  345
c ---[1211]---> BDD-cost:  309
c ---[1210]---> BDD-cost:  332
c ---[1209]---> BDD-cost:  340
c ---[1208]---> BDD-cost:  309
c ---[1207]---> BDD-cost:  340
c ---[1206]---> BDD-cost:  309
c ---[1205]---> BDD-cost:  261
c ---[1204]---> BDD-cost:  309
c ---[1203]---> BDD-cost:  261
c ---[1202]---> BDD-cost:  309
c ---[1201]---> BDD-cost:  322
c ---[1200]---> BDD-cost:  309
c ---[1199]---> BDD-cost:  314
c ---[1198]---> BDD-cost:  322
c ---[1197]---> BDD-cost:  309
c ---[1196]---> BDD-cost:  352
c ---[1195]---> BDD-cost:  309
c ---[1194]---> BDD-cost:  352
c ---[1193]---> BDD-cost:  309
c ---[1192]---> BDD-cost:  329
c ---[1191]---> BDD-cost:  309
c ---[1190]---> BDD-cost:  329
c ---[1189]---> BDD-cost:  309
c ---[1188]---> BDD-cost:  332
c ---[1187]---> BDD-cost:  310
c ---[1186]---> BDD-cost:  309
c ---[1185]---> BDD-cost:  310
c ---[1184]---> BDD-cost:  321
c ---[1183]---> BDD-cost:  277
c ---[1182]---> BDD-cost:  321
c ---[1181]---> BDD-cost:  277
c ---[1180]---> BDD-cost:  321
c ---[1179]---> BDD-cost:  295
c ---[1178]---> BDD-cost:  321
c ---[1177]---> BDD-cost:  298
c ---[1176]---> BDD-cost:  332
c ---[1175]---> BDD-cost:  295
c ---[1174]---> BDD-cost:  321
c ---[1173]---> BDD-cost:  351
c ---[1172]---> BDD-cost:  321
c ---[1171]---> BDD-cost:  351
c ---[1170]---> BDD-cost:  321
c ---[1169]---> BDD-cost:  345
c ---[1168]---> BDD-cost:  321
c ---[1167]---> BDD-cost:  345
c ---[1166]---> BDD-cost:  321
c ---[1165]---> BDD-cost:  332
c ---[1164]---> BDD-cost:  340
c ---[1163]---> BDD-cost:  321
c ---[1162]---> BDD-cost:  340
c ---[1161]---> BDD-cost:  321
c ---[1160]---> BDD-cost:  261
c ---[1159]---> BDD-cost:  321
c ---[1158]---> BDD-cost:  261
c ---[1157]---> BDD-cost:  321
c ---[1156]---> BDD-cost:  322
c ---[1155]---> BDD-cost:  321
c ---[1154]---> BDD-cost:  332
c ---[1153]---> BDD-cost:  322
c ---[1152]---> BDD-cost:  321
c ---[1151]---> BDD-cost:  352
c ---[1150]---> BDD-cost:  321
c ---[1149]---> BDD-cost:  352
c ---[1148]---> BDD-cost:  321
c ---[1147]---> BDD-cost:  329
c ---[1146]---> BDD-cost:  321
c ---[1145]---> BDD-cost:  329
c ---[1144]---> BDD-cost:  321
c ---[1143]---> BDD-cost:  332
c ---[1142]---> BDD-cost:  310
c ---[1141]---> BDD-cost:  321
c ---[1140]---> BDD-cost:  310
c ---[1139]---> BDD-cost:  277
c ---[1138]---> BDD-cost:  295
c ---[1137]---> BDD-cost:  277
c ---[1136]---> BDD-cost:  295
c ---[1135]---> BDD-cost:  277
c ---[1134]---> BDD-cost:  351
c ---[1133]---> BDD-cost:  277
c ---[1132]---> BDD-cost:  293
c ---[1131]---> BDD-cost:  351
c ---[1130]---> BDD-cost:  277
c ---[1129]---> BDD-cost:  345
c ---[1128]---> BDD-cost:  277
c ---[1127]---> BDD-cost:  345
c ---[1126]---> BDD-cost:  277
c ---[1125]---> BDD-cost:  340
c ---[1124]---> BDD-cost:  277
c ---[1123]---> BDD-cost:  340
c ---[1122]---> BDD-cost:  277
c ---[1121]---> BDD-cost:  332
c ---[1120]---> BDD-cost:  261
c ---[1119]---> BDD-cost:  277
c ---[1118]---> BDD-cost:  261
c ---[1117]---> BDD-cost:  277
c ---[1116]---> BDD-cost:  322
c ---[1115]---> BDD-cost:  277
c ---[1114]---> BDD-cost:  322
c ---[1113]---> BDD-cost:  277
c ---[1112]---> BDD-cost:  352
c ---[1111]---> BDD-cost:  277
c ---[1110]---> BDD-cost:  293
c ---[1109]---> BDD-cost:  352
c ---[1108]---> BDD-cost:  277
c ---[1107]---> BDD-cost:  329
c ---[1106]---> BDD-cost:  277
c ---[1105]---> BDD-cost:  329
c ---[1104]---> BDD-cost:  277
c ---[1103]---> BDD-cost:  310
c ---[1102]---> BDD-cost:  277
c ---[1101]---> BDD-cost:  310
c ---[1100]---> BDD-cost:  295
c ---[1099]---> BDD-cost:  332
c ---[1098]---> BDD-cost:  351
c ---[1097]---> BDD-cost:  295
c ---[1096]---> BDD-cost:  351
c ---[1095]---> BDD-cost:  295
c ---[1094]---> BDD-cost:  345
c ---[1093]---> BDD-cost:  295
c ---[1092]---> BDD-cost:  345
c ---[1091]---> BDD-cost:  295
c ---[1090]---> BDD-cost:  340
c ---[1089]---> BDD-cost:  295
c ---[1088]---> BDD-cost:  345
c ---[1087]---> BDD-cost:  340
c ---[1086]---> BDD-cost:  295
c ---[1085]---> BDD-cost:  261
c ---[1084]---> BDD-cost:  295
c ---[1083]---> BDD-cost:  261
c ---[1082]---> BDD-cost:  295
c ---[1081]---> BDD-cost:  322
c ---[1080]---> BDD-cost:  295
c ---[1079]---> BDD-cost:  322
c ---[1078]---> BDD-cost:  295
c ---[1077]---> BDD-cost:  332
c ---[1076]---> BDD-cost:  352
c ---[1075]---> BDD-cost:  295
c ---[1074]---> BDD-cost:  352
c ---[1073]---> BDD-cost:  295
c ---[1072]---> BDD-cost:  329
c ---[1071]---> BDD-cost:  295
c ---[1070]---> BDD-cost:  329
c ---[1069]---> BDD-cost:  295
c ---[1068]---> BDD-cost:  310
c ---[1067]---> BDD-cost:  295
c ---[1066]---> BDD-cost:  332
c ---[1065]---> BDD-cost:  330
c ---[1064]---> BDD-cost:  345
c ---[1063]---> BDD-cost:  310
c ---[1062]---> BDD-cost:  351
c ---[1061]---> BDD-cost:  345
c ---[1060]---> BDD-cost:  351
c ---[1059]---> BDD-cost:  345
c ---[1058]---> BDD-cost:  351
c ---[1057]---> BDD-cost:  340
c ---[1056]---> BDD-cost:  351
c ---[1055]---> BDD-cost:  340
c ---[1054]---> BDD-cost:  351
c ---[1053]---> BDD-cost:  332
c ---[1052]---> BDD-cost:  261
c ---[1051]---> BDD-cost:  351
c ---[1050]---> BDD-cost:  261
c ---[1049]---> BDD-cost:  351
c ---[1048]---> BDD-cost:  322
c ---[1047]---> BDD-cost:  351
c ---[1046]---> BDD-cost:  322
c ---[1045]---> BDD-cost:  351
c ---[1044]---> BDD-cost:  352
c ---[1043]---> BDD-cost:  351
c ---[1042]---> BDD-cost:  359
c ---[1041]---> BDD-cost:  352
c ---[1040]---> BDD-cost:  351
c ---[1039]---> BDD-cost:  329
c ---[1038]---> BDD-cost:  351
c ---[1037]---> BDD-cost:  329
c ---[1036]---> BDD-cost:  351
c ---[1035]---> BDD-cost:  310
c ---[1034]---> BDD-cost:  351
c ---[1033]---> BDD-cost:  310
c ---[1032]---> BDD-cost:  345
c ---[1031]---> BDD-cost:  332
c ---[1030]---> BDD-cost:  340
c ---[1029]---> BDD-cost:  345
c ---[1028]---> BDD-cost:  340
c ---[1027]---> BDD-cost:  345
c ---[1026]---> BDD-cost:  261
c ---[1025]---> BDD-cost:  345
c ---[1024]---> BDD-cost:  261
c ---[1023]---> BDD-cost:  345
c ---[1022]---> BDD-cost:  322
c ---[1021]---> BDD-cost:  345
c ---[1020]---> BDD-cost:  359
c ---[1019]---> BDD-cost:  322
c ---[1018]---> BDD-cost:  345
c ---[1017]---> BDD-cost:  352
c ---[1016]---> BDD-cost:  345
c ---[1015]---> BDD-cost:  352
c ---[1014]---> BDD-cost:  345
c ---[1013]---> BDD-cost:  329
c ---[1012]---> BDD-cost:  345
c ---[1011]---> BDD-cost:  329
c ---[1010]---> BDD-cost:  345
c ---[1009]---> BDD-cost:  332
c ---[1008]---> BDD-cost:  310
c ---[1007]---> BDD-cost:  345
c ---[1006]---> BDD-cost:  310
c ---[1005]---> BDD-cost:  340
c ---[1004]---> BDD-cost:  261
c ---[1003]---> BDD-cost:  340
c ---[1002]---> BDD-cost:  261
c ---[1001]---> BDD-cost:  340
c ---[1000]---> BDD-cost:  322
c ---[ 999]---> BDD-cost:  340
c ---[ 998]---> BDD-cost:  309
c ---[ 997]---> BDD-cost:  322
c ---[ 996]---> BDD-cost:  340
c ---[ 995]---> BDD-cost:  352
c ---[ 994]---> BDD-cost:  340
c ---[ 993]---> BDD-cost:  352
c ---[ 992]---> BDD-cost:  340
c ---[ 991]---> BDD-cost:  329
c ---[ 990]---> BDD-cost:  340
c ---[ 989]---> BDD-cost:  329
c ---[ 988]---> BDD-cost:  340
c ---[ 987]---> BDD-cost:  332
c ---[ 986]---> BDD-cost:  310
c ---[ 985]---> BDD-cost:  340
c ---[ 984]---> BDD-cost:  310
c ---[ 983]---> BDD-cost:  261
c ---[ 982]---> BDD-cost:  322
c ---[ 981]---> BDD-cost:  261
c ---[ 980]---> BDD-cost:  322
c ---[ 979]---> BDD-cost:  261
c ---[ 978]---> BDD-cost:  352
c ---[ 977]---> BDD-cost:  261
c ---[ 976]---> BDD-cost:  309
c ---[ 975]---> BDD-cost:  352
c ---[ 974]---> BDD-cost:  261
c ---[ 973]---> BDD-cost:  329
c ---[ 972]---> BDD-cost:  261
c ---[ 971]---> BDD-cost:  329
c ---[ 970]---> BDD-cost:  261
c ---[ 969]---> BDD-cost:  310
c ---[ 968]---> BDD-cost:  261
c ---[ 967]---> BDD-cost:  310
c ---[ 966]---> BDD-cost:  322
c ---[ 965]---> BDD-cost:  332
c ---[ 964]---> BDD-cost:  352
c ---[ 963]---> BDD-cost:  322
c ---[ 962]---> BDD-cost:  352
c ---[ 961]---> BDD-cost:  322
c ---[ 960]---> BDD-cost:  329
c ---[ 959]---> BDD-cost:  322
c ---[ 958]---> BDD-cost:  329
c ---[ 957]---> BDD-cost:  322
c ---[ 956]---> BDD-cost:  310
c ---[ 955]---> BDD-cost:  322
c ---[ 954]---> BDD-cost:  298
c ---[ 953]---> BDD-cost:  321
c ---[ 952]---> BDD-cost:  310
c ---[ 951]---> BDD-cost:  352
c ---[ 950]---> BDD-cost:  329
c ---[ 949]---> BDD-cost:  352
c ---[ 948]---> BDD-cost:  329
c ---[ 947]---> BDD-cost:  352
c ---[ 946]---> BDD-cost:  310
c ---[ 945]---> BDD-cost:  352
c ---[ 944]---> BDD-cost:  310
c ---[ 943]---> BDD-cost:  329
c ---[ 942]---> BDD-cost:  332
c ---[ 941]---> BDD-cost:  310
c ---[ 940]---> BDD-cost:  329
c ---[ 939]---> BDD-cost:  310
c ---[ 938]---> BDD-cost:  145
c ---[ 937]---> BDD-cost:  145
c ---[ 936]---> BDD-cost:  157
c ---[ 935]---> BDD-cost:  157
c ---[ 934]---> BDD-cost:  125
c ---[ 933]---> BDD-cost:  125
c ---[ 932]---> BDD-cost:  153
c ---[ 931]---> BDD-cost:  321
c ---[ 930]---> BDD-cost:  153
c ---[ 929]---> BDD-cost:  157
c ---[ 928]---> BDD-cost:  157
c ---[ 927]---> BDD-cost:  157
c ---[ 926]---> BDD-cost:  157
c ---[ 925]---> BDD-cost:  149
c ---[ 924]---> BDD-cost:  149
c ---[ 923]---> BDD-cost:  157
c ---[ 922]---> BDD-cost:  157
c ---[ 921]---> BDD-cost:  145
c ---[ 920]---> BDD-cost:  332
c ---[ 919]---> BDD-cost:  145
c ---[ 918]---> BDD-cost:  141
c ---[ 917]---> BDD-cost:  141
c ---[ 916]---> BDD-cost:  141
c ---[ 915]---> BDD-cost:  141
c ---[ 914]---> BDD-cost:  154
c ---[ 913]---> BDD-cost:  154
c ---[ 912]---> BDD-cost:  123
c ---[ 911]---> BDD-cost:  123
c ---[ 910]---> BDD-cost:  127
c ---[ 909]---> BDD-cost:  277
c ---[ 908]---> BDD-cost:  127
c ---[ 907]---> BDD-cost:  153
c ---[ 906]---> BDD-cost:  153
c ---[ 905]---> BDD-cost:  154
c ---[ 904]---> BDD-cost:  154
c ---[ 903]---> BDD-cost:  143
c ---[ 902]---> BDD-cost:  143
c ---[ 901]---> BDD-cost:  144
c ---[ 900]---> BDD-cost:  144
c ---[ 899]---> BDD-cost:  152
c ---[ 898]---> BDD-cost:  332
c ---[ 897]---> BDD-cost:  152
c ---[ 896]---> BDD-cost:  151
c ---[ 895]---> BDD-cost:  151
c ---[ 894]---> BDD-cost:  160
c ---[ 893]---> BDD-cost:  160
c ---[ 892]---> BDD-cost:  141
c ---[ 891]---> BDD-cost:  141
c ---[ 890]---> BDD-cost:  146
c ---[ 889]---> BDD-cost:  146
c ---[ 888]---> BDD-cost:  129
c ---[ 887]---> BDD-cost:  277
c ---[ 886]---> BDD-cost:  129
c ---[ 885]---> BDD-cost:  130
c ---[ 884]---> BDD-cost:  130
c ---[ 883]---> BDD-cost:  157
c ---[ 882]---> BDD-cost:  157
c ---[ 881]---> BDD-cost:  148
c ---[ 880]---> BDD-cost:  148
c ---[ 879]---> BDD-cost:  154
c ---[ 878]---> BDD-cost:  154
c ---[ 877]---> BDD-cost:  123
c ---[ 876]---> BDD-cost:  332
c ---[ 875]---> BDD-cost:  123
c ---[ 874]---> BDD-cost:  149
c ---[ 873]---> BDD-cost:  149
c ---[ 872]---> BDD-cost:  157
c ---[ 871]---> BDD-cost:  157
c ---[ 870]---> BDD-cost:  150
c ---[ 869]---> BDD-cost:  150
c ---[ 868]---> BDD-cost:  145
c ---[ 867]---> BDD-cost:  145
c ---[ 866]---> BDD-cost:  295
c ---[ 865]---> BDD-cost:  332
c ---[ 864]---> BDD-cost:  343
c ---[ 863]---> BDD-cost:  295
c ---[ 862]---> BDD-cost:  332
c ---[ 861]---> BDD-cost:  351
c ---[ 860]---> BDD-cost:  332
c ---[ 859]---> BDD-cost:  351
c ---[ 858]---> BDD-cost:  332
c ---[ 857]---> BDD-cost:  345
c ---[ 856]---> BDD-cost:  332
c ---[ 855]---> BDD-cost:  345
c ---[ 854]---> BDD-cost:  332
c ---[ 853]---> BDD-cost:  298
c ---[ 852]---> BDD-cost:  340
c ---[ 851]---> BDD-cost:  332
c ---[ 850]---> BDD-cost:  340
c ---[ 849]---> BDD-cost:  332
c ---[ 848]---> BDD-cost:  261
c ---[ 847]---> BDD-cost:  332
c ---[ 846]---> BDD-cost:  261
c ---[ 845]---> BDD-cost:  332
c ---[ 844]---> BDD-cost:  322
c ---[ 843]---> BDD-cost:  332
c ---[ 842]---> BDD-cost:  343
c ---[ 841]---> BDD-cost:  322
c ---[ 840]---> BDD-cost:  332
c ---[ 839]---> BDD-cost:  352
c ---[ 838]---> BDD-cost:  332
c ---[ 837]---> BDD-cost:  352
c ---[ 836]---> BDD-cost:  332
c ---[ 835]---> BDD-cost:  329
c ---[ 834]---> BDD-cost:  332
c ---[ 833]---> BDD-cost:  329
c ---[ 832]---> BDD-cost:  332
c ---[ 831]---> BDD-cost:  298
c ---[ 830]---> BDD-cost:  310
c ---[ 829]---> BDD-cost:  332
c ---[ 828]---> BDD-cost:  310
c ---[ 827]---> BDD-cost:  270
c ---[ 826]---> BDD-cost:  367
c ---[ 825]---> BDD-cost:  270
c ---[ 824]---> BDD-cost:  367
c ---[ 823]---> BDD-cost:  270
c ---[ 822]---> BDD-cost:  352
c ---[ 821]---> BDD-cost:  270
c ---[ 820]---> BDD-cost:  342
c ---[ 819]---> BDD-cost:  352
c ---[ 818]---> BDD-cost:  270
c ---[ 817]---> BDD-cost:  330
c ---[ 816]---> BDD-cost:  270
c ---[ 815]---> BDD-cost:  330
c ---[ 814]---> BDD-cost:  270
c ---[ 813]---> BDD-cost:  343
c ---[ 812]---> BDD-cost:  270
c ---[ 811]---> BDD-cost:  343
c ---[ 810]---> BDD-cost:  270
c ---[ 809]---> BDD-cost:  298
c ---[ 808]---> BDD-cost:  342
c ---[ 807]---> BDD-cost:  270
c ---[ 806]---> BDD-cost:  342
c ---[ 805]---> BDD-cost:  270
c ---[ 804]---> BDD-cost:  298
c ---[ 803]---> BDD-cost:  270
c ---[ 802]---> BDD-cost:  298
c ---[ 801]---> BDD-cost:  270
c ---[ 800]---> BDD-cost:  292
c ---[ 799]---> BDD-cost:  270
c ---[ 798]---> BDD-cost:  342
c ---[ 797]---> BDD-cost:  292
c ---[ 796]---> BDD-cost:  270
c ---[ 795]---> BDD-cost:  292
c ---[ 794]---> BDD-cost:  270
c ---[ 793]---> BDD-cost:  292
c ---[ 792]---> BDD-cost:  270
c ---[ 791]---> BDD-cost:  340
c ---[ 790]---> BDD-cost:  270
c ---[ 789]---> BDD-cost:  340
c ---[ 788]---> BDD-cost:  270
c ---[ 787]---> BDD-cost:  298
c ---[ 786]---> BDD-cost:  259
c ---[ 785]---> BDD-cost:  270
c ---[ 784]---> BDD-cost:  259
c ---[ 783]---> BDD-cost:  270
c ---[ 782]---> BDD-cost:  274
c ---[ 781]---> BDD-cost:  270
c ---[ 780]---> BDD-cost:  274
c ---[ 779]---> BDD-cost:  270
c ---[ 778]---> BDD-cost:  350
c ---[ 777]---> BDD-cost:  270
c ---[ 776]---> BDD-cost:  298
c ---[ 775]---> BDD-cost:  298
c ---[ 774]---> BDD-cost:  350
c ---[ 773]---> BDD-cost:  270
c ---[ 772]---> BDD-cost:  347
c ---[ 771]---> BDD-cost:  270
c ---[ 770]---> BDD-cost:  347
c ---[ 769]---> BDD-cost:  270
c ---[ 768]---> BDD-cost:  314
c ---[ 767]---> BDD-cost:  270
c ---[ 766]---> BDD-cost:  314
c ---[ 765]---> BDD-cost:  270
c ---[ 764]---> BDD-cost:  298
c ---[ 763]---> BDD-cost:  332
c ---[ 762]---> BDD-cost:  270
c ---[ 761]---> BDD-cost:  332
c ---[ 760]---> BDD-cost:  270
c ---[ 759]---> BDD-cost:  293
c ---[ 758]---> BDD-cost:  270
c ---[ 757]---> BDD-cost:  293
c ---[ 756]---> BDD-cost:  270
c ---[ 755]---> BDD-cost:  345
c ---[ 754]---> BDD-cost:  270
c ---[ 753]---> BDD-cost:  298
c ---[ 752]---> BDD-cost:  345
c ---[ 751]---> BDD-cost:  270
c ---[ 750]---> BDD-cost:  359
c ---[ 749]---> BDD-cost:  270
c ---[ 748]---> BDD-cost:  359
c ---[ 747]---> BDD-cost:  270
c ---[ 746]---> BDD-cost:  309
c ---[ 745]---> BDD-cost:  270
c ---[ 744]---> BDD-cost:  309
c ---[ 743]---> BDD-cost:  270
c ---[ 742]---> BDD-cost:  298
c ---[ 741]---> BDD-cost:  321
c ---[ 740]---> BDD-cost:  270
c ---[ 739]---> BDD-cost:  321
c ---[ 738]---> BDD-cost:  270
c ---[ 737]---> BDD-cost:  277
c ---[ 736]---> BDD-cost:  270
c ---[ 735]---> BDD-cost:  277
c ---[ 734]---> BDD-cost:  270
c ---[ 733]---> BDD-cost:  295
c ---[ 732]---> BDD-cost:  270
c ---[ 731]---> BDD-cost:  292
c ---[ 730]---> BDD-cost:  295
c ---[ 729]---> BDD-cost:  270
c ---[ 728]---> BDD-cost:  351
c ---[ 727]---> BDD-cost:  270
c ---[ 726]---> BDD-cost:  351
c ---[ 725]---> BDD-cost:  270
c ---[ 724]---> BDD-cost:  345
c ---[ 723]---> BDD-cost:  270
c ---[ 722]---> BDD-cost:  345
c ---[ 721]---> BDD-cost:  270
c ---[ 720]---> BDD-cost:  298
c ---[ 719]---> BDD-cost:  340
c ---[ 718]---> BDD-cost:  270
c ---[ 717]---> BDD-cost:  340
c ---[ 716]---> BDD-cost:  270
c ---[ 715]---> BDD-cost:  261
c ---[ 714]---> BDD-cost:  270
c ---[ 713]---> BDD-cost:  261
c ---[ 712]---> BDD-cost:  270
c ---[ 711]---> BDD-cost:  322
c ---[ 710]---> BDD-cost:  270
c ---[ 709]---> BDD-cost:  292
c ---[ 708]---> BDD-cost:  322
c ---[ 707]---> BDD-cost:  270
c ---[ 706]---> BDD-cost:  352
c ---[ 705]---> BDD-cost:  270
c ---[ 704]---> BDD-cost:  352
c ---[ 703]---> BDD-cost:  270
c ---[ 702]---> BDD-cost:  329
c ---[ 701]---> BDD-cost:  270
c ---[ 700]---> BDD-cost:  329
c ---[ 699]---> BDD-cost:  270
c ---[ 698]---> BDD-cost:  298
c ---[ 697]---> BDD-cost:  310
c ---[ 696]---> BDD-cost:  270
c ---[ 695]---> BDD-cost:  310
c ---[ 694]---> BDD-cost:  367
c ---[ 693]---> BDD-cost:  352
c ---[ 692]---> BDD-cost:  367
c ---[ 691]---> BDD-cost:  352
c ---[ 690]---> BDD-cost:  367
c ---[ 689]---> BDD-cost:  330
c ---[ 688]---> BDD-cost:  367
c ---[ 687]---> BDD-cost:  292
c ---[ 686]---> BDD-cost:  330
c ---[ 685]---> BDD-cost:  367
c ---[ 684]---> BDD-cost:  343
c ---[ 683]---> BDD-cost:  367
c ---[ 682]---> BDD-cost:  343
c ---[ 681]---> BDD-cost:  367
c ---[ 680]---> BDD-cost:  342
c ---[ 679]---> BDD-cost:  367
c ---[ 678]---> BDD-cost:  342
c ---[ 677]---> BDD-cost:  367
c ---[ 676]---> BDD-cost:  298
c ---[ 675]---> BDD-cost:  298
c ---[ 674]---> BDD-cost:  367
c ---[ 673]---> BDD-cost:  298
c ---[ 672]---> BDD-cost:  367
c ---[ 671]---> BDD-cost:  292
c ---[ 670]---> BDD-cost:  367
c ---[ 669]---> BDD-cost:  292
c ---[ 668]---> BDD-cost:  367
c ---[ 667]---> BDD-cost:  292
c ---[ 666]---> BDD-cost:  367
c ---[ 665]---> BDD-cost:  332
c ---[ 664]---> BDD-cost:  292
c ---[ 663]---> BDD-cost:  292
c ---[ 662]---> BDD-cost:  367
c ---[ 661]---> BDD-cost:  340
c ---[ 660]---> BDD-cost:  367
c ---[ 659]---> BDD-cost:  340
c ---[ 658]---> BDD-cost:  367
c ---[ 657]---> BDD-cost:  259
c ---[ 656]---> BDD-cost:  367
c ---[ 655]---> BDD-cost:  259
c ---[ 654]---> BDD-cost:  367
c ---[ 653]---> BDD-cost:  298
c ---[ 652]---> BDD-cost:  274
c ---[ 651]---> BDD-cost:  367
c ---[ 650]---> BDD-cost:  274
c ---[ 649]---> BDD-cost:  367
c ---[ 648]---> BDD-cost:  350
c ---[ 647]---> BDD-cost:  367
c ---[ 646]---> BDD-cost:  350
c ---[ 645]---> BDD-cost:  367
c ---[ 644]---> BDD-cost:  347
c ---[ 643]---> BDD-cost:  367
c ---[ 642]---> BDD-cost:  340
c ---[ 641]---> BDD-cost:  347
c ---[ 640]---> BDD-cost:  367
c ---[ 639]---> BDD-cost:  314
c ---[ 638]---> BDD-cost:  367
c ---[ 637]---> BDD-cost:  314
c ---[ 636]---> BDD-cost:  367
c ---[ 635]---> BDD-cost:  332
c ---[ 634]---> BDD-cost:  367
c ---[ 633]---> BDD-cost:  332
c ---[ 632]---> BDD-cost:  367
c ---[ 631]---> BDD-cost:  298
c ---[ 630]---> BDD-cost:  293
c ---[ 629]---> BDD-cost:  367
c ---[ 628]---> BDD-cost:  293
c ---[ 627]---> BDD-cost:  367
c ---[ 626]---> BDD-cost:  345
c ---[ 625]---> BDD-cost:  367
c ---[ 624]---> BDD-cost:  345
c ---[ 623]---> BDD-cost:  367
c ---[ 622]---> BDD-cost:  359
c ---[ 621]---> BDD-cost:  367
c ---[ 620]---> BDD-cost:  340
c ---[ 619]---> BDD-cost:  359
c ---[ 618]---> BDD-cost:  367
c ---[ 617]---> BDD-cost:  309
c ---[ 616]---> BDD-cost:  367
c ---[ 615]---> BDD-cost:  309
c ---[ 614]---> BDD-cost:  367
c ---[ 613]---> BDD-cost:  321
c ---[ 612]---> BDD-cost:  367
c ---[ 611]---> BDD-cost:  321
c ---[ 610]---> BDD-cost:  367
c ---[ 609]---> BDD-cost:  298
c ---[ 608]---> BDD-cost:  277
c ---[ 607]---> BDD-cost:  367
c ---[ 606]---> BDD-cost:  277
c ---[ 605]---> BDD-cost:  367
c ---[ 604]---> BDD-cost:  295
c ---[ 603]---> BDD-cost:  367
c ---[ 602]---> BDD-cost:  295
c ---[ 601]---> BDD-cost:  367
c ---[ 600]---> BDD-cost:  351
c ---[ 599]---> BDD-cost:  367
c ---[ 598]---> BDD-cost:  259
c ---[ 597]---> BDD-cost:  351
c ---[ 596]---> BDD-cost:  367
c ---[ 595]---> BDD-cost:  345
c ---[ 594]---> BDD-cost:  367
c ---[ 593]---> BDD-cost:  345
c ---[ 592]---> BDD-cost:  367
c ---[ 591]---> BDD-cost:  340
c ---[ 590]---> BDD-cost:  367
c ---[ 589]---> BDD-cost:  340
c ---[ 588]---> BDD-cost:  367
c ---[ 587]---> BDD-cost:  298
c ---[ 586]---> BDD-cost:  261
c ---[ 585]---> BDD-cost:  367
c ---[ 584]---> BDD-cost:  261
c ---[ 583]---> BDD-cost:  367
c ---[ 582]---> BDD-cost:  322
c ---[ 581]---> BDD-cost:  367
c ---[ 580]---> BDD-cost:  322
c ---[ 579]---> BDD-cost:  367
c ---[ 578]---> BDD-cost:  352
c ---[ 577]---> BDD-cost:  367
c ---[ 576]---> BDD-cost:  259
c ---[ 575]---> BDD-cost:  352
c ---[ 574]---> BDD-cost:  367
c ---[ 573]---> BDD-cost:  329
c ---[ 572]---> BDD-cost:  367
c ---[ 571]---> BDD-cost:  329
c ---[ 570]---> BDD-cost:  367
c ---[ 569]---> BDD-cost:  310
c ---[ 568]---> BDD-cost:  367
c ---[ 567]---> BDD-cost:  310
c ---[ 566]---> BDD-cost:  352
c ---[ 565]---> BDD-cost:  298
c ---[ 564]---> BDD-cost:  330
c ---[ 563]---> BDD-cost:  352
c ---[ 562]---> BDD-cost:  330
c ---[ 561]---> BDD-cost:  352
c ---[ 560]---> BDD-cost:  343
c ---[ 559]---> BDD-cost:  352
c ---[ 558]---> BDD-cost:  343
c ---[ 557]---> BDD-cost:  352
c ---[ 556]---> BDD-cost:  342
c ---[ 555]---> BDD-cost:  352
c ---[ 554]---> BDD-cost:  298
c ---[ 553]---> BDD-cost:  274
c ---[ 552]---> BDD-cost:  342
c ---[ 551]---> BDD-cost:  352
c ---[ 550]---> BDD-cost:  298
c ---[ 549]---> BDD-cost:  352
c ---[ 548]---> BDD-cost:  298
c ---[ 547]---> BDD-cost:  352
c ---[ 546]---> BDD-cost:  292
c ---[ 545]---> BDD-cost:  352
c ---[ 544]---> BDD-cost:  292
c ---[ 543]---> BDD-cost:  352
c ---[ 542]---> BDD-cost:  298
c ---[ 541]---> BDD-cost:  292
c ---[ 540]---> BDD-cost:  352
c ---[ 539]---> BDD-cost:  292
c ---[ 538]---> BDD-cost:  352
c ---[ 537]---> BDD-cost:  340
c ---[ 536]---> BDD-cost:  352
c ---[ 535]---> BDD-cost:  340
c ---[ 534]---> BDD-cost:  352
c ---[ 533]---> BDD-cost:  259
c ---[ 532]---> BDD-cost:  352
c ---[ 531]---> BDD-cost:  274
c ---[ 530]---> BDD-cost:  259
c ---[ 529]---> BDD-cost:  352
c ---[ 528]---> BDD-cost:  274
c ---[ 527]---> BDD-cost:  352
c ---[ 526]---> BDD-cost:  274
c ---[ 525]---> BDD-cost:  352
c ---[ 524]---> BDD-cost:  350
c ---[ 523]---> BDD-cost:  352
c ---[ 522]---> BDD-cost:  350
c ---[ 521]---> BDD-cost:  352
c ---[ 520]---> BDD-cost:  298
c ---[ 519]---> BDD-cost:  347
c ---[ 518]---> BDD-cost:  352
c ---[ 517]---> BDD-cost:  347
c ---[ 516]---> BDD-cost:  352
c ---[ 515]---> BDD-cost:  314
c ---[ 514]---> BDD-cost:  352
c ---[ 513]---> BDD-cost:  314
c ---[ 512]---> BDD-cost:  352
c ---[ 511]---> BDD-cost:  332
c ---[ 510]---> BDD-cost:  352
c ---[ 509]---> BDD-cost:  350
c ---[ 508]---> BDD-cost:  332
c ---[ 507]---> BDD-cost:  352
c ---[ 506]---> BDD-cost:  293
c ---[ 505]---> BDD-cost:  352
c ---[ 504]---> BDD-cost:  293
c ---[ 503]---> BDD-cost:  352
c ---[ 502]---> BDD-cost:  345
c ---[ 501]---> BDD-cost:  352
c ---[ 500]---> BDD-cost:  345
c ---[ 499]---> BDD-cost:  352
c ---[ 498]---> BDD-cost:  298
c ---[ 497]---> BDD-cost:  359
c ---[ 496]---> BDD-cost:  352
c ---[ 495]---> BDD-cost:  359
c ---[ 494]---> BDD-cost:  352
c ---[ 493]---> BDD-cost:  309
c ---[ 492]---> BDD-cost:  352
c ---[ 491]---> BDD-cost:  309
c ---[ 490]---> BDD-cost:  352
c ---[ 489]---> BDD-cost:  321
c ---[ 488]---> BDD-cost:  352
c ---[ 487]---> BDD-cost:  350
c ---[ 486]---> BDD-cost:  321
c ---[ 485]---> BDD-cost:  352
c ---[ 484]---> BDD-cost:  277
c ---[ 483]---> BDD-cost:  352
c ---[ 482]---> BDD-cost:  277
c ---[ 481]---> BDD-cost:  352
c ---[ 480]---> BDD-cost:  295
c ---[ 479]---> BDD-cost:  352
c ---[ 478]---> BDD-cost:  295
c ---[ 477]---> BDD-cost:  352
c ---[ 476]---> BDD-cost:  298
c ---[ 475]---> BDD-cost:  351
c ---[ 474]---> BDD-cost:  352
c ---[ 473]---> BDD-cost:  351
c ---[ 472]---> BDD-cost:  352
c ---[ 471]---> BDD-cost:  345
c ---[ 470]---> BDD-cost:  352
c ---[ 469]---> BDD-cost:  345
c ---[ 468]---> BDD-cost:  352
c ---[ 467]---> BDD-cost:  340
c ---[ 466]---> BDD-cost:  352
c ---[ 465]---> BDD-cost:  347
c ---[ 464]---> BDD-cost:  340
c ---[ 463]---> BDD-cost:  352
c ---[ 462]---> BDD-cost:  261
c ---[ 461]---> BDD-cost:  352
c ---[ 460]---> BDD-cost:  261
c ---[ 459]---> BDD-cost:  352
c ---[ 458]---> BDD-cost:  322
c ---[ 457]---> BDD-cost:  352
c ---[ 456]---> BDD-cost:  322
c ---[ 455]---> BDD-cost:  352
c ---[ 454]---> BDD-cost:  298
c ---[ 453]---> BDD-cost:  352
c ---[ 452]---> BDD-cost:  352
c ---[ 451]---> BDD-cost:  352
c ---[ 450]---> BDD-cost:  352
c ---[ 449]---> BDD-cost:  329
c ---[ 448]---> BDD-cost:  352
c ---[ 447]---> BDD-cost:  329
c ---[ 446]---> BDD-cost:  352
c ---[ 445]---> BDD-cost:  310
c ---[ 444]---> BDD-cost:  352
c ---[ 443]---> BDD-cost:  270
c ---[ 442]---> BDD-cost:  347
c ---[ 441]---> BDD-cost:  310
c ---[ 440]---> BDD-cost:  330
c ---[ 439]---> BDD-cost:  343
c ---[ 438]---> BDD-cost:  330
c ---[ 437]---> BDD-cost:  343
c ---[ 436]---> BDD-cost:  330
c ---[ 435]---> BDD-cost:  342
c ---[ 434]---> BDD-cost:  330
c ---[ 433]---> BDD-cost:  342
c ---[ 432]---> BDD-cost:  330
c ---[ 431]---> BDD-cost:  298
c ---[ 430]---> BDD-cost:  298
c ---[ 429]---> BDD-cost:  330
c ---[ 428]---> BDD-cost:  298
c ---[ 427]---> BDD-cost:  330
c ---[ 426]---> BDD-cost:  292
c ---[ 425]---> BDD-cost:  330
c ---[ 424]---> BDD-cost:  292
c ---[ 423]---> BDD-cost:  330
c ---[ 422]---> BDD-cost:  292
c ---[ 421]---> BDD-cost:  330
c ---[ 420]---> BDD-cost:  314
c ---[ 419]---> BDD-cost:  292
c ---[ 418]---> BDD-cost:  330
c ---[ 417]---> BDD-cost:  340
c ---[ 416]---> BDD-cost:  330
c ---[ 415]---> BDD-cost:  340
c ---[ 414]---> BDD-cost:  330
c ---[ 413]---> BDD-cost:  259
c ---[ 412]---> BDD-cost:  330
c ---[ 411]---> BDD-cost:  259
c ---[ 410]---> BDD-cost:  330
c ---[ 409]---> BDD-cost:  298
c ---[ 408]---> BDD-cost:  274
c ---[ 407]---> BDD-cost:  330
c ---[ 406]---> BDD-cost:  274
c ---[ 405]---> BDD-cost:  330
c ---[ 404]---> BDD-cost:  350
c ---[ 403]---> BDD-cost:  330
c ---[ 402]---> BDD-cost:  350
c ---[ 401]---> BDD-cost:  330
c ---[ 400]---> BDD-cost:  347
c ---[ 399]---> BDD-cost:  330
c ---[ 398]---> BDD-cost:  314
c ---[ 397]---> BDD-cost:  347
c ---[ 396]---> BDD-cost:  330
c ---[ 395]---> BDD-cost:  314
c ---[ 394]---> BDD-cost:  330
c ---[ 393]---> BDD-cost:  314
c ---[ 392]---> BDD-cost:  330
c ---[ 391]---> BDD-cost:  332
c ---[ 390]---> BDD-cost:  330
c ---[ 389]---> BDD-cost:  332
c ---[ 388]---> BDD-cost:  330
c ---[ 387]---> BDD-cost:  298
c ---[ 386]---> BDD-cost:  293
c ---[ 385]---> BDD-cost:  330
c ---[ 384]---> BDD-cost:  293
c ---[ 383]---> BDD-cost:  330
c ---[ 382]---> BDD-cost:  345
c ---[ 381]---> BDD-cost:  330
c ---[ 380]---> BDD-cost:  345
c ---[ 379]---> BDD-cost:  330
c ---[ 378]---> BDD-cost:  359
c ---[ 377]---> BDD-cost:  330
c ---[ 376]---> BDD-cost:  332
c ---[ 375]---> BDD-cost:  359
c ---[ 374]---> BDD-cost:  330
c ---[ 373]---> BDD-cost:  309
c ---[ 372]---> BDD-cost:  330
c ---[ 371]---> BDD-cost:  309
c ---[ 370]---> BDD-cost:  330
c ---[ 369]---> BDD-cost:  321
c ---[ 368]---> BDD-cost:  330
c ---[ 367]---> BDD-cost:  321
c ---[ 366]---> BDD-cost:  330
c ---[ 365]---> BDD-cost:  298
c ---[ 364]---> BDD-cost:  277
c ---[ 363]---> BDD-cost:  330
c ---[ 362]---> BDD-cost:  277
c ---[ 361]---> BDD-cost:  330
c ---[ 360]---> BDD-cost:  295
c ---[ 359]---> BDD-cost:  330
c ---[ 358]---> BDD-cost:  295
c ---[ 357]---> BDD-cost:  330
c ---[ 356]---> BDD-cost:  351
c ---[ 355]---> BDD-cost:  330
c ---[ 354]---> BDD-cost:  332
c ---[ 353]---> BDD-cost:  351
c ---[ 352]---> BDD-cost:  330
c ---[ 351]---> BDD-cost:  345
c ---[ 350]---> BDD-cost:  330
c ---[ 349]---> BDD-cost:  345
c ---[ 348]---> BDD-cost:  330
c ---[ 347]---> BDD-cost:  340
c ---[ 346]---> BDD-cost:  330
c ---[ 345]---> BDD-cost:  340
c ---[ 344]---> BDD-cost:  330
c ---[ 343]---> BDD-cost:  298
c ---[ 342]---> BDD-cost:  261
c ---[ 341]---> BDD-cost:  330
c ---[ 340]---> BDD-cost:  261
c ---[ 339]---> BDD-cost:  330
c ---[ 338]---> BDD-cost:  322
c ---[ 337]---> BDD-cost:  330
c ---[ 336]---> BDD-cost:  322
c ---[ 335]---> BDD-cost:  330
c ---[ 334]---> BDD-cost:  352
c ---[ 333]---> BDD-cost:  330
c ---[ 332]---> BDD-cost:  298
c ---[ 331]---> BDD-cost:  293
c ---[ 330]---> BDD-cost:  352
c ---[ 329]---> BDD-cost:  330
c ---[ 328]---> BDD-cost:  329
c ---[ 327]---> BDD-cost:  330
c ---[ 326]---> BDD-cost:  329
c ---[ 325]---> BDD-cost:  330
c ---[ 324]---> BDD-cost:  310
c ---[ 323]---> BDD-cost:  330
c ---[ 322]---> BDD-cost:  310
c ---[ 321]---> BDD-cost:  343
c ---[ 320]---> BDD-cost:  298
c ---[ 319]---> BDD-cost:  342
c ---[ 318]---> BDD-cost:  343
c ---[ 317]---> BDD-cost:  342
c ---[ 316]---> BDD-cost:  343
c ---[ 315]---> BDD-cost:  298
c ---[ 314]---> BDD-cost:  343
c ---[ 313]---> BDD-cost:  298
c ---[ 312]---> BDD-cost:  343
c ---[ 311]---> BDD-cost:  292
c ---[ 310]---> BDD-cost:  343
c ---[ 309]---> BDD-cost:  293
c ---[ 308]---> BDD-cost:  292
c ---[ 307]---> BDD-cost:  343
c ---[ 306]---> BDD-cost:  292
c ---[ 305]---> BDD-cost:  343
c ---[ 304]---> BDD-cost:  292
c ---[ 303]---> BDD-cost:  343
c ---[ 302]---> BDD-cost:  340
c ---[ 301]---> BDD-cost:  343
c ---[ 300]---> BDD-cost:  340
c ---[ 299]---> BDD-cost:  343
c ---[ 298]---> BDD-cost:  298
c ---[ 297]---> BDD-cost:  259
c ---[ 296]---> BDD-cost:  343
c ---[ 295]---> BDD-cost:  259
c ---[ 294]---> BDD-cost:  343
c ---[ 293]---> BDD-cost:  274
c ---[ 292]---> BDD-cost:  343
c ---[ 291]---> BDD-cost:  274
c ---[ 290]---> BDD-cost:  343
c ---[ 289]---> BDD-cost:  350
c ---[ 288]---> BDD-cost:  343
c ---[ 287]---> BDD-cost:  345
c ---[ 286]---> BDD-cost:  350
c ---[ 285]---> BDD-cost:  343
c ---[ 284]---> BDD-cost:  347
c ---[ 283]---> BDD-cost:  343
c ---[ 282]---> BDD-cost:  347
c ---[ 281]---> BDD-cost:  343
c ---[ 280]---> BDD-cost:  314
c ---[ 279]---> BDD-cost:  343
c ---[ 278]---> BDD-cost:  314
c ---[ 277]---> BDD-cost:  343
c ---[ 276]---> BDD-cost:  298
c ---[ 275]---> BDD-cost:  332
c ---[ 274]---> BDD-cost:  343
c ---[ 273]---> BDD-cost:  332
c ---[ 272]---> BDD-cost:  343
c ---[ 271]---> BDD-cost:  293
c ---[ 270]---> BDD-cost:  343
c ---[ 269]---> BDD-cost:  293
c ---[ 268]---> BDD-cost:  343
c ---[ 267]---> BDD-cost:  345
c ---[ 266]---> BDD-cost:  343
c ---[ 265]---> BDD-cost:  345
c ---[ 264]---> BDD-cost:  345
c ---[ 263]---> BDD-cost:  343
c ---[ 262]---> BDD-cost:  359
c ---[ 261]---> BDD-cost:  343
c ---[ 260]---> BDD-cost:  359
c ---[ 259]---> BDD-cost:  343
c ---[ 258]---> BDD-cost:  309
c ---[ 257]---> BDD-cost:  343
c ---[ 256]---> BDD-cost:  309
c ---[ 255]---> BDD-cost:  343
c ---[ 254]---> BDD-cost:  298
c ---[ 253]---> BDD-cost:  321
c ---[ 252]---> BDD-cost:  343
c ---[ 251]---> BDD-cost:  321
c ---[ 250]---> BDD-cost:  343
c ---[ 249]---> BDD-cost:  277
c ---[ 248]---> BDD-cost:  343
c ---[ 247]---> BDD-cost:  277
c ---[ 246]---> BDD-cost:  343
c ---[ 245]---> BDD-cost:  295
c ---[ 244]---> BDD-cost:  343
c ---[ 243]---> BDD-cost:  359
c ---[ 242]---> BDD-cost:  295
c ---[ 241]---> BDD-cost:  343
c ---[ 240]---> BDD-cost:  351
c ---[ 239]---> BDD-cost:  343
c ---[ 238]---> BDD-cost:  351
c ---[ 237]---> BDD-cost:  343
c ---[ 236]---> BDD-cost:  345
c ---[ 235]---> BDD-cost:  343
c ---[ 234]---> BDD-cost:  345
c ---[ 233]---> BDD-cost:  343
c ---[ 232]---> BDD-cost:  298
c ---[ 231]---> BDD-cost:  340
c ---[ 230]---> BDD-cost:  343
c ---[ 229]---> BDD-cost:  340
c ---[ 228]---> BDD-cost:  343
c ---[ 227]---> BDD-cost:  261
c ---[ 226]---> BDD-cost:  343
c ---[ 225]---> BDD-cost:  261
c ---[ 224]---> BDD-cost:  343
c ---[ 223]---> BDD-cost:  322
c ---[ 222]---> BDD-cost:  343
c ---[ 221]---> BDD-cost:  270
c ---[ 220]---> BDD-cost:  359
c ---[ 219]---> BDD-cost:  322
c ---[ 218]---> BDD-cost:  343
c ---[ 217]---> BDD-cost:  352
c ---[ 216]---> BDD-cost:  343
c ---[ 215]---> BDD-cost:  352
c ---[ 214]---> BDD-cost:  343
c ---[ 213]---> BDD-cost:  329
c ---[ 212]---> BDD-cost:  343
c ---[ 211]---> BDD-cost:  329
c ---[ 210]---> BDD-cost:  343
c ---[ 209]---> BDD-cost:  298
c ---[ 208]---> BDD-cost:  310
c ---[ 207]---> BDD-cost:  343
c ---[ 206]---> BDD-cost:  310
c ---[ 205]---> BDD-cost:  342
c ---[ 204]---> BDD-cost:  298
c ---[ 203]---> BDD-cost:  342
c ---[ 202]---> BDD-cost:  298
c ---[ 201]---> BDD-cost:  342
c ---[ 200]---> BDD-cost:  292
c ---[ 199]---> BDD-cost:  342
c ---[ 198]---> BDD-cost:  309
c ---[ 197]---> BDD-cost:  292
c ---[ 196]---> BDD-cost:  342
c ---[ 195]---> BDD-cost:  292
c ---[ 194]---> BDD-cost:  342
c ---[ 193]---> BDD-cost:  292
c ---[ 192]---> BDD-cost:  342
c ---[ 191]---> BDD-cost:  340
c ---[ 190]---> BDD-cost:  342
c ---[ 189]---> BDD-cost:  340
c ---[ 188]---> BDD-cost:  342
c ---[ 187]---> BDD-cost:  298
c ---[ 186]---> BDD-cost:  259
c ---[ 185]---> BDD-cost:  342
c ---[ 184]---> BDD-cost:  259
c ---[ 183]---> BDD-cost:  342
c ---[ 182]---> BDD-cost:  274
c ---[ 181]---> BDD-cost:  342
c ---[ 180]---> BDD-cost:  274
c ---[ 179]---> BDD-cost:  342
c ---[ 178]---> BDD-cost:  350
c ---[ 177]---> BDD-cost:  342
c ---[ 176]---> BDD-cost:  309
c ---[ 175]---> BDD-cost:  350
c ---[ 174]---> BDD-cost:  342
c ---[ 173]---> BDD-cost:  347
c ---[ 172]---> BDD-cost:  342
c ---[ 171]---> BDD-cost:  347
c ---[ 170]---> BDD-cost:  342
c ---[ 169]---> BDD-cost:  314
c ---[ 168]---> BDD-cost:  342
c ---[ 167]---> BDD-cost:  314
c ---[ 166]---> BDD-cost:  342
c ---[ 165]---> BDD-cost:  298
c ---[ 164]---> BDD-cost:  332
c ---[ 163]---> BDD-cost:  342
c ---[ 162]---> BDD-cost:  332
c ---[ 161]---> BDD-cost:  342
c ---[ 160]---> BDD-cost:  293
c ---[ 159]---> BDD-cost:  342
c ---[ 158]---> BDD-cost:  293
c ---[ 157]---> BDD-cost:  342
c ---[ 156]---> BDD-cost:  345
c ---[ 155]---> BDD-cost:  342
c ---[ 154]---> BDD-cost:  321
c ---[ 153]---> BDD-cost:  345
c ---[ 152]---> BDD-cost:  342
c ---[ 151]---> BDD-cost:  359
c ---[ 150]---> BDD-cost:  342
c ---[ 149]---> BDD-cost:  359
c ---[ 148]---> BDD-cost:  342
c ---[ 147]---> BDD-cost:  309
c ---[ 146]---> BDD-cost:  342
c ---[ 145]---> BDD-cost:  309
c ---[ 144]---> BDD-cost:  342
c ---[ 143]---> BDD-cost:  298
c ---[ 142]---> BDD-cost:  321
c ---[ 141]---> BDD-cost:  342
c ---[ 140]---> BDD-cost:  321
c ---[ 139]---> BDD-cost:  342
c ---[ 138]---> BDD-cost:  277
c ---[ 137]---> BDD-cost:  342
c ---[ 136]---> BDD-cost:  277
c ---[ 135]---> BDD-cost:  342
c ---[ 134]---> BDD-cost:  295
c ---[ 133]---> BDD-cost:  342
c ---[ 132]---> BDD-cost:  321
c ---[ 131]---> BDD-cost:  295
c ---[ 130]---> BDD-cost:  342
c ---[ 129]---> BDD-cost:  351
c ---[ 128]---> BDD-cost:  342
c ---[ 127]---> BDD-cost:  351
c ---[ 126]---> BDD-cost:  342
c ---[ 125]---> BDD-cost:  345
c ---[ 124]---> BDD-cost:  342
c ---[ 123]---> BDD-cost:  345
c ---[ 122]---> BDD-cost:  342
c ---[ 121]---> BDD-cost:  298
c ---[ 120]---> BDD-cost:  340
c ---[ 119]---> BDD-cost:  342
c ---[ 118]---> BDD-cost:  340
c ---[ 117]---> BDD-cost:  342
c ---[ 116]---> BDD-cost:  261
c ---[ 115]---> BDD-cost:  342
c ---[ 114]---> BDD-cost:  261
c ---[ 113]---> BDD-cost:  342
c ---[ 112]---> BDD-cost:  322
c ---[ 111]---> BDD-cost:  342
c ---[ 110]---> BDD-cost:  298
c ---[ 109]---> BDD-cost:  277
c ---[ 108]---> BDD-cost:  322
c ---[ 107]---> BDD-cost:  342
c ---[ 106]---> BDD-cost:  352
c ---[ 105]---> BDD-cost:  342
c ---[ 104]---> BDD-cost:  352
c ---[ 103]---> BDD-cost:  342
c ---[ 102]---> BDD-cost:  329
c ---[ 101]---> BDD-cost:  342
c ---[ 100]---> BDD-cost:  329
c ---[  99]---> BDD-cost:  342
c ---[  98]---> BDD-cost:  298
c ---[  97]---> BDD-cost:  310
c ---[  96]---> BDD-cost:  342
c ---[  95]---> BDD-cost:  310
c ---[  94]---> BDD-cost:  298
c ---[  93]---> BDD-cost:  292
c ---[  92]---> BDD-cost:  298
c ---[  91]---> BDD-cost:  292
c ---[  90]---> BDD-cost:  298
c ---[  89]---> BDD-cost:  292
c ---[  88]---> BDD-cost:  298
c ---[  87]---> BDD-cost:  277
c ---[  86]---> BDD-cost:  292
c ---[  85]---> BDD-cost:  298
c ---[  84]---> BDD-cost:  340
c ---[  83]---> BDD-cost:  298
c ---[  82]---> BDD-cost:  340
c ---[  81]---> BDD-cost:  298
c ---[  80]---> BDD-cost:  259
c ---[  79]---> BDD-cost:  298
c ---[  78]---> BDD-cost:  259
c ---[  77]---> BDD-cost:  298
c ---[  76]---> BDD-cost:  298
c ---[  75]---> BDD-cost:  274
c ---[  74]---> BDD-cost:  298
c ---[  73]---> BDD-cost:  274
c ---[  72]---> BDD-cost:  298
c ---[  71]---> BDD-cost:  350
c ---[  70]---> BDD-cost:  298
c ---[  69]---> BDD-cost:  350
c ---[  68]---> BDD-cost:  298
c ---[  67]---> BDD-cost:  347
c ---[  66]---> BDD-cost:  298
c ---[  65]---> BDD-cost:  295
c ---[  64]---> BDD-cost:  347
c ---[  63]---> BDD-cost:  298
c ---[  62]---> BDD-cost:  314
c ---[  61]---> BDD-cost:  298
c ---[  60]---> BDD-cost:  314
c ---[  59]---> BDD-cost:  298
c ---[  58]---> BDD-cost:  332
c ---[  57]---> BDD-cost:  298
c ---[  56]---> BDD-cost:  332
c ---[  55]---> BDD-cost:  298
c ---[  54]---> BDD-cost:  298
c ---[  53]---> BDD-cost:  293
c ---[  52]---> BDD-cost:  298
c ---[  51]---> BDD-cost:  293
c ---[  50]---> BDD-cost:  298
c ---[  49]---> BDD-cost:  345
c ---[  48]---> BDD-cost:  298
c ---[  47]---> BDD-cost:  345
c ---[  46]---> BDD-cost:  298
c ---[  45]---> BDD-cost:  359
c ---[  44]---> BDD-cost:  298
c ---[  43]---> BDD-cost:  295
c ---[  42]---> BDD-cost:  359
c ---[  41]---> BDD-cost:  298
c ---[  40]---> BDD-cost:  309
c ---[  39]---> BDD-cost:  298
c ---[  38]---> BDD-cost:  309
c ---[  37]---> BDD-cost:  298
c ---[  36]---> BDD-cost:  321
c ---[  35]---> BDD-cost:  298
c ---[  34]---> BDD-cost:  321
c ---[  33]---> BDD-cost:  298
c ---[  32]---> BDD-cost:  298
c ---[  31]---> BDD-cost:  277
c ---[  30]---> BDD-cost:  298
c ---[  29]---> BDD-cost:  277
c ---[  28]---> BDD-cost:  298
c ---[  27]---> BDD-cost:  295
c ---[  26]---> BDD-cost:  298
c ---[  25]---> BDD-cost:  295
c ---[  24]---> BDD-cost:  298
c ---[  23]---> BDD-cost:  351
c ---[  22]---> BDD-cost:  298
c ---[  21]---> BDD-cost:  351
c ---[  20]---> BDD-cost:  351
c ---[  19]---> BDD-cost:  298
c ---[  18]---> BDD-cost:  345
c ---[  17]---> BDD-cost:  298
c ---[  16]---> BDD-cost:  345
c ---[  15]---> BDD-cost:  298
c ---[  14]---> BDD-cost:  340
c ---[  13]---> BDD-cost:  298
c ---[  12]---> BDD-cost:  340
c ---[  11]---> BDD-cost:  298
c ---[  10]---> BDD-cost:  298
c ---[   9]---> BDD-cost:  261
c ---[   8]---> BDD-cost:  298
c ---[   7]---> BDD-cost:  261
c ---[   6]---> BDD-cost:  298
c ---[   5]---> BDD-cost:  322
c ---[   4]---> BDD-cost:  298
c ---[   3]---> BDD-cost:  322
c ---[   2]---> BDD-cost:  298
c ---[   1]---> BDD-cost:  352
c ---[   0]---> BDD-cost:  298
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1325270  3692568 |  441756       0        0     nan |  0.000 % |
c |       100 | 1325270  3692568 |  485931     100     1102    11.0 |  0.385 % |
c |       250 | 1325270  3692568 |  534524     250     2058     8.2 |  0.385 % |
c |       476 | 1325270  3692568 |  587977     476     4973    10.4 |  0.385 % |
c |       813 | 1325270  3692568 |  646774     813     8312    10.2 |  0.385 % |
c |      1319 | 1325270  3692568 |  711452    1319    14420    10.9 |  0.385 % |
c |      2078 | 1325270  3692568 |  782597    2078    22572    10.9 |  0.385 % |
c |      3217 | 1325270  3692568 |  860857    3217    34674    10.8 |  0.385 % |
c |      4925 | 1325270  3692568 |  946943    4925    61452    12.5 |  0.385 % |
c |      7489 | 1325270  3692568 | 1041637    7489   114381    15.3 |  0.385 % |
c |     11333 | 1325270  3692568 | 1145801   11333   192980    17.0 |  0.385 % |
c |     17099 | 1325270  3692568 | 1260381   17099   300162    17.6 |  0.385 % |
c |     25748 | 1325270  3692568 | 1386419   25748   593033    23.0 |  0.385 % |
c |     38722 | 1325270  3692568 | 1525061   38722   888654    22.9 |  0.385 % |
c ==============================================================================
c [1mFound solution: 538947292[0m
c ---[   0]---> Sorter-cost:  166     Base: 2 2 2 2 2 2 2 2 2 2 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 |     42214 | 1325587  3693316 |  441862   42214  1000790    23.7 |  0.385 % |
c |     42315 | 1325587  3693316 |  486048   42315  1001948    23.7 |  0.385 % |
c |     42465 | 1325587  3693316 |  534653   42465  1004402    23.7 |  0.385 % |
c |     42690 | 1325587  3693316 |  588118   42690  1007161    23.6 |  0.385 % |
c |     43027 | 1325587  3693316 |  646930   43027  1012586    23.5 |  0.385 % |
c |     43534 | 1325587  3693316 |  711623   43534  1024545    23.5 |  0.385 % |
c |     44294 | 1325587  3693316 |  782785   44294  1038655    23.4 |  0.385 % |
c |     45433 | 1325587  3693316 |  861064   45433  1055741    23.2 |  0.385 % |
c |     47141 | 1325587  3693316 |  947170   47141  1115579    23.7 |  0.385 % |
c |     49703 | 1325587  3693316 | 1041887   49703  1186262    23.9 |  0.385 % |
c |     53547 | 1325587  3693316 | 1146076   53547  1263261    23.6 |  0.385 % |
c |     59315 | 1325587  3693316 | 1260683   59315  1415240    23.9 |  0.385 % |
c ==============================================================================
c [1mFound solution: 537920542[0m
c ---[   0]---> Sorter-cost:  196     Base: 2 2 2 2 2 2 2 2 2 2 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 |     60814 | 1325967  3694200 |  441989   60814  1464445    24.1 |  0.385 % |
c |     60915 | 1325967  3694200 |  486187   60915  1466156    24.1 |  0.385 % |
c |     61067 | 1325967  3694200 |  534806   61067  1467571    24.0 |  0.385 % |
c |     61293 | 1325967  3694200 |  588287   61293  1471280    24.0 |  0.385 % |
c |     61630 | 1325967  3694200 |  647116   61630  1476748    24.0 |  0.385 % |
c |     62136 | 1325967  3694200 |  711827   62136  1490127    24.0 |  0.385 % |
c |     62895 | 1325967  3694200 |  783010   62895  1512742    24.1 |  0.385 % |
c ==============================================================================
c [1mFound solution: 536875004[0m
c ---[   0]---> Sorter-cost:  148     Base: 2 2 2 2 2 2 2 2 2 2 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 |     63732 | 1326230  3694816 |  442076   63732  1528439    24.0 |  0.385 % |
c |     63833 | 1326230  3694816 |  486283   63833  1529721    24.0 |  0.386 % |
c |     63983 | 1326230  3694816 |  534911   63983  1532249    23.9 |  0.386 % |
c |     64208 | 1326230  3694816 |  588403   64208  1536219    23.9 |  0.386 % |
c |     64545 | 1326230  3694816 |  647243   64545  1544978    23.9 |  0.386 % |
c |     65052 | 1326230  3694816 |  711967   65052  1557152    23.9 |  0.386 % |
c |     65811 | 1326230  3694816 |  783164   65811  1578202    24.0 |  0.386 % |
c |     66950 | 1326230  3694816 |  861481   66950  1625076    24.3 |  0.386 % |
c |     68658 | 1326230  3694816 |  947629   68658  1652495    24.1 |  0.386 % |
c ==============================================================================
c [1mFound solution: 536871930[0m
c ---[   0]---> Sorter-cost:  169     Base: 2 2 2 2 2 2 2 2 2 2 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 |     69374 | 1326535  3695528 |  442178   69374  1665020    24.0 |  0.386 % |
c |     69474 | 1326535  3695528 |  486395   69474  1666560    24.0 |  0.386 % |
c |     69625 | 1326535  3695528 |  535035   69625  1667914    24.0 |  0.386 % |
c |     69850 | 1326535  3695528 |  588538   69850  1674061    24.0 |  0.386 % |
c ==============================================================================
c [1mFound solution: 268434398[0m
c ---[   0]---> Sorter-cost:  779     Base: 2 2 2 2 2 3 11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     70142 | 1283389  3569679 |  427796   61946  1247143    20.1 |  0.386 % |
c |     70243 | 1283389  3569679 |  470575   62047  1248154    20.1 |  2.534 % |
c |     70393 | 1283389  3569679 |  517633   62197  1250759    20.1 |  2.534 % |
c |     70618 | 1283389  3569679 |  569396   62422  1253658    20.1 |  2.534 % |
c |     70955 | 1283389  3569679 |  626336   62759  1260929    20.1 |  2.534 % |
c |     71461 | 1283389  3569679 |  688969   63265  1272037    20.1 |  2.534 % |
c |     72220 | 1283389  3569679 |  757866   64024  1297677    20.3 |  2.534 % |
c ==============================================================================
c [1mFound solution: 164759916[0m
c ---[   0]---> Sorter-cost:  166     Base: 2 2 2 2 2 2 2 2 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 |     72933 | 1283721  3570456 |  427907   64737  1327441    20.5 |  2.534 % |
c |     73034 | 1283717  3570447 |  470697   64837  1329228    20.5 |  2.534 % |
c |     73184 | 1283717  3570447 |  517767   64987  1332063    20.5 |  2.534 % |
c |     73409 | 1283717  3570447 |  569544   65212  1336019    20.5 |  2.534 % |
c |     73747 | 1283717  3570447 |  626498   65550  1344758    20.5 |  2.534 % |
c |     74253 | 1283717  3570447 |  689148   66056  1353878    20.5 |  2.534 % |
c |     75012 | 1283717  3570447 |  758063   66815  1371785    20.5 |  2.534 % |
c |     76151 | 1283717  3570447 |  833869   67954  1394620    20.5 |  2.534 % |
c ==============================================================================
c [1mFound solution: 135054036[0m
c ---[   0]---> Sorter-cost:  161     Base: 2 2 2 2 2 2 2 2 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 |     77404 | 1284030  3571178 |  428010   69207  1418140    20.5 |  2.534 % |
c |     77504 | 1284030  3571178 |  470811   69307  1419387    20.5 |  2.534 % |
c |     77654 | 1284030  3571178 |  517892   69457  1421879    20.5 |  2.534 % |
c |     77879 | 1284030  3571178 |  569681   69682  1426046    20.5 |  2.534 % |
c |     78216 | 1284030  3571178 |  626649   70019  1433160    20.5 |  2.534 % |
c |     78723 | 1284030  3571178 |  689314   70526  1451627    20.6 |  2.534 % |
c |     79483 | 1284030  3571178 |  758245   71286  1468246    20.6 |  2.534 % |
c |     80623 | 1284030  3571178 |  834070   72426  1501077    20.7 |  2.534 % |
c |     82331 | 1284030  3571178 |  917477   74134  1555460    21.0 |  2.534 % |
c |     84894 | 1284030  3571178 | 1009225   76697  1638656    21.4 |  2.534 % |
c ==============================================================================
c [1mFound solution: 48693098[0m
c ---[   0]---> Sorter-cost:  127     Base: 2 2 2 2 2 2 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 |     86107 | 1230019  3417751 |  410006   68911  1350672    19.6 |  2.534 % |
c |     86207 | 1230019  3417751 |  451006   69011  1352125    19.6 |  5.244 % |
c |     86359 | 1230019  3417751 |  496107   69163  1356417    19.6 |  5.244 % |
c |     86584 | 1230019  3417751 |  545717   69388  1361010    19.6 |  5.244 % |
c |     86924 | 1230019  3417751 |  600289   69728  1371987    19.7 |  5.244 % |
c |     87430 | 1230019  3417751 |  660318   70234  1391315    19.8 |  5.244 % |
c |     88191 | 1230019  3417751 |  726350   70995  1407451    19.8 |  5.244 % |
c |     89331 | 1230019  3417751 |  798985   72135  1449525    20.1 |  5.244 % |
c ==============================================================================
c [1mFound solution: 16179082[0m
c ---[   0]---> Sorter-cost:  385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     89770 | 1176497  3262300 |  392165   59236   959091    16.2 |  5.244 % |
c |     89870 | 1176497  3262300 |  431381   59336   960927    16.2 |  7.592 % |
c |     90020 | 1176497  3262300 |  474519   59486   963643    16.2 |  7.592 % |
c ==============================================================================
c [1mFound solution: 11951858[0m
c ---[   0]---> Sorter-cost:  124     Base: 2 2 2 2 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 |     90066 | 1176729  3262850 |  392243   59532   964158    16.2 |  7.592 % |
c ==============================================================================
c [1mFound solution: 11950874[0m
c ---[   0]---> Sorter-cost:  114     Base: 2 2 2 2 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 |     90095 | 1176943  3263354 |  392314   59561   964533    16.2 |  7.592 % |
c ==============================================================================
c [1mFound solution: 11943668[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 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90164 | 1177120  3263776 |  392373   59630   965529    16.2 |  7.592 % |
c |     90264 | 1177120  3263776 |  431610   59730   967199    16.2 |  7.589 % |
c ==============================================================================
c [1mFound solution: 11731082[0m
c ---[   0]---> Sorter-cost:  127     Base: 2 2 2 2 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 |     90346 | 1177362  3264341 |  392454   59812   968948    16.2 |  7.589 % |
c ==============================================================================
c [1mFound solution: 9527132[0m
c ---[   0]---> Sorter-cost:  110     Base: 2 2 2 2 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 |     90430 | 1177563  3264815 |  392521   59896   970971    16.2 |  7.589 % |
c |     90530 | 1177563  3264815 |  431773   59996   973017    16.2 |  7.586 % |
c ==============================================================================
c [1mFound solution: 8871898[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 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90593 | 1177713  3265173 |  392571   60059   974750    16.2 |  7.586 % |
c |     90693 | 1177713  3265173 |  431828   60159   977378    16.2 |  7.585 % |
c ==============================================================================
c [1mFound solution: 8860986[0m
c ---[   0]---> Sorter-cost:  101     Base: 2 2 2 2 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 |     90780 | 1177893  3265596 |  392631   60246   978990    16.2 |  7.585 % |
c |     90880 | 1177893  3265596 |  431894   60346   981997    16.3 |  7.584 % |
c ==============================================================================
c [1mFound solution: 8649620[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 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90988 | 1178055  3265982 |  392685   60454   984250    16.3 |  7.584 % |
c ==============================================================================
c [1mFound solution: 8588974[0m
c ---[   0]---> Sorter-cost:  119     Base: 2 2 2 2 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 |     91067 | 1178269  3266484 |  392756   60533   985728    16.3 |  7.584 % |
c ==============================================================================
c [1mFound solution: 6293900[0m
c ---[   0]---> Sorter-cost:  305     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     91144 | 1132855  3140780 |  377618   49081   655793    13.4 |  7.584 % |
c ==============================================================================
c [1mFound solution: 5119866[0m
c ---[   0]---> Sorter-cost:  120     Base: 2 2 2 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 |     91188 | 1133077  3141307 |  377692   49125   656448    13.4 |  7.584 % |
c |     91288 | 1133077  3141307 |  415461   49225   659128    13.4 |  9.311 % |
c ==============================================================================
c [1mFound solution: 4785002[0m
c ---[   0]---> Sorter-cost:  119     Base: 2 2 2 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 |     91421 | 1133307  3141845 |  377769   49358   661832    13.4 |  9.311 % |
c |     91522 | 1133307  3141845 |  415545   49459   663974    13.4 |  9.309 % |
c ==============================================================================
c [1mFound solution: 4751602[0m
c ---[   0]---> Sorter-cost:  120     Base: 2 2 2 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 |     91653 | 1133529  3142364 |  377843   49590   667014    13.5 |  9.309 % |
c |     91753 | 1133529  3142364 |  415627   49690   669159    13.5 |  9.308 % |
c ==============================================================================
c [1mFound solution: 4743922[0m
c ---[   0]---> Sorter-cost:   78     Base: 2 2 2 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 |     91815 | 1133670  3142693 |  377890   49752   670243    13.5 |  9.308 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 27100 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.95 0.97 0.91 2/54 27095
Raw data (stat): 27095 (runsolver) R 27094 1586 1585 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854214367 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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+9.99953 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.96 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.0008 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.0013 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.0022 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.0015 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.0021 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.0023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27100
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.063 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 3/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.069 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.083 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.089 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.094 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.093 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.76 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 27102
Raw data (stat): 27095 (minisat+_script) S 27094 1586 1585 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 854214367 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.76
CPU time (s): 1229.94
CPU user time (s): 1228.45
CPU system time (s): 1.49077
CPU usage (%): 100.014
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####