PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-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.9513
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 13289

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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:        541368 kB
Buffers:         34360 kB
Cached:         423708 kB
SwapCached:        456 kB
Active:         166792 kB
Inactive:       293860 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        541116 kB
SwapTotal:     2097892 kB
SwapFree:      2096984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6228 kB
Slab:            26948 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 20:43:59 (client local time) WITH STATUS 0 IN 1200.61 SECONDS
stats: 15234 7 1200.61 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.85 0.60 0.26 2/55 9479
Raw data (stat): 9479 (runsolver) R 9478 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539284653 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.0008 s]
Raw data (loadavg): 0.87 0.62 0.27 2/55 9479
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 30269 0 0 0 924 74 0 0 25 0 1 0 539284653 135565312 28835 4294967295 134512640 134672761 3221224544 3220793712 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33097 28835 603 41 0 33056 0
vsize: 132388
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.63 0.28 2/55 9479
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 62322 0 0 0 1841 157 0 0 25 0 1 0 539284653 279670784 60888 4294967295 134512640 134672761 3221224544 3221223088 134621238 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.0021 s]
Raw data (loadavg): 0.91 0.64 0.28 2/55 9479
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 62322 0 0 0 2841 157 0 0 25 0 1 0 539284653 279670784 60888 4294967295 134512640 134672761 3221224544 3221223088 134621071 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.0028 s]
Raw data (loadavg): 0.92 0.65 0.29 2/55 9479
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 67542 0 0 0 3822 177 0 0 25 0 1 0 539284653 293539840 64188 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71665 64188 603 41 0 71624 0
vsize: 286660
[startup+50.0037 s]
Raw data (loadavg): 0.93 0.66 0.30 2/55 9479
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 69748 0 0 0 4809 188 0 0 25 0 1 0 539284653 302829568 66394 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 73933 66394 603 41 0 73892 0
vsize: 295732
[startup+60.0035 s]
Raw data (loadavg): 0.94 0.67 0.30 2/55 9479
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 71038 0 0 0 5801 196 0 0 25 0 1 0 539284653 308441088 67684 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 75303 67684 603 41 0 75262 0
vsize: 301212
[startup+70.017 s]
Raw data (loadavg): 0.95 0.68 0.31 2/55 9479
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 72148 0 0 0 6797 202 0 0 25 0 1 0 539284653 313208832 68794 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76467 68794 603 41 0 76426 0
vsize: 305868
[startup+80.0304 s]
Raw data (loadavg): 0.96 0.69 0.32 2/55 9479
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 73448 0 0 0 7793 207 0 0 25 0 1 0 539284653 318951424 70094 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 77869 70094 603 41 0 77828 0
vsize: 311476
[startup+90.0366 s]
Raw data (loadavg): 0.96 0.70 0.32 2/55 9479
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 75304 0 0 0 8780 220 0 0 25 0 1 0 539284653 326942720 71950 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79820 71950 603 41 0 79779 0
vsize: 319280
[startup+100.037 s]
Raw data (loadavg): 0.97 0.71 0.33 2/55 9479
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 77607 0 0 0 9767 232 0 0 25 0 1 0 539284653 336678912 74253 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 82197 74253 603 41 0 82156 0
vsize: 328788
[startup+110.051 s]
Raw data (loadavg): 0.97 0.72 0.34 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 78854 0 0 0 10760 239 0 0 25 0 1 0 539284653 341610496 75500 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 83401 75500 603 41 0 83360 0
vsize: 333604
[startup+120.051 s]
Raw data (loadavg): 0.98 0.73 0.34 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 80214 0 0 0 11753 247 0 0 25 0 1 0 539284653 347582464 76860 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 84859 76860 603 41 0 84818 0
vsize: 339436
[startup+130.067 s]
Raw data (loadavg): 0.98 0.74 0.35 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 81686 0 0 0 12747 253 0 0 25 0 1 0 539284653 354062336 78332 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 86441 78332 603 41 0 86400 0
vsize: 345764
[startup+140.067 s]
Raw data (loadavg): 0.98 0.75 0.36 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 82558 0 0 0 13741 259 0 0 25 0 1 0 539284653 358125568 79204 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 87433 79204 603 41 0 87392 0
vsize: 349732
[startup+150.071 s]
Raw data (loadavg): 0.98 0.75 0.36 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 82997 0 0 0 14738 263 0 0 25 0 1 0 539284653 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.071 s]
Raw data (loadavg): 0.99 0.76 0.37 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 83732 0 0 0 15735 266 0 0 25 0 1 0 539284653 363515904 80378 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 88749 80378 603 41 0 88708 0
vsize: 354996
[startup+170.07 s]
Raw data (loadavg): 0.99 0.77 0.38 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 84309 0 0 0 16730 271 0 0 25 0 1 0 539284653 365957120 80955 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 89345 80955 603 41 0 89304 0
vsize: 357380
[startup+180.071 s]
Raw data (loadavg): 0.99 0.78 0.38 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 85060 0 0 0 17725 276 0 0 25 0 1 0 539284653 369496064 81706 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90209 81706 603 41 0 90168 0
vsize: 360836
[startup+190.075 s]
Raw data (loadavg): 0.99 0.78 0.39 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 86081 0 0 0 18719 282 0 0 25 0 1 0 539284653 374104064 82727 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91334 82727 603 41 0 91293 0
vsize: 365336
[startup+200.075 s]
Raw data (loadavg): 0.99 0.79 0.39 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 86838 0 0 0 19712 286 0 0 25 0 1 0 539284653 377536512 83484 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 92172 83484 603 41 0 92131 0
vsize: 368688
[startup+210.075 s]
Raw data (loadavg): 0.99 0.80 0.40 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 88859 0 0 0 20701 297 0 0 25 0 1 0 539284653 386080768 85505 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 94258 85505 603 41 0 94217 0
vsize: 377032
[startup+220.075 s]
Raw data (loadavg): 0.99 0.80 0.41 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 90117 0 0 0 21694 303 0 0 25 0 1 0 539284653 391499776 86763 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 95581 86763 603 41 0 95540 0
vsize: 382324
[startup+230.076 s]
Raw data (loadavg): 0.99 0.81 0.41 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 91456 0 0 0 22686 312 0 0 25 0 1 0 539284653 397557760 88102 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 97060 88102 603 41 0 97019 0
vsize: 388240
[startup+240.076 s]
Raw data (loadavg): 0.99 0.81 0.42 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 92925 0 0 0 23680 318 0 0 25 0 1 0 539284653 403947520 89571 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 98620 89571 603 41 0 98579 0
vsize: 394480
[startup+250.077 s]
Raw data (loadavg): 0.99 0.82 0.42 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 93822 0 0 0 24674 324 0 0 25 0 1 0 539284653 407949312 90468 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 99597 90468 603 41 0 99556 0
vsize: 398388
[startup+260.078 s]
Raw data (loadavg): 0.99 0.83 0.43 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 94665 0 0 0 25669 328 0 0 25 0 1 0 539284653 411488256 91311 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 100461 91311 603 41 0 100420 0
vsize: 401844
[startup+270.078 s]
Raw data (loadavg): 0.99 0.83 0.43 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 96144 0 0 0 26659 339 0 0 25 0 1 0 539284653 417644544 92790 4294967295 134512640 134672761 3221224544 3221222752 1075730206 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 101964 92790 603 41 0 101923 0
vsize: 407856
[startup+280.079 s]
Raw data (loadavg): 0.99 0.84 0.44 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 97094 0 0 0 27652 345 0 0 25 0 1 0 539284653 421629952 93740 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 102937 93740 603 41 0 102896 0
vsize: 411748
[startup+290.079 s]
Raw data (loadavg): 0.99 0.84 0.45 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 98172 0 0 0 28644 353 0 0 25 0 1 0 539284653 426557440 94818 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 104140 94818 603 41 0 104099 0
vsize: 416560
[startup+300.085 s]
Raw data (loadavg): 0.99 0.85 0.45 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 99247 0 0 0 29639 358 0 0 25 0 1 0 539284653 431087616 95893 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 105246 95893 603 41 0 105205 0
vsize: 420984
[startup+310.085 s]
Raw data (loadavg): 0.99 0.85 0.46 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 100287 0 0 0 30634 363 0 0 25 0 1 0 539284653 435830784 96933 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 106404 96933 603 41 0 106363 0
vsize: 425616
[startup+320.086 s]
Raw data (loadavg): 0.99 0.85 0.46 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 100845 0 0 0 31630 367 0 0 25 0 1 0 539284653 438415360 97491 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 107035 97491 603 41 0 106994 0
vsize: 428140
[startup+330.087 s]
Raw data (loadavg): 0.99 0.86 0.47 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 101401 0 0 0 32627 370 0 0 25 0 1 0 539284653 440864768 98047 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 107633 98047 603 41 0 107592 0
vsize: 430532
[startup+340.087 s]
Raw data (loadavg): 1.07 0.88 0.48 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 102150 0 0 0 33622 374 0 0 25 0 1 0 539284653 444260352 98796 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 108462 98796 603 41 0 108421 0
vsize: 433848
[startup+350.088 s]
Raw data (loadavg): 1.06 0.88 0.48 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 102804 0 0 0 34617 379 0 0 25 0 1 0 539284653 447250432 99450 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109192 99450 603 41 0 109151 0
vsize: 436768
[startup+360.089 s]
Raw data (loadavg): 1.05 0.89 0.49 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 103575 0 0 0 35612 384 0 0 25 0 1 0 539284653 450527232 100221 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 109992 100221 603 41 0 109951 0
vsize: 439968
[startup+370.089 s]
Raw data (loadavg): 1.04 0.89 0.49 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 104873 0 0 0 36603 393 0 0 25 0 1 0 539284653 455876608 101519 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 111298 101519 603 41 0 111257 0
vsize: 445192
[startup+380.089 s]
Raw data (loadavg): 1.03 0.89 0.50 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 105659 0 0 0 37599 397 0 0 25 0 1 0 539284653 459837440 102305 4294967295 134512640 134672761 3221224544 3221222992 134643612 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112265 102305 603 41 0 112224 0
vsize: 449060
[startup+390.09 s]
Raw data (loadavg): 1.03 0.89 0.50 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 106165 0 0 0 38596 400 0 0 25 0 1 0 539284653 462233600 102811 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 112850 102811 603 41 0 112809 0
vsize: 451400
[startup+400.094 s]
Raw data (loadavg): 1.02 0.90 0.51 2/55 9481
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 106860 0 0 0 39592 404 0 0 25 0 1 0 539284653 465412096 103506 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 113626 103506 603 41 0 113585 0
vsize: 454504
[startup+410.094 s]
Raw data (loadavg): 1.02 0.90 0.51 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 107307 0 0 0 40589 407 0 0 25 0 1 0 539284653 467472384 103953 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114129 103953 603 41 0 114088 0
vsize: 456516
[startup+420.094 s]
Raw data (loadavg): 1.02 0.90 0.52 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 107401 0 0 0 41584 412 0 0 25 0 1 0 539284653 467947520 104047 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114245 104047 603 41 0 114204 0
vsize: 456980
[startup+430.095 s]
Raw data (loadavg): 1.01 0.91 0.52 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 107408 0 0 0 42582 414 0 0 25 0 1 0 539284653 467947520 104054 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114245 104054 603 41 0 114204 0
vsize: 456980
[startup+440.095 s]
Raw data (loadavg): 1.01 0.91 0.53 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 107408 0 0 0 43579 416 0 0 25 0 1 0 539284653 467947520 104054 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114245 104054 603 41 0 114204 0
vsize: 456980
[startup+450.096 s]
Raw data (loadavg): 1.01 0.91 0.53 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 107408 0 0 0 44577 419 0 0 25 0 1 0 539284653 467947520 104054 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114245 104054 603 41 0 114204 0
vsize: 456980
[startup+460.096 s]
Raw data (loadavg): 1.01 0.91 0.54 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 107409 0 0 0 45575 421 0 0 25 0 1 0 539284653 467947520 104055 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114245 104055 603 41 0 114204 0
vsize: 456980
[startup+470.096 s]
Raw data (loadavg): 1.00 0.92 0.54 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 107669 0 0 0 46572 423 0 0 25 0 1 0 539284653 468930560 104315 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 114485 104315 603 41 0 114444 0
vsize: 457940
[startup+480.096 s]
Raw data (loadavg): 1.00 0.92 0.55 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 108345 0 0 0 47569 427 0 0 25 0 1 0 539284653 472354816 104991 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 115321 104991 603 41 0 115280 0
vsize: 461284
[startup+490.096 s]
Raw data (loadavg): 1.00 0.92 0.55 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 108991 0 0 0 48565 431 0 0 25 0 1 0 539284653 475455488 105637 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 116078 105637 603 41 0 116037 0
vsize: 464312
[startup+500.097 s]
Raw data (loadavg): 1.00 0.92 0.55 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 109575 0 0 0 49560 434 0 0 25 0 1 0 539284653 477978624 106221 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 116694 106221 603 41 0 116653 0
vsize: 466776
[startup+510.098 s]
Raw data (loadavg): 1.00 0.92 0.56 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 111077 0 0 0 50552 442 0 0 25 0 1 0 539284653 484679680 107723 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 118330 107723 603 41 0 118289 0
vsize: 473320
[startup+520.098 s]
Raw data (loadavg): 1.00 0.93 0.56 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 112068 0 0 0 51546 448 0 0 25 0 1 0 539284653 488927232 108714 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 119367 108714 603 41 0 119326 0
vsize: 477468
[startup+530.099 s]
Raw data (loadavg): 1.00 0.93 0.57 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 112637 0 0 0 52543 451 0 0 25 0 1 0 539284653 491880448 109283 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120088 109283 603 41 0 120047 0
vsize: 480352
[startup+540.099 s]
Raw data (loadavg): 1.00 0.93 0.57 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 112890 0 0 0 53540 454 0 0 25 0 1 0 539284653 493023232 109536 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120367 109536 603 41 0 120326 0
vsize: 481468
[startup+550.099 s]
Raw data (loadavg): 1.00 0.93 0.57 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 112951 0 0 0 54537 457 0 0 25 0 1 0 539284653 493174784 109597 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 120404 109597 603 41 0 120363 0
vsize: 481616
[startup+560.1 s]
Raw data (loadavg): 1.00 0.93 0.58 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 113443 0 0 0 55534 460 0 0 25 0 1 0 539284653 495693824 110089 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121019 110089 603 41 0 120978 0
vsize: 484076
[startup+570.1 s]
Raw data (loadavg): 1.00 0.94 0.58 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 113937 0 0 0 56532 462 0 0 25 0 1 0 539284653 497946624 110583 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 121569 110583 603 41 0 121528 0
vsize: 486276
[startup+580.102 s]
Raw data (loadavg): 1.00 0.94 0.58 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 114302 0 0 0 57530 465 0 0 25 0 1 0 539284653 499732480 110948 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122005 110948 603 41 0 121964 0
vsize: 488020
[startup+590.102 s]
Raw data (loadavg): 1.00 0.94 0.59 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 114817 0 0 0 58527 468 0 0 25 0 1 0 539284653 501956608 111463 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 122548 111463 603 41 0 122507 0
vsize: 490192
[startup+600.104 s]
Raw data (loadavg): 1.00 0.94 0.59 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 115333 0 0 0 59525 470 0 0 25 0 1 0 539284653 504320000 111979 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123125 111979 603 41 0 123084 0
vsize: 492500
[startup+610.104 s]
Raw data (loadavg): 1.00 0.94 0.60 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 115597 0 0 0 60523 472 0 0 25 0 1 0 539284653 505630720 112243 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123445 112243 603 41 0 123404 0
vsize: 493780
[startup+620.105 s]
Raw data (loadavg): 1.00 0.94 0.60 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 115942 0 0 0 61521 475 0 0 25 0 1 0 539284653 507330560 112588 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 123860 112588 603 41 0 123819 0
vsize: 495440
[startup+630.105 s]
Raw data (loadavg): 1.00 0.94 0.60 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 116344 0 0 0 62519 476 0 0 25 0 1 0 539284653 509190144 112990 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124314 112990 603 41 0 124273 0
vsize: 497256
[startup+640.105 s]
Raw data (loadavg): 1.00 0.95 0.61 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 116764 0 0 0 63518 478 0 0 25 0 1 0 539284653 511029248 113410 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 124763 113410 603 41 0 124722 0
vsize: 499052
[startup+650.105 s]
Raw data (loadavg): 1.00 0.95 0.61 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 117285 0 0 0 64515 481 0 0 25 0 1 0 539284653 513548288 113931 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 125378 113931 603 41 0 125337 0
vsize: 501512
[startup+660.105 s]
Raw data (loadavg): 1.00 0.95 0.62 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 117908 0 0 0 65511 485 0 0 25 0 1 0 539284653 516161536 114554 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 126016 114554 603 41 0 125975 0
vsize: 504064
[startup+670.112 s]
Raw data (loadavg): 1.00 0.95 0.62 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 118646 0 0 0 66509 488 0 0 25 0 1 0 539284653 519614464 115292 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 126859 115292 603 41 0 126818 0
vsize: 507436
[startup+680.113 s]
Raw data (loadavg): 1.00 0.95 0.62 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 119165 0 0 0 67505 492 0 0 25 0 1 0 539284653 521961472 115811 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 127432 115811 603 41 0 127391 0
vsize: 509728
[startup+690.115 s]
Raw data (loadavg): 1.00 0.95 0.63 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 119729 0 0 0 68503 495 0 0 25 0 1 0 539284653 524316672 116375 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 128007 116375 603 41 0 127966 0
vsize: 512028
[startup+700.12 s]
Raw data (loadavg): 1.00 0.95 0.63 2/55 9483
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 120128 0 0 0 69501 497 0 0 25 0 1 0 539284653 525963264 116774 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 128409 116774 603 41 0 128368 0
vsize: 513636
[startup+710.13 s]
Raw data (loadavg): 1.00 0.95 0.64 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 120567 0 0 0 70500 499 0 0 25 0 1 0 539284653 527978496 117213 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 128901 117213 603 41 0 128860 0
vsize: 515604
[startup+720.13 s]
Raw data (loadavg): 1.00 0.95 0.64 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 121002 0 0 0 71498 501 0 0 25 0 1 0 539284653 529952768 117648 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 129383 117648 603 41 0 129342 0
vsize: 517532
[startup+730.131 s]
Raw data (loadavg): 1.00 0.95 0.64 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 121369 0 0 0 72497 503 0 0 25 0 1 0 539284653 531709952 118015 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 129812 118015 603 41 0 129771 0
vsize: 519248
[startup+740.132 s]
Raw data (loadavg): 1.00 0.96 0.64 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 121672 0 0 0 73493 505 0 0 25 0 1 0 539284653 532873216 118318 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 130096 118318 603 41 0 130055 0
vsize: 520384
[startup+750.132 s]
Raw data (loadavg): 1.00 0.96 0.65 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 121849 0 0 0 74491 508 0 0 25 0 1 0 539284653 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.133 s]
Raw data (loadavg): 1.00 0.96 0.65 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 121851 0 0 0 75489 509 0 0 25 0 1 0 539284653 533712896 118497 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 130301 118497 603 41 0 130260 0
vsize: 521204
[startup+770.132 s]
Raw data (loadavg): 1.00 0.96 0.65 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 121925 0 0 0 76488 511 0 0 25 0 1 0 539284653 534106112 118571 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 130397 118571 603 41 0 130356 0
vsize: 521588
[startup+780.133 s]
Raw data (loadavg): 1.00 0.96 0.66 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 122228 0 0 0 77485 514 0 0 25 0 1 0 539284653 535588864 118874 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 130759 118874 603 41 0 130718 0
vsize: 523036
[startup+790.133 s]
Raw data (loadavg): 1.00 0.96 0.66 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 122686 0 0 0 78483 516 0 0 25 0 1 0 539284653 537755648 119332 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 131288 119332 603 41 0 131247 0
vsize: 525152
[startup+800.134 s]
Raw data (loadavg): 1.00 0.96 0.66 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 123013 0 0 0 79481 518 0 0 25 0 1 0 539284653 539226112 119659 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 131647 119659 603 41 0 131606 0
vsize: 526588
[startup+810.135 s]
Raw data (loadavg): 1.00 0.96 0.67 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 123239 0 0 0 80480 519 0 0 25 0 1 0 539284653 540176384 119885 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 131879 119885 603 41 0 131838 0
vsize: 527516
[startup+820.135 s]
Raw data (loadavg): 1.00 0.96 0.67 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 123596 0 0 0 81478 522 0 0 25 0 1 0 539284653 542015488 120242 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 132328 120242 603 41 0 132287 0
vsize: 529312
[startup+830.135 s]
Raw data (loadavg): 1.00 0.96 0.67 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 123958 0 0 0 82476 523 0 0 25 0 1 0 539284653 543805440 120604 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 132765 120604 603 41 0 132724 0
vsize: 531060
[startup+840.136 s]
Raw data (loadavg): 1.00 0.97 0.67 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 124288 0 0 0 83475 525 0 0 25 0 1 0 539284653 545243136 120934 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133116 120934 603 41 0 133075 0
vsize: 532464
[startup+850.137 s]
Raw data (loadavg): 1.00 0.97 0.68 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 124620 0 0 0 84473 526 0 0 25 0 1 0 539284653 546721792 121266 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133477 121266 603 41 0 133436 0
vsize: 533908
[startup+860.138 s]
Raw data (loadavg): 1.08 0.98 0.69 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 124811 0 0 0 85469 530 0 0 25 0 1 0 539284653 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.143 s]
Raw data (loadavg): 1.14 1.00 0.69 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 124812 0 0 0 86466 534 0 0 25 0 1 0 539284653 547368960 121458 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133635 121458 603 41 0 133594 0
vsize: 534540
[startup+880.246 s]
Raw data (loadavg): 1.12 1.00 0.70 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 124813 0 0 0 87473 536 0 0 25 0 1 0 539284653 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+890.246 s]
Raw data (loadavg): 1.10 1.00 0.70 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 124824 0 0 0 88471 539 0 0 25 0 1 0 539284653 547516416 121470 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133671 121470 603 41 0 133630 0
vsize: 534684
[startup+900.247 s]
Raw data (loadavg): 1.08 1.00 0.70 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 124905 0 0 0 89466 544 0 0 25 0 1 0 539284653 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.351 s]
Raw data (loadavg): 1.07 1.00 0.71 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 124908 0 0 0 90473 546 0 0 25 0 1 0 539284653 547844096 121554 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133751 121554 603 41 0 133710 0
vsize: 535004
[startup+920.351 s]
Raw data (loadavg): 1.06 1.00 0.71 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 124910 0 0 0 91470 548 0 0 25 0 1 0 539284653 547844096 121556 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133751 121556 603 41 0 133710 0
vsize: 535004
[startup+930.351 s]
Raw data (loadavg): 1.05 1.00 0.71 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 124912 0 0 0 92467 551 0 0 25 0 1 0 539284653 547844096 121558 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 133751 121558 603 41 0 133710 0
vsize: 535004
[startup+940.352 s]
Raw data (loadavg): 1.04 1.00 0.71 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 125180 0 0 0 93465 553 0 0 25 0 1 0 539284653 549011456 121826 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 134036 121826 603 41 0 133995 0
vsize: 536144
[startup+950.352 s]
Raw data (loadavg): 1.04 1.00 0.72 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 125820 0 0 0 94461 557 0 0 25 0 1 0 539284653 551858176 122466 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 134731 122466 603 41 0 134690 0
vsize: 538924
[startup+960.354 s]
Raw data (loadavg): 1.03 1.00 0.72 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 126402 0 0 0 95457 561 0 0 25 0 1 0 539284653 554651648 123048 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135413 123048 603 41 0 135372 0
vsize: 541652
[startup+970.353 s]
Raw data (loadavg): 1.02 1.00 0.72 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 126810 0 0 0 96454 563 0 0 25 0 1 0 539284653 556683264 123456 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 135909 123456 603 41 0 135868 0
vsize: 543636
[startup+980.355 s]
Raw data (loadavg): 1.02 1.00 0.73 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 127247 0 0 0 97452 565 0 0 25 0 1 0 539284653 558706688 123893 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 136403 123893 603 41 0 136362 0
vsize: 545612
[startup+990.357 s]
Raw data (loadavg): 1.02 1.00 0.73 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 127713 0 0 0 98449 568 0 0 25 0 1 0 539284653 560779264 124359 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 136909 124359 603 41 0 136868 0
vsize: 547636
[startup+1000.36 s]
Raw data (loadavg): 1.01 1.00 0.73 2/55 9485
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 128418 0 0 0 99445 572 0 0 25 0 1 0 539284653 564072448 125064 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 137713 125064 603 41 0 137672 0
vsize: 550852
[startup+1010.36 s]
Raw data (loadavg): 1.01 1.00 0.73 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 129015 0 0 0 100442 576 0 0 25 0 1 0 539284653 566874112 125661 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 138397 125661 603 41 0 138356 0
vsize: 553588
[startup+1020.4 s]
Raw data (loadavg): 1.01 1.00 0.73 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 129443 0 0 0 101443 579 0 0 25 0 1 0 539284653 568946688 126089 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 138903 126089 603 41 0 138862 0
vsize: 555612
[startup+1030.4 s]
Raw data (loadavg): 1.01 1.00 0.74 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 130154 0 0 0 102440 582 0 0 25 0 1 0 539284653 572194816 126800 4294967295 134512640 134672761 3221224544 3221222992 134643954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 139696 126800 603 41 0 139655 0
vsize: 558784
[startup+1040.4 s]
Raw data (loadavg): 1.01 1.00 0.74 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 130871 0 0 0 103435 585 0 0 25 0 1 0 539284653 575418368 127517 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 140483 127517 603 41 0 140442 0
vsize: 561932
[startup+1050.4 s]
Raw data (loadavg): 1.00 1.00 0.74 3/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 131510 0 0 0 104433 588 0 0 25 0 1 0 539284653 578596864 128156 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141259 128156 603 41 0 141218 0
vsize: 565036
[startup+1060.4 s]
Raw data (loadavg): 1.00 1.00 0.74 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 132060 0 0 0 105429 591 0 0 25 0 1 0 539284653 581050368 128706 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 141858 128706 603 41 0 141817 0
vsize: 567432
[startup+1070.4 s]
Raw data (loadavg): 1.00 1.00 0.74 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 132370 0 0 0 106425 593 0 0 25 0 1 0 539284653 582291456 129016 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 142161 129016 603 41 0 142120 0
vsize: 568644
[startup+1080.41 s]
Raw data (loadavg): 1.00 1.00 0.75 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 132680 0 0 0 107424 595 0 0 25 0 1 0 539284653 583766016 129326 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 142521 129326 603 41 0 142480 0
vsize: 570084
[startup+1090.41 s]
Raw data (loadavg): 1.00 1.00 0.75 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 133198 0 0 0 108422 598 0 0 25 0 1 0 539284653 586366976 129844 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 143156 129844 603 41 0 143115 0
vsize: 572624
[startup+1100.41 s]
Raw data (loadavg): 1.15 1.03 0.76 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 133710 0 0 0 109419 601 0 0 25 0 1 0 539284653 588771328 130356 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 143743 130356 603 41 0 143702 0
vsize: 574972
[startup+1110.41 s]
Raw data (loadavg): 1.13 1.03 0.76 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 134176 0 0 0 110417 603 0 0 25 0 1 0 539284653 591028224 130822 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 144294 130822 603 41 0 144253 0
vsize: 577176
[startup+1120.41 s]
Raw data (loadavg): 1.11 1.03 0.76 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 134656 0 0 0 111415 605 0 0 25 0 1 0 539284653 593059840 131302 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 144790 131302 603 41 0 144749 0
vsize: 579160
[startup+1130.41 s]
Raw data (loadavg): 1.09 1.03 0.77 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 135133 0 0 0 112412 608 0 0 25 0 1 0 539284653 595431424 131779 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 145369 131779 603 41 0 145328 0
vsize: 581476
[startup+1140.41 s]
Raw data (loadavg): 1.08 1.03 0.77 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 135473 0 0 0 113410 610 0 0 25 0 1 0 539284653 597131264 132119 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 145784 132119 603 41 0 145743 0
vsize: 583136
[startup+1150.41 s]
Raw data (loadavg): 1.06 1.03 0.77 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 135755 0 0 0 114408 613 0 0 25 0 1 0 539284653 598376448 132401 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 146088 132401 603 41 0 146047 0
vsize: 584352
[startup+1160.43 s]
Raw data (loadavg): 1.05 1.02 0.77 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 136082 0 0 0 115407 616 0 0 25 0 1 0 539284653 599773184 132728 4294967295 134512640 134672761 3221224544 3221222960 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 146429 132728 603 41 0 146388 0
vsize: 585716
[startup+1170.43 s]
Raw data (loadavg): 1.05 1.02 0.77 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 136734 0 0 0 116404 619 0 0 25 0 1 0 539284653 602902528 133380 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 147193 133380 603 41 0 147152 0
vsize: 588772
[startup+1180.43 s]
Raw data (loadavg): 1.04 1.02 0.78 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 137323 0 0 0 117399 622 0 0 25 0 1 0 539284653 605659136 133969 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 147866 133969 603 41 0 147825 0
vsize: 591464
[startup+1190.43 s]
Raw data (loadavg): 1.03 1.02 0.78 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 137919 0 0 0 118396 626 0 0 25 0 1 0 539284653 608444416 134565 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 148546 134565 603 41 0 148505 0
vsize: 594184
[startup+1200.44 s]
Raw data (loadavg): 1.03 1.02 0.78 2/55 9487
Raw data (stat): 9479 (minisat+) R 9478 20024 20023 0 -1 0 138582 0 0 0 119394 629 0 0 25 0 1 0 539284653 611295232 135228 4294967295 134512640 134672761 3221224544 3221222960 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 149242 135228 603 41 0 149201 0
vsize: 596968
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.82 s]
Raw data (loadavg): 1.03 1.02 0.78 1/55 9487
Raw data (stat): 9479 (minisat+) Z 9478 20024 20023 0 -1 12 138582 0 0 0 119394 666 0 0 25 0 1 0 539284653 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.82
CPU time (s): 1200.61
CPU user time (s): 1193.95
CPU system time (s): 6.66699
CPU usage (%): 99.9827
Max. virtual memory (Kb): 596968
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####