PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        652896 kB
Buffers:         33828 kB
Cached:         325076 kB
SwapCached:          0 kB
Active:         127664 kB
Inactive:       234084 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        652644 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14400 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:45:15 (client local time) WITH STATUS 1 IN 1061.65 SECONDS
stats: 20233 7 1061.65 1
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1739 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ===========
c   -- Clauses(.)/Splits(s): s...s.ssssssss.ss........ss...ssss..ss.s..ss.s..s..ssssssssssss...s.s.ss.s.s..s.s..s..s...sss.ss.s...s.s.s..ssss..s.ss.s..ss.s.s......sss..ss.ss...sssss.s..ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss.ssssssssss.ssssssssssssssss.ssss..sss..s..s...sss...s.s..ssssss.ss.ssss.sss...s....ssssssss..s.ss....sssssss.s.sssssssssssssss.ss.ss.ssss.s..sssssssssss..ss.ssssss.sss.sss..ss..s...ss.s.ss.sss.ssssss...ss.sssssssss.sss.ss.ss.s.sssssssss.ssss..ss..s.ssss.s.s.....ssss...s.s..sssss.ss....s...s.
c ---[2139]---> BDD-cost:   19
c ---[2138]---> BDD-cost:   27
c ---[2137]---> BDD-cost:   27
c ---[2136]---> BDD-cost:   27
c ---[2135]---> BDD-cost:   25
c ---[2134]---> BDD-cost:   25
c ---[2133]---> BDD-cost:    3
c ---[2132]---> BDD-cost:   19
c ---[2130]---> BDD-cost:    3
c ---[2127]---> BDD-cost:    7
c ---[2126]---> BDD-cost:   11
c ---[2125]---> BDD-cost:   19
c ---[2124]---> BDD-cost:   11
c ---[2123]---> BDD-cost:   19
c ---[2122]---> BDD-cost:    9
c ---[2121]---> BDD-cost:   11
c ---[2120]---> BDD-cost:    7
c ---[2119]---> BDD-cost:    7
c ---[2117]---> BDD-cost:   31
c ---[2116]---> BDD-cost:   31
c ---[2115]---> BDD-cost:   21
c ---[2114]---> BDD-cost:   23
c ---[2113]---> BDD-cost:   19
c ---[2112]---> BDD-cost:   19
c ---[2111]---> BDD-cost:   27
c ---[2110]---> BDD-cost:   33
c ---[2109]---> BDD-cost:   29
c ---[2108]---> BDD-cost:   27
c ---[2106]---> BDD-cost:    7
c ---[2105]---> BDD-cost:   27
c ---[2104]---> BDD-cost:   33
c ---[2103]---> BDD-cost:   37
c ---[2102]---> BDD-cost:   37
c ---[2101]---> BDD-cost:   37
c ---[2100]---> BDD-cost:   37
c ---[2099]---> BDD-cost:   37
c ---[2098]---> BDD-cost:    7
c ---[2097]---> BDD-cost:   19
c ---[2095]---> BDD-cost:    9
c ---[2094]---> BDD-cost:    7
c ---[2093]---> BDD-cost:    5
c ---[2092]---> BDD-cost:   19
c ---[2091]---> BDD-cost:   23
c ---[2090]---> BDD-cost:    3
c ---[2089]---> BDD-cost:   27
c ---[2088]---> BDD-cost:   27
c ---[2087]---> BDD-cost:   29
c ---[2086]---> BDD-cost:   19
c ---[2084]---> BDD-cost:   19
c ---[2083]---> BDD-cost:   19
c ---[2082]---> BDD-cost:   31
c ---[2081]---> BDD-cost:   37
c ---[2080]---> BDD-cost:   31
c ---[2079]---> BDD-cost:   37
c ---[2078]---> BDD-cost:   11
c ---[2077]---> BDD-cost:   13
c ---[2076]---> BDD-cost:   13
c ---[2075]---> BDD-cost:   37
c ---[2073]---> BDD-cost:   37
c ---[2072]---> BDD-cost:   37
c ---[2071]---> BDD-cost:   37
c ---[2070]---> BDD-cost:   31
c ---[2069]---> BDD-cost:   37
c ---[2068]---> BDD-cost:   31
c ---[2067]---> BDD-cost:   37
c ---[2066]---> BDD-cost:   19
c ---[2065]---> BDD-cost:   19
c ---[2064]---> BDD-cost:    7
c ---[2062]---> BDD-cost:   11
c ---[2061]---> BDD-cost:   27
c ---[2060]---> BDD-cost:   31
c ---[2059]---> BDD-cost:   37
c ---[2058]---> BDD-cost:   27
c ---[2057]---> BDD-cost:   37
c ---[2056]---> BDD-cost:   29
c ---[2055]---> BDD-cost:    7
c ---[2054]---> BDD-cost:    7
c ---[2053]---> BDD-cost:    7
c ---[2051]---> BDD-cost:    7
c ---[2050]---> BDD-cost:   27
c ---[2049]---> BDD-cost:   27
c ---[2048]---> BDD-cost:   37
c ---[2047]---> BDD-cost:   11
c ---[2046]---> BDD-cost:   37
c ---[2045]---> BDD-cost:    7
c ---[2044]---> BDD-cost:   11
c ---[2043]---> BDD-cost:   23
c ---[2042]---> BDD-cost:   29
c ---[2040]---> BDD-cost:   37
c ---[2039]---> BDD-cost:   29
c ---[2038]---> BDD-cost:    7
c ---[2037]---> BDD-cost:   29
c ---[2036]---> BDD-cost:   37
c ---[2035]---> BDD-cost:   19
c ---[2034]---> BDD-cost:   29
c ---[2033]---> BDD-cost:   37
c ---[2032]---> BDD-cost:   27
c ---[2031]---> BDD-cost:    9
c ---[2028]---> BDD-cost:   27
c ---[2027]---> BDD-cost:   27
c ---[2026]---> BDD-cost:   21
c ---[2025]---> BDD-cost:    9
c ---[2024]---> BDD-cost:   11
c ---[2023]---> BDD-cost:   29
c ---[2022]---> BDD-cost:   37
c ---[2021]---> BDD-cost:   37
c ---[2020]---> BDD-cost:   37
c ---[2019]---> BDD-cost:   37
c ---[2017]---> BDD-cost:   37
c ---[2016]---> BDD-cost:   27
c ---[2015]---> BDD-cost:   19
c ---[2014]---> BDD-cost:   27
c ---[2013]---> BDD-cost:   27
c ---[2012]---> BDD-cost:   37
c ---[2011]---> BDD-cost:   25
c ---[2010]---> BDD-cost:    9
c ---[2009]---> BDD-cost:   19
c ---[2008]---> BDD-cost:    9
c ---[2006]---> BDD-cost:    9
c ---[2005]---> BDD-cost:    9
c ---[2004]---> BDD-cost:    7
c ---[2003]---> BDD-cost:    5
c ---[2002]---> BDD-cost:   19
c ---[2001]---> BDD-cost:    3
c ---[2000]---> BDD-cost:    5
c ---[1999]---> BDD-cost:   19
c ---[1998]---> BDD-cost:   19
c ---[1997]---> BDD-cost:   27
c ---[1994]---> BDD-cost:   27
c ---[1993]---> BDD-cost:   27
c ---[1991]---> BDD-cost:    7
c ---[1990]---> BDD-cost:    3
c ---[1989]---> BDD-cost:    9
c ---[1988]---> BDD-cost:    7
c ---[1985]---> BDD-cost:    9
c ---[1984]---> BDD-cost:   27
c ---[1983]---> BDD-cost:   25
c ---[1982]---> BDD-cost:   27
c ---[1981]---> BDD-cost:   27
c ---[1979]---> BDD-cost:    3
c ---[1977]---> BDD-cost:    9
c ---[1976]---> BDD-cost:    9
c ---[1975]---> BDD-cost:   23
c ---[1974]---> BDD-cost:   19
c ---[1973]---> BDD-cost:   19
c ---[1972]---> BDD-cost:   19
c ---[1971]---> BDD-cost:   23
c ---[1970]---> BDD-cost:   37
c ---[1969]---> BDD-cost:   27
c ---[1968]---> BDD-cost:   19
c ---[1966]---> BDD-cost:   19
c ---[1965]---> BDD-cost:   19
c ---[1964]---> BDD-cost:   37
c ---[1963]---> BDD-cost:   19
c ---[1962]---> BDD-cost:   19
c ---[1961]---> BDD-cost:   23
c ---[1960]---> BDD-cost:   23
c ---[1959]---> BDD-cost:   23
c ---[1958]---> BDD-cost:   19
c ---[1957]---> BDD-cost:   23
c ---[1955]---> BDD-cost:    7
c ---[1953]---> BDD-cost:    5
c ---[1952]---> BDD-cost:    5
c ---[1951]---> BDD-cost:    7
c ---[1949]---> BDD-cost:    5
c ---[1947]---> BDD-cost:    5
c ---[1946]---> BDD-cost:   27
c ---[1944]---> BDD-cost:   27
c ---[1943]---> BDD-cost:   19
c ---[1942]---> BDD-cost:   19
c ---[1941]---> BDD-cost:   19
c ---[1940]---> BDD-cost:   19
c ---[1939]---> BDD-cost:   19
c ---[1938]---> BDD-cost:    7
c ---[1937]---> BDD-cost:   19
c ---[1936]---> BDD-cost:   27
c ---[1935]---> BDD-cost:    7
c ---[1933]---> BDD-cost:    7
c ---[1932]---> BDD-cost:   27
c ---[1931]---> BDD-cost:   27
c ---[1930]---> BDD-cost:    7
c ---[1929]---> BDD-cost:    7
c ---[1928]---> BDD-cost:   19
c ---[1927]---> BDD-cost:    7
c ---[1926]---> BDD-cost:   19
c ---[1925]---> BDD-cost:    7
c ---[1924]---> BDD-cost:    7
c ---[1921]---> BDD-cost:   19
c ---[1920]---> BDD-cost:   19
c ---[1919]---> BDD-cost:   19
c ---[1918]---> BDD-cost:   19
c ---[1917]---> BDD-cost:   31
c ---[1916]---> BDD-cost:   19
c ---[1915]---> BDD-cost:   19
c ---[1914]---> BDD-cost:    7
c ---[1913]---> BDD-cost:   19
c ---[1912]---> BDD-cost:   19
c ---[1910]---> BDD-cost:   19
c ---[1909]---> BDD-cost:   27
c ---[1908]---> BDD-cost:   27
c ---[1907]---> BDD-cost:    7
c ---[1906]---> BDD-cost:    7
c ---[1905]---> BDD-cost:    7
c ---[1904]---> BDD-cost:   27
c ---[1903]---> BDD-cost:    7
c ---[1902]---> BDD-cost:   19
c ---[1901]---> BDD-cost:   37
c ---[1899]---> BDD-cost:   27
c ---[1898]---> BDD-cost:   19
c ---[1897]---> BDD-cost:    7
c ---[1896]---> BDD-cost:   37
c ---[1895]---> BDD-cost:   37
c ---[1894]---> BDD-cost:   37
c ---[1893]---> BDD-cost:   19
c ---[1892]---> BDD-cost:   27
c ---[1891]---> BDD-cost:   33
c ---[1890]---> BDD-cost:   37
c ---[1888]---> BDD-cost:    7
c ---[1887]---> BDD-cost:    7
c ---[1886]---> BDD-cost:    9
c ---[1885]---> BDD-cost:    3
c ---[1884]---> BDD-cost:    3
c ---[1883]---> BDD-cost:    7
c ---[1882]---> BDD-cost:    7
c ---[1881]---> BDD-cost: 1710
c ---[1880]---> BDD-cost:   11
c ---[1879]---> BDD-cost:    7
c ---[1878]---> BDD-cost:    7
c ---[1877]---> BDD-cost:    7
c ---[1876]---> BDD-cost:   27
c ---[1875]---> BDD-cost:    7
c ---[1874]---> BDD-cost:    7
c ---[1873]---> BDD-cost:    3
c ---[1872]---> BDD-cost:    3
c ---[1870]---> BDD-cost:    7
c ---[1869]---> BDD-cost:    7
c ---[1868]---> BDD-cost:    5
c ---[1867]---> BDD-cost:    7
c ---[1866]---> BDD-cost:    7
c ---[1865]---> BDD-cost:    3
c ---[1864]---> BDD-cost:   19
c ---[1863]---> BDD-cost:   13
c ---[1862]---> BDD-cost:   19
c ---[1861]---> BDD-cost:   31
c ---[1859]---> BDD-cost:   37
c ---[1858]---> BDD-cost:   13
c ---[1857]---> BDD-cost:   37
c ---[1856]---> BDD-cost:   27
c ---[1855]---> BDD-cost:   27
c ---[1854]---> BDD-cost:   19
c ---[1853]---> BDD-cost:   31
c ---[1852]---> BDD-cost:   37
c ---[1851]---> BDD-cost:   15
c ---[1850]---> BDD-cost:   37
c ---[1848]---> BDD-cost:   19
c ---[1847]---> BDD-cost:   27
c ---[1846]---> BDD-cost:   19
c ---[1845]---> BDD-cost:   19
c ---[1844]---> BDD-cost:   19
c ---[1843]---> BDD-cost:   29
c ---[1842]---> BDD-cost:   37
c ---[1841]---> BDD-cost:   19
c ---[1840]---> BDD-cost:   15
c ---[1839]---> BDD-cost:   37
c ---[1837]---> BDD-cost:   27
c ---[1836]---> BDD-cost:   27
c ---[1835]---> BDD-cost:   19
c ---[1834]---> BDD-cost:   27
c ---[1833]---> BDD-cost:   31
c ---[1832]---> BDD-cost:   37
c ---[1831]---> BDD-cost:   17
c ---[1830]---> BDD-cost:   37
c ---[1829]---> BDD-cost:   15
c ---[1828]---> BDD-cost:   27
c ---[1826]---> BDD-cost:   27
c ---[1825]---> BDD-cost:   27
c ---[1824]---> BDD-cost:   27
c ---[1823]---> BDD-cost:   37
c ---[1822]---> BDD-cost:   27
c ---[1821]---> BDD-cost:    3
c ---[1820]---> BDD-cost:   27
c ---[1819]---> BDD-cost:    7
c ---[1818]---> BDD-cost:    9
c ---[1817]---> BDD-cost:    5
c ---[1814]---> BDD-cost:   11
c ---[1813]---> BDD-cost:   29
c ---[1812]---> BDD-cost:   27
c ---[1811]---> BDD-cost:   23
c ---[1810]---> BDD-cost:   19
c ---[1809]---> BDD-cost:   27
c ---[1808]---> BDD-cost:   27
c ---[1806]---> BDD-cost:    3
c ---[1805]---> BDD-cost:    9
c ---[1802]---> BDD-cost:    5
c ---[1801]---> BDD-cost:    5
c ---[1800]---> BDD-cost:    3
c ---[1799]---> BDD-cost:    3
c ---[1798]---> BDD-cost:    9
c ---[1797]---> BDD-cost:    3
c ---[1796]---> BDD-cost:    9
c ---[1795]---> BDD-cost:    9
c ---[1791]---> BDD-cost:    9
c ---[1790]---> BDD-cost:   11
c ---[1789]---> BDD-cost:    3
c ---[1788]---> BDD-cost:   13
c ---[1786]---> BDD-cost:   13
c ---[1785]---> BDD-cost:    9
c ---[1784]---> BDD-cost:   37
c ---[1783]---> BDD-cost:   37
c ---[1781]---> BDD-cost:   31
c ---[1780]---> BDD-cost:    5
c ---[1779]---> BDD-cost:    7
c ---[1778]---> BDD-cost:    9
c ---[1777]---> BDD-cost:   11
c ---[1776]---> BDD-cost:   11
c ---[1775]---> BDD-cost:   29
c ---[1774]---> BDD-cost:   21
c ---[1773]---> BDD-cost:   37
c ---[1772]---> BDD-cost:   27
c ---[1770]---> BDD-cost:   37
c ---[1769]---> BDD-cost:   29
c ---[1768]---> BDD-cost:    5
c ---[1767]---> BDD-cost:    7
c ---[1766]---> BDD-cost:    9
c ---[1765]---> BDD-cost:   11
c ---[1764]---> BDD-cost:   11
c ---[1763]---> BDD-cost:   31
c ---[1762]---> BDD-cost:   21
c ---[1761]---> BDD-cost:   11
c ---[1759]---> BDD-cost:   29
c ---[1758]---> BDD-cost:   29
c ---[1757]---> BDD-cost:   11
c ---[1756]---> BDD-cost:   31
c ---[1755]---> BDD-cost:   27
c ---[1754]---> BDD-cost:   37
c ---[1753]---> BDD-cost:   35
c ---[1752]---> BDD-cost:   19
c ---[1751]---> BDD-cost:   31
c ---[1750]---> BDD-cost:   15
c ---[1748]---> BDD-cost:   31
c ---[1747]---> BDD-cost:   31
c ---[1746]---> BDD-cost:   31
c ---[1745]---> BDD-cost:   15
c ---[1744]---> BDD-cost:   27
c ---[1743]---> BDD-cost:   27
c ---[1742]---> BDD-cost:   29
c ---[1741]---> BDD-cost:   15
c ---[1740]---> BDD-cost:   19
c ---[1739]---> BDD-cost:   29
c ---[1737]---> BDD-cost:   19
c ---[1736]---> BDD-cost:   37
c ---[1735]---> BDD-cost:   37
c ---[1734]---> BDD-cost:   35
c ---[1733]---> BDD-cost:   29
c ---[1732]---> BDD-cost:   37
c ---[1731]---> BDD-cost:   29
c ---[1730]---> BDD-cost:   19
c ---[1729]---> BDD-cost:   37
c ---[1728]---> BDD-cost:   27
c ---[1726]---> BDD-cost:   19
c ---[1725]---> BDD-cost:   29
c ---[1724]---> BDD-cost:   27
c ---[1723]---> BDD-cost:   19
c ---[1722]---> BDD-cost:   31
c ---[1721]---> BDD-cost:   31
c ---[1720]---> BDD-cost:   29
c ---[1719]---> BDD-cost:   15
c ---[1718]---> BDD-cost:   25
c ---[1717]---> BDD-cost:    7
c ---[1715]---> BDD-cost:   19
c ---[1714]---> BDD-cost:    3
c ---[1713]---> BDD-cost:   27
c ---[1712]---> BDD-cost:   27
c ---[1711]---> BDD-cost:   31
c ---[1710]---> BDD-cost:   29
c ---[1709]---> BDD-cost:   31
c ---[1708]---> BDD-cost:   29
c ---[1707]---> BDD-cost:    7
c ---[1706]---> BDD-cost:   27
c ---[1703]---> BDD-cost:   19
c ---[1702]---> BDD-cost:   11
c ---[1701]---> BDD-cost:   27
c ---[1700]---> BDD-cost:   19
c ---[1699]---> BDD-cost:   37
c ---[1698]---> BDD-cost:   29
c ---[1697]---> BDD-cost:   31
c ---[1696]---> BDD-cost:   19
c ---[1695]---> BDD-cost:   19
c ---[1694]---> BDD-cost:   37
c ---[1692]---> BDD-cost:   21
c ---[1691]---> BDD-cost:   37
c ---[1690]---> BDD-cost:   27
c ---[1689]---> BDD-cost:   27
c ---[1688]---> BDD-cost:   19
c ---[1687]---> BDD-cost:   19
c ---[1686]---> BDD-cost:   31
c ---[1685]---> BDD-cost:   31
c ---[1684]---> BDD-cost:   19
c ---[1683]---> BDD-cost:   13
c ---[1681]---> BDD-cost:    7
c ---[1680]---> BDD-cost:   11
c ---[1679]---> BDD-cost:    5
c ---[1678]---> BDD-cost:    7
c ---[1677]---> BDD-cost:    7
c ---[1676]---> BDD-cost:    7
c ---[1675]---> BDD-cost:   27
c ---[1674]---> BDD-cost:   27
c ---[1673]---> BDD-cost:    7
c ---[1672]---> BDD-cost:    7
c ---[1670]---> BDD-cost:    7
c ---[1669]---> BDD-cost:    7
c ---[1668]---> BDD-cost:    3
c ---[1667]---> BDD-cost:    7
c ---[1666]---> BDD-cost:    7
c ---[1664]---> BDD-cost:    3
c ---[1663]---> BDD-cost:    9
c ---[1662]---> BDD-cost:    9
c ---[1660]---> BDD-cost:    9
c ---[1659]---> BDD-cost:   29
c ---[1658]---> BDD-cost:   29
c ---[1657]---> BDD-cost:   31
c ---[1656]---> BDD-cost:   31
c ---[1655]---> BDD-cost:   37
c ---[1654]---> BDD-cost:   37
c ---[1653]---> BDD-cost:   31
c ---[1652]---> BDD-cost:   25
c ---[1651]---> BDD-cost:   25
c ---[1649]---> BDD-cost:   33
c ---[1648]---> BDD-cost:   37
c ---[1647]---> BDD-cost:   31
c ---[1646]---> BDD-cost:   29
c ---[1645]---> BDD-cost:   29
c ---[1644]---> BDD-cost:   37
c ---[1643]---> BDD-cost:   31
c ---[1642]---> BDD-cost:   37
c ---[1641]---> BDD-cost:   15
c ---[1640]---> BDD-cost:   31
c ---[1638]---> BDD-cost:   37
c ---[1637]---> BDD-cost:   29
c ---[1636]---> BDD-cost:   29
c ---[1635]---> BDD-cost:   37
c ---[1634]---> BDD-cost:   29
c ---[1633]---> BDD-cost:   25
c ---[1632]---> BDD-cost:   31
c ---[1631]---> BDD-cost:   37
c ---[1629]---> BDD-cost:    9
c ---[1626]---> BDD-cost:   37
c ---[1625]---> BDD-cost:   25
c ---[1624]---> BDD-cost:   37
c ---[1623]---> BDD-cost:   25
c ---[1622]---> BDD-cost:   37
c ---[1621]---> BDD-cost:   11
c ---[1620]---> BDD-cost:   37
c ---[1619]---> BDD-cost:   37
c ---[1618]---> BDD-cost:   31
c ---[1616]---> BDD-cost:   29
c ---[1615]---> BDD-cost:   37
c ---[1614]---> BDD-cost:   27
c ---[1613]---> BDD-cost:   37
c ---[1612]---> BDD-cost:   37
c ---[1611]---> BDD-cost:   15
c ---[1610]---> BDD-cost:    7
c ---[1609]---> BDD-cost:   29
c ---[1608]---> BDD-cost:   31
c ---[1607]---> BDD-cost:   13
c ---[1605]---> BDD-cost:   37
c ---[1603]---> BDD-cost:    7
c ---[1602]---> BDD-cost:   19
c ---[1601]---> BDD-cost:    7
c ---[1600]---> BDD-cost:    5
c ---[1599]---> BDD-cost:   19
c ---[1598]---> BDD-cost:   19
c ---[1597]---> BDD-cost:   19
c ---[1596]---> BDD-cost:   27
c ---[1593]---> BDD-cost:    3
c ---[1592]---> BDD-cost:   37
c ---[1591]---> BDD-cost:   37
c ---[1590]---> BDD-cost:   37
c ---[1589]---> BDD-cost:   37
c ---[1588]---> BDD-cost:    3
c ---[1587]---> BDD-cost:   37
c ---[1586]---> BDD-cost:   27
c ---[1585]---> BDD-cost:   33
c ---[1584]---> BDD-cost:   37
c ---[1582]---> BDD-cost:   37
c ---[1581]---> BDD-cost:   25
c ---[1580]---> BDD-cost:   37
c ---[1579]---> BDD-cost:   37
c ---[1578]---> BDD-cost:    9
c ---[1577]---> BDD-cost:    9
c ---[1576]---> BDD-cost:    3
c ---[1572]---> BDD-cost:    5
c ---[1570]---> BDD-cost:    5
c ---[1569]---> BDD-cost:    5
c ---[1568]---> BDD-cost:    5
c ---[1567]---> BDD-cost:   27
c ---[1566]---> BDD-cost:   27
c ---[1565]---> BDD-cost:   27
c ---[1564]---> BDD-cost:   27
c ---[1562]---> BDD-cost:    9
c ---[1561]---> BDD-cost:    9
c ---[1560]---> BDD-cost:   27
c ---[1559]---> BDD-cost:   19
c ---[1558]---> BDD-cost:   19
c ---[1557]---> BDD-cost:    5
c ---[1556]---> BDD-cost:   11
c ---[1555]---> BDD-cost:    5
c ---[1554]---> BDD-cost:   11
c ---[1553]---> BDD-cost:   31
c ---[1551]---> BDD-cost:   31
c ---[1550]---> BDD-cost:   31
c ---[1549]---> BDD-cost:    7
c ---[1548]---> BDD-cost:   11
c ---[1547]---> BDD-cost:   27
c ---[1546]---> BDD-cost:   27
c ---[1545]---> BDD-cost:   19
c ---[1544]---> BDD-cost:    5
c ---[1543]---> BDD-cost:    3
c ---[1542]---> BDD-cost:   23
c ---[1540]---> BDD-cost:   37
c ---[1539]---> BDD-cost:   19
c ---[1538]---> BDD-cost:   19
c ---[1537]---> BDD-cost:   19
c ---[1536]---> BDD-cost:   19
c ---[1535]---> BDD-cost:   27
c ---[1534]---> BDD-cost:   19
c ---[1533]---> BDD-cost:   19
c ---[1532]---> BDD-cost:   27
c ---[1531]---> BDD-cost:   25
c ---[1529]---> BDD-cost:   27
c ---[1528]---> BDD-cost:   27
c ---[1527]---> BDD-cost:   27
c ---[1526]---> BDD-cost:   27
c ---[1525]---> BDD-cost:   19
c ---[1524]---> BDD-cost:   27
c ---[1523]---> BDD-cost:   27
c ---[1522]---> BDD-cost:   37
c ---[1521]---> BDD-cost:   27
c ---[1520]---> BDD-cost:    5
c ---[1518]---> BDD-cost:   19
c ---[1517]---> BDD-cost:    5
c ---[1516]---> BDD-cost:    5
c ---[1515]---> BDD-cost:    5
c ---[1514]---> BDD-cost:    5
c ---[1513]---> BDD-cost:    5
c ---[1512]---> BDD-cost:    5
c ---[1511]---> BDD-cost:    9
c ---[1510]---> BDD-cost:   27
c ---[1509]---> BDD-cost:    5
c ---[1507]---> BDD-cost:    3
c ---[1506]---> BDD-cost:    3
c ---[1505]---> BDD-cost:    3
c ---[1504]---> BDD-cost:    5
c ---[1503]---> BDD-cost:    5
c ---[1502]---> BDD-cost:    5
c ---[1501]---> BDD-cost:   27
c ---[1500]---> BDD-cost:   35
c ---[1499]---> BDD-cost:   15
c ---[1498]---> BDD-cost:   27
c ---[1496]---> BDD-cost:   27
c ---[1495]---> BDD-cost:   27
c ---[1494]---> BDD-cost:   37
c ---[1493]---> BDD-cost:   27
c ---[1492]---> BDD-cost:   37
c ---[1491]---> BDD-cost:    9
c ---[1490]---> BDD-cost:    9
c ---[1489]---> BDD-cost:    9
c ---[1484]---> BDD-cost:   11
c ---[1483]---> BDD-cost:    3
c ---[1482]---> BDD-cost:   13
c ---[1481]---> BDD-cost:    9
c ---[1480]---> BDD-cost:   19
c ---[1479]---> BDD-cost:   27
c ---[1478]---> BDD-cost:   19
c ---[1477]---> BDD-cost:   27
c ---[1476]---> BDD-cost:   27
c ---[1475]---> BDD-cost:   27
c ---[1473]---> BDD-cost:   27
c ---[1472]---> BDD-cost:    3
c ---[1471]---> BDD-cost:   37
c ---[1470]---> BDD-cost:   29
c ---[1469]---> BDD-cost:   33
c ---[1468]---> BDD-cost:   29
c ---[1467]---> BDD-cost:   37
c ---[1466]---> BDD-cost:    3
c ---[1464]---> BDD-cost:    3
c ---[1462]---> BDD-cost:    3
c ---[1461]---> BDD-cost:    3
c ---[1460]---> BDD-cost:    3
c ---[1459]---> BDD-cost:    5
c ---[1458]---> BDD-cost:   27
c ---[1457]---> BDD-cost:   19
c ---[1456]---> BDD-cost:    5
c ---[1455]---> BDD-cost:    7
c ---[1453]---> BDD-cost:    9
c ---[1452]---> BDD-cost:   13
c ---[1451]---> BDD-cost:    7
c ---[1450]---> BDD-cost:   19
c ---[1449]---> BDD-cost:   23
c ---[1448]---> BDD-cost:    5
c ---[1447]---> BDD-cost:    5
c ---[1446]---> BDD-cost:   19
c ---[1445]---> BDD-cost:   27
c ---[1444]---> BDD-cost:    5
c ---[1442]---> BDD-cost:   19
c ---[1441]---> BDD-cost:   27
c ---[1440]---> BDD-cost:   27
c ---[1439]---> BDD-cost:   27
c ---[1438]---> BDD-cost:   27
c ---[1437]---> BDD-cost:   27
c ---[1436]---> BDD-cost:   25
c ---[1435]---> BDD-cost:   19
c ---[1434]---> BDD-cost:   23
c ---[1433]---> BDD-cost:    3
c ---[1431]---> BDD-cost:   27
c ---[1430]---> BDD-cost:   27
c ---[1429]---> BDD-cost:   27
c ---[1428]---> BDD-cost:   27
c ---[1427]---> BDD-cost:   27
c ---[1426]---> BDD-cost:   27
c ---[1425]---> BDD-cost:    3
c ---[1424]---> BDD-cost:    3
c ---[1423]---> BDD-cost:    3
c ---[1422]---> BDD-cost:    3
c ---[1420]---> BDD-cost:    7
c ---[1419]---> BDD-cost:    7
c ---[1417]---> BDD-cost:    3
c ---[1416]---> BDD-cost:    7
c ---[1415]---> BDD-cost:    7
c ---[1413]---> BDD-cost:   27
c ---[1409]---> BDD-cost:   19
c ---[1408]---> BDD-cost:   37
c ---[1407]---> BDD-cost:   19
c ---[1406]---> BDD-cost:   23
c ---[1405]---> BDD-cost:   29
c ---[1404]---> BDD-cost:   31
c ---[1403]---> BDD-cost:   31
c ---[1401]---> BDD-cost:   37
c ---[1400]---> BDD-cost:   11
c ---[1399]---> BDD-cost:   11
c ---[1398]---> BDD-cost:    5
c ---[1396]---> BDD-cost:    5
c ---[1395]---> BDD-cost:   11
c ---[1394]---> BDD-cost:   21
c ---[1393]---> BDD-cost:   37
c ---[1392]---> BDD-cost:   31
c ---[1390]---> BDD-cost:    5
c ---[1389]---> BDD-cost:   31
c ---[1388]---> BDD-cost:   19
c ---[1387]---> BDD-cost:   29
c ---[1386]---> BDD-cost:   37
c ---[1385]---> BDD-cost:   29
c ---[1384]---> BDD-cost:   31
c ---[1383]---> BDD-cost:   21
c ---[1382]---> BDD-cost:    5
c ---[1378]---> BDD-cost:   31
c ---[1377]---> BDD-cost:   37
c ---[1376]---> BDD-cost:   29
c ---[1375]---> BDD-cost:   31
c ---[1374]---> BDD-cost:   27
c ---[1373]---> BDD-cost:   19
c ---[1372]---> BDD-cost:   37
c ---[1371]---> BDD-cost:   37
c ---[1370]---> BDD-cost:   29
c ---[1369]---> BDD-cost:   19
c ---[1367]---> BDD-cost:   37
c ---[1366]---> BDD-cost:   23
c ---[1365]---> BDD-cost:   35
c ---[1364]---> BDD-cost:   37
c ---[1363]---> BDD-cost:   19
c ---[1362]---> BDD-cost:   19
c ---[1361]---> BDD-cost:   23
c ---[1360]---> BDD-cost:   15
c ---[1359]---> BDD-cost:   15
c ---[1358]---> BDD-cost:    9
c ---[1357]---> BDD-cost: 6392
c ---[1356]---> BDD-cost:    3
c ---[1355]---> BDD-cost:   21
c ---[1354]---> BDD-cost:   23
c ---[1353]---> BDD-cost:   19
c ---[1352]---> BDD-cost:   19
c ---[1351]---> BDD-cost:   23
c ---[1350]---> BDD-cost:    7
c ---[1349]---> BDD-cost:   27
c ---[1348]---> BDD-cost:   37
c ---[1347]---> BDD-cost:   29
c ---[1346]---> Adder-cost: 4750   maxlim: 20   bits: 6/5
c ---[1345]---> BDD-cost:   37
c ---[1344]---> BDD-cost:   15
c ---[1343]---> BDD-cost:   27
c ---[1342]---> BDD-cost:   27
c ---[1341]---> BDD-cost:   27
c ---[1340]---> BDD-cost:   27
c ---[1339]---> BDD-cost:   27
c ---[1338]---> BDD-cost:   31
c ---[1337]---> BDD-cost:   25
c ---[1336]---> BDD-cost:   27
c ---[1334]---> BDD-cost:   27
c ---[1333]---> BDD-cost:   27
c ---[1332]---> BDD-cost:   37
c ---[1331]---> BDD-cost:   15
c ---[1330]---> BDD-cost:    3
c ---[1329]---> BDD-cost:    7
c ---[1328]---> BDD-cost:    5
c ---[1327]---> BDD-cost:    5
c ---[1325]---> BDD-cost:   27
c ---[1324]---> BDD-cost:   27
c ---[1323]---> BDD-cost:   27
c ---[1322]---> BDD-cost:   27
c ---[1321]---> BDD-cost:   11
c ---[1319]---> BDD-cost:    3
c ---[1317]---> BDD-cost:    3
c ---[1316]---> BDD-cost:    3
c ---[1305]---> BDD-cost: 6529
c ---[1225]---> BDD-cost: 4492
c ---[1160]---> Adder-cost: 4287   maxlim: 12   bits: 5/4
c ---[1135]---> Adder-cost: 1014   maxlim: 12   bits: 5/4
c ---[1115]---> BDD-cost:   19
c ---[1054]---> BDD-cost: 2117
c ---[ 898]---> BDD-cost:   19
c ---[ 897]---> BDD-cost:   19
c ---[ 896]---> BDD-cost:   27
c ---[ 895]---> BDD-cost:   27
c ---[ 894]---> BDD-cost:   15
c ---[ 893]---> BDD-cost:   29
c ---[ 892]---> BDD-cost:   23
c ---[ 891]---> BDD-cost:   29
c ---[ 890]---> BDD-cost:   27
c ---[ 889]---> BDD-cost:   29
c ---[ 887]---> BDD-cost:   19
c ---[ 886]---> BDD-cost:   21
c ---[ 885]---> BDD-cost:   17
c ---[ 884]---> BDD-cost:   29
c ---[ 883]---> BDD-cost:   37
c ---[ 882]---> BDD-cost:   37
c ---[ 881]---> BDD-cost:   37
c ---[ 880]---> BDD-cost:   27
c ---[ 879]---> BDD-cost:   27
c ---[ 878]---> BDD-cost:   27
c ---[ 876]---> BDD-cost:   19
c ---[ 875]---> BDD-cost:   27
c ---[ 874]---> BDD-cost:   19
c ---[ 873]---> BDD-cost:   37
c ---[ 872]---> BDD-cost:   15
c ---[ 871]---> BDD-cost:   27
c ---[ 870]---> BDD-cost:   15
c ---[ 869]---> BDD-cost:    5
c ---[ 868]---> BDD-cost:   19
c ---[ 867]---> BDD-cost:   27
c ---[ 865]---> BDD-cost:   23
c ---[ 864]---> BDD-cost:   23
c ---[ 863]---> BDD-cost:   23
c ---[ 862]---> BDD-cost:   23
c ---[ 861]---> BDD-cost:   19
c ---[ 860]---> BDD-cost:   31
c ---[ 859]---> BDD-cost:   19
c ---[ 858]---> BDD-cost:   19
c ---[ 857]---> BDD-cost:    3
c ---[ 856]---> BDD-cost:   19
c ---[ 854]---> BDD-cost:    5
c ---[ 853]---> BDD-cost:   27
c ---[ 852]---> BDD-cost:   19
c ---[ 851]---> BDD-cost:   19
c ---[ 850]---> BDD-cost:   19
c ---[ 849]---> BDD-cost:    9
c ---[ 848]---> BDD-cost:   27
c ---[ 847]---> BDD-cost:   19
c ---[ 846]---> BDD-cost:   23
c ---[ 845]---> BDD-cost:   23
c ---[ 842]---> BDD-cost:   23
c ---[ 841]---> BDD-cost:    3
c ---[ 840]---> BDD-cost:   19
c ---[ 839]---> BDD-cost:   19
c ---[ 838]---> BDD-cost:   23
c ---[ 837]---> BDD-cost:   19
c ---[ 836]---> BDD-cost:   19
c ---[ 835]---> BDD-cost:   19
c ---[ 834]---> BDD-cost:   19
c ---[ 833]---> BDD-cost:   19
c ---[ 831]---> BDD-cost:   23
c ---[ 830]---> BDD-cost:   23
c ---[ 829]---> BDD-cost:   19
c ---[ 828]---> BDD-cost:   19
c ---[ 827]---> BDD-cost:   19
c ---[ 826]---> BDD-cost:    5
c ---[ 825]---> BDD-cost:   27
c ---[ 824]---> BDD-cost:   23
c ---[ 823]---> BDD-cost:   19
c ---[ 822]---> BDD-cost:   19
c ---[ 820]---> BDD-cost:   19
c ---[ 819]---> BDD-cost:   19
c ---[ 818]---> BDD-cost:   19
c ---[ 817]---> BDD-cost:   23
c ---[ 816]---> BDD-cost:   23
c ---[ 815]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:   23
c ---[ 813]---> BDD-cost:    5
c ---[ 812]---> BDD-cost:   19
c ---[ 811]---> BDD-cost:   19
c ---[ 809]---> BDD-cost:   19
c ---[ 808]---> BDD-cost:   19
c ---[ 807]---> BDD-cost:   19
c ---[ 806]---> BDD-cost:   19
c ---[ 805]---> BDD-cost:   19
c ---[ 804]---> BDD-cost:   19
c ---[ 803]---> BDD-cost:   19
c ---[ 802]---> BDD-cost:   19
c ---[ 801]---> BDD-cost:   25
c ---[ 800]---> BDD-cost:   25
c ---[ 799]---> BDD-cost: 7839
c ---[ 798]---> BDD-cost:   23
c ---[ 797]---> BDD-cost:   23
c ---[ 796]---> BDD-cost:   23
c ---[ 795]---> BDD-cost:   25
c ---[ 794]---> BDD-cost:   23
c ---[ 793]---> BDD-cost:   25
c ---[ 792]---> BDD-cost:    5
c ---[ 791]---> BDD-cost:   31
c ---[ 790]---> BDD-cost:   27
c ---[ 789]---> BDD-cost:    3
c ---[ 787]---> BDD-cost:    3
c ---[ 786]---> BDD-cost:   27
c ---[ 785]---> BDD-cost:   27
c ---[ 784]---> BDD-cost:   27
c ---[ 783]---> BDD-cost:   27
c ---[ 782]---> BDD-cost:   27
c ---[ 781]---> BDD-cost:    9
c ---[ 780]---> BDD-cost:    5
c ---[ 779]---> BDD-cost:    3
c ---[ 778]---> BDD-cost:    3
c ---[ 777]---> BDD-cost: 6871
c ---[ 776]---> BDD-cost:    3
c ---[ 775]---> BDD-cost:   25
c ---[ 774]---> BDD-cost:   27
c ---[ 773]---> BDD-cost:   29
c ---[ 772]---> BDD-cost:   27
c ---[ 771]---> BDD-cost:   27
c ---[ 770]---> BDD-cost:   29
c ---[ 769]---> BDD-cost:   27
c ---[ 768]---> BDD-cost:   25
c ---[ 767]---> BDD-cost:   37
c ---[ 766]---> Adder-cost: 4736   maxlim: 26   bits: 6/5
c ---[ 765]---> BDD-cost:   37
c ---[ 764]---> BDD-cost:   27
c ---[ 763]---> BDD-cost:   37
c ---[ 762]---> BDD-cost:   27
c ---[ 761]---> BDD-cost:   27
c ---[ 760]---> BDD-cost:   27
c ---[ 759]---> BDD-cost:   27
c ---[ 758]---> BDD-cost:   27
c ---[ 757]---> BDD-cost:   31
c ---[ 756]---> BDD-cost:   31
c ---[ 754]---> BDD-cost:   27
c ---[ 753]---> BDD-cost:   25
c ---[ 752]---> BDD-cost:   37
c ---[ 751]---> BDD-cost:   37
c ---[ 750]---> BDD-cost:   37
c ---[ 749]---> BDD-cost:   27
c ---[ 748]---> BDD-cost:   25
c ---[ 747]---> BDD-cost:   27
c ---[ 746]---> BDD-cost:    9
c ---[ 745]---> BDD-cost:   25
c ---[ 743]---> BDD-cost:   27
c ---[ 742]---> BDD-cost:   27
c ---[ 741]---> BDD-cost:   27
c ---[ 740]---> BDD-cost:   37
c ---[ 739]---> BDD-cost:   37
c ---[ 738]---> BDD-cost:   27
c ---[ 737]---> BDD-cost:   27
c ---[ 736]---> BDD-cost:   27
c ---[ 735]---> BDD-cost:   37
c ---[ 734]---> BDD-cost:   27
c ---[ 731]---> BDD-cost:   27
c ---[ 730]---> BDD-cost:   37
c ---[ 729]---> BDD-cost:    5
c ---[ 728]---> BDD-cost:    5
c ---[ 727]---> BDD-cost:   37
c ---[ 725]---> BDD-cost:   27
c ---[ 724]---> BDD-cost:   31
c ---[ 723]---> BDD-cost:   19
c ---[ 720]---> BDD-cost:   27
c ---[ 719]---> BDD-cost:   27
c ---[ 718]---> BDD-cost:   37
c ---[ 717]---> BDD-cost:   37
c ---[ 716]---> BDD-cost:   19
c ---[ 715]---> BDD-cost:   27
c ---[ 714]---> BDD-cost:   23
c ---[ 712]---> BDD-cost:    3
c ---[ 711]---> BDD-cost:   27
c ---[ 709]---> BDD-cost:    5
c ---[ 708]---> BDD-cost:    7
c ---[ 707]---> BDD-cost:   27
c ---[ 706]---> BDD-cost:   27
c ---[ 705]---> BDD-cost:   27
c ---[ 704]---> BDD-cost:   27
c ---[ 703]---> BDD-cost:   27
c ---[ 702]---> BDD-cost:   27
c ---[ 701]---> BDD-cost:   27
c ---[ 700]---> BDD-cost:   27
c ---[ 698]---> BDD-cost:   27
c ---[ 697]---> BDD-cost:   27
c ---[ 696]---> BDD-cost:   19
c ---[ 695]---> BDD-cost:    3
c ---[ 694]---> BDD-cost:    7
c ---[ 693]---> BDD-cost:   19
c ---[ 692]---> BDD-cost:    9
c ---[ 691]---> BDD-cost:   37
c ---[ 690]---> BDD-cost:   37
c ---[ 689]---> BDD-cost:   37
c ---[ 687]---> BDD-cost:   27
c ---[ 686]---> BDD-cost:   27
c ---[ 685]---> BDD-cost:    5
c ---[ 684]---> BDD-cost:   19
c ---[ 683]---> BDD-cost:    5
c ---[ 682]---> BDD-cost:   27
c ---[ 681]---> BDD-cost:   27
c ---[ 680]---> BDD-cost:   27
c ---[ 679]---> BDD-cost:   27
c ---[ 678]---> BDD-cost:   19
c ---[ 675]---> BDD-cost:   29
c ---[ 674]---> BDD-cost:   19
c ---[ 673]---> BDD-cost:   27
c ---[ 672]---> BDD-cost:   19
c ---[ 671]---> BDD-cost:   27
c ---[ 670]---> BDD-cost:   19
c ---[ 669]---> BDD-cost:    3
c ---[ 668]---> BDD-cost:    3
c ---[ 667]---> BDD-cost:   19
c ---[ 664]---> BDD-cost:   27
c ---[ 663]---> BDD-cost:    3
c ---[ 662]---> BDD-cost:   27
c ---[ 661]---> BDD-cost:   37
c ---[ 660]---> BDD-cost:   27
c ---[ 659]---> BDD-cost:   27
c ---[ 658]---> BDD-cost:   27
c ---[ 657]---> BDD-cost:   27
c ---[ 656]---> BDD-cost:   15
c ---[ 654]---> BDD-cost:   27
c ---[ 653]---> BDD-cost:   27
c ---[ 652]---> BDD-cost:   27
c ---[ 651]---> BDD-cost:   27
c ---[ 650]---> BDD-cost:   25
c ---[ 649]---> BDD-cost:   37
c ---[ 648]---> BDD-cost:   31
c ---[ 647]---> BDD-cost:   37
c ---[ 646]---> BDD-cost:    5
c ---[ 645]---> BDD-cost:   19
c ---[ 643]---> BDD-cost:   27
c ---[ 642]---> BDD-cost:    3
c ---[ 640]---> BDD-cost:   19
c ---[ 638]---> BDD-cost:    3
c ---[ 636]---> BDD-cost:   31
c ---[ 635]---> BDD-cost:   23
c ---[ 634]---> BDD-cost:   25
c ---[ 632]---> BDD-cost:   37
c ---[ 631]---> BDD-cost:   31
c ---[ 630]---> BDD-cost:   27
c ---[ 629]---> BDD-cost:   19
c ---[ 628]---> BDD-cost:   27
c ---[ 627]---> BDD-cost:   19
c ---[ 626]---> BDD-cost:   19
c ---[ 625]---> BDD-cost:   19
c ---[ 624]---> BDD-cost:   37
c ---[ 623]---> BDD-cost:   37
c ---[ 620]---> BDD-cost:   27
c ---[ 619]---> BDD-cost:   27
c ---[ 618]---> BDD-cost:   27
c ---[ 617]---> BDD-cost:   19
c ---[ 616]---> BDD-cost:   27
c ---[ 615]---> BDD-cost:   27
c ---[ 614]---> BDD-cost:   37
c ---[ 613]---> BDD-cost:   25
c ---[ 612]---> BDD-cost:   19
c ---[ 611]---> BDD-cost:   19
c ---[ 609]---> BDD-cost:   13
c ---[ 608]---> BDD-cost:   19
c ---[ 607]---> BDD-cost:   19
c ---[ 606]---> BDD-cost:   19
c ---[ 605]---> BDD-cost:    7
c ---[ 604]---> BDD-cost:    7
c ---[ 603]---> BDD-cost:   27
c ---[ 602]---> BDD-cost:   27
c ---[ 601]---> BDD-cost:    5
c ---[ 600]---> BDD-cost: 8648
c ---[ 599]---> BDD-cost:    7
c ---[ 598]---> BDD-cost:    5
c ---[ 597]---> BDD-cost:    3
c ---[ 596]---> BDD-cost:    7
c ---[ 595]---> BDD-cost:   35
c ---[ 594]---> BDD-cost:   37
c ---[ 593]---> BDD-cost:   19
c ---[ 592]---> BDD-cost:   31
c ---[ 591]---> BDD-cost:   15
c ---[ 589]---> BDD-cost:   25
c ---[ 588]---> BDD-cost:   15
c ---[ 587]---> BDD-cost:   37
c ---[ 586]---> BDD-cost:   37
c ---[ 585]---> BDD-cost:   29
c ---[ 584]---> BDD-cost:    3
c ---[ 583]---> BDD-cost:    7
c ---[ 582]---> BDD-cost:   19
c ---[ 580]---> BDD-cost:    7
c ---[ 578]---> BDD-cost:   37
c ---[ 577]---> BDD-cost:   27
c ---[ 576]---> BDD-cost:   27
c ---[ 575]---> BDD-cost:   25
c ---[ 574]---> BDD-cost:   27
c ---[ 573]---> BDD-cost:   27
c ---[ 572]---> BDD-cost:   27
c ---[ 571]---> BDD-cost:    3
c ---[ 567]---> BDD-cost:   33
c ---[ 566]---> BDD-cost:   29
c ---[ 565]---> BDD-cost:   31
c ---[ 564]---> BDD-cost:   37
c ---[ 563]---> BDD-cost:   31
c ---[ 562]---> BDD-cost:   15
c ---[ 561]---> BDD-cost:   13
c ---[ 560]---> BDD-cost:   29
c ---[ 559]---> BDD-cost:   37
c ---[ 557]---> BDD-cost:   13
c ---[ 556]---> BDD-cost:   37
c ---[ 555]---> BDD-cost:   27
c ---[ 554]---> BDD-cost:   27
c ---[ 553]---> BDD-cost:   19
c ---[ 552]---> BDD-cost:   15
c ---[ 551]---> BDD-cost:   37
c ---[ 550]---> BDD-cost:   15
c ---[ 549]---> BDD-cost:   27
c ---[ 548]---> BDD-cost:   29
c ---[ 546]---> BDD-cost:   29
c ---[ 545]---> BDD-cost:   31
c ---[ 544]---> BDD-cost:   37
c ---[ 543]---> BDD-cost:   37
c ---[ 542]---> BDD-cost:   31
c ---[ 541]---> BDD-cost:   29
c ---[ 540]---> BDD-cost:   31
c ---[ 539]---> BDD-cost:   31
c ---[ 538]---> BDD-cost:   31
c ---[ 537]---> BDD-cost:   37
c ---[ 535]---> BDD-cost:   31
c ---[ 534]---> BDD-cost:   31
c ---[ 533]---> BDD-cost:   31
c ---[ 532]---> BDD-cost:   29
c ---[ 531]---> BDD-cost:   29
c ---[ 530]---> BDD-cost:   29
c ---[ 529]---> BDD-cost:   29
c ---[ 528]---> BDD-cost:   31
c ---[ 527]---> BDD-cost:   37
c ---[ 526]---> BDD-cost:   37
c ---[ 524]---> BDD-cost:   37
c ---[ 523]---> BDD-cost:   37
c ---[ 522]---> BDD-cost:   35
c ---[ 521]---> BDD-cost:   33
c ---[ 520]---> BDD-cost:   37
c ---[ 519]---> BDD-cost:   35
c ---[ 518]---> BDD-cost:   37
c ---[ 517]---> BDD-cost:   31
c ---[ 516]---> BDD-cost:   31
c ---[ 515]---> BDD-cost:   31
c ---[ 512]---> BDD-cost:   33
c ---[ 511]---> BDD-cost:   37
c ---[ 510]---> BDD-cost:   31
c ---[ 509]---> BDD-cost:   31
c ---[ 508]---> BDD-cost:   31
c ---[ 507]---> BDD-cost:   31
c ---[ 506]---> BDD-cost:   29
c ---[ 505]---> BDD-cost:   31
c ---[ 504]---> BDD-cost:   37
c ---[ 503]---> BDD-cost:   29
c ---[ 501]---> BDD-cost:   37
c ---[ 500]---> BDD-cost:   33
c ---[ 499]---> BDD-cost:   31
c ---[ 498]---> BDD-cost:   29
c ---[ 497]---> BDD-cost:   31
c ---[ 496]---> BDD-cost:   29
c ---[ 495]---> BDD-cost:   31
c ---[ 494]---> BDD-cost:   35
c ---[ 493]---> BDD-cost:   37
c ---[ 492]---> BDD-cost:   29
c ---[ 490]---> BDD-cost:   29
c ---[ 489]---> BDD-cost:   31
c ---[ 488]---> BDD-cost:   31
c ---[ 487]---> BDD-cost:   35
c ---[ 485]---> BDD-cost:    5
c ---[ 484]---> BDD-cost:    3
c ---[ 483]---> BDD-cost:    9
c ---[ 482]---> BDD-cost:    9
c ---[ 481]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:   19
c ---[ 478]---> BDD-cost:   19
c ---[ 477]---> BDD-cost:   37
c ---[ 476]---> BDD-cost:   37
c ---[ 475]---> BDD-cost:   29
c ---[ 474]---> BDD-cost:    5
c ---[ 473]---> BDD-cost:   13
c ---[ 472]---> BDD-cost:    9
c ---[ 471]---> BDD-cost:   11
c ---[ 470]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:   31
c ---[ 467]---> BDD-cost:   21
c ---[ 466]---> BDD-cost:   23
c ---[ 465]---> BDD-cost:   19
c ---[ 464]---> BDD-cost:    5
c ---[ 463]---> BDD-cost:    5
c ---[ 462]---> BDD-cost:    7
c ---[ 461]---> BDD-cost:    7
c ---[ 460]---> BDD-cost:   19
c ---[ 459]---> BDD-cost:   19
c ---[ 457]---> BDD-cost:   37
c ---[ 456]---> BDD-cost:    5
c ---[ 455]---> BDD-cost:   11
c ---[ 454]---> BDD-cost:   31
c ---[ 453]---> BDD-cost:   31
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    9
c ---[ 449]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    5
c ---[ 446]---> BDD-cost:   19
c ---[ 445]---> BDD-cost:   23
c ---[ 443]---> BDD-cost:   27
c ---[ 442]---> BDD-cost:   27
c ---[ 441]---> BDD-cost:   19
c ---[ 440]---> BDD-cost:    3
c ---[ 439]---> BDD-cost:   37
c ---[ 438]---> BDD-cost:   27
c ---[ 437]---> BDD-cost:   27
c ---[ 435]---> BDD-cost:   27
c ---[ 434]---> BDD-cost:   19
c ---[ 433]---> BDD-cost:   27
c ---[ 432]---> BDD-cost:   27
c ---[ 431]---> BDD-cost:   27
c ---[ 430]---> BDD-cost:   19
c ---[ 428]---> BDD-cost:    3
c ---[ 424]---> BDD-cost:    3
c ---[ 423]---> BDD-cost:    9
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    5
c ---[ 420]---> BDD-cost:   19
c ---[ 419]---> BDD-cost:   19
c ---[ 418]---> BDD-cost:    3
c ---[ 417]---> BDD-cost:    5
c ---[ 416]---> BDD-cost:   27
c ---[ 415]---> BDD-cost:    5
c ---[ 413]---> BDD-cost:   27
c ---[ 412]---> BDD-cost:   27
c ---[ 411]---> BDD-cost:   19
c ---[ 410]---> BDD-cost:    3
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:   37
c ---[ 407]---> BDD-cost:   37
c ---[ 406]---> BDD-cost:   27
c ---[ 405]---> BDD-cost:   27
c ---[ 404]---> BDD-cost:   27
c ---[ 403]---> BDD-cost: 2076
c ---[ 402]---> BDD-cost:  908
c ---[ 401]---> BDD-cost:  282
c ---[ 400]---> BDD-cost:   66
c ---[ 399]---> BDD-cost:   24
c ---[ 398]---> BDD-cost:  458
c ---[ 397]---> BDD-cost:    1
c ---[ 396]---> BDD-cost:  142
c ---[ 395]---> BDD-cost:   69
c ---[ 394]---> BDD-cost:   69
c ---[ 393]---> BDD-cost:  188
c ---[ 392]---> BDD-cost:   60
c ---[ 391]---> BDD-cost:  286
c ---[ 390]---> BDD-cost:   76
c ---[ 389]---> BDD-cost:  136
c ---[ 388]---> BDD-cost:  212
c ---[ 387]---> BDD-cost:  286
c ---[ 386]---> BDD-cost: 1841
c ---[ 385]---> BDD-cost: 2354
c ---[ 384]---> Adder-cost: 957   maxlim: 14   bits: 5/4
c ---[ 383]---> BDD-cost:   62
c ---[ 382]---> BDD-cost:   70
c ---[ 381]---> BDD-cost:   36
c ---[ 380]---> BDD-cost:   22
c ---[ 379]---> BDD-cost:   32
c ---[ 378]---> BDD-cost:   56
c ---[ 377]---> BDD-cost: 1461
c ---[ 376]---> BDD-cost: 1569
c ---[ 375]---> BDD-cost:  846
c ---[ 374]---> BDD-cost:   95
c ---[ 373]---> BDD-cost:  151
c ---[ 372]---> BDD-cost:  371
c ---[ 371]---> BDD-cost:  296
c ---[ 370]---> BDD-cost:  521
c ---[ 369]---> BDD-cost:  151
c ---[ 368]---> Adder-cost: 110   maxlim: 11   bits: 5/4
c ---[ 367]---> BDD-cost: 3498
c ---[ 366]---> BDD-cost:  238
c ---[ 365]---> BDD-cost:   72
c ---[ 364]---> BDD-cost:   24
c ---[ 363]---> BDD-cost:   12
c ---[ 362]---> BDD-cost:   70
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:  108
c ---[ 359]---> BDD-cost:   38
c ---[ 358]---> BDD-cost: 3147
c ---[ 357]---> BDD-cost:   56
c ---[ 356]---> BDD-cost:   74
c ---[ 355]---> BDD-cost:  116
c ---[ 354]---> BDD-cost:   28
c ---[ 353]---> BDD-cost:  302
c ---[ 352]---> BDD-cost:   72
c ---[ 351]---> BDD-cost:   78
c ---[ 350]---> BDD-cost:  663
c ---[ 349]---> BDD-cost: 1344
c ---[ 348]---> BDD-cost:  277
c ---[ 347]---> BDD-cost:  114
c ---[ 346]---> BDD-cost:   26
c ---[ 345]---> BDD-cost:  996
c ---[ 344]---> BDD-cost:   14
c ---[ 343]---> BDD-cost:    8
c ---[ 342]---> BDD-cost:  124
c ---[ 341]---> BDD-cost:   28
c ---[ 340]---> BDD-cost:  511
c ---[ 339]---> BDD-cost: 1291
c ---[ 338]---> BDD-cost:  595
c ---[ 337]---> BDD-cost: 1788
c ---[ 336]---> BDD-cost: 2664
c ---[ 335]---> BDD-cost: 2280
c ---[ 334]---> BDD-cost: 3516
c ---[ 333]---> BDD-cost:   38
c ---[ 332]---> BDD-cost: 2211
c ---[ 331]---> BDD-cost: 2709
c ---[ 330]---> BDD-cost:   24
c ---[ 329]---> BDD-cost:   92
c ---[ 328]---> BDD-cost:   46
c ---[ 327]---> BDD-cost:  312
c ---[ 326]---> BDD-cost:   94
c ---[ 325]---> BDD-cost:   44
c ---[ 324]---> BDD-cost:   20
c ---[ 323]---> BDD-cost:   62
c ---[ 322]---> BDD-cost:    8
c ---[ 321]---> BDD-cost:  306
c ---[ 320]---> BDD-cost:  342
c ---[ 319]---> BDD-cost: 4547
c ---[ 318]---> BDD-cost:  548
c ---[ 317]---> BDD-cost:  781
c ---[ 316]---> BDD-cost:  627
c ---[ 315]---> BDD-cost: 1748
c ---[ 314]---> BDD-cost:  720
c ---[ 313]---> BDD-cost:  880
c ---[ 312]---> BDD-cost: 3295
c ---[ 311]---> BDD-cost: 1668
c ---[ 310]---> BDD-cost: 2411
c ---[ 309]---> BDD-cost: 2415
c ---[ 308]---> BDD-cost: 2403
c ---[ 307]---> BDD-cost:  860
c ---[ 306]---> BDD-cost:  462
c ---[ 305]---> BDD-cost:  176
c ---[ 304]---> BDD-cost: 1611
c ---[ 303]---> BDD-cost:  871
c ---[ 302]---> BDD-cost:  949
c ---[ 301]---> BDD-cost:  196
c ---[ 300]---> BDD-cost:  221
c ---[ 299]---> BDD-cost: 2254
c ---[ 298]---> BDD-cost: 2011
c ---[ 297]---> BDD-cost: 3585
c ---[ 296]---> BDD-cost:  277
c ---[ 295]---> BDD-cost:  303
c ---[ 294]---> BDD-cost: 3565
c ---[ 293]---> BDD-cost:  498
c ---[ 292]---> BDD-cost: 2702
c ---[ 291]---> BDD-cost:  954
c ---[ 290]---> BDD-cost: 1050
c ---[ 289]---> BDD-cost:  997
c ---[ 288]---> BDD-cost: 1251
c ---[ 287]---> BDD-cost: 2066
c ---[ 286]---> BDD-cost: 2373
c ---[ 285]---> BDD-cost:  250
c ---[ 284]---> BDD-cost:  280
c ---[ 283]---> BDD-cost:  158
c ---[ 282]---> BDD-cost:  834
c ---[ 281]---> BDD-cost: 3948
c ---[ 280]---> BDD-cost: 4777
c ---[ 279]---> BDD-cost: 4829
c ---[ 278]---> BDD-cost: 2776
c ---[ 277]---> BDD-cost:  178
c ---[ 276]---> BDD-cost:  203
c ---[ 275]---> BDD-cost: 1409
c ---[ 274]---> BDD-cost:  106
c ---[ 273]---> BDD-cost:  121
c ---[ 272]---> BDD-cost:  290
c ---[ 271]---> BDD-cost: 1672
c ---[ 270]---> BDD-cost: 2035
c ---[ 269]---> BDD-cost:  610
c ---[ 268]---> BDD-cost:  675
c ---[ 267]---> BDD-cost: 1359
c ---[ 266]---> BDD-cost: 1630
c ---[ 265]---> BDD-cost:  488
c ---[ 264]---> BDD-cost:  630
c ---[ 263]---> BDD-cost:  689
c ---[ 262]---> BDD-cost:  440
c ---[ 261]---> BDD-cost:   74
c ---[ 260]---> BDD-cost:  485
c ---[ 259]---> BDD-cost: 2754
c ---[ 258]---> BDD-cost: 3636
c ---[ 257]---> BDD-cost: 1450
c ---[ 256]---> BDD-cost: 1830
c ---[ 255]---> BDD-cost:  236
c ---[ 254]---> BDD-cost:  271
c ---[ 253]---> BDD-cost:  832
c ---[ 252]---> BDD-cost:  909
c ---[ 251]---> BDD-cost: 4202
c ---[ 250]---> BDD-cost:  594
c ---[ 249]---> BDD-cost: 5072
c ---[ 248]---> BDD-cost:  958
c ---[ 247]---> BDD-cost: 1096
c ---[ 246]---> BDD-cost:    1
c ---[ 245]---> BDD-cost: 1018
c ---[ 244]---> BDD-cost:  258
c ---[ 243]---> BDD-cost:  288
c ---[ 242]---> Adder-cost: 3392   maxlim: 10   bits: 5/4
c ---[ 241]---> BDD-cost: 1066
c ---[ 240]---> BDD-cost: 1860
c ---[ 239]---> BDD-cost: 2798
c ---[ 238]---> BDD-cost:  142
c ---[ 237]---> BDD-cost:  168
c ---[ 236]---> BDD-cost:  192
c ---[ 235]---> BDD-cost: 3957
c ---[ 234]---> BDD-cost:  970
c ---[ 233]---> BDD-cost: 1582
c ---[ 232]---> BDD-cost:  344
c ---[ 231]---> BDD-cost: 1448
c ---[ 230]---> BDD-cost:  100
c ---[ 229]---> BDD-cost:  116
c ---[ 228]---> BDD-cost: 1253
c ---[ 227]---> BDD-cost:  468
c ---[ 226]---> BDD-cost: 1904
c ---[ 225]---> BDD-cost:  419
c ---[ 224]---> BDD-cost:  460
c ---[ 223]---> BDD-cost: 1658
c ---[ 222]---> BDD-cost:  701
c ---[ 221]---> BDD-cost: 2130
c ---[ 220]---> BDD-cost:   80
c ---[ 219]---> BDD-cost:   95
c ---[ 218]---> BDD-cost: 3979
c ---[ 217]---> BDD-cost:  458
c ---[ 216]---> BDD-cost: 5600
c ---[ 215]---> BDD-cost:   90
c ---[ 214]---> BDD-cost:  565
c ---[ 213]---> BDD-cost:  730
c ---[ 212]---> BDD-cost:  441
c ---[ 211]---> BDD-cost:  753
c ---[ 210]---> BDD-cost:  562
c ---[ 209]---> BDD-cost:  617
c ---[ 208]---> BDD-cost:  704
c ---[ 207]---> BDD-cost:  773
c ---[ 206]---> BDD-cost:  457
c ---[ 205]---> BDD-cost:  506
c ---[ 204]---> BDD-cost:  692
c ---[ 203]---> BDD-cost: 5059
c ---[ 202]---> Adder-cost: 1594   maxlim: 8   bits: 5/4
c ---[ 201]---> Adder-cost: 1215   maxlim: 6   bits: 4/3
c ---[ 200]---> BDD-cost:  897
c ---[ 199]---> BDD-cost: 1064
c ---[ 198]---> BDD-cost:  892
c ---[ 197]---> BDD-cost: 2574
c ---[ 196]---> BDD-cost:  328
c ---[ 195]---> BDD-cost: 3535
c ---[ 194]---> BDD-cost: 2951
c ---[ 193]---> BDD-cost:  321
c ---[ 192]---> BDD-cost:  415
c ---[ 191]---> BDD-cost: 3033
c ---[ 190]---> Adder-cost: 2487   maxlim: 7   bits: 4/3
c ---[ 189]---> BDD-cost:  795
c ---[ 188]---> BDD-cost:  181
c ---[ 187]---> BDD-cost:  706
c ---[ 186]---> BDD-cost:  152
c ---[ 185]---> BDD-cost: 1295
c ---[ 184]---> BDD-cost:  873
c ---[ 183]---> BDD-cost: 6611
c ---[ 182]---> BDD-cost: 2264
c ---[ 181]---> Adder-cost: 1990   maxlim: 5   bits: 4/3
c ---[ 180]---> BDD-cost:  917
c ---[ 179]---> BDD-cost: 1337
c ---[ 178]---> Adder-cost: 5443   maxlim: 20   bits: 6/5
c ---[ 177]---> BDD-cost:  148
c ---[ 176]---> BDD-cost:  160
c ---[ 175]---> BDD-cost: 3125
c ---[ 174]---> Adder-cost: 1114   maxlim: 5   bits: 4/3
c ---[ 173]---> Adder-cost: 1274   maxlim: 5   bits: 4/3
c ---[ 172]---> BDD-cost:  794
c ---[ 171]---> BDD-cost: 5956
c ---[ 170]---> BDD-cost:  896
c ---[ 169]---> BDD-cost:  292
c ---[ 168]---> BDD-cost:  142
c ---[ 167]---> BDD-cost:  186
c ---[ 166]---> BDD-cost:  418
c ---[ 165]---> BDD-cost:  856
c ---[ 164]---> BDD-cost: 1182
c ---[ 163]---> BDD-cost:  178
c ---[ 162]---> BDD-cost:  677
c ---[ 161]---> BDD-cost:    4
c ---[ 160]---> BDD-cost: 1166
c ---[ 159]---> BDD-cost:  526
c ---[ 158]---> BDD-cost:  382
c ---[ 157]---> BDD-cost: 1636
c ---[ 156]---> BDD-cost:  616
c ---[ 155]---> BDD-cost:  392
c ---[ 154]---> BDD-cost:  800
c ---[ 153]---> BDD-cost:   32
c ---[ 152]---> BDD-cost:    8
c ---[ 151]---> BDD-cost:    8
c ---[ 150]---> Adder-cost: 2320   maxlim: 8   bits: 5/4
c ---[ 149]---> BDD-cost:   26
c ---[ 148]---> BDD-cost:   22
c ---[ 147]---> BDD-cost:  710
c ---[ 146]---> BDD-cost:  978
c ---[ 145]---> BDD-cost:  452
c ---[ 144]---> BDD-cost: 1682
c ---[ 143]---> BDD-cost:  258
c ---[ 142]---> BDD-cost:  288
c ---[ 141]---> BDD-cost:   86
c ---[ 140]---> BDD-cost:  490
c ---[ 139]---> BDD-cost:  400
c ---[ 138]---> BDD-cost:   28
c ---[ 137]---> Adder-cost: 1217   maxlim: 12   bits: 5/4
c ---[ 136]---> BDD-cost:    6
c ---[ 135]---> BDD-cost:  784
c ---[ 134]---> BDD-cost:    2
c ---[ 133]---> BDD-cost:  576
c ---[ 132]---> BDD-cost:  924
c ---[ 131]---> BDD-cost:  398
c ---[ 130]---> BDD-cost:  132
c ---[ 129]---> BDD-cost:  122
c ---[ 128]---> BDD-cost:  342
c ---[ 127]---> BDD-cost:  272
c ---[ 126]---> BDD-cost:  173
c ---[ 125]---> BDD-cost:  475
c ---[ 124]---> BDD-cost: 1894
c ---[ 123]---> BDD-cost: 1520
c ---[ 122]---> BDD-cost:  292
c ---[ 121]---> BDD-cost:   78
c ---[ 120]---> BDD-cost: 1290
c ---[ 119]---> BDD-cost:  350
c ---[ 118]---> BDD-cost:  746
c ---[ 117]---> BDD-cost:  110
c ---[ 116]---> BDD-cost:  942
c ---[ 115]---> BDD-cost:   68
c ---[ 114]---> BDD-cost:  801
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:   38
c ---[ 111]---> BDD-cost: 1109
c ---[ 110]---> BDD-cost:  262
c ---[ 109]---> BDD-cost:  912
c ---[ 108]---> BDD-cost:    1
c ---[ 107]---> BDD-cost:    1
c ---[ 106]---> BDD-cost:    1
c ---[ 105]---> BDD-cost: 1102
c ---[ 104]---> BDD-cost:  197
c ---[ 103]---> BDD-cost:    1
c ---[ 102]---> BDD-cost:   26
c ---[ 101]---> BDD-cost:   90
c ---[ 100]---> BDD-cost:  237
c ---[  99]---> BDD-cost: 5235
c ---[  98]---> BDD-cost:   64
c ---[  97]---> BDD-cost:   70
c ---[  96]---> BDD-cost:  593
c ---[  95]---> BDD-cost:  349
c ---[  94]---> BDD-cost:    1
c ---[  93]---> BDD-cost:  842
c ---[  92]---> BDD-cost:    1
c ---[  91]---> BDD-cost:  903
c ---[  90]---> BDD-cost:  176
c ---[  89]---> BDD-cost:   30
c ---[  88]---> BDD-cost: 2094
c ---[  87]---> BDD-cost: 2881
c ---[  86]---> BDD-cost:  456
c ---[  85]---> BDD-cost:  190
c ---[  84]---> BDD-cost: 1917
c ---[  83]---> BDD-cost:  578
c ---[  82]---> BDD-cost: 1815
c ---[  81]---> BDD-cost:  861
c ---[  80]---> BDD-cost: 1838
c ---[  79]---> BDD-cost:  220
c ---[  78]---> BDD-cost:  229
c ---[  77]---> Adder-cost: 1975   maxlim: 8   bits: 5/4
c ---[  76]---> BDD-cost:  299
c ---[  75]---> BDD-cost:   30
c ---[  74]---> BDD-cost:  152
c ---[  73]---> BDD-cost:  750
c ---[  72]---> BDD-cost:  366
c ---[  71]---> BDD-cost: 3010
c ---[  70]---> BDD-cost:  742
c ---[  69]---> BDD-cost: 1038
c ---[  68]---> BDD-cost:  634
c ---[  67]---> BDD-cost:  342
c ---[  66]---> BDD-cost:  102
c ---[  65]---> BDD-cost:  120
c ---[  64]---> BDD-cost:  618
c ---[  63]---> BDD-cost:  164
c ---[  62]---> BDD-cost:   56
c ---[  61]---> BDD-cost:  286
c ---[  60]---> BDD-cost:   18
c ---[  59]---> BDD-cost:  816
c ---[  58]---> BDD-cost:  268
c ---[  57]---> BDD-cost:  186
c ---[  56]---> BDD-cost:   48
c ---[  55]---> BDD-cost:  438
c ---[  54]---> BDD-cost: 1298
c ---[  53]---> BDD-cost: 1097
c ---[  52]---> BDD-cost:  775
c ---[  51]---> BDD-cost:  202
c ---[  50]---> BDD-cost:    1
c ---[  49]---> BDD-cost: 1035
c ---[  48]---> BDD-cost:  254
c ---[  47]---> BDD-cost: 1285
c ---[  46]---> BDD-cost:  439
c ---[  45]---> BDD-cost:   28
c ---[  44]---> BDD-cost:  870
c ---[  43]---> BDD-cost:  368
c ---[  42]---> BDD-cost:  502
c ---[  41]---> BDD-cost:  355
c ---[  40]---> BDD-cost:  226
c ---[  39]---> BDD-cost:  204
c ---[  38]---> BDD-cost:  188
c ---[  37]---> BDD-cost:   38
c ---[  36]---> BDD-cost: 2379
c ---[  35]---> BDD-cost:  306
c ---[  34]---> BDD-cost:  329
c ---[  33]---> BDD-cost:  128
c ---[  32]---> BDD-cost:   66
c ---[  31]---> BDD-cost:   20
c ---[  30]---> BDD-cost:   18
c ---[  29]---> BDD-cost:    8
c ---[  28]---> BDD-cost:   74
c ---[  27]---> BDD-cost:    6
c ---[  26]---> BDD-cost: 3282
c ---[  25]---> BDD-cost: 2908
c ---[  24]---> Adder-cost: 3792   maxlim: 12   bits: 5/4
c ---[  23]---> BDD-cost:   18
c ---[  22]---> BDD-cost: 2567
c ---[  21]---> BDD-cost:   58
c ---[  20]---> BDD-cost:   20
c ---[  19]---> BDD-cost: 1689
c ---[  18]---> Adder-cost: 2581   maxlim: 18   bits: 6/5
c ---[  17]---> BDD-cost:  122
c ---[  16]---> BDD-cost:   54
c ---[  15]---> BDD-cost: 1550
c ---[  14]---> BDD-cost:    1
c ---[  13]---> BDD-cost:   88
c ---[  12]---> BDD-cost:  135
c ---[  11]---> Adder-cost: 4525   maxlim: 11   bits: 5/4
c ---[  10]---> BDD-cost:    1
c ---[   9]---> Adder-cost: 3442   maxlim: 9   bits: 5/4
c ---[   8]---> BDD-cost: 2087
c ---[   7]---> BDD-cost:  552
c ---[   6]---> BDD-cost:    6
c ---[   5]---> BDD-cost:    2
c ---[   4]---> BDD-cost:  974
c ---[   3]---> BDD-cost: 3462
c ---[   2]---> BDD-cost: 4771
c ---[   1]---> BDD-cost:  424
c ---[   0]---> BDD-cost:  118
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1134362  3742257 |  378120       0        0     nan |  0.000 % |
c |       100 | 1134300  3742083 |  415932      89      400     4.5 |  0.376 % |
c |       252 | 1134292  3742059 |  457525     236     1759     7.5 |  0.377 % |
c |       477 | 1134262  3741969 |  503277     447     2569     5.7 |  0.379 % |
c |       814 | 1134211  3741820 |  553605     757     3900     5.2 |  0.382 % |
c |      1320 | 1134201  3741790 |  608966    1259     6268     5.0 |  0.382 % |
c |      2079 | 1134014  3741247 |  669862    1938     9242     4.8 |  0.395 % |
c |      3218 | 1133919  3740976 |  736848    3058    15788     5.2 |  0.403 % |
c |      4926 | 1133861  3740802 |  810533    4747    25914     5.5 |  0.406 % |
c |      7489 | 1133342  3739317 |  891587    7151    43568     6.1 |  0.443 % |
c |     11333 | 1132565  3736994 |  980745   10701    70669     6.6 |  0.495 % |
c |     17100 | 1131986  3735236 | 1078820   16243   105474     6.5 |  0.531 % |
c |     25749 | 1131299  3733075 | 1186702   24638   166089     6.7 |  0.571 % |
c |     38724 | 1130407  3730299 | 1305372   37263   267874     7.2 |  0.623 % |
c |     58185 | 1129554  3727418 | 1435910   56406   462514     8.2 |  0.654 % |
c |     87377 | 1128731  3724675 | 1579501   85217   811244     9.5 |  0.689 % |
ERROR! Too large constants encountered in constraint.
c ==============================================================================
c [1mFound solution: 1493690025[0m
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.94 0.90 2/54 18635
Raw data (stat): 18635 (runsolver) R 18634 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 468608841 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 27782 0 0 0 933 65 0 0 25 0 1 0 468608841 132988928 26333 4294967295 134512640 134672761 3221224624 3221219072 134555357 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32468 26333 603 41 0 32427 0
vsize: 129872
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 36632 0 0 0 1914 84 0 0 25 0 1 0 468608841 164257792 35183 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40102 35183 603 41 0 40061 0
vsize: 160408
[startup+30.0021 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 37330 0 0 0 2912 86 0 0 25 0 1 0 468608841 167096320 35881 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40795 35881 603 41 0 40754 0
vsize: 163180
[startup+40.0019 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 37600 0 0 0 3911 87 0 0 25 0 1 0 468608841 168177664 36151 4294967295 134512640 134672761 3221224624 3221223808 134557980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41059 36151 603 41 0 41018 0
vsize: 164236
[startup+50.0027 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 37778 0 0 0 4910 88 0 0 25 0 1 0 468608841 168988672 36329 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41257 36329 603 41 0 41216 0
vsize: 165028
[startup+60.0034 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38003 0 0 0 5910 88 0 0 25 0 1 0 468608841 169799680 36554 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41455 36554 603 41 0 41414 0
vsize: 165820
[startup+70.0043 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38154 0 0 0 6909 89 0 0 25 0 1 0 468608841 170332160 36705 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41585 36705 603 41 0 41544 0
vsize: 166340
[startup+80.0046 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38330 0 0 0 7909 89 0 0 25 0 1 0 468608841 170868736 36881 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41716 36881 603 41 0 41675 0
vsize: 166864
[startup+90.0049 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38366 0 0 0 8908 90 0 0 25 0 1 0 468608841 171003904 36917 4294967295 134512640 134672761 3221224624 3221223792 134564451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41749 36917 603 41 0 41708 0
vsize: 166996
[startup+100.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38492 0 0 0 9908 90 0 0 25 0 1 0 468608841 171544576 37043 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41881 37043 603 41 0 41840 0
vsize: 167524
[startup+110.019 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38602 0 0 0 10908 91 0 0 25 0 1 0 468608841 171950080 37153 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41980 37153 603 41 0 41939 0
vsize: 167920
[startup+120.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38606 0 0 0 11908 91 0 0 25 0 1 0 468608841 171950080 37157 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41980 37157 603 41 0 41939 0
vsize: 167920
[startup+130.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38644 0 0 0 12908 91 0 0 25 0 1 0 468608841 172085248 37195 4294967295 134512640 134672761 3221224624 3221223816 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42013 37195 603 41 0 41972 0
vsize: 168052
[startup+140.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38705 0 0 0 13908 92 0 0 25 0 1 0 468608841 172355584 37256 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42079 37256 603 41 0 42038 0
vsize: 168316
[startup+150.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38724 0 0 0 14908 92 0 0 25 0 1 0 468608841 172355584 37275 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42079 37275 603 41 0 42038 0
vsize: 168316
[startup+160.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38779 0 0 0 15908 92 0 0 25 0 1 0 468608841 172490752 37330 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42112 37330 603 41 0 42071 0
vsize: 168448
[startup+170.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38839 0 0 0 16907 93 0 0 25 0 1 0 468608841 172761088 37390 4294967295 134512640 134672761 3221224624 3221223792 134564451 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42178 37390 603 41 0 42137 0
vsize: 168712
[startup+180.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38867 0 0 0 17907 93 0 0 25 0 1 0 468608841 172761088 37418 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42178 37418 603 41 0 42137 0
vsize: 168712
[startup+190.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38898 0 0 0 18906 94 0 0 25 0 1 0 468608841 172896256 37449 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42211 37449 603 41 0 42170 0
vsize: 168844
[startup+200.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38916 0 0 0 19906 94 0 0 25 0 1 0 468608841 173031424 37467 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42244 37467 603 41 0 42203 0
vsize: 168976
[startup+210.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38936 0 0 0 20907 94 0 0 25 0 1 0 468608841 173031424 37487 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42244 37487 603 41 0 42203 0
vsize: 168976
[startup+220.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38948 0 0 0 21907 94 0 0 25 0 1 0 468608841 173031424 37499 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42244 37499 603 41 0 42203 0
vsize: 168976
[startup+230.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38974 0 0 0 22907 94 0 0 25 0 1 0 468608841 173166592 37525 4294967295 134512640 134672761 3221224624 3221223748 134566045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42277 37525 603 41 0 42236 0
vsize: 169108
[startup+240.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 38990 0 0 0 23907 94 0 0 25 0 1 0 468608841 173166592 37541 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42277 37541 603 41 0 42236 0
vsize: 169108
[startup+250.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39004 0 0 0 24907 94 0 0 25 0 1 0 468608841 173301760 37555 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42310 37555 603 41 0 42269 0
vsize: 169240
[startup+260.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39029 0 0 0 25907 94 0 0 25 0 1 0 468608841 173514752 37580 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42362 37580 603 41 0 42321 0
vsize: 169448
[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39031 0 0 0 26907 94 0 0 25 0 1 0 468608841 173514752 37582 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42362 37582 603 41 0 42321 0
vsize: 169448
[startup+280.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39045 0 0 0 27908 94 0 0 25 0 1 0 468608841 173514752 37596 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42362 37596 603 41 0 42321 0
vsize: 169448
[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39110 0 0 0 28907 95 0 0 25 0 1 0 468608841 173649920 37661 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42395 37661 603 41 0 42354 0
vsize: 169580
[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39122 0 0 0 29908 95 0 0 25 0 1 0 468608841 173649920 37673 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42395 37673 603 41 0 42354 0
vsize: 169580
[startup+310.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39137 0 0 0 30908 95 0 0 25 0 1 0 468608841 173649920 37688 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42395 37688 603 41 0 42354 0
vsize: 169580
[startup+320.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39154 0 0 0 31908 95 0 0 25 0 1 0 468608841 173785088 37705 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42428 37705 603 41 0 42387 0
vsize: 169712
[startup+330.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39165 0 0 0 32908 95 0 0 25 0 1 0 468608841 173785088 37716 4294967295 134512640 134672761 3221224624 3221223792 134564686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42428 37716 603 41 0 42387 0
vsize: 169712
[startup+340.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39180 0 0 0 33908 95 0 0 25 0 1 0 468608841 173785088 37731 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42428 37731 603 41 0 42387 0
vsize: 169712
[startup+350.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39191 0 0 0 34908 95 0 0 25 0 1 0 468608841 173920256 37742 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42461 37742 603 41 0 42420 0
vsize: 169844
[startup+360.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39206 0 0 0 35908 95 0 0 25 0 1 0 468608841 173920256 37757 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42461 37757 603 41 0 42420 0
vsize: 169844
[startup+370.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39219 0 0 0 36909 95 0 0 25 0 1 0 468608841 174055424 37770 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42494 37770 603 41 0 42453 0
vsize: 169976
[startup+380.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39240 0 0 0 37909 95 0 0 25 0 1 0 468608841 174055424 37791 4294967295 134512640 134672761 3221224624 3221223824 134557876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42494 37791 603 41 0 42453 0
vsize: 169976
[startup+390.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39255 0 0 0 38909 95 0 0 25 0 1 0 468608841 174186496 37806 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42526 37806 603 41 0 42485 0
vsize: 170104
[startup+400.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39264 0 0 0 39909 95 0 0 25 0 1 0 468608841 174186496 37815 4294967295 134512640 134672761 3221224624 3221223840 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42526 37815 603 41 0 42485 0
vsize: 170104
[startup+410.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39277 0 0 0 40909 95 0 0 25 0 1 0 468608841 174186496 37828 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42526 37828 603 41 0 42485 0
vsize: 170104
[startup+420.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39292 0 0 0 41909 95 0 0 25 0 1 0 468608841 174321664 37843 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42559 37843 603 41 0 42518 0
vsize: 170236
[startup+430.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39303 0 0 0 42910 95 0 0 25 0 1 0 468608841 174321664 37854 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42559 37854 603 41 0 42518 0
vsize: 170236
[startup+440.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39353 0 0 0 43910 95 0 0 25 0 1 0 468608841 174321664 37904 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42559 37904 603 41 0 42518 0
vsize: 170236
[startup+450.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39364 0 0 0 44910 95 0 0 25 0 1 0 468608841 174321664 37915 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42559 37915 603 41 0 42518 0
vsize: 170236
[startup+460.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39398 0 0 0 45910 95 0 0 25 0 1 0 468608841 174583808 37949 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42623 37949 603 41 0 42582 0
vsize: 170492
[startup+470.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39399 0 0 0 46910 95 0 0 25 0 1 0 468608841 174583808 37950 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42623 37950 603 41 0 42582 0
vsize: 170492
[startup+480.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39400 0 0 0 47910 95 0 0 25 0 1 0 468608841 174583808 37951 4294967295 134512640 134672761 3221224624 3221223840 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42623 37951 603 41 0 42582 0
vsize: 170492
[startup+490.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39416 0 0 0 48911 96 0 0 25 0 1 0 468608841 174718976 37967 4294967295 134512640 134672761 3221224624 3221223840 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42656 37967 603 41 0 42615 0
vsize: 170624
[startup+500.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39437 0 0 0 49911 96 0 0 25 0 1 0 468608841 174854144 37988 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42689 37988 603 41 0 42648 0
vsize: 170756
[startup+510.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39451 0 0 0 50910 96 0 0 25 0 1 0 468608841 174854144 38002 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42689 38002 603 41 0 42648 0
vsize: 170756
[startup+520.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39463 0 0 0 51911 96 0 0 25 0 1 0 468608841 174854144 38014 4294967295 134512640 134672761 3221224624 3221223852 134557474 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42689 38014 603 41 0 42648 0
vsize: 170756
[startup+530.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39524 0 0 0 52910 96 0 0 25 0 1 0 468608841 174989312 38075 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42722 38075 603 41 0 42681 0
vsize: 170888
[startup+540.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39541 0 0 0 53911 96 0 0 25 0 1 0 468608841 175124480 38092 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42755 38092 603 41 0 42714 0
vsize: 171020
[startup+550.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39554 0 0 0 54911 96 0 0 25 0 1 0 468608841 175124480 38105 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42755 38105 603 41 0 42714 0
vsize: 171020
[startup+560.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39572 0 0 0 55911 96 0 0 25 0 1 0 468608841 175124480 38123 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42755 38123 603 41 0 42714 0
vsize: 171020
[startup+570.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39585 0 0 0 56911 96 0 0 25 0 1 0 468608841 175259648 38136 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42788 38136 603 41 0 42747 0
vsize: 171152
[startup+580.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39601 0 0 0 57911 96 0 0 25 0 1 0 468608841 175259648 38152 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42788 38152 603 41 0 42747 0
vsize: 171152
[startup+590.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39625 0 0 0 58911 96 0 0 25 0 1 0 468608841 175394816 38176 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42821 38176 603 41 0 42780 0
vsize: 171284
[startup+600.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39642 0 0 0 59912 96 0 0 25 0 1 0 468608841 175394816 38193 4294967295 134512640 134672761 3221224624 3221223824 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42821 38193 603 41 0 42780 0
vsize: 171284
[startup+610.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39665 0 0 0 60912 96 0 0 25 0 1 0 468608841 175525888 38216 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42853 38216 603 41 0 42812 0
vsize: 171412
[startup+620.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39682 0 0 0 61912 96 0 0 25 0 1 0 468608841 175661056 38233 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42886 38233 603 41 0 42845 0
vsize: 171544
[startup+630.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39713 0 0 0 62912 96 0 0 25 0 1 0 468608841 175661056 38264 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42886 38264 603 41 0 42845 0
vsize: 171544
[startup+640.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39727 0 0 0 63912 96 0 0 25 0 1 0 468608841 175796224 38278 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42919 38278 603 41 0 42878 0
vsize: 171676
[startup+650.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39764 0 0 0 64913 96 0 0 25 0 1 0 468608841 175931392 38315 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42952 38315 603 41 0 42911 0
vsize: 171808
[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39781 0 0 0 65913 97 0 0 25 0 1 0 468608841 175931392 38332 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42952 38332 603 41 0 42911 0
vsize: 171808
[startup+670.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39794 0 0 0 66914 97 0 0 25 0 1 0 468608841 176066560 38345 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42985 38345 603 41 0 42944 0
vsize: 171940
[startup+680.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39856 0 0 0 67914 97 0 0 25 0 1 0 468608841 176336896 38407 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43051 38407 603 41 0 43010 0
vsize: 172204
[startup+690.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39869 0 0 0 68915 97 0 0 25 0 1 0 468608841 176336896 38420 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43051 38420 603 41 0 43010 0
vsize: 172204
[startup+700.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39891 0 0 0 69915 97 0 0 25 0 1 0 468608841 176472064 38442 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43084 38442 603 41 0 43043 0
vsize: 172336
[startup+710.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39907 0 0 0 70916 97 0 0 25 0 1 0 468608841 176472064 38458 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43084 38458 603 41 0 43043 0
vsize: 172336
[startup+720.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39925 0 0 0 71916 97 0 0 25 0 1 0 468608841 176607232 38476 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43117 38476 603 41 0 43076 0
vsize: 172468
[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39944 0 0 0 72916 97 0 0 25 0 1 0 468608841 176607232 38495 4294967295 134512640 134672761 3221224624 3221223816 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43117 38495 603 41 0 43076 0
vsize: 172468
[startup+740.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39953 0 0 0 73916 97 0 0 25 0 1 0 468608841 176607232 38504 4294967295 134512640 134672761 3221224624 3221223812 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43117 38504 603 41 0 43076 0
vsize: 172468
[startup+750.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 39978 0 0 0 74916 97 0 0 25 0 1 0 468608841 176742400 38529 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43150 38529 603 41 0 43109 0
vsize: 172600
[startup+760.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40061 0 0 0 75917 97 0 0 25 0 1 0 468608841 177274880 38612 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43280 38612 603 41 0 43239 0
vsize: 173120
[startup+770.072 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40116 0 0 0 76916 97 0 0 25 0 1 0 468608841 177545216 38667 4294967295 134512640 134672761 3221224624 3221223760 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43346 38667 603 41 0 43305 0
vsize: 173384
[startup+780.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40150 0 0 0 77916 97 0 0 25 0 1 0 468608841 177680384 38701 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43379 38701 603 41 0 43338 0
vsize: 173516
[startup+790.073 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40178 0 0 0 78917 97 0 0 25 0 1 0 468608841 177815552 38729 4294967295 134512640 134672761 3221224624 3221223824 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43412 38729 603 41 0 43371 0
vsize: 173648
[startup+800.074 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40195 0 0 0 79917 97 0 0 25 0 1 0 468608841 177815552 38746 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43412 38746 603 41 0 43371 0
vsize: 173648
[startup+810.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40242 0 0 0 80917 98 0 0 25 0 1 0 468608841 178085888 38793 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43478 38793 603 41 0 43437 0
vsize: 173912
[startup+820.075 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40268 0 0 0 81917 98 0 0 25 0 1 0 468608841 178085888 38819 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43478 38819 603 41 0 43437 0
vsize: 173912
[startup+830.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40281 0 0 0 82917 98 0 0 25 0 1 0 468608841 178221056 38832 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43511 38832 603 41 0 43470 0
vsize: 174044
[startup+840.076 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40295 0 0 0 83917 98 0 0 25 0 1 0 468608841 178221056 38846 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43511 38846 603 41 0 43470 0
vsize: 174044
[startup+850.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40307 0 0 0 84917 98 0 0 25 0 1 0 468608841 178356224 38858 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43544 38858 603 41 0 43503 0
vsize: 174176
[startup+860.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40326 0 0 0 85918 98 0 0 25 0 1 0 468608841 178356224 38877 4294967295 134512640 134672761 3221224624 3221223792 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43544 38877 603 41 0 43503 0
vsize: 174176
[startup+870.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40340 0 0 0 86918 98 0 0 25 0 1 0 468608841 178491392 38891 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43577 38891 603 41 0 43536 0
vsize: 174308
[startup+880.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40355 0 0 0 87918 98 0 0 25 0 1 0 468608841 178491392 38906 4294967295 134512640 134672761 3221224624 3221223776 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43577 38906 603 41 0 43536 0
vsize: 174308
[startup+890.077 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40377 0 0 0 88918 98 0 0 25 0 1 0 468608841 178626560 38928 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43610 38928 603 41 0 43569 0
vsize: 174440
[startup+900.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40396 0 0 0 89918 98 0 0 25 0 1 0 468608841 178626560 38947 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43610 38947 603 41 0 43569 0
vsize: 174440
[startup+910.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40428 0 0 0 90918 98 0 0 25 0 1 0 468608841 178761728 38979 4294967295 134512640 134672761 3221224624 3221223796 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43643 38979 603 41 0 43602 0
vsize: 174572
[startup+920.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40465 0 0 0 91918 99 0 0 25 0 1 0 468608841 178896896 39016 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43676 39016 603 41 0 43635 0
vsize: 174704
[startup+930.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40516 0 0 0 92918 99 0 0 25 0 1 0 468608841 179163136 39067 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43741 39067 603 41 0 43700 0
vsize: 174964
[startup+940.078 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40567 0 0 0 93918 99 0 0 25 0 1 0 468608841 179298304 39118 4294967295 134512640 134672761 3221224624 3221223812 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43774 39118 603 41 0 43733 0
vsize: 175096
[startup+950.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40588 0 0 0 94918 99 0 0 25 0 1 0 468608841 179433472 39139 4294967295 134512640 134672761 3221224624 3221223840 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43807 39139 603 41 0 43766 0
vsize: 175228
[startup+960.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40646 0 0 0 95918 99 0 0 25 0 1 0 468608841 179568640 39197 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43840 39197 603 41 0 43799 0
vsize: 175360
[startup+970.079 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40677 0 0 0 96918 99 0 0 25 0 1 0 468608841 179703808 39228 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43873 39228 603 41 0 43832 0
vsize: 175492
[startup+980.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40703 0 0 0 97918 99 0 0 25 0 1 0 468608841 179838976 39254 4294967295 134512640 134672761 3221224624 3221223824 134557965 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43906 39254 603 41 0 43865 0
vsize: 175624
[startup+990.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40714 0 0 0 98918 99 0 0 25 0 1 0 468608841 179838976 39265 4294967295 134512640 134672761 3221224624 3221223776 134564785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43906 39265 603 41 0 43865 0
vsize: 175624
[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40739 0 0 0 99919 99 0 0 25 0 1 0 468608841 179974144 39290 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43939 39290 603 41 0 43898 0
vsize: 175756
[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40770 0 0 0 100919 99 0 0 25 0 1 0 468608841 180109312 39321 4294967295 134512640 134672761 3221224624 3221223748 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43972 39321 603 41 0 43931 0
vsize: 175888
[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40801 0 0 0 101919 100 0 0 25 0 1 0 468608841 180244480 39352 4294967295 134512640 134672761 3221224624 3221223792 134560811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44005 39352 603 41 0 43964 0
vsize: 176020
[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40817 0 0 0 102919 100 0 0 25 0 1 0 468608841 180244480 39368 4294967295 134512640 134672761 3221224624 3221223840 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44005 39368 603 41 0 43964 0
vsize: 176020
[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40843 0 0 0 103919 100 0 0 25 0 1 0 468608841 180379648 39394 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44038 39394 603 41 0 43997 0
vsize: 176152
[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40856 0 0 0 104919 100 0 0 25 0 1 0 468608841 180379648 39407 4294967295 134512640 134672761 3221224624 3221223824 134557849 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44038 39407 603 41 0 43997 0
vsize: 176152
[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40874 0 0 0 105919 100 0 0 25 0 1 0 468608841 180514816 39425 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44071 39425 603 41 0 44030 0
vsize: 176284
[startup+1061.54 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 18635
Raw data (stat): 18635 (minisat+) R 18634 26667 26666 0 -1 0 40874 0 0 0 105919 100 0 0 25 0 1 0 468608841 180514816 39425 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44071 39425 603 41 0 44030 0
vsize: 0

Child status: 1
Real time (s): 1061.54
CPU time (s): 1061.65
CPU user time (s): 1060.56
CPU system time (s): 1.09283
CPU usage (%): 100.011
Max. virtual memory (Kb): 176284
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####