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 14275

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        498504 kB
Buffers:         35800 kB
Cached:         476780 kB
SwapCached:          4 kB
Active:         117160 kB
Inactive:       398316 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        498252 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6940 kB
Slab:            14944 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 23:45:11 (client local time) WITH STATUS 0 IN 1200.46 SECONDS
stats: 20239 7 1200.46 0
#### 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]--#### 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.91 0.95 0.90 2/54 26710
Raw data (stat): 26710 (runsolver) R 26709 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482164166 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 29968 0 0 0 918 80 0 0 25 0 1 0 482164166 134754304 28534 4294967295 134512640 134672761 3221224544 3221181552 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32899 28534 603 41 0 32858 0
vsize: 131596
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 62322 0 0 0 1833 164 0 0 25 0 1 0 482164166 279670784 60888 4294967295 134512640 134672761 3221224544 3221223088 134621211 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68279 60888 603 41 0 68238 0
vsize: 273116
[startup+30.0006 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 62322 0 0 0 2833 164 0 0 25 0 1 0 482164166 279670784 60888 4294967295 134512640 134672761 3221224544 3221223088 134621186 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68279 60888 603 41 0 68238 0
vsize: 273116
[startup+40.0003 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 67511 0 0 0 3814 183 0 0 25 0 1 0 482164166 293404672 64157 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71632 64157 603 41 0 71591 0
vsize: 286528
[startup+50.0009 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 69718 0 0 0 4802 196 0 0 25 0 1 0 482164166 302690304 66364 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73899 66364 603 41 0 73858 0
vsize: 295596
[startup+60.0006 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 71023 0 0 0 5793 205 0 0 25 0 1 0 482164166 308441088 67669 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75303 67669 603 41 0 75262 0
vsize: 301212
[startup+70.0012 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 72125 0 0 0 6787 211 0 0 25 0 1 0 482164166 313069568 68771 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 76433 68771 603 41 0 76392 0
vsize: 305732
[startup+80.0021 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 73424 0 0 0 7781 217 0 0 25 0 1 0 482164166 318816256 70070 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77836 70070 603 41 0 77795 0
vsize: 311344
[startup+90.0014 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 75256 0 0 0 8770 228 0 0 25 0 1 0 482164166 326668288 71902 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79753 71902 603 41 0 79712 0
vsize: 319012
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 77577 0 0 0 9758 240 0 0 25 0 1 0 482164166 336543744 74223 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82164 74223 603 41 0 82123 0
vsize: 328656
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 78849 0 0 0 10751 247 0 0 25 0 1 0 482164166 341610496 75495 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83401 75495 603 41 0 83360 0
vsize: 333604
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 80196 0 0 0 11743 255 0 0 25 0 1 0 482164166 347582464 76842 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84859 76842 603 41 0 84818 0
vsize: 339436
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 81672 0 0 0 12737 261 0 0 25 0 1 0 482164166 354062336 78318 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86441 78318 603 41 0 86400 0
vsize: 345764
[startup+140.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 82557 0 0 0 13732 266 0 0 25 0 1 0 482164166 358125568 79203 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87433 79203 603 41 0 87392 0
vsize: 349732
[startup+150.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 82997 0 0 0 14728 269 0 0 25 0 1 0 482164166 360185856 79643 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87936 79643 603 41 0 87895 0
vsize: 351744
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 83719 0 0 0 15725 273 0 0 25 0 1 0 482164166 363515904 80365 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88749 80365 603 41 0 88708 0
vsize: 354996
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 84308 0 0 0 16721 277 0 0 25 0 1 0 482164166 365957120 80954 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 89345 80954 603 41 0 89304 0
vsize: 357380
[startup+180.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 85056 0 0 0 17718 280 0 0 25 0 1 0 482164166 369360896 81702 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 90176 81702 603 41 0 90135 0
vsize: 360704
[startup+190.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 86063 0 0 0 18713 285 0 0 25 0 1 0 482164166 374104064 82709 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 91334 82709 603 41 0 91293 0
vsize: 365336
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 86819 0 0 0 19709 289 0 0 25 0 1 0 482164166 377536512 83465 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 92172 83465 603 41 0 92131 0
vsize: 368688
[startup+210.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 88819 0 0 0 20698 300 0 0 25 0 1 0 482164166 385929216 85465 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 94221 85465 603 41 0 94180 0
vsize: 376884
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 90081 0 0 0 21691 307 0 0 25 0 1 0 482164166 391217152 86727 4294967295 134512640 134672761 3221224544 3221222764 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 95512 86727 603 41 0 95471 0
vsize: 382048
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 91419 0 0 0 22684 314 0 0 25 0 1 0 482164166 397414400 88065 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 97025 88065 603 41 0 96984 0
vsize: 388100
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 92912 0 0 0 23679 319 0 0 25 0 1 0 482164166 403947520 89558 4294967295 134512640 134672761 3221224544 3221222752 1075730206 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 98620 89558 603 41 0 98579 0
vsize: 394480
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 93808 0 0 0 24672 325 0 0 25 0 1 0 482164166 407949312 90454 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 99597 90454 603 41 0 99556 0
vsize: 398388
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 94663 0 0 0 25666 331 0 0 25 0 1 0 482164166 411488256 91309 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 100461 91309 603 41 0 100420 0
vsize: 401844
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 96139 0 0 0 26657 340 0 0 25 0 1 0 482164166 417644544 92785 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 101964 92785 603 41 0 101923 0
vsize: 407856
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 97101 0 0 0 27651 347 0 0 25 0 1 0 482164166 421629952 93747 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 102937 93747 603 41 0 102896 0
vsize: 411748
[startup+290.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 98200 0 0 0 28644 353 0 0 25 0 1 0 482164166 426557440 94846 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 104140 94846 603 41 0 104099 0
vsize: 416560
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 99275 0 0 0 29638 360 0 0 25 0 1 0 482164166 431222784 95921 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 105279 95921 603 41 0 105238 0
vsize: 421116
[startup+310.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 100334 0 0 0 30633 364 0 0 25 0 1 0 482164166 435974144 96980 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 106439 96980 603 41 0 106398 0
vsize: 425756
[startup+320.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 100861 0 0 0 31629 369 0 0 25 0 1 0 482164166 438415360 97507 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 107035 97507 603 41 0 106994 0
vsize: 428140
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 101445 0 0 0 32626 372 0 0 25 0 1 0 482164166 441012224 98091 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 107669 98091 603 41 0 107628 0
vsize: 430676
[startup+340.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 102188 0 0 0 33621 376 0 0 25 0 1 0 482164166 444424192 98834 4294967295 134512640 134672761 3221224544 3221223032 134644405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 108502 98834 603 41 0 108461 0
vsize: 434008
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 102818 0 0 0 34618 380 0 0 25 0 1 0 482164166 447250432 99464 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 109192 99464 603 41 0 109151 0
vsize: 436768
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 103853 0 0 0 35612 386 0 0 25 0 1 0 482164166 451743744 100499 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 110289 100499 603 41 0 110248 0
vsize: 441156
[startup+370.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 104913 0 0 0 36606 393 0 0 25 0 1 0 482164166 456167424 101559 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 111369 101559 603 41 0 111328 0
vsize: 445476
[startup+380.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 105717 0 0 0 37602 396 0 0 25 0 1 0 482164166 460124160 102363 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 112335 102363 603 41 0 112294 0
vsize: 449340
[startup+390.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 106229 0 0 0 38600 399 0 0 25 0 1 0 482164166 462561280 102875 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 112930 102875 603 41 0 112889 0
vsize: 451720
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 106960 0 0 0 39596 403 0 0 25 0 1 0 482164166 465981440 103606 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 113765 103606 603 41 0 113724 0
vsize: 455060
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 107370 0 0 0 40593 406 0 0 25 0 1 0 482164166 467783680 104016 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114205 104016 603 41 0 114164 0
vsize: 456820
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 107401 0 0 0 41589 410 0 0 25 0 1 0 482164166 467947520 104047 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114245 104047 603 41 0 114204 0
vsize: 456980
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 107408 0 0 0 42586 413 0 0 25 0 1 0 482164166 467947520 104054 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114245 104054 603 41 0 114204 0
vsize: 456980
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 107408 0 0 0 43584 415 0 0 25 0 1 0 482164166 467947520 104054 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114245 104054 603 41 0 114204 0
vsize: 456980
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 107409 0 0 0 44583 417 0 0 25 0 1 0 482164166 467947520 104055 4294967295 134512640 134672761 3221224544 3221222992 134606977 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114245 104055 603 41 0 114204 0
vsize: 456980
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 107409 0 0 0 45581 419 0 0 25 0 1 0 482164166 467947520 104055 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114245 104055 603 41 0 114204 0
vsize: 456980
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 107812 0 0 0 46578 422 0 0 25 0 1 0 482164166 469528576 104458 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 114631 104458 603 41 0 114590 0
vsize: 458524
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 108467 0 0 0 47575 425 0 0 25 0 1 0 482164166 472961024 105113 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 115469 105113 603 41 0 115428 0
vsize: 461876
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 109098 0 0 0 48571 429 0 0 25 0 1 0 482164166 475893760 105744 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116185 105744 603 41 0 116144 0
vsize: 464740
[startup+500.004 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 109892 0 0 0 49566 434 0 0 25 0 1 0 482164166 479412224 106538 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 117044 106538 603 41 0 117003 0
vsize: 468176
[startup+510.004 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 111429 0 0 0 50559 441 0 0 25 0 1 0 482164166 486227968 108075 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 118708 108075 603 41 0 118667 0
vsize: 474832
[startup+520.004 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 112189 0 0 0 51554 446 0 0 25 0 1 0 482164166 489508864 108835 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 119509 108835 603 41 0 119468 0
vsize: 478036
[startup+530.004 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 112730 0 0 0 52551 449 0 0 25 0 1 0 482164166 492191744 109376 4294967295 134512640 134672761 3221224544 3221222960 134644277 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120164 109376 603 41 0 120123 0
vsize: 480656
[startup+540.004 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 112890 0 0 0 53548 452 0 0 25 0 1 0 482164166 493023232 109536 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120367 109536 603 41 0 120326 0
vsize: 481468
[startup+550.005 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 113076 0 0 0 54547 454 0 0 25 0 1 0 482164166 493760512 109722 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 120547 109722 603 41 0 120506 0
vsize: 482188
[startup+560.006 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 113582 0 0 0 55544 456 0 0 25 0 1 0 482164166 496238592 110228 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121152 110228 603 41 0 121111 0
vsize: 484608
[startup+570.005 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 114033 0 0 0 56542 459 0 0 25 0 1 0 482164166 498388992 110679 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 121677 110679 603 41 0 121636 0
vsize: 486708
[startup+580.006 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 114460 0 0 0 57539 462 0 0 25 0 1 0 482164166 500359168 111106 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 122158 111106 603 41 0 122117 0
vsize: 488632
[startup+590.005 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 114963 0 0 0 58537 464 0 0 25 0 1 0 482164166 502685696 111609 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 122726 111609 603 41 0 122685 0
vsize: 490904
[startup+600.006 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 115438 0 0 0 59533 468 0 0 25 0 1 0 482164166 504811520 112084 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 123245 112084 603 41 0 123204 0
vsize: 492980
[startup+610.006 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 115726 0 0 0 60531 470 0 0 25 0 1 0 482164166 506281984 112372 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 123604 112372 603 41 0 123563 0
vsize: 494416
[startup+620.006 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 116050 0 0 0 61528 472 0 0 25 0 1 0 482164166 507793408 112696 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 123973 112696 603 41 0 123932 0
vsize: 495892
[startup+630.007 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 116491 0 0 0 62526 475 0 0 25 0 1 0 482164166 509874176 113137 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124481 113137 603 41 0 124440 0
vsize: 497924
[startup+640.007 s]
Raw data (loadavg): 1.01 1.00 0.92 3/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 116905 0 0 0 63524 476 0 0 25 0 1 0 482164166 511782912 113551 4294967295 134512640 134672761 3221224544 3221222788 1075346600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 124947 113551 603 41 0 124906 0
vsize: 499788
[startup+650.007 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 117500 0 0 0 64518 482 0 0 25 0 1 0 482164166 514420736 114146 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 125591 114146 603 41 0 125550 0
vsize: 502364
[startup+660.006 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 118191 0 0 0 65515 485 0 0 25 0 1 0 482164166 517349376 114837 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 126306 114837 603 41 0 126265 0
vsize: 505224
[startup+670.012 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 118924 0 0 0 66512 488 0 0 25 0 1 0 482164166 520908800 115570 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 127175 115570 603 41 0 127134 0
vsize: 508700
[startup+680.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 119399 0 0 0 67508 492 0 0 25 0 1 0 482164166 523014144 116045 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 127689 116045 603 41 0 127648 0
vsize: 510756
[startup+690.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 119859 0 0 0 68505 495 0 0 25 0 1 0 482164166 524972032 116505 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128167 116505 603 41 0 128126 0
vsize: 512668
[startup+700.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 120318 0 0 0 69502 498 0 0 25 0 1 0 482164166 526872576 116964 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 128631 116964 603 41 0 128590 0
vsize: 514524
[startup+710.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 120748 0 0 0 70499 501 0 0 25 0 1 0 482164166 528777216 117394 4294967295 134512640 134672761 3221224544 3221222720 134621235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 129096 117394 603 41 0 129055 0
vsize: 516384
[startup+720.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 121180 0 0 0 71496 504 0 0 25 0 1 0 482164166 530890752 117826 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 129612 117826 603 41 0 129571 0
vsize: 518448
[startup+730.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 121509 0 0 0 72494 506 0 0 25 0 1 0 482164166 532201472 118155 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 129932 118155 603 41 0 129891 0
vsize: 519728
[startup+740.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 121832 0 0 0 73492 508 0 0 25 0 1 0 482164166 533549056 118478 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 130261 118478 603 41 0 130220 0
vsize: 521044
[startup+750.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 121849 0 0 0 74490 510 0 0 25 0 1 0 482164166 533712896 118495 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 130301 118495 603 41 0 130260 0
vsize: 521204
[startup+760.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 121860 0 0 0 75488 512 0 0 25 0 1 0 482164166 533712896 118506 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 130301 118506 603 41 0 130260 0
vsize: 521204
[startup+770.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 122012 0 0 0 76488 513 0 0 25 0 1 0 482164166 534433792 118658 4294967295 134512640 134672761 3221224544 3221222896 134605852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 130477 118658 603 41 0 130436 0
vsize: 521908
[startup+780.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 122405 0 0 0 77486 515 0 0 25 0 1 0 482164166 536453120 119051 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 130970 119051 603 41 0 130929 0
vsize: 523880
[startup+790.021 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 122882 0 0 0 78483 517 0 0 25 0 1 0 482164166 538669056 119528 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 131511 119528 603 41 0 131470 0
vsize: 526044
[startup+800.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 123105 0 0 0 79482 519 0 0 25 0 1 0 482164166 539586560 119751 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 131735 119751 603 41 0 131694 0
vsize: 526940
[startup+810.026 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 123398 0 0 0 80481 521 0 0 25 0 1 0 482164166 541024256 120044 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 132086 120044 603 41 0 132045 0
vsize: 528344
[startup+820.038 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 123749 0 0 0 81480 522 0 0 25 0 1 0 482164166 542842880 120395 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 132530 120395 603 41 0 132489 0
vsize: 530120
[startup+830.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 124078 0 0 0 82478 524 0 0 25 0 1 0 482164166 544296960 120724 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 132885 120724 603 41 0 132844 0
vsize: 531540
[startup+840.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 124443 0 0 0 83477 526 0 0 25 0 1 0 482164166 545902592 121089 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133277 121089 603 41 0 133236 0
vsize: 533108
[startup+850.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 124780 0 0 0 84474 529 0 0 25 0 1 0 482164166 547205120 121426 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133595 121426 603 41 0 133554 0
vsize: 534380
[startup+860.041 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 124811 0 0 0 85470 533 0 0 25 0 1 0 482164166 547368960 121457 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133635 121457 603 41 0 133594 0
vsize: 534540
[startup+870.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 124813 0 0 0 86467 537 0 0 25 0 1 0 482164166 547368960 121459 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133635 121459 603 41 0 133594 0
vsize: 534540
[startup+880.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 124818 0 0 0 87464 539 0 0 25 0 1 0 482164166 547516416 121464 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133671 121464 603 41 0 133630 0
vsize: 534684
[startup+890.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 124866 0 0 0 88461 542 0 0 25 0 1 0 482164166 547680256 121512 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 133711 121512 603 41 0 133670 0
vsize: 534844
[startup+900.04 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 124905 0 0 0 89455 547 0 0 25 0 1 0 482164166 547844096 121551 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133751 121551 603 41 0 133710 0
vsize: 535004
[startup+910.039 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 124909 0 0 0 90453 549 0 0 25 0 1 0 482164166 547844096 121555 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133751 121555 603 41 0 133710 0
vsize: 535004
[startup+920.043 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 124911 0 0 0 91451 552 0 0 25 0 1 0 482164166 547844096 121557 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133751 121557 603 41 0 133710 0
vsize: 535004
[startup+930.046 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 124913 0 0 0 92448 554 0 0 25 0 1 0 482164166 547844096 121559 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133751 121559 603 41 0 133710 0
vsize: 535004
[startup+940.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 125354 0 0 0 93445 557 0 0 25 0 1 0 482164166 549765120 122000 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 134220 122000 603 41 0 134179 0
vsize: 536880
[startup+950.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 126042 0 0 0 94442 561 0 0 25 0 1 0 482164166 552873984 122688 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 134979 122688 603 41 0 134938 0
vsize: 539916
[startup+960.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 126594 0 0 0 95438 564 0 0 25 0 1 0 482164166 555528192 123240 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135627 123240 603 41 0 135586 0
vsize: 542508
[startup+970.045 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 126961 0 0 0 96436 566 0 0 25 0 1 0 482164166 557305856 123607 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 136061 123607 603 41 0 136020 0
vsize: 544244
[startup+980.049 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 127406 0 0 0 97434 569 0 0 25 0 1 0 482164166 559452160 124052 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 136585 124052 603 41 0 136544 0
vsize: 546340
[startup+990.048 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 127968 0 0 0 98431 572 0 0 25 0 1 0 482164166 562106368 124614 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 137233 124614 603 41 0 137192 0
vsize: 548932
[startup+1000.06 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 128659 0 0 0 99427 577 0 0 25 0 1 0 482164166 565243904 125305 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 137999 125305 603 41 0 137958 0
vsize: 551996
[startup+1010.06 s]
Raw data (loadavg): 1.08 1.02 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 129121 0 0 0 100423 581 0 0 25 0 1 0 482164166 567365632 125767 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 138517 125767 603 41 0 138476 0
vsize: 554068
[startup+1020.06 s]
Raw data (loadavg): 1.07 1.02 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 129697 0 0 0 101420 584 0 0 25 0 1 0 482164166 570155008 126343 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 139198 126343 603 41 0 139157 0
vsize: 556792
[startup+1030.06 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 130389 0 0 0 102417 587 0 0 25 0 1 0 482164166 573169664 127035 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 139934 127035 603 41 0 139893 0
vsize: 559736
[startup+1040.06 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 131096 0 0 0 103414 590 0 0 25 0 1 0 482164166 576561152 127742 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 140762 127742 603 41 0 140721 0
vsize: 563048
[startup+1050.06 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 131734 0 0 0 104410 594 0 0 25 0 1 0 482164166 579575808 128380 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 141498 128380 603 41 0 141457 0
vsize: 565992
[startup+1060.06 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 132166 0 0 0 105408 597 0 0 25 0 1 0 482164166 581361664 128812 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 141934 128812 603 41 0 141893 0
vsize: 567736
[startup+1070.06 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 132470 0 0 0 106406 599 0 0 25 0 1 0 482164166 582782976 129116 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 142281 129116 603 41 0 142240 0
vsize: 569124
[startup+1080.06 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 132865 0 0 0 107404 601 0 0 25 0 1 0 482164166 584630272 129511 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 142732 129511 603 41 0 142691 0
vsize: 570928
[startup+1090.06 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 133357 0 0 0 108401 604 0 0 25 0 1 0 482164166 587194368 130003 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 143358 130003 603 41 0 143317 0
vsize: 573432
[startup+1100.07 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 133872 0 0 0 109400 606 0 0 25 0 1 0 482164166 589496320 130518 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 143920 130518 603 41 0 143879 0
vsize: 575680
[startup+1110.07 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 134328 0 0 0 110398 609 0 0 25 0 1 0 482164166 591589376 130974 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 144431 130974 603 41 0 144390 0
vsize: 577724
[startup+1120.07 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 134819 0 0 0 111395 611 0 0 25 0 1 0 482164166 593895424 131465 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 144994 131465 603 41 0 144953 0
vsize: 579976
[startup+1130.07 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 135244 0 0 0 112393 613 0 0 25 0 1 0 482164166 595922944 131890 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 145489 131890 603 41 0 145448 0
vsize: 581956
[startup+1140.07 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 135543 0 0 0 113390 616 0 0 25 0 1 0 482164166 597295104 132189 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 145824 132189 603 41 0 145783 0
vsize: 583296
[startup+1150.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 135826 0 0 0 114388 619 0 0 25 0 1 0 482164166 598736896 132472 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 146176 132472 603 41 0 146135 0
vsize: 584704
[startup+1160.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 136308 0 0 0 115384 623 0 0 25 0 1 0 482164166 600875008 132954 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 146698 132954 603 41 0 146657 0
vsize: 586792
[startup+1170.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 136937 0 0 0 116381 626 0 0 25 0 1 0 482164166 603803648 133583 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 147413 133583 603 41 0 147372 0
vsize: 589652
[startup+1180.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 137519 0 0 0 117378 629 0 0 25 0 1 0 482164166 606605312 134165 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 148097 134165 603 41 0 148056 0
vsize: 592388
[startup+1190.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 138117 0 0 0 118375 631 0 0 25 0 1 0 482164166 609456128 134763 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 148793 134763 603 41 0 148752 0
vsize: 595172
[startup+1200.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 26710
Raw data (stat): 26710 (minisat+) R 26709 22932 22931 0 -1 0 138659 0 0 0 119373 634 0 0 25 0 1 0 482164166 611598336 135305 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 149316 135305 603 41 0 149275 0
vsize: 597264
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.45 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 26710
Raw data (stat): 26710 (minisat+) Z 26709 22932 22931 0 -1 12 138659 0 0 0 119373 672 0 0 25 0 1 0 482164166 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.45
CPU time (s): 1200.46
CPU user time (s): 1193.73
CPU system time (s): 6.72398
CPU usage (%): 100.001
Max. virtual memory (Kb): 597264
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####