PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-cap6000.opb
MD5SUM	f72618c4c62a4e83b66d53971e0bdc53
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-260522
Optimality of the best value was proved	NO
Number of terms in the objective function	5995
Biggest coefficient in the objective function	91110
Number of bits for the biggest coefficient in the objective function	17
Sum of the numbers in the objective function	12969603
Number of bits of the sum of numbers in the objective function	24
Biggest number in a constraint	800000
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	28761906
Number of bits of the biggest sum of numbers	25
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.17
Number of variables	6000
Total number of constraints	8176
Number of constraints which are clauses	222
Number of constraints which are cardinality constraints (but not clauses)	7919
Number of constraints which are nor clauses,nor cardinality constraints	35
Minimum length of a constraint	1
Maximum length of a constraint	6000
Trace number 15476

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        688132 kB
Buffers:         17444 kB
Cached:         301124 kB
SwapCached:        556 kB
Active:          81300 kB
Inactive:       239404 kB
HighTotal:      131008 kB
HighFree:          280 kB
LowTotal:       903652 kB
LowFree:        687852 kB
SwapTotal:     2097892 kB
SwapFree:      2096436 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5200 kB
Slab:            20276 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 04:56:27 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 17477 7 1200.36 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2294 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###########################################################################################################################
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................
c ---[2293]---> Adder-cost: 61016   maxlim: 27161905   bits: 25/25
c ---[2292]---> BDD-cost:    3
c ---[2291]---> BDD-cost:    3
c ---[2290]---> BDD-cost:    3
c ---[2289]---> BDD-cost:    3
c ---[2288]---> BDD-cost:    3
c ---[2287]---> BDD-cost:    3
c ---[2286]---> BDD-cost:    3
c ---[2285]---> BDD-cost:    3
c ---[2284]---> BDD-cost:    3
c ---[2283]---> BDD-cost:    3
c ---[2282]---> BDD-cost:    3
c ---[2281]---> BDD-cost:    3
c ---[2280]---> BDD-cost:    3
c ---[2279]---> BDD-cost:    3
c ---[2278]---> BDD-cost:    3
c ---[2277]---> BDD-cost:    3
c ---[2276]---> BDD-cost:    3
c ---[2275]---> BDD-cost:    3
c ---[2274]---> BDD-cost:    3
c ---[2273]---> BDD-cost:    3
c ---[2272]---> BDD-cost:    3
c ---[2271]---> BDD-cost:    3
c ---[2270]---> BDD-cost:    3
c ---[2269]---> BDD-cost:    3
c ---[2268]---> BDD-cost:    3
c ---[2267]---> BDD-cost:    3
c ---[2266]---> BDD-cost:    3
c ---[2265]---> BDD-cost:    3
c ---[2264]---> BDD-cost:    3
c ---[2263]---> BDD-cost:    3
c ---[2262]---> BDD-cost:    3
c ---[2261]---> BDD-cost:    3
c ---[2260]---> BDD-cost:    3
c ---[2259]---> BDD-cost:    3
c ---[2258]---> BDD-cost:    3
c ---[2257]---> BDD-cost:    3
c ---[2256]---> BDD-cost:    3
c ---[2255]---> BDD-cost:    3
c ---[2254]---> BDD-cost:    3
c ---[2253]---> BDD-cost:    3
c ---[2252]---> BDD-cost:    3
c ---[2251]---> BDD-cost:    3
c ---[2250]---> BDD-cost:    3
c ---[2249]---> BDD-cost:    3
c ---[2248]---> BDD-cost:    3
c ---[2247]---> BDD-cost:    3
c ---[2246]---> BDD-cost:    3
c ---[2245]---> BDD-cost:    3
c ---[2244]---> BDD-cost:    3
c ---[2243]---> BDD-cost:    3
c ---[2242]---> BDD-cost:    3
c ---[2241]---> BDD-cost:    3
c ---[2240]---> BDD-cost:    3
c ---[2239]---> BDD-cost:    3
c ---[2238]---> BDD-cost:    3
c ---[2237]---> BDD-cost:    3
c ---[2236]---> BDD-cost:    3
c ---[2235]---> BDD-cost:    3
c ---[2234]---> BDD-cost:    3
c ---[2233]---> BDD-cost:    3
c ---[2232]---> BDD-cost:    3
c ---[2231]---> BDD-cost:    3
c ---[2230]---> BDD-cost:    3
c ---[2229]---> BDD-cost:    3
c ---[2228]---> BDD-cost:    3
c ---[2227]---> BDD-cost:    3
c ---[2226]---> BDD-cost:    3
c ---[2225]---> BDD-cost:    3
c ---[2224]---> BDD-cost:    3
c ---[2223]---> BDD-cost:    3
c ---[2222]---> BDD-cost:    3
c ---[2221]---> BDD-cost:    3
c ---[2220]---> BDD-cost:    3
c ---[2219]---> BDD-cost:    3
c ---[2218]---> BDD-cost:    3
c ---[2217]---> BDD-cost:    3
c ---[2216]---> BDD-cost:    3
c ---[2215]---> BDD-cost:    3
c ---[2214]---> BDD-cost:    3
c ---[2213]---> BDD-cost:    3
c ---[2212]---> BDD-cost:    3
c ---[2211]---> BDD-cost:    3
c ---[2210]---> BDD-cost:    3
c ---[2209]---> BDD-cost:    3
c ---[2208]---> BDD-cost:    3
c ---[2207]---> BDD-cost:    3
c ---[2206]---> BDD-cost:    3
c ---[2205]---> BDD-cost:    3
c ---[2204]---> BDD-cost:    3
c ---[2203]---> BDD-cost:    3
c ---[2202]---> BDD-cost:    3
c ---[2201]---> BDD-cost:    3
c ---[2200]---> BDD-cost:    3
c ---[2199]---> BDD-cost:    3
c ---[2198]---> BDD-cost:    3
c ---[2197]---> BDD-cost:    3
c ---[2196]---> BDD-cost:    3
c ---[2195]---> BDD-cost:    3
c ---[2194]---> BDD-cost:    3
c ---[2193]---> BDD-cost:    3
c ---[2192]---> BDD-cost:    3
c ---[2191]---> BDD-cost:    3
c ---[2190]---> BDD-cost:    3
c ---[2189]---> BDD-cost:    3
c ---[2188]---> BDD-cost:    3
c ---[2187]---> BDD-cost:    3
c ---[2186]---> BDD-cost:    3
c ---[2185]---> BDD-cost:    3
c ---[2184]---> BDD-cost:    3
c ---[2183]---> BDD-cost:    3
c ---[2182]---> BDD-cost:    3
c ---[2181]---> BDD-cost:    3
c ---[2180]---> BDD-cost:    3
c ---[2179]---> BDD-cost:    3
c ---[2178]---> BDD-cost:    3
c ---[2177]---> BDD-cost:    3
c ---[2176]---> BDD-cost:    3
c ---[2175]---> BDD-cost:    3
c ---[2174]---> BDD-cost:    3
c ---[2173]---> BDD-cost:    3
c ---[2172]---> BDD-cost:    3
c ---[2171]---> BDD-cost:    3
c ---[2170]---> BDD-cost:    3
c ---[2169]---> BDD-cost:    3
c ---[2168]---> BDD-cost:    3
c ---[2167]---> BDD-cost:    3
c ---[2166]---> BDD-cost:    3
c ---[2165]---> BDD-cost:    3
c ---[2164]---> BDD-cost:    3
c ---[2163]---> BDD-cost:    3
c ---[2162]---> BDD-cost:    3
c ---[2161]---> BDD-cost:    3
c ---[2160]---> BDD-cost:    3
c ---[2159]---> BDD-cost:    3
c ---[2158]---> BDD-cost:    3
c ---[2157]---> BDD-cost:    3
c ---[2156]---> BDD-cost:    3
c ---[2155]---> BDD-cost:    3
c ---[2154]---> BDD-cost:    3
c ---[2153]---> BDD-cost:    3
c ---[2152]---> BDD-cost:    3
c ---[2151]---> BDD-cost:    3
c ---[2150]---> BDD-cost:    3
c ---[2149]---> BDD-cost:    3
c ---[2148]---> BDD-cost:    3
c ---[2147]---> BDD-cost:    3
c ---[2146]---> BDD-cost:    3
c ---[2145]---> BDD-cost:    3
c ---[2144]---> BDD-cost:    3
c ---[2143]---> BDD-cost:    3
c ---[2142]---> BDD-cost:    3
c ---[2141]---> BDD-cost:    3
c ---[2140]---> BDD-cost:    3
c ---[2139]---> BDD-cost:    3
c ---[2138]---> BDD-cost:    3
c ---[2137]---> BDD-cost:    3
c ---[2136]---> BDD-cost:    3
c ---[2135]---> BDD-cost:    3
c ---[2134]---> BDD-cost:    3
c ---[2133]---> BDD-cost:    3
c ---[2132]---> BDD-cost:    3
c ---[2131]---> BDD-cost:    3
c ---[2130]---> BDD-cost:    3
c ---[2129]---> BDD-cost:    3
c ---[2128]---> BDD-cost:    3
c ---[2127]---> BDD-cost:    3
c ---[2126]---> BDD-cost:    3
c ---[2125]---> BDD-cost:    3
c ---[2124]---> BDD-cost:    3
c ---[2123]---> BDD-cost:    3
c ---[2122]---> BDD-cost:    3
c ---[2121]---> BDD-cost:    3
c ---[2120]---> BDD-cost:    3
c ---[2119]---> BDD-cost:    3
c ---[2118]---> BDD-cost:    3
c ---[2117]---> BDD-cost:    3
c ---[2116]---> BDD-cost:    3
c ---[2115]---> BDD-cost:    3
c ---[2114]---> BDD-cost:    3
c ---[2113]---> BDD-cost:    3
c ---[2112]---> BDD-cost:    3
c ---[2111]---> BDD-cost:    3
c ---[2110]---> BDD-cost:    3
c ---[2109]---> BDD-cost:    3
c ---[2108]---> BDD-cost:    3
c ---[2107]---> BDD-cost:    3
c ---[2106]---> BDD-cost:    3
c ---[2105]---> BDD-cost:    3
c ---[2104]---> BDD-cost:    3
c ---[2103]---> BDD-cost:    3
c ---[2102]---> BDD-cost:    3
c ---[2101]---> BDD-cost:    3
c ---[2100]---> BDD-cost:    3
c ---[2099]---> BDD-cost:    3
c ---[2098]---> BDD-cost:    3
c ---[2097]---> BDD-cost:    3
c ---[2096]---> BDD-cost:    3
c ---[2095]---> BDD-cost:    3
c ---[2094]---> BDD-cost:    3
c ---[2093]---> BDD-cost:    3
c ---[2092]---> BDD-cost:    3
c ---[2091]---> BDD-cost:    3
c ---[2090]---> BDD-cost:    3
c ---[2089]---> BDD-cost:    3
c ---[2088]---> BDD-cost:    3
c ---[2087]---> BDD-cost:    3
c ---[2086]---> BDD-cost:    3
c ---[2085]---> BDD-cost:    3
c ---[2084]---> BDD-cost:    3
c ---[2083]---> BDD-cost:    3
c ---[2082]---> BDD-cost:    3
c ---[2081]---> BDD-cost:    3
c ---[2080]---> BDD-cost:    3
c ---[2079]---> BDD-cost:    3
c ---[2078]---> BDD-cost:    3
c ---[2077]---> BDD-cost:    3
c ---[2076]---> BDD-cost:    3
c ---[2075]---> BDD-cost:    3
c ---[2074]---> BDD-cost:    3
c ---[2073]---> BDD-cost:    3
c ---[2072]---> BDD-cost:    3
c ---[2071]---> BDD-cost:    3
c ---[2070]---> BDD-cost:    3
c ---[2069]---> BDD-cost:    3
c ---[2068]---> BDD-cost:    3
c ---[2067]---> BDD-cost:    3
c ---[2066]---> BDD-cost:    3
c ---[2065]---> BDD-cost:    3
c ---[2064]---> BDD-cost:    3
c ---[2063]---> BDD-cost:    3
c ---[2062]---> BDD-cost:    3
c ---[2061]---> BDD-cost:    3
c ---[2060]---> BDD-cost:    3
c ---[2059]---> BDD-cost:    3
c ---[2058]---> BDD-cost:    3
c ---[2057]---> BDD-cost:    3
c ---[2056]---> BDD-cost:    3
c ---[2055]---> BDD-cost:    3
c ---[2054]---> BDD-cost:    3
c ---[2053]---> BDD-cost:    3
c ---[2052]---> BDD-cost:    3
c ---[2051]---> BDD-cost:    3
c ---[2050]---> BDD-cost:    3
c ---[2049]---> BDD-cost:    3
c ---[2048]---> BDD-cost:    3
c ---[2047]---> BDD-cost:    3
c ---[2046]---> BDD-cost:    3
c ---[2045]---> BDD-cost:    3
c ---[2044]---> BDD-cost:    3
c ---[2043]---> BDD-cost:    3
c ---[2042]---> BDD-cost:    3
c ---[2041]---> BDD-cost:    3
c ---[2040]---> BDD-cost:    3
c ---[2039]---> BDD-cost:    3
c ---[2038]---> BDD-cost:    3
c ---[2037]---> BDD-cost:    3
c ---[2036]---> BDD-cost:    3
c ---[2035]---> BDD-cost:    3
c ---[2034]---> BDD-cost:    3
c ---[2033]---> BDD-cost:    3
c ---[2032]---> BDD-cost:    3
c ---[2031]---> BDD-cost:    3
c ---[2030]---> BDD-cost:    3
c ---[2029]---> BDD-cost:    3
c ---[2028]---> BDD-cost:    3
c ---[2027]---> BDD-cost:    3
c ---[2026]---> BDD-cost:    3
c ---[2025]---> BDD-cost:    3
c ---[2024]---> BDD-cost:    3
c ---[2023]---> BDD-cost:    3
c ---[2022]---> BDD-cost:    3
c ---[2021]---> BDD-cost:    3
c ---[2020]---> BDD-cost:    3
c ---[2019]---> BDD-cost:    3
c ---[2018]---> BDD-cost:    3
c ---[2017]---> BDD-cost:    3
c ---[2016]---> BDD-cost:    3
c ---[2015]---> BDD-cost:    3
c ---[2014]---> BDD-cost:    3
c ---[2013]---> BDD-cost:    3
c ---[2012]---> BDD-cost:    3
c ---[2011]---> BDD-cost:    3
c ---[2010]---> BDD-cost:    3
c ---[2009]---> BDD-cost:    3
c ---[2008]---> BDD-cost:    3
c ---[2007]---> BDD-cost:    3
c ---[2006]---> BDD-cost:    3
c ---[2004]---> BDD-cost:    3
c ---[2002]---> BDD-cost:    3
c ---[2001]---> BDD-cost:    3
c ---[1999]---> BDD-cost:    3
c ---[1997]---> BDD-cost:    3
c ---[1995]---> BDD-cost:    3
c ---[1993]---> BDD-cost:    3
c ---[1991]---> BDD-cost:    3
c ---[1989]---> BDD-cost:    3
c ---[1987]---> BDD-cost:    3
c ---[1985]---> BDD-cost:    3
c ---[1983]---> BDD-cost:    3
c ---[1981]---> BDD-cost:    3
c ---[1980]---> BDD-cost:    3
c ---[1978]---> BDD-cost:    3
c ---[1976]---> BDD-cost:    3
c ---[1974]---> BDD-cost:    3
c ---[1972]---> BDD-cost:    3
c ---[1970]---> BDD-cost:    3
c ---[1968]---> BDD-cost:    3
c ---[1966]---> BDD-cost:    3
c ---[1964]---> BDD-cost:    3
c ---[1962]---> BDD-cost:    3
c ---[1960]---> BDD-cost:    3
c ---[1959]---> BDD-cost:    3
c ---[1957]---> BDD-cost:    3
c ---[1955]---> BDD-cost:    3
c ---[1953]---> BDD-cost:    3
c ---[1951]---> BDD-cost:    3
c ---[1949]---> BDD-cost:    3
c ---[1947]---> BDD-cost:    3
c ---[1945]---> BDD-cost:    3
c ---[1943]---> BDD-cost:    3
c ---[1941]---> BDD-cost:    3
c ---[1939]---> BDD-cost:    3
c ---[1938]---> BDD-cost:    3
c ---[1936]---> BDD-cost:    3
c ---[1934]---> BDD-cost:    3
c ---[1932]---> BDD-cost:    3
c ---[1930]---> BDD-cost:    3
c ---[1928]---> BDD-cost:    3
c ---[1926]---> BDD-cost:    3
c ---[1924]---> BDD-cost:    3
c ---[1922]---> BDD-cost:    3
c ---[1919]---> BDD-cost:    3
c ---[1918]---> BDD-cost:    3
c ---[1907]---> BDD-cost:    3
c ---[1896]---> BDD-cost:    3
c ---[1885]---> BDD-cost:    3
c ---[1874]---> BDD-cost:    3
c ---[1863]---> BDD-cost:    3
c ---[1852]---> BDD-cost:    3
c ---[1841]---> BDD-cost:    3
c ---[1830]---> BDD-cost:    1
c ---[1829]---> BDD-cost:    3
c ---[1827]---> BDD-cost:    1
c ---[1825]---> BDD-cost:    1
c ---[1823]---> BDD-cost:    1
c ---[1821]---> BDD-cost:    1
c ---[1819]---> BDD-cost:    1
c ---[1817]---> BDD-cost:    1
c ---[1815]---> BDD-cost:    1
c ---[1813]---> BDD-cost:    1
c ---[1811]---> BDD-cost:    1
c ---[1809]---> BDD-cost:    1
c ---[1808]---> BDD-cost:    3
c ---[1806]---> BDD-cost:    1
c ---[1804]---> BDD-cost:    1
c ---[1802]---> BDD-cost:    1
c ---[1800]---> BDD-cost:    1
c ---[1798]---> BDD-cost:    1
c ---[1796]---> BDD-cost:    1
c ---[1794]---> BDD-cost:    1
c ---[1792]---> BDD-cost:    1
c ---[1790]---> BDD-cost:    1
c ---[1788]---> BDD-cost:    1
c ---[1787]---> BDD-cost:    3
c ---[1786]---> BDD-cost:    3
c ---[1784]---> BDD-cost:    1
c ---[1782]---> BDD-cost:    1
c ---[1780]---> BDD-cost:    1
c ---[1778]---> BDD-cost:    1
c ---[1776]---> BDD-cost:    1
c ---[1774]---> BDD-cost:    1
c ---[1772]---> BDD-cost:    1
c ---[1770]---> BDD-cost:    1
c ---[1768]---> BDD-cost:    1
c ---[1766]---> BDD-cost:    1
c ---[1765]---> BDD-cost:    3
c ---[1763]---> BDD-cost:    1
c ---[1761]---> BDD-cost:    1
c ---[1759]---> BDD-cost:    1
c ---[1757]---> BDD-cost:    1
c ---[1755]---> BDD-cost:    1
c ---[1753]---> BDD-cost:    1
c ---[1751]---> BDD-cost:    1
c ---[1749]---> BDD-cost:    1
c ---[1747]---> BDD-cost:    1
c ---[1745]---> BDD-cost:    1
c ---[1744]---> BDD-cost:    3
c ---[1742]---> BDD-cost:    1
c ---[1741]---> BDD-cost:    5
c ---[1740]---> BDD-cost:    5
c ---[1739]---> BDD-cost:    5
c ---[1738]---> BDD-cost:    5
c ---[1737]---> BDD-cost:    5
c ---[1736]---> BDD-cost:    5
c ---[1735]---> BDD-cost:    5
c ---[1734]---> BDD-cost:    5
c ---[1733]---> BDD-cost:    5
c ---[1732]---> BDD-cost:    3
c ---[1731]---> BDD-cost:    5
c ---[1730]---> BDD-cost:    5
c ---[1729]---> BDD-cost:    5
c ---[1728]---> BDD-cost:    5
c ---[1727]---> BDD-cost:    5
c ---[1726]---> BDD-cost:    5
c ---[1725]---> BDD-cost:    5
c ---[1724]---> BDD-cost:    5
c ---[1723]---> BDD-cost:    5
c ---[1722]---> BDD-cost:    5
c ---[1721]---> BDD-cost:    3
c ---[1720]---> BDD-cost:    5
c ---[1719]---> BDD-cost:    5
c ---[1718]---> BDD-cost:    5
c ---[1717]---> BDD-cost:    5
c ---[1716]---> BDD-cost:    5
c ---[1715]---> BDD-cost:    5
c ---[1714]---> BDD-cost:    5
c ---[1713]---> BDD-cost:    5
c ---[1712]---> BDD-cost:    5
c ---[1711]---> BDD-cost:    5
c ---[1710]---> BDD-cost:    3
c ---[1709]---> BDD-cost:    5
c ---[1708]---> BDD-cost:    5
c ---[1707]---> BDD-cost:    5
c ---[1706]---> BDD-cost:    5
c ---[1705]---> BDD-cost:    5
c ---[1704]---> BDD-cost:    5
c ---[1703]---> BDD-cost:    5
c ---[1702]---> BDD-cost:    5
c ---[1700]---> BDD-cost:    5
c ---[1698]---> BDD-cost:    5
c ---[1697]---> BDD-cost:    3
c ---[1695]---> BDD-cost:    5
c ---[1694]---> BDD-cost:    3
c ---[1693]---> BDD-cost:    3
c ---[1692]---> BDD-cost:    3
c ---[1691]---> BDD-cost:    3
c ---[1690]---> BDD-cost:    3
c ---[1689]---> BDD-cost:    3
c ---[1688]---> BDD-cost:    3
c ---[1687]---> BDD-cost:    3
c ---[1686]---> BDD-cost:    3
c ---[1685]---> BDD-cost:    3
c ---[1684]---> BDD-cost:    3
c ---[1683]---> BDD-cost:    3
c ---[1682]---> BDD-cost:    3
c ---[1681]---> BDD-cost:    3
c ---[1680]---> BDD-cost:    3
c ---[1679]---> BDD-cost:    3
c ---[1678]---> BDD-cost:    3
c ---[1677]---> BDD-cost:    3
c ---[1676]---> BDD-cost:    3
c ---[1675]---> BDD-cost:    3
c ---[1674]---> BDD-cost:    3
c ---[1673]---> BDD-cost:    3
c ---[1672]---> BDD-cost:    3
c ---[1671]---> BDD-cost:    3
c ---[1670]---> BDD-cost:    3
c ---[1669]---> BDD-cost:    3
c ---[1668]---> BDD-cost:    3
c ---[1667]---> BDD-cost:    3
c ---[1666]---> BDD-cost:    3
c ---[1665]---> BDD-cost:    3
c ---[1664]---> BDD-cost:    3
c ---[1663]---> BDD-cost:    3
c ---[1662]---> BDD-cost:    3
c ---[1661]---> BDD-cost:    3
c ---[1660]---> BDD-cost:    3
c ---[1659]---> BDD-cost:    3
c ---[1658]---> BDD-cost:    3
c ---[1657]---> BDD-cost:    3
c ---[1656]---> BDD-cost:    3
c ---[1655]---> BDD-cost:    3
c ---[1654]---> BDD-cost:    3
c ---[1653]---> BDD-cost:    3
c ---[1652]---> BDD-cost:    3
c ---[1651]---> BDD-cost:    3
c ---[1650]---> BDD-cost:    3
c ---[1649]---> BDD-cost:    3
c ---[1648]---> BDD-cost:    3
c ---[1647]---> BDD-cost:    3
c ---[1646]---> BDD-cost:    3
c ---[1645]---> BDD-cost:    3
c ---[1644]---> BDD-cost:    3
c ---[1643]---> BDD-cost:    3
c ---[1642]---> BDD-cost:    3
c ---[1641]---> BDD-cost:    3
c ---[1640]---> BDD-cost:    3
c ---[1639]---> BDD-cost:    3
c ---[1638]---> BDD-cost:    3
c ---[1637]---> BDD-cost:    3
c ---[1636]---> BDD-cost:    3
c ---[1635]---> BDD-cost:    3
c ---[1634]---> BDD-cost:    3
c ---[1633]---> BDD-cost:    3
c ---[1632]---> BDD-cost:    3
c ---[1631]---> BDD-cost:    3
c ---[1630]---> BDD-cost:    3
c ---[1629]---> BDD-cost:    3
c ---[1628]---> BDD-cost:    3
c ---[1627]---> BDD-cost:    3
c ---[1626]---> BDD-cost:    3
c ---[1625]---> BDD-cost:    3
c ---[1624]---> BDD-cost:    3
c ---[1623]---> BDD-cost:    3
c ---[1622]---> BDD-cost:    3
c ---[1621]---> BDD-cost:    3
c ---[1620]---> BDD-cost:    3
c ---[1619]---> BDD-cost:    3
c ---[1618]---> BDD-cost:    3
c ---[1617]---> BDD-cost:    3
c ---[1616]---> BDD-cost:    3
c ---[1615]---> BDD-cost:    3
c ---[1614]---> BDD-cost:    3
c ---[1613]---> BDD-cost:    3
c ---[1612]---> BDD-cost:    3
c ---[1611]---> BDD-cost:    3
c ---[1610]---> BDD-cost:    3
c ---[1609]---> BDD-cost:    3
c ---[1608]---> BDD-cost:    3
c ---[1607]---> BDD-cost:    3
c ---[1606]---> BDD-cost:    3
c ---[1605]---> BDD-cost:    3
c ---[1604]---> BDD-cost:    3
c ---[1603]---> BDD-cost:    3
c ---[1602]---> BDD-cost:    3
c ---[1601]---> BDD-cost:    3
c ---[1600]---> BDD-cost:    3
c ---[1599]---> BDD-cost:    3
c ---[1598]---> BDD-cost:    3
c ---[1597]---> BDD-cost:    3
c ---[1596]---> BDD-cost:    3
c ---[1595]---> BDD-cost:    3
c ---[1594]---> BDD-cost:    3
c ---[1593]---> BDD-cost:    3
c ---[1592]---> BDD-cost:    3
c ---[1591]---> BDD-cost:    3
c ---[1590]---> BDD-cost:    3
c ---[1589]---> BDD-cost:    3
c ---[1588]---> BDD-cost:    3
c ---[1587]---> BDD-cost:    3
c ---[1586]---> BDD-cost:    3
c ---[1585]---> BDD-cost:    3
c ---[1584]---> BDD-cost:    3
c ---[1583]---> BDD-cost:    3
c ---[1582]---> BDD-cost:    3
c ---[1581]---> BDD-cost:    3
c ---[1580]---> BDD-cost:    3
c ---[1579]---> BDD-cost:    3
c ---[1578]---> BDD-cost:    3
c ---[1577]---> BDD-cost:    3
c ---[1576]---> BDD-cost:    3
c ---[1575]---> BDD-cost:    3
c ---[1574]---> BDD-cost:    3
c ---[1573]---> BDD-cost:    3
c ---[1572]---> BDD-cost:    3
c ---[1571]---> BDD-cost:    3
c ---[1570]---> BDD-cost:    3
c ---[1569]---> BDD-cost:    3
c ---[1568]---> BDD-cost:    3
c ---[1567]---> BDD-cost:    3
c ---[1566]---> BDD-cost:    3
c ---[1565]---> BDD-cost:    3
c ---[1564]---> BDD-cost:    3
c ---[1563]---> BDD-cost:    3
c ---[1562]---> BDD-cost:    3
c ---[1561]---> BDD-cost:    3
c ---[1560]---> BDD-cost:    3
c ---[1559]---> BDD-cost:    3
c ---[1558]---> BDD-cost:    3
c ---[1557]---> BDD-cost:    3
c ---[1556]---> BDD-cost:    3
c ---[1555]---> BDD-cost:    3
c ---[1554]---> BDD-cost:    3
c ---[1553]---> BDD-cost:    3
c ---[1552]---> BDD-cost:    3
c ---[1551]---> BDD-cost:    3
c ---[1550]---> BDD-cost:    3
c ---[1549]---> BDD-cost:    3
c ---[1548]---> BDD-cost:    3
c ---[1547]---> BDD-cost:    3
c ---[1546]---> BDD-cost:    3
c ---[1545]---> BDD-cost:    3
c ---[1544]---> BDD-cost:    3
c ---[1543]---> BDD-cost:    3
c ---[1542]---> BDD-cost:    3
c ---[1541]---> BDD-cost:    3
c ---[1540]---> BDD-cost:    3
c ---[1539]---> BDD-cost:    3
c ---[1538]---> BDD-cost:    3
c ---[1537]---> BDD-cost:    3
c ---[1536]---> BDD-cost:    3
c ---[1535]---> BDD-cost:    3
c ---[1534]---> BDD-cost:    3
c ---[1533]---> BDD-cost:    3
c ---[1532]---> BDD-cost:    3
c ---[1531]---> BDD-cost:    3
c ---[1530]---> BDD-cost:    3
c ---[1529]---> BDD-cost:    3
c ---[1528]---> BDD-cost:    3
c ---[1527]---> BDD-cost:    3
c ---[1526]---> BDD-cost:    3
c ---[1525]---> BDD-cost:    3
c ---[1524]---> BDD-cost:    3
c ---[1523]---> BDD-cost:    3
c ---[1522]---> BDD-cost:    3
c ---[1521]---> BDD-cost:    3
c ---[1520]---> BDD-cost:    3
c ---[1518]---> BDD-cost:    3
c ---[1517]---> BDD-cost:    3
c ---[1515]---> BDD-cost:    3
c ---[1513]---> BDD-cost:    3
c ---[1511]---> BDD-cost:    3
c ---[1509]---> BDD-cost:    1
c ---[1508]---> BDD-cost:    3
c ---[1507]---> BDD-cost:    3
c ---[1506]---> BDD-cost:    3
c ---[1505]---> BDD-cost:    3
c ---[1504]---> BDD-cost:    3
c ---[1503]---> BDD-cost:    3
c ---[1502]---> BDD-cost:    3
c ---[1501]---> BDD-cost:    3
c ---[1500]---> BDD-cost:    3
c ---[1499]---> BDD-cost:    3
c ---[1498]---> BDD-cost:    3
c ---[1497]---> BDD-cost:    3
c ---[1496]---> BDD-cost:    3
c ---[1495]---> BDD-cost:    3
c ---[1494]---> BDD-cost:    3
c ---[1493]---> BDD-cost:    3
c ---[1492]---> BDD-cost:    3
c ---[1491]---> BDD-cost:    3
c ---[1490]---> BDD-cost:    3
c ---[1489]---> BDD-cost:    3
c ---[1488]---> BDD-cost:    3
c ---[1487]---> BDD-cost:    3
c ---[1486]---> BDD-cost:    3
c ---[1485]---> BDD-cost:    3
c ---[1484]---> BDD-cost:    3
c ---[1483]---> BDD-cost:    3
c ---[1482]---> BDD-cost:    3
c ---[1481]---> BDD-cost:    3
c ---[1480]---> BDD-cost:    3
c ---[1479]---> BDD-cost:    3
c ---[1478]---> BDD-cost:    3
c ---[1477]---> BDD-cost:    3
c ---[1476]---> BDD-cost:    3
c ---[1475]---> BDD-cost:    3
c ---[1474]---> BDD-cost:    3
c ---[1473]---> BDD-cost:    3
c ---[1472]---> BDD-cost:    3
c ---[1471]---> BDD-cost:    3
c ---[1470]---> BDD-cost:    3
c ---[1469]---> BDD-cost:    3
c ---[1468]---> BDD-cost:    3
c ---[1467]---> BDD-cost:    3
c ---[1466]---> BDD-cost:    3
c ---[1465]---> BDD-cost:    3
c ---[1464]---> BDD-cost:    3
c ---[1463]---> BDD-cost:    3
c ---[1462]---> BDD-cost:    3
c ---[1461]---> BDD-cost:    3
c ---[1460]---> BDD-cost:    3
c ---[1459]---> BDD-cost:    3
c ---[1458]---> BDD-cost:    3
c ---[1457]---> BDD-cost:    3
c ---[1456]---> BDD-cost:    3
c ---[1455]---> BDD-cost:    3
c ---[1454]---> BDD-cost:    3
c ---[1453]---> BDD-cost:    3
c ---[1452]---> BDD-cost:    3
c ---[1451]---> BDD-cost:    3
c ---[1450]---> BDD-cost:    3
c ---[1449]---> BDD-cost:    3
c ---[1448]---> BDD-cost:    3
c ---[1447]---> BDD-cost:    3
c ---[1446]---> BDD-cost:    3
c ---[1445]---> BDD-cost:    3
c ---[1444]---> BDD-cost:    3
c ---[1443]---> BDD-cost:    3
c ---[1442]---> BDD-cost:    3
c ---[1441]---> BDD-cost:    3
c ---[1440]---> BDD-cost:    3
c ---[1439]---> BDD-cost:    3
c ---[1438]---> BDD-cost:    3
c ---[1437]---> BDD-cost:    3
c ---[1436]---> BDD-cost:    3
c ---[1435]---> BDD-cost:    3
c ---[1434]---> BDD-cost:    3
c ---[1433]---> BDD-cost:    3
c ---[1432]---> BDD-cost:    3
c ---[1431]---> BDD-cost:    3
c ---[1430]---> BDD-cost:    3
c ---[1429]---> BDD-cost:    3
c ---[1428]---> BDD-cost:    3
c ---[1427]---> BDD-cost:    3
c ---[1426]---> BDD-cost:    3
c ---[1425]---> BDD-cost:    3
c ---[1424]---> BDD-cost:    3
c ---[1423]---> BDD-cost:    3
c ---[1422]---> BDD-cost:    3
c ---[1421]---> BDD-cost:    3
c ---[1420]---> BDD-cost:    3
c ---[1419]---> BDD-cost:    3
c ---[1418]---> BDD-cost:    3
c ---[1417]---> BDD-cost:    3
c ---[1416]---> BDD-cost:    3
c ---[1415]---> BDD-cost:    3
c ---[1414]---> BDD-cost:    3
c ---[1413]---> BDD-cost:    3
c ---[1412]---> BDD-cost:    3
c ---[1411]---> BDD-cost:    3
c ---[1410]---> BDD-cost:    3
c ---[1409]---> BDD-cost:    3
c ---[1408]---> BDD-cost:    3
c ---[1407]---> BDD-cost:    3
c ---[1406]---> BDD-cost:    3
c ---[1405]---> BDD-cost:    3
c ---[1404]---> BDD-cost:    3
c ---[1403]---> BDD-cost:    3
c ---[1402]---> BDD-cost:    3
c ---[1401]---> BDD-cost:    3
c ---[1400]---> BDD-cost:    3
c ---[1399]---> BDD-cost:    3
c ---[1398]---> BDD-cost:    3
c ---[1397]---> BDD-cost:    3
c ---[1396]---> BDD-cost:    3
c ---[1395]---> BDD-cost:    3
c ---[1394]---> BDD-cost:    3
c ---[1393]---> BDD-cost:    3
c ---[1392]---> BDD-cost:    3
c ---[1391]---> BDD-cost:    3
c ---[1390]---> BDD-cost:    3
c ---[1389]---> BDD-cost:    3
c ---[1388]---> BDD-cost:    3
c ---[1387]---> BDD-cost:    3
c ---[1386]---> BDD-cost:    3
c ---[1385]---> BDD-cost:    3
c ---[1384]---> BDD-cost:    3
c ---[1383]---> BDD-cost:    3
c ---[1382]---> BDD-cost:    3
c ---[1381]---> BDD-cost:    3
c ---[1380]---> BDD-cost:    3
c ---[1379]---> BDD-cost:    3
c ---[1378]---> BDD-cost:    3
c ---[1377]---> BDD-cost:    3
c ---[1376]---> BDD-cost:    3
c ---[1375]---> BDD-cost:    3
c ---[1374]---> BDD-cost:    3
c ---[1373]---> BDD-cost:    3
c ---[1372]---> BDD-cost:    3
c ---[1371]---> BDD-cost:    3
c ---[1370]---> BDD-cost:    3
c ---[1369]---> BDD-cost:    3
c ---[1368]---> BDD-cost:    3
c ---[1367]---> BDD-cost:    3
c ---[1366]---> BDD-cost:    3
c ---[1365]---> BDD-cost:    3
c ---[1364]---> BDD-cost:    3
c ---[1363]---> BDD-cost:    3
c ---[1362]---> BDD-cost:    3
c ---[1361]---> BDD-cost:    3
c ---[1360]---> BDD-cost:    3
c ---[1359]---> BDD-cost:    3
c ---[1358]---> BDD-cost:    3
c ---[1357]---> BDD-cost:    3
c ---[1356]---> BDD-cost:    3
c ---[1355]---> BDD-cost:    3
c ---[1354]---> BDD-cost:    3
c ---[1353]---> BDD-cost:    3
c ---[1352]---> BDD-cost:    3
c ---[1351]---> BDD-cost:    3
c ---[1350]---> BDD-cost:    3
c ---[1349]---> BDD-cost:    3
c ---[1348]---> BDD-cost:    3
c ---[1347]---> BDD-cost:    3
c ---[1346]---> BDD-cost:    3
c ---[1345]---> BDD-cost:    3
c ---[1344]---> BDD-cost:    3
c ---[1343]---> BDD-cost:    3
c ---[1342]---> BDD-cost:    3
c ---[1341]---> BDD-cost:    3
c ---[1340]---> BDD-cost:    3
c ---[1339]---> BDD-cost:    3
c ---[1338]---> BDD-cost:    3
c ---[1337]---> BDD-cost:    3
c ---[1336]---> BDD-cost:    3
c ---[1335]---> BDD-cost:    3
c ---[1334]---> BDD-cost:    3
c ---[1333]---> BDD-cost:    3
c ---[1332]---> BDD-cost:    3
c ---[1331]---> BDD-cost:    3
c ---[1330]---> BDD-cost:    3
c ---[1329]---> BDD-cost:    3
c ---[1328]---> BDD-cost:    3
c ---[1327]---> BDD-cost:    3
c ---[1326]---> BDD-cost:    3
c ---[1325]---> BDD-cost:    3
c ---[1324]---> BDD-cost:    3
c ---[1323]---> BDD-cost:    3
c ---[1322]---> BDD-cost:    3
c ---[1321]---> BDD-cost:    3
c ---[1320]---> BDD-cost:    3
c ---[1319]---> BDD-cost:    3
c ---[1318]---> BDD-cost:    3
c ---[1317]---> BDD-cost:    3
c ---[1316]---> BDD-cost:    3
c ---[1315]---> BDD-cost:    3
c ---[1314]---> BDD-cost:    3
c ---[1313]---> BDD-cost:    3
c ---[1312]---> BDD-cost:    3
c ---[1311]---> BDD-cost:    3
c ---[1310]---> BDD-cost:    3
c ---[1309]---> BDD-cost:    3
c ---[1308]---> BDD-cost:    3
c ---[1307]---> BDD-cost:    3
c ---[1306]---> BDD-cost:    3
c ---[1305]---> BDD-cost:    3
c ---[1304]---> BDD-cost:    3
c ---[1303]---> BDD-cost:    3
c ---[1302]---> BDD-cost:    3
c ---[1301]---> BDD-cost:    3
c ---[1300]---> BDD-cost:    3
c ---[1299]---> BDD-cost:    3
c ---[1298]---> BDD-cost:    3
c ---[1297]---> BDD-cost:    3
c ---[1296]---> BDD-cost:    3
c ---[1295]---> BDD-cost:    3
c ---[1294]---> BDD-cost:    3
c ---[1293]---> BDD-cost:    3
c ---[1292]---> BDD-cost:    3
c ---[1291]---> BDD-cost:    3
c ---[1290]---> BDD-cost:    3
c ---[1289]---> BDD-cost:    3
c ---[1288]---> BDD-cost:    3
c ---[1287]---> BDD-cost:    3
c ---[1286]---> BDD-cost:    3
c ---[1285]---> BDD-cost:    3
c ---[1284]---> BDD-cost:    3
c ---[1283]---> BDD-cost:    3
c ---[1282]---> BDD-cost:    3
c ---[1281]---> BDD-cost:    3
c ---[1280]---> BDD-cost:    3
c ---[1279]---> BDD-cost:    3
c ---[1278]---> BDD-cost:    3
c ---[1277]---> BDD-cost:    3
c ---[1276]---> BDD-cost:    3
c ---[1275]---> BDD-cost:    3
c ---[1274]---> BDD-cost:    3
c ---[1273]---> BDD-cost:    3
c ---[1272]---> BDD-cost:    3
c ---[1271]---> BDD-cost:    3
c ---[1270]---> BDD-cost:    3
c ---[1269]---> BDD-cost:    3
c ---[1268]---> BDD-cost:    3
c ---[1267]---> BDD-cost:    3
c ---[1266]---> BDD-cost:    3
c ---[1265]---> BDD-cost:    3
c ---[1264]---> BDD-cost:    3
c ---[1263]---> BDD-cost:    3
c ---[1262]---> BDD-cost:    3
c ---[1261]---> BDD-cost:    3
c ---[1260]---> BDD-cost:    3
c ---[1259]---> BDD-cost:    3
c ---[1258]---> BDD-cost:    3
c ---[1257]---> BDD-cost:    3
c ---[1256]---> BDD-cost:    3
c ---[1255]---> BDD-cost:    3
c ---[1254]---> BDD-cost:    3
c ---[1253]---> BDD-cost:    3
c ---[1252]---> BDD-cost:    3
c ---[1251]---> BDD-cost:    3
c ---[1250]---> BDD-cost:    3
c ---[1249]---> BDD-cost:    3
c ---[1248]---> BDD-cost:    3
c ---[1247]---> BDD-cost:    3
c ---[1246]---> BDD-cost:    3
c ---[1245]---> BDD-cost:    3
c ---[1244]---> BDD-cost:    3
c ---[1243]---> BDD-cost:    3
c ---[1242]---> BDD-cost:    3
c ---[1241]---> BDD-cost:    3
c ---[1240]---> BDD-cost:    3
c ---[1239]---> BDD-cost:    3
c ---[1238]---> BDD-cost:    3
c ---[1237]---> BDD-cost:    3
c ---[1236]---> BDD-cost:    3
c ---[1235]---> BDD-cost:    3
c ---[1234]---> BDD-cost:    3
c ---[1233]---> BDD-cost:    3
c ---[1232]---> BDD-cost:    3
c ---[1231]---> BDD-cost:    3
c ---[1230]---> BDD-cost:    3
c ---[1229]---> BDD-cost:    3
c ---[1228]---> BDD-cost:    3
c ---[1227]---> BDD-cost:    3
c ---[1226]---> BDD-cost:    3
c ---[1225]---> BDD-cost:    3
c ---[1224]---> BDD-cost:    3
c ---[1223]---> BDD-cost:    3
c ---[1222]---> BDD-cost:    3
c ---[1221]---> BDD-cost:    3
c ---[1220]---> BDD-cost:    3
c ---[1219]---> BDD-cost:    3
c ---[1218]---> BDD-cost:    3
c ---[1217]---> BDD-cost:    3
c ---[1216]---> BDD-cost:    3
c ---[1215]---> BDD-cost:    3
c ---[1214]---> BDD-cost:    3
c ---[1213]---> BDD-cost:    3
c ---[1212]---> BDD-cost:    3
c ---[1211]---> BDD-cost:    3
c ---[1210]---> BDD-cost:    3
c ---[1209]---> BDD-cost:    3
c ---[1208]---> BDD-cost:    3
c ---[1207]---> BDD-cost:    3
c ---[1206]---> BDD-cost:    3
c ---[1205]---> BDD-cost:    3
c ---[1204]---> BDD-cost:    3
c ---[1203]---> BDD-cost:    3
c ---[1202]---> BDD-cost:    3
c ---[1201]---> BDD-cost:    3
c ---[1200]---> BDD-cost:    3
c ---[1199]---> BDD-cost:    3
c ---[1198]---> BDD-cost:    3
c ---[1197]---> BDD-cost:    3
c ---[1196]---> BDD-cost:    3
c ---[1195]---> BDD-cost:    3
c ---[1194]---> BDD-cost:    3
c ---[1193]---> BDD-cost:    3
c ---[1192]---> BDD-cost:    3
c ---[1191]---> BDD-cost:    3
c ---[1190]---> BDD-cost:    3
c ---[1189]---> BDD-cost:    3
c ---[1188]---> BDD-cost:    3
c ---[1187]---> BDD-cost:    3
c ---[1186]---> BDD-cost:    3
c ---[1185]---> BDD-cost:    3
c ---[1184]---> BDD-cost:    3
c ---[1183]---> BDD-cost:    3
c ---[1182]---> BDD-cost:    3
c ---[1181]---> BDD-cost:    3
c ---[1180]---> BDD-cost:    3
c ---[1179]---> BDD-cost:    3
c ---[1178]---> BDD-cost:    3
c ---[1177]---> BDD-cost:    3
c ---[1176]---> BDD-cost:    3
c ---[1175]---> BDD-cost:    3
c ---[1174]---> BDD-cost:    3
c ---[1173]---> BDD-cost:    3
c ---[1172]---> BDD-cost:    3
c ---[1171]---> BDD-cost:    3
c ---[1170]---> BDD-cost:    3
c ---[1169]---> BDD-cost:    3
c ---[1168]---> BDD-cost:    3
c ---[1167]---> BDD-cost:    3
c ---[1166]---> BDD-cost:    3
c ---[1165]---> BDD-cost:    3
c ---[1164]---> BDD-cost:    3
c ---[1163]---> BDD-cost:    3
c ---[1162]---> BDD-cost:    3
c ---[1161]---> BDD-cost:    3
c ---[1160]---> BDD-cost:    3
c ---[1159]---> BDD-cost:    3
c ---[1158]---> BDD-cost:    3
c ---[1157]---> BDD-cost:    3
c ---[1156]---> BDD-cost:    3
c ---[1155]---> BDD-cost:    3
c ---[1154]---> BDD-cost:    3
c ---[1153]---> BDD-cost:    3
c ---[1152]---> BDD-cost:    3
c ---[1151]---> BDD-cost:    3
c ---[1150]---> BDD-cost:    3
c ---[1149]---> BDD-cost:    3
c ---[1148]---> BDD-cost:    3
c ---[1147]---> BDD-cost:    3
c ---[1146]---> BDD-cost:    3
c ---[1145]---> BDD-cost:    3
c ---[1144]---> BDD-cost:    3
c ---[1143]---> BDD-cost:    3
c ---[1142]---> BDD-cost:    3
c ---[1141]---> BDD-cost:    3
c ---[1140]---> BDD-cost:    3
c ---[1139]---> BDD-cost:    3
c ---[1138]---> BDD-cost:    3
c ---[1137]---> BDD-cost:    3
c ---[1136]---> BDD-cost:    3
c ---[1135]---> BDD-cost:    3
c ---[1134]---> BDD-cost:    3
c ---[1133]---> BDD-cost:    3
c ---[1132]---> BDD-cost:    3
c ---[1131]---> BDD-cost:    3
c ---[1130]---> BDD-cost:    3
c ---[1129]---> BDD-cost:    3
c ---[1128]---> BDD-cost:    3
c ---[1127]---> BDD-cost:    3
c ---[1126]---> BDD-cost:    3
c ---[1125]---> BDD-cost:    3
c ---[1124]---> BDD-cost:    3
c ---[1123]---> BDD-cost:    3
c ---[1122]---> BDD-cost:    3
c ---[1121]---> BDD-cost:    3
c ---[1120]---> BDD-cost:    3
c ---[1119]---> BDD-cost:    3
c ---[1118]---> BDD-cost:    3
c ---[1117]---> BDD-cost:    3
c ---[1116]---> BDD-cost:    3
c ---[1115]---> BDD-cost:    3
c ---[1114]---> BDD-cost:    3
c ---[1113]---> BDD-cost:    3
c ---[1112]---> BDD-cost:    3
c ---[1111]---> BDD-cost:    3
c ---[1110]---> BDD-cost:    3
c ---[1109]---> BDD-cost:    3
c ---[1108]---> BDD-cost:    3
c ---[1107]---> BDD-cost:    3
c ---[1106]---> BDD-cost:    3
c ---[1105]---> BDD-cost:    3
c ---[1104]---> BDD-cost:    3
c ---[1103]---> BDD-cost:    3
c ---[1102]---> BDD-cost:    3
c ---[1101]---> BDD-cost:    3
c ---[1100]---> BDD-cost:    3
c ---[1099]---> BDD-cost:    3
c ---[1098]---> BDD-cost:    3
c ---[1097]---> BDD-cost:    3
c ---[1096]---> BDD-cost:    3
c ---[1095]---> BDD-cost:    3
c ---[1094]---> BDD-cost:    3
c ---[1093]---> BDD-cost:    3
c ---[1092]---> Adder-cost: 59486   maxlim: 14773890   bits: 24/24
c ---[1091]---> BDD-cost:    3
c ---[1090]---> BDD-cost:    3
c ---[1089]---> BDD-cost:    3
c ---[1088]---> BDD-cost:    3
c ---[1087]---> BDD-cost:    3
c ---[1085]---> BDD-cost:    1
c ---[1083]---> BDD-cost:    1
c ---[1081]---> BDD-cost:    1
c ---[1079]---> BDD-cost:    1
c ---[1077]---> BDD-cost:    1
c ---[1075]---> BDD-cost:    1
c ---[1073]---> BDD-cost:    1
c ---[1072]---> BDD-cost:    3
c ---[1070]---> BDD-cost:    1
c ---[1068]---> BDD-cost:    1
c ---[1066]---> BDD-cost:    1
c ---[1064]---> BDD-cost:    1
c ---[1062]---> BDD-cost:    1
c ---[1060]---> BDD-cost:    1
c ---[1058]---> BDD-cost:    1
c ---[1056]---> BDD-cost:    1
c ---[1054]---> BDD-cost:    1
c ---[1052]---> BDD-cost:    1
c ---[1051]---> BDD-cost:    3
c ---[1049]---> BDD-cost:    1
c ---[1047]---> BDD-cost:    1
c ---[1045]---> BDD-cost:    1
c ---[1037]---> BDD-cost:    3
c ---[1026]---> BDD-cost:    3
c ---[1015]---> BDD-cost:    3
c ---[1004]---> BDD-cost:    3
c ---[ 993]---> BDD-cost:    3
c ---[ 982]---> BDD-cost:    3
c ---[ 971]---> BDD-cost:    3
c ---[ 960]---> BDD-cost:    3
c ---[ 959]---> BDD-cost:    3
c ---[ 948]---> BDD-cost:    3
c ---[ 937]---> BDD-cost:    3
c ---[ 926]---> BDD-cost:    3
c ---[ 915]---> BDD-cost:    3
c ---[ 904]---> BDD-cost:    3
c ---[ 902]---> BDD-cost:    1
c ---[ 900]---> BDD-cost:    1
c ---[ 898]---> BDD-cost:    1
c ---[ 896]---> BDD-cost:    1
c ---[ 894]---> BDD-cost:    1
c ---[ 892]---> BDD-cost:    1
c ---[ 890]---> BDD-cost:    1
c ---[ 888]---> BDD-cost:    1
c ---[ 886]---> BDD-cost:    1
c ---[ 884]---> BDD-cost:    1
c ---[ 883]---> BDD-cost:    3
c ---[ 881]---> BDD-cost:    1
c ---[ 879]---> BDD-cost:    1
c ---[ 877]---> BDD-cost:    1
c ---[ 869]---> BDD-cost:    3
c ---[ 861]---> BDD-cost:    3
c ---[ 860]---> BDD-cost:    3
c ---[ 859]---> BDD-cost:    3
c ---[ 858]---> BDD-cost:    3
c ---[ 857]---> BDD-cost:    3
c ---[ 856]---> BDD-cost:    3
c ---[ 855]---> BDD-cost:    3
c ---[ 854]---> BDD-cost:    3
c ---[ 853]---> BDD-cost:    3
c ---[ 852]---> BDD-cost:    3
c ---[ 851]---> BDD-cost:    3
c ---[ 850]---> BDD-cost:    3
c ---[ 849]---> BDD-cost:    3
c ---[ 848]---> BDD-cost:    3
c ---[ 847]---> BDD-cost:    3
c ---[ 846]---> BDD-cost:    3
c ---[ 845]---> BDD-cost:    3
c ---[ 844]---> BDD-cost:    3
c ---[ 843]---> BDD-cost:    3
c ---[ 842]---> BDD-cost:    3
c ---[ 841]---> BDD-cost:    3
c ---[ 840]---> BDD-cost:    3
c ---[ 839]---> BDD-cost:    3
c ---[ 838]---> BDD-cost:    3
c ---[ 837]---> BDD-cost:    3
c ---[ 836]---> BDD-cost:    3
c ---[ 835]---> BDD-cost:    3
c ---[ 834]---> BDD-cost:    3
c ---[ 833]---> BDD-cost:    3
c ---[ 832]---> BDD-cost:    3
c ---[ 831]---> BDD-cost:    3
c ---[ 830]---> BDD-cost:    3
c ---[ 829]---> BDD-cost:    3
c ---[ 828]---> BDD-cost:    3
c ---[ 827]---> BDD-cost:    3
c ---[ 826]---> BDD-cost:    3
c ---[ 825]---> BDD-cost:    3
c ---[ 824]---> BDD-cost:    3
c ---[ 823]---> BDD-cost:    3
c ---[ 822]---> BDD-cost:    3
c ---[ 821]---> BDD-cost:    3
c ---[ 820]---> BDD-cost:    3
c ---[ 819]---> BDD-cost:    3
c ---[ 818]---> BDD-cost:    3
c ---[ 817]---> BDD-cost:    3
c ---[ 816]---> BDD-cost:    3
c ---[ 815]---> BDD-cost:    3
c ---[ 814]---> BDD-cost:    3
c ---[ 813]---> BDD-cost:    3
c ---[ 812]---> BDD-cost:    3
c ---[ 811]---> BDD-cost:    3
c ---[ 810]---> BDD-cost:    3
c ---[ 809]---> BDD-cost:    3
c ---[ 808]---> BDD-cost:    3
c ---[ 807]---> BDD-cost:    3
c ---[ 806]---> BDD-cost:    3
c ---[ 805]---> BDD-cost:    3
c ---[ 804]---> BDD-cost:    3
c ---[ 803]---> BDD-cost:    3
c ---[ 802]---> BDD-cost:    3
c ---[ 801]---> BDD-cost:    3
c ---[ 800]---> BDD-cost:    3
c ---[ 799]---> BDD-cost:    3
c ---[ 798]---> BDD-cost:    3
c ---[ 797]---> BDD-cost:    3
c ---[ 796]---> BDD-cost:    3
c ---[ 795]---> BDD-cost:    3
c ---[ 794]---> BDD-cost:    3
c ---[ 793]---> BDD-cost:    3
c ---[ 792]---> BDD-cost:    3
c ---[ 791]---> BDD-cost:    3
c ---[ 790]---> BDD-cost:    3
c ---[ 789]---> BDD-cost:    3
c ---[ 788]---> BDD-cost:    3
c ---[ 787]---> BDD-cost:    3
c ---[ 786]---> BDD-cost:    3
c ---[ 785]---> BDD-cost:    3
c ---[ 784]---> BDD-cost:    3
c ---[ 783]---> BDD-cost:    3
c ---[ 782]---> BDD-cost:    3
c ---[ 781]---> BDD-cost:    3
c ---[ 780]---> BDD-cost:    3
c ---[ 779]---> BDD-cost:    3
c ---[ 778]---> BDD-cost:    3
c ---[ 777]---> BDD-cost:    3
c ---[ 776]---> BDD-cost:    3
c ---[ 775]---> BDD-cost:    3
c ---[ 774]---> BDD-cost:    3
c ---[ 773]---> BDD-cost:    3
c ---[ 772]---> BDD-cost:    3
c ---[ 771]---> BDD-cost:    3
c ---[ 770]---> BDD-cost:    3
c ---[ 769]---> BDD-cost:    3
c ---[ 768]---> BDD-cost:    3
c ---[ 767]---> BDD-cost:    3
c ---[ 766]---> BDD-cost:    3
c ---[ 765]---> BDD-cost:    3
c ---[ 764]---> BDD-cost:    3
c ---[ 763]---> BDD-cost:    3
c ---[ 762]---> BDD-cost:    3
c ---[ 761]---> BDD-cost:    3
c ---[ 760]---> BDD-cost:    3
c ---[ 759]---> BDD-cost:    3
c ---[ 758]---> BDD-cost:    3
c ---[ 757]---> BDD-cost:    3
c ---[ 756]---> BDD-cost:    3
c ---[ 755]---> BDD-cost:    3
c ---[ 754]---> BDD-cost:    3
c ---[ 753]---> BDD-cost:    3
c ---[ 752]---> BDD-cost:    3
c ---[ 751]---> BDD-cost:    3
c ---[ 750]---> BDD-cost:    3
c ---[ 749]---> BDD-cost:    3
c ---[ 748]---> BDD-cost:    3
c ---[ 747]---> BDD-cost:    3
c ---[ 746]---> BDD-cost:    3
c ---[ 745]---> BDD-cost:    3
c ---[ 744]---> BDD-cost:    3
c ---[ 743]---> BDD-cost:    3
c ---[ 742]---> BDD-cost:    3
c ---[ 741]---> BDD-cost:    3
c ---[ 740]---> BDD-cost:    3
c ---[ 739]---> BDD-cost:    3
c ---[ 738]---> BDD-cost:    3
c ---[ 737]---> BDD-cost:    3
c ---[ 736]---> BDD-cost:    3
c ---[ 735]---> BDD-cost:    3
c ---[ 734]---> BDD-cost:    3
c ---[ 733]---> BDD-cost:    3
c ---[ 732]---> BDD-cost:    3
c ---[ 731]---> BDD-cost:    3
c ---[ 730]---> BDD-cost:    3
c ---[ 729]---> BDD-cost:    3
c ---[ 728]---> BDD-cost:    3
c ---[ 727]---> BDD-cost:    3
c ---[ 726]---> BDD-cost:    3
c ---[ 725]---> BDD-cost:    3
c ---[ 724]---> BDD-cost:    3
c ---[ 723]---> BDD-cost:    3
c ---[ 722]---> BDD-cost:    3
c ---[ 721]---> BDD-cost:    3
c ---[ 720]---> BDD-cost:    3
c ---[ 719]---> BDD-cost:    3
c ---[ 718]---> BDD-cost:    3
c ---[ 717]---> BDD-cost:    3
c ---[ 716]---> BDD-cost:    3
c ---[ 715]---> BDD-cost:    3
c ---[ 714]---> BDD-cost:    3
c ---[ 713]---> BDD-cost:    3
c ---[ 712]---> BDD-cost:    3
c ---[ 711]---> BDD-cost:    3
c ---[ 710]---> BDD-cost:    3
c ---[ 709]---> BDD-cost:    3
c ---[ 708]---> BDD-cost:    3
c ---[ 707]---> BDD-cost:    3
c ---[ 706]---> BDD-cost:    3
c ---[ 705]---> BDD-cost:    3
c ---[ 704]---> BDD-cost:    3
c ---[ 703]---> BDD-cost:    3
c ---[ 702]---> BDD-cost:    3
c ---[ 701]---> BDD-cost:    3
c ---[ 700]---> BDD-cost:    3
c ---[ 699]---> BDD-cost:    3
c ---[ 698]---> BDD-cost:    3
c ---[ 697]---> BDD-cost:    3
c ---[ 696]---> BDD-cost:    3
c ---[ 695]---> BDD-cost:    3
c ---[ 694]---> BDD-cost:    3
c ---[ 693]---> BDD-cost:    3
c ---[ 692]---> BDD-cost:    3
c ---[ 691]---> BDD-cost:    3
c ---[ 690]---> BDD-cost:    3
c ---[ 689]---> BDD-cost:    3
c ---[ 688]---> BDD-cost:    3
c ---[ 687]---> BDD-cost:    3
c ---[ 686]---> BDD-cost:    3
c ---[ 685]---> BDD-cost:    3
c ---[ 684]---> BDD-cost:    3
c ---[ 683]---> BDD-cost:    3
c ---[ 682]---> BDD-cost:    3
c ---[ 681]---> BDD-cost:    3
c ---[ 680]---> BDD-cost:    3
c ---[ 679]---> BDD-cost:    3
c ---[ 678]---> BDD-cost:    3
c ---[ 677]---> BDD-cost:    3
c ---[ 676]---> BDD-cost:    3
c ---[ 675]---> BDD-cost:    3
c ---[ 674]---> BDD-cost:    3
c ---[ 673]---> BDD-cost:    3
c ---[ 672]---> BDD-cost:    3
c ---[ 671]---> BDD-cost:    3
c ---[ 670]---> BDD-cost:    3
c ---[ 669]---> BDD-cost:    3
c ---[ 668]---> BDD-cost:    3
c ---[ 667]---> BDD-cost:    3
c ---[ 666]---> BDD-cost:    3
c ---[ 665]---> BDD-cost:    3
c ---[ 664]---> BDD-cost:    3
c ---[ 663]---> BDD-cost:    3
c ---[ 662]---> BDD-cost:    3
c ---[ 661]---> BDD-cost:    3
c ---[ 660]---> BDD-cost:    3
c ---[ 659]---> BDD-cost:    3
c ---[ 658]---> BDD-cost:    3
c ---[ 657]---> BDD-cost:    3
c ---[ 656]---> BDD-cost:    3
c ---[ 655]---> BDD-cost:    3
c ---[ 654]---> BDD-cost:    3
c ---[ 653]---> BDD-cost:    3
c ---[ 652]---> BDD-cost:    3
c ---[ 651]---> BDD-cost:    3
c ---[ 650]---> BDD-cost:    3
c ---[ 649]---> BDD-cost:    3
c ---[ 648]---> BDD-cost:    3
c ---[ 647]---> BDD-cost:    3
c ---[ 646]---> BDD-cost:    3
c ---[ 645]---> BDD-cost:    3
c ---[ 644]---> BDD-cost:    3
c ---[ 643]---> BDD-cost:    3
c ---[ 642]---> BDD-cost:    3
c ---[ 641]---> BDD-cost:    3
c ---[ 640]---> BDD-cost:    3
c ---[ 639]---> BDD-cost:    3
c ---[ 638]---> BDD-cost:    3
c ---[ 637]---> BDD-cost:    3
c ---[ 636]---> BDD-cost:    3
c ---[ 635]---> BDD-cost:    3
c ---[ 634]---> BDD-cost:    3
c ---[ 633]---> BDD-cost:    3
c ---[ 632]---> BDD-cost:    3
c ---[ 631]---> BDD-cost:    3
c ---[ 630]---> BDD-cost:    3
c ---[ 629]---> BDD-cost:    3
c ---[ 628]---> BDD-cost:    3
c ---[ 627]---> BDD-cost:    3
c ---[ 626]---> BDD-cost:    3
c ---[ 625]---> BDD-cost:    3
c ---[ 624]---> BDD-cost:    3
c ---[ 623]---> BDD-cost:    3
c ---[ 622]---> BDD-cost:    3
c ---[ 621]---> BDD-cost:    3
c ---[ 620]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    3
c ---[ 618]---> BDD-cost:    3
c ---[ 617]---> BDD-cost:    3
c ---[ 616]---> BDD-cost:    3
c ---[ 615]---> BDD-cost:    3
c ---[ 614]---> BDD-cost:    3
c ---[ 613]---> BDD-cost:    3
c ---[ 612]---> BDD-cost:    3
c ---[ 611]---> BDD-cost:    3
c ---[ 610]---> BDD-cost:    3
c ---[ 609]---> BDD-cost:    3
c ---[ 608]---> BDD-cost:    3
c ---[ 607]---> BDD-cost:    3
c ---[ 606]---> BDD-cost:    3
c ---[ 605]---> BDD-cost:    3
c ---[ 604]---> BDD-cost:    3
c ---[ 603]---> BDD-cost:    3
c ---[ 602]---> BDD-cost:    3
c ---[ 601]---> BDD-cost:    3
c ---[ 600]---> BDD-cost:    3
c ---[ 599]---> BDD-cost:    3
c ---[ 598]---> BDD-cost:    3
c ---[ 597]---> BDD-cost:    3
c ---[ 596]---> BDD-cost:    3
c ---[ 595]---> BDD-cost:    3
c ---[ 594]---> BDD-cost:    3
c ---[ 593]---> BDD-cost:    3
c ---[ 592]---> BDD-cost:    3
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:    3
c ---[ 589]---> BDD-cost:    3
c ---[ 588]---> BDD-cost:    3
c ---[ 587]---> BDD-cost:    3
c ---[ 586]---> BDD-cost:    3
c ---[ 585]---> BDD-cost:    3
c ---[ 584]---> BDD-cost:    3
c ---[ 583]---> BDD-cost:    3
c ---[ 582]---> BDD-cost:    3
c ---[ 581]---> BDD-cost:    3
c ---[ 580]---> BDD-cost:    3
c ---[ 579]---> BDD-cost:    3
c ---[ 578]---> BDD-cost:    3
c ---[ 577]---> BDD-cost:    3
c ---[ 576]---> BDD-cost:    3
c ---[ 575]---> BDD-cost:    3
c ---[ 574]---> BDD-cost:    3
c ---[ 573]---> BDD-cost:    3
c ---[ 572]---> BDD-cost:    3
c ---[ 571]---> BDD-cost:    3
c ---[ 570]---> BDD-cost:    3
c ---[ 569]---> BDD-cost:    3
c ---[ 568]---> BDD-cost:    3
c ---[ 567]---> BDD-cost:    3
c ---[ 566]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    3
c ---[ 564]---> BDD-cost:    3
c ---[ 563]---> BDD-cost:    3
c ---[ 562]---> BDD-cost:    3
c ---[ 561]---> BDD-cost:    3
c ---[ 560]---> BDD-cost:    3
c ---[ 559]---> BDD-cost:    3
c ---[ 558]---> BDD-cost:    3
c ---[ 557]---> BDD-cost:    3
c ---[ 556]---> BDD-cost:    3
c ---[ 555]---> BDD-cost:    3
c ---[ 554]---> BDD-cost:    3
c ---[ 553]---> BDD-cost:    3
c ---[ 552]---> BDD-cost:    3
c ---[ 551]---> BDD-cost:    3
c ---[ 550]---> BDD-cost:    3
c ---[ 549]---> BDD-cost:    3
c ---[ 548]---> BDD-cost:    3
c ---[ 547]---> BDD-cost:    3
c ---[ 546]---> BDD-cost:    3
c ---[ 545]---> BDD-cost:    3
c ---[ 544]---> BDD-cost:    3
c ---[ 543]---> BDD-cost:    3
c ---[ 542]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    3
c ---[ 540]---> BDD-cost:    3
c ---[ 539]---> BDD-cost:    3
c ---[ 538]---> BDD-cost:    3
c ---[ 537]---> BDD-cost:    3
c ---[ 536]---> BDD-cost:    3
c ---[ 535]---> BDD-cost:    3
c ---[ 534]---> BDD-cost:    3
c ---[ 533]---> BDD-cost:    3
c ---[ 532]---> BDD-cost:    3
c ---[ 531]---> BDD-cost:    3
c ---[ 530]---> BDD-cost:    3
c ---[ 529]---> BDD-cost:    3
c ---[ 528]---> BDD-cost:    3
c ---[ 527]---> BDD-cost:    3
c ---[ 526]---> BDD-cost:    3
c ---[ 525]---> BDD-cost:    3
c ---[ 524]---> BDD-cost:    3
c ---[ 523]---> BDD-cost:    3
c ---[ 522]---> BDD-cost:    3
c ---[ 521]---> BDD-cost:    3
c ---[ 520]---> BDD-cost:    3
c ---[ 519]---> BDD-cost:    3
c ---[ 518]---> BDD-cost:    3
c ---[ 517]---> BDD-cost:    3
c ---[ 516]---> BDD-cost:    3
c ---[ 515]---> BDD-cost:    3
c ---[ 514]---> BDD-cost:    3
c ---[ 513]---> BDD-cost:    3
c ---[ 512]---> BDD-cost:    3
c ---[ 511]---> BDD-cost:    3
c ---[ 510]---> BDD-cost:    3
c ---[ 509]---> BDD-cost:    3
c ---[ 508]---> BDD-cost:    3
c ---[ 507]---> BDD-cost:    3
c ---[ 506]---> BDD-cost:    3
c ---[ 505]---> BDD-cost:    3
c ---[ 504]---> BDD-cost:    3
c ---[ 503]---> BDD-cost:    3
c ---[ 502]---> BDD-cost:    3
c ---[ 501]---> BDD-cost:    3
c ---[ 500]---> BDD-cost:    3
c ---[ 499]---> BDD-cost:    3
c ---[ 498]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:    3
c ---[ 496]---> BDD-cost:    3
c ---[ 495]---> BDD-cost:    3
c ---[ 494]---> BDD-cost:    3
c ---[ 493]---> BDD-cost:    3
c ---[ 492]---> BDD-cost:    3
c ---[ 491]---> BDD-cost:    3
c ---[ 490]---> BDD-cost:    3
c ---[ 489]---> BDD-cost:    3
c ---[ 488]---> BDD-cost:    3
c ---[ 487]---> BDD-cost:    3
c ---[ 486]---> BDD-cost:    3
c ---[ 485]---> BDD-cost:    3
c ---[ 484]---> BDD-cost:    3
c ---[ 483]---> BDD-cost:    3
c ---[ 482]---> BDD-cost:    3
c ---[ 481]---> BDD-cost:    3
c ---[ 480]---> BDD-cost:    3
c ---[ 479]---> BDD-cost:    3
c ---[ 478]---> BDD-cost:    3
c ---[ 477]---> BDD-cost:    3
c ---[ 476]---> BDD-cost:    3
c ---[ 475]---> BDD-cost:    3
c ---[ 474]---> BDD-cost:    3
c ---[ 473]---> BDD-cost:    3
c ---[ 472]---> BDD-cost:    3
c ---[ 471]---> BDD-cost:    3
c ---[ 470]---> BDD-cost:    3
c ---[ 469]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:    3
c ---[ 467]---> BDD-cost:    3
c ---[ 466]---> BDD-cost:    3
c ---[ 465]---> BDD-cost:    3
c ---[ 464]---> BDD-cost:    3
c ---[ 463]---> BDD-cost:    3
c ---[ 462]---> BDD-cost:    3
c ---[ 461]---> BDD-cost:    3
c ---[ 460]---> BDD-cost:    3
c ---[ 459]---> BDD-cost:    3
c ---[ 458]---> BDD-cost:    3
c ---[ 457]---> BDD-cost:    3
c ---[ 456]---> BDD-cost:    3
c ---[ 455]---> BDD-cost:    3
c ---[ 454]---> BDD-cost:    3
c ---[ 453]---> BDD-cost:    3
c ---[ 452]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    3
c ---[ 450]---> BDD-cost:    3
c ---[ 449]---> BDD-cost:    3
c ---[ 448]---> BDD-cost:    3
c ---[ 447]---> BDD-cost:    3
c ---[ 446]---> BDD-cost:    3
c ---[ 445]---> BDD-cost:    3
c ---[ 444]---> BDD-cost:    3
c ---[ 443]---> BDD-cost:    3
c ---[ 442]---> BDD-cost:    3
c ---[ 441]---> BDD-cost:    3
c ---[ 440]---> BDD-cost:    3
c ---[ 439]---> BDD-cost:    3
c ---[ 438]---> BDD-cost:    3
c ---[ 437]---> BDD-cost:    3
c ---[ 436]---> BDD-cost:    3
c ---[ 435]---> BDD-cost:    3
c ---[ 434]---> BDD-cost:    3
c ---[ 433]---> BDD-cost:    3
c ---[ 432]---> BDD-cost:    3
c ---[ 431]---> BDD-cost:    3
c ---[ 430]---> BDD-cost:    3
c ---[ 429]---> BDD-cost:    3
c ---[ 428]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:    3
c ---[ 426]---> BDD-cost:    3
c ---[ 425]---> BDD-cost:    3
c ---[ 424]---> BDD-cost:    3
c ---[ 423]---> BDD-cost:    3
c ---[ 422]---> BDD-cost:    3
c ---[ 421]---> BDD-cost:    3
c ---[ 420]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    3
c ---[ 418]---> BDD-cost:    3
c ---[ 417]---> BDD-cost:    3
c ---[ 416]---> BDD-cost:    3
c ---[ 415]---> BDD-cost:    3
c ---[ 414]---> BDD-cost:    3
c ---[ 413]---> BDD-cost:    3
c ---[ 412]---> BDD-cost:    3
c ---[ 411]---> BDD-cost:    3
c ---[ 410]---> BDD-cost:    3
c ---[ 409]---> BDD-cost:    3
c ---[ 408]---> BDD-cost:    3
c ---[ 407]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:    3
c ---[ 405]---> BDD-cost:    3
c ---[ 404]---> BDD-cost:    3
c ---[ 403]---> BDD-cost:    3
c ---[ 402]---> BDD-cost:    3
c ---[ 401]---> BDD-cost:    3
c ---[ 400]---> BDD-cost:    3
c ---[ 399]---> BDD-cost:    3
c ---[ 398]---> BDD-cost:    3
c ---[ 397]---> BDD-cost:    3
c ---[ 396]---> BDD-cost:    3
c ---[ 395]---> BDD-cost:    3
c ---[ 394]---> BDD-cost:    3
c ---[ 393]---> BDD-cost:    3
c ---[ 392]---> BDD-cost:    3
c ---[ 391]---> BDD-cost:    3
c ---[ 390]---> BDD-cost:    3
c ---[ 389]---> BDD-cost:    3
c ---[ 388]---> BDD-cost:    3
c ---[ 387]---> BDD-cost:    3
c ---[ 386]---> BDD-cost:    3
c ---[ 385]---> BDD-cost:    3
c ---[ 384]---> BDD-cost:    3
c ---[ 383]---> BDD-cost:    3
c ---[ 382]---> BDD-cost:    3
c ---[ 381]---> BDD-cost:    3
c ---[ 380]---> BDD-cost:    3
c ---[ 379]---> BDD-cost:    3
c ---[ 378]---> BDD-cost:    3
c ---[ 377]---> BDD-cost:    3
c ---[ 376]---> BDD-cost:    3
c ---[ 375]---> BDD-cost:    3
c ---[ 374]---> BDD-cost:    3
c ---[ 373]---> BDD-cost:    3
c ---[ 372]---> BDD-cost:    3
c ---[ 371]---> BDD-cost:    3
c ---[ 370]---> BDD-cost:    3
c ---[ 369]---> BDD-cost:    3
c ---[ 368]---> BDD-cost:    3
c ---[ 367]---> BDD-cost:    3
c ---[ 366]---> BDD-cost:    3
c ---[ 365]---> BDD-cost:    3
c ---[ 364]---> BDD-cost:    3
c ---[ 363]---> BDD-cost:    3
c ---[ 362]---> BDD-cost:    3
c ---[ 361]---> BDD-cost:    3
c ---[ 360]---> BDD-cost:    3
c ---[ 359]---> BDD-cost:    3
c ---[ 358]---> BDD-cost:    3
c ---[ 357]---> BDD-cost:    3
c ---[ 356]---> BDD-cost:    3
c ---[ 355]---> BDD-cost:    3
c ---[ 354]---> BDD-cost:    3
c ---[ 353]---> BDD-cost:    3
c ---[ 352]---> BDD-cost:    3
c ---[ 351]---> BDD-cost:    3
c ---[ 350]---> BDD-cost:    3
c ---[ 349]---> BDD-cost:    3
c ---[ 348]---> BDD-cost:    3
c ---[ 347]---> BDD-cost:    3
c ---[ 346]---> BDD-cost:    3
c ---[ 345]---> BDD-cost:    3
c ---[ 344]---> BDD-cost:    3
c ---[ 343]---> BDD-cost:    3
c ---[ 342]---> BDD-cost:    3
c ---[ 341]---> BDD-cost:    3
c ---[ 340]---> BDD-cost:    3
c ---[ 339]---> BDD-cost:    3
c ---[ 338]---> BDD-cost:    3
c ---[ 337]---> BDD-cost:    3
c ---[ 336]---> BDD-cost:    3
c ---[ 335]---> BDD-cost:    3
c ---[ 334]---> BDD-cost:    3
c ---[ 333]---> BDD-cost:    3
c ---[ 332]---> BDD-cost:    3
c ---[ 331]---> BDD-cost:    3
c ---[ 330]---> BDD-cost:    3
c ---[ 329]---> BDD-cost:    3
c ---[ 328]---> BDD-cost:    3
c ---[ 327]---> BDD-cost:    3
c ---[ 326]---> BDD-cost:    3
c ---[ 325]---> BDD-cost:    3
c ---[ 324]---> BDD-cost:    3
c ---[ 323]---> BDD-cost:    3
c ---[ 322]---> BDD-cost:    3
c ---[ 321]---> BDD-cost:    3
c ---[ 320]---> BDD-cost:    3
c ---[ 319]---> BDD-cost:    3
c ---[ 318]---> BDD-cost:    3
c ---[ 317]---> BDD-cost:    3
c ---[ 316]---> BDD-cost:    3
c ---[ 315]---> BDD-cost:    3
c ---[ 314]---> BDD-cost:    3
c ---[ 313]---> BDD-cost:    3
c ---[ 312]---> BDD-cost:    3
c ---[ 311]---> BDD-cost:    3
c ---[ 310]---> BDD-cost:    3
c ---[ 309]---> BDD-cost:    3
c ---[ 308]---> BDD-cost:    3
c ---[ 307]---> BDD-cost:    3
c ---[ 306]---> BDD-cost:    3
c ---[ 305]---> BDD-cost:    3
c ---[ 304]---> BDD-cost:    3
c ---[ 303]---> BDD-cost:    3
c ---[ 302]---> BDD-cost:    3
c ---[ 301]---> BDD-cost:    3
c ---[ 300]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    3
c ---[ 298]---> BDD-cost:    3
c ---[ 297]---> BDD-cost:    3
c ---[ 296]---> BDD-cost:    3
c ---[ 295]---> BDD-cost:    3
c ---[ 294]---> BDD-cost:    3
c ---[ 293]---> BDD-cost:    3
c ---[ 292]---> BDD-cost:    3
c ---[ 291]---> BDD-cost:    3
c ---[ 290]---> BDD-cost:    3
c ---[ 289]---> BDD-cost:    3
c ---[ 288]---> BDD-cost:    3
c ---[ 287]---> BDD-cost:    3
c ---[ 286]---> BDD-cost:    3
c ---[ 285]---> BDD-cost:    3
c ---[ 284]---> BDD-cost:    3
c ---[ 283]---> BDD-cost:    3
c ---[ 282]---> BDD-cost:    3
c ---[ 281]---> BDD-cost:    3
c ---[ 280]---> BDD-cost:    3
c ---[ 279]---> BDD-cost:    3
c ---[ 278]---> BDD-cost:    3
c ---[ 277]---> BDD-cost:    3
c ---[ 276]---> BDD-cost:    3
c ---[ 275]---> BDD-cost:    3
c ---[ 274]---> BDD-cost:    3
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    3
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 268]---> BDD-cost:    3
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 263]---> BDD-cost:    3
c ---[ 262]---> BDD-cost:    3
c ---[ 261]---> BDD-cost:    3
c ---[ 260]---> BDD-cost:    3
c ---[ 259]---> BDD-cost:    3
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:    3
c ---[ 254]---> BDD-cost:    3
c ---[ 253]---> BDD-cost:    3
c ---[ 252]---> BDD-cost:    3
c ---[ 251]---> BDD-cost:    3
c ---[ 250]---> BDD-cost:    3
c ---[ 249]---> BDD-cost:    3
c ---[ 248]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    3
c ---[ 246]---> BDD-cost:    3
c ---[ 245]---> BDD-cost:    3
c ---[ 244]---> BDD-cost:    3
c ---[ 243]---> BDD-cost:    3
c ---[ 242]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    3
c ---[ 240]---> BDD-cost:    3
c ---[ 239]---> BDD-cost:    3
c ---[ 238]---> BDD-cost:    3
c ---[ 237]---> BDD-cost:    3
c ---[ 236]---> BDD-cost:    3
c ---[ 235]---> BDD-cost:    3
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    3
c ---[ 232]---> BDD-cost:    3
c ---[ 231]---> BDD-cost:    3
c ---[ 230]---> BDD-cost:    3
c ---[ 229]---> BDD-cost:    3
c ---[ 228]---> BDD-cost:    3
c ---[ 227]---> BDD-cost:    3
c ---[ 226]---> BDD-cost:    3
c ---[ 225]---> BDD-cost:    3
c ---[ 224]---> BDD-cost:    3
c ---[ 223]---> BDD-cost:    3
c ---[ 222]---> BDD-cost:    3
c ---[ 221]---> BDD-cost:    3
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:    3
c ---[ 218]---> BDD-cost:    3
c ---[ 217]---> BDD-cost:    3
c ---[ 216]---> BDD-cost:    3
c ---[ 215]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:    3
c ---[ 213]---> BDD-cost:    3
c ---[ 212]---> BDD-cost:    3
c ---[ 211]---> BDD-cost:    3
c ---[ 210]---> BDD-cost:    3
c ---[ 209]---> BDD-cost:    3
c ---[ 208]---> BDD-cost:    3
c ---[ 207]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    3
c ---[ 204]---> BDD-cost:    3
c ---[ 203]---> BDD-cost:    3
c ---[ 202]---> BDD-cost:    3
c ---[ 201]---> BDD-cost:    3
c ---[ 200]---> BDD-cost:    3
c ---[ 199]---> BDD-cost:    3
c ---[ 198]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    3
c ---[ 196]---> BDD-cost:    3
c ---[ 195]---> BDD-cost:    3
c ---[ 194]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    3
c ---[ 192]---> BDD-cost:    3
c ---[ 191]---> BDD-cost:    3
c ---[ 190]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:    3
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    3
c ---[ 186]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 184]---> BDD-cost:    3
c ---[ 183]---> BDD-cost:    3
c ---[ 182]---> BDD-cost:    3
c ---[ 181]---> BDD-cost:    3
c ---[ 180]---> BDD-cost:    3
c ---[ 179]---> BDD-cost:    3
c ---[ 178]---> BDD-cost:    3
c ---[ 177]---> BDD-cost:    3
c ---[ 176]---> BDD-cost:    3
c ---[ 175]---> BDD-cost:    3
c ---[ 174]---> BDD-cost:    3
c ---[ 173]---> BDD-cost:    3
c ---[ 172]---> BDD-cost:    3
c ---[ 171]---> BDD-cost:    3
c ---[ 170]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 168]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:    3
c ---[ 157]---> BDD-cost:    3
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    3
c ---[ 145]---> BDD-cost:    3
c ---[ 144]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 131]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 125]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    3
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    3
c ---[ 118]---> BDD-cost:    3
c ---[ 117]---> BDD-cost:    3
c ---[ 116]---> BDD-cost:    3
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:    3
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    3
c ---[ 110]---> BDD-cost:    3
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    3
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:    3
c ---[ 105]---> BDD-cost:    3
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    3
c ---[ 101]---> BDD-cost:    3
c ---[ 100]---> BDD-cost:    3
c ---[  99]---> BDD-cost:    3
c ---[  98]---> BDD-cost:    3
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    3
c ---[  95]---> BDD-cost:    3
c ---[  94]---> BDD-cost:    3
c ---[  93]---> BDD-cost:    3
c ---[  92]---> BDD-cost:    3
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  89]---> BDD-cost:    3
c ---[  88]---> BDD-cost:    3
c ---[  87]---> BDD-cost:    3
c ---[  86]---> BDD-cost:    3
c ---[  85]---> BDD-cost:    3
c ---[  84]---> BDD-cost:    3
c ---[  83]---> BDD-cost:    3
c ---[  82]---> BDD-cost:    3
c ---[  81]---> BDD-cost:    3
c ---[  80]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  77]---> BDD-cost:    3
c ---[  76]---> BDD-cost:    3
c ---[  75]---> BDD-cost:    3
c ---[  74]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  71]---> BDD-cost:    3
c ---[  70]---> BDD-cost:    3
c ---[  69]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  65]---> BDD-cost:    3
c ---[  64]---> BDD-cost:    3
c ---[  63]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  58]---> BDD-cost:    3
c ---[  57]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  53]---> BDD-cost:    3
c ---[  52]---> BDD-cost:    3
c ---[  51]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    3
c ---[  44]---> BDD-cost:    3
c ---[  43]---> BDD-cost:    3
c ---[  42]---> BDD-cost:    3
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:    3
c ---[  39]---> BDD-cost:    3
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    3
c ---[  36]---> BDD-cost:    3
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:    3
c ---[  33]---> BDD-cost:    3
c ---[  32]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    3
c ---[  26]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    3
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:    3
c ---[  12]---> BDD-cost:    3
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:    3
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    3
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    3
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  855124  3043296 |  285041       0        0     nan |  0.000 % |
c |       102 |  855100  3043214 |  313545      99      317     3.2 |  1.497 % |
c |       252 |  854948  3042698 |  344899     229      768     3.4 |  1.519 % |
c |       477 |  854948  3042698 |  379389     454     1640     3.6 |  1.519 % |
c |       814 |  854948  3042698 |  417328     791     6663     8.4 |  1.519 % |
c |      1320 |  854948  3042698 |  459061    1297     8773     6.8 |  1.519 % |
c |      2079 |  854859  3042384 |  504967    2053    13440     6.5 |  1.524 % |
c |      3218 |  854796  3042158 |  555464    3191    18905     5.9 |  1.525 % |
c |      4926 |  854488  3041062 |  611010    4892    28983     5.9 |  1.531 % |
c |      7488 |  854381  3040678 |  672111    7452    68033     9.1 |  1.532 % |
c |     11333 |  854288  3040342 |  739322   11296   169208    15.0 |  1.533 % |
c |     17099 |  854243  3040182 |  813255   17061   338731    19.9 |  1.534 % |
c |     25748 |  854180  3039956 |  894580   25709   583498    22.7 |  1.534 % |
c |     38726 |  854047  3039480 |  984038   38685  1117336    28.9 |  1.536 % |
c |     58188 |  853997  3039300 | 1082442   58146  2044607    35.2 |  1.537 % |
c |     87380 |  853997  3039300 | 1190686   87338  4944346    56.6 |  1.537 % |
c |    131170 |  853940  3039096 | 1309755  131127  6434703    49.1 |  1.537 % |
c |    196854 |  853865  3038826 | 1440731  196810 11033684    56.1 |  1.538 % |
c |    295380 |  853584  3037816 | 1584804  295331 16369076    55.4 |  1.542 % |
#### 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.84 0.94 0.92 2/55 20357
Raw data (stat): 20357 (runsolver) R 20356 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542243465 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.94 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 3989 0 0 0 988 10 0 0 25 0 1 0 542243465 12025856 2368 4294967295 134512640 134672761 3221224624 3221222320 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2936 2368 603 41 0 2895 0
vsize: 11744
[startup+20.0024 s]
Raw data (loadavg): 0.89 0.94 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 14379 0 0 0 1965 33 0 0 25 0 1 0 542243465 46694400 10174 4294967295 134512640 134672761 3221224624 3221223808 134593685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11400 10174 603 41 0 11359 0
vsize: 45600
[startup+30.0023 s]
Raw data (loadavg): 0.90 0.94 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 15087 0 0 0 2963 35 0 0 25 0 1 0 542243465 46755840 10212 4294967295 134512640 134672761 3221224624 3221222896 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11415 10212 603 41 0 11374 0
vsize: 45660
[startup+40.0027 s]
Raw data (loadavg): 0.92 0.94 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 30924 0 0 0 3927 71 0 0 25 0 1 0 542243465 127651840 25992 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31165 25992 603 41 0 31124 0
vsize: 124660
[startup+50.004 s]
Raw data (loadavg): 0.93 0.94 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 31349 0 0 0 4926 73 0 0 25 0 1 0 542243465 129417216 26417 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31596 26417 603 41 0 31555 0
vsize: 126384
[startup+60.004 s]
Raw data (loadavg): 0.94 0.95 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 31867 0 0 0 5924 74 0 0 25 0 1 0 542243465 131653632 26935 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32142 26935 603 41 0 32101 0
vsize: 128568
[startup+70.0046 s]
Raw data (loadavg): 0.95 0.95 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 32461 0 0 0 6922 76 0 0 25 0 1 0 542243465 133943296 27529 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32701 27529 603 41 0 32660 0
vsize: 130804
[startup+80.1077 s]
Raw data (loadavg): 0.96 0.95 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 32997 0 0 0 7930 78 0 0 25 0 1 0 542243465 136220672 28065 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33257 28065 603 41 0 33216 0
vsize: 133028
[startup+90.1079 s]
Raw data (loadavg): 0.96 0.95 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 33560 0 0 0 8929 80 0 0 25 0 1 0 542243465 138506240 28628 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33815 28628 603 41 0 33774 0
vsize: 135260
[startup+100.108 s]
Raw data (loadavg): 0.97 0.95 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 34131 0 0 0 9927 81 0 0 25 0 1 0 542243465 140795904 29199 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34374 29199 603 41 0 34333 0
vsize: 137496
[startup+110.109 s]
Raw data (loadavg): 0.97 0.95 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 34654 0 0 0 10926 83 0 0 25 0 1 0 542243465 142991360 29722 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34910 29722 603 41 0 34869 0
vsize: 139640
[startup+120.109 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 35341 0 0 0 11924 85 0 0 25 0 1 0 542243465 146075648 30409 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35663 30409 603 41 0 35622 0
vsize: 142652
[startup+130.109 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 35880 0 0 0 12921 88 0 0 25 0 1 0 542243465 148213760 30948 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36185 30948 603 41 0 36144 0
vsize: 144740
[startup+140.11 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 36493 0 0 0 13919 90 0 0 25 0 1 0 542243465 150769664 31561 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36809 31561 603 41 0 36768 0
vsize: 147236
[startup+150.11 s]
Raw data (loadavg): 0.98 0.95 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 36939 0 0 0 14918 92 0 0 25 0 1 0 542243465 152518656 32007 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37236 32007 603 41 0 37195 0
vsize: 148944
[startup+160.111 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 37410 0 0 0 15917 93 0 0 25 0 1 0 542243465 154406912 32478 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37697 32478 603 41 0 37656 0
vsize: 150788
[startup+170.112 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 37757 0 0 0 16916 94 0 0 25 0 1 0 542243465 155885568 32825 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38058 32825 603 41 0 38017 0
vsize: 152232
[startup+180.112 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 38172 0 0 0 17914 96 0 0 25 0 1 0 542243465 157499392 33240 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38452 33240 603 41 0 38411 0
vsize: 153808
[startup+190.111 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 38525 0 0 0 18913 97 0 0 25 0 1 0 542243465 158982144 33593 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38814 33593 603 41 0 38773 0
vsize: 155256
[startup+200.112 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 38796 0 0 0 19912 98 0 0 25 0 1 0 542243465 160067584 33864 4294967295 134512640 134672761 3221224624 3221223792 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39079 33864 603 41 0 39038 0
vsize: 156316
[startup+210.112 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 20357
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 39052 0 0 0 20911 99 0 0 25 0 1 0 542243465 161161216 34120 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39346 34120 603 41 0 39305 0
vsize: 157384
[startup+220.113 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 39311 0 0 0 21910 100 0 0 25 0 1 0 542243465 162672640 34379 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39715 34379 603 41 0 39674 0
vsize: 158860
[startup+230.113 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 39537 0 0 0 22910 101 0 0 25 0 1 0 542243465 163614720 34605 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39945 34605 603 41 0 39904 0
vsize: 159780
[startup+240.113 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 39819 0 0 0 23908 102 0 0 25 0 1 0 542243465 164810752 34887 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40237 34887 603 41 0 40196 0
vsize: 160948
[startup+250.113 s]
Raw data (loadavg): 0.99 0.96 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 40144 0 0 0 24907 103 0 0 25 0 1 0 542243465 166019072 35212 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40532 35212 603 41 0 40491 0
vsize: 162128
[startup+260.114 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 40441 0 0 0 25907 104 0 0 25 0 1 0 542243465 167223296 35509 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40826 35509 603 41 0 40785 0
vsize: 163304
[startup+270.114 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 40722 0 0 0 26906 105 0 0 25 0 1 0 542243465 168431616 35790 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41121 35790 603 41 0 41080 0
vsize: 164484
[startup+280.114 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 40950 0 0 0 27905 106 0 0 25 0 1 0 542243465 169377792 36018 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41352 36018 603 41 0 41311 0
vsize: 165408
[startup+290.116 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 41197 0 0 0 28904 107 0 0 25 0 1 0 542243465 170455040 36265 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41615 36265 603 41 0 41574 0
vsize: 166460
[startup+300.116 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 41443 0 0 0 29904 107 0 0 25 0 1 0 542243465 171401216 36511 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41846 36511 603 41 0 41805 0
vsize: 167384
[startup+310.117 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 41658 0 0 0 30903 108 0 0 25 0 1 0 542243465 172355584 36726 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42079 36726 603 41 0 42038 0
vsize: 168316
[startup+320.118 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 41868 0 0 0 31903 109 0 0 25 0 1 0 542243465 173162496 36936 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42276 36936 603 41 0 42235 0
vsize: 169104
[startup+330.118 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 42054 0 0 0 32901 110 0 0 25 0 1 0 542243465 173961216 37122 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42471 37122 603 41 0 42430 0
vsize: 169884
[startup+340.118 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 42226 0 0 0 33901 111 0 0 25 0 1 0 542243465 174628864 37294 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42634 37294 603 41 0 42593 0
vsize: 170536
[startup+350.119 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 42585 0 0 0 34900 112 0 0 25 0 1 0 542243465 176123904 37653 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42999 37653 603 41 0 42958 0
vsize: 171996
[startup+360.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 43053 0 0 0 35898 114 0 0 25 0 1 0 542243465 178003968 38121 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43458 38121 603 41 0 43417 0
vsize: 173832
[startup+370.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 43480 0 0 0 36897 116 0 0 25 0 1 0 542243465 179748864 38548 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43884 38548 603 41 0 43843 0
vsize: 175536
[startup+380.12 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 43869 0 0 0 37895 117 0 0 25 0 1 0 542243465 181370880 38937 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44280 38937 603 41 0 44239 0
vsize: 177120
[startup+390.121 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 44275 0 0 0 38894 118 0 0 25 0 1 0 542243465 183119872 39343 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44707 39343 603 41 0 44666 0
vsize: 178828
[startup+400.121 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 44532 0 0 0 39893 120 0 0 25 0 1 0 542243465 184074240 39600 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44940 39600 603 41 0 44899 0
vsize: 179760
[startup+410.122 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 44811 0 0 0 40892 120 0 0 25 0 1 0 542243465 185282560 39879 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45235 39879 603 41 0 45194 0
vsize: 180940
[startup+420.123 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 45228 0 0 0 41892 121 0 0 25 0 1 0 542243465 186892288 40296 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45628 40296 603 41 0 45587 0
vsize: 182512
[startup+430.122 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 45540 0 0 0 42891 122 0 0 25 0 1 0 542243465 188239872 40608 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45957 40608 603 41 0 45916 0
vsize: 183828
[startup+440.122 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 45892 0 0 0 43890 123 0 0 25 0 1 0 542243465 189714432 40960 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46317 40960 603 41 0 46276 0
vsize: 185268
[startup+450.123 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 46246 0 0 0 44889 124 0 0 25 0 1 0 542243465 191062016 41314 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46646 41314 603 41 0 46605 0
vsize: 186584
[startup+460.123 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 46567 0 0 0 45888 126 0 0 25 0 1 0 542243465 192413696 41635 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46976 41635 603 41 0 46935 0
vsize: 187904
[startup+470.124 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 46885 0 0 0 46887 127 0 0 25 0 1 0 542243465 193765376 41953 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47306 41953 603 41 0 47265 0
vsize: 189224
[startup+480.124 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 47033 0 0 0 47886 128 0 0 25 0 1 0 542243465 194342912 42101 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47447 42101 603 41 0 47406 0
vsize: 189788
[startup+490.125 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 47139 0 0 0 48885 129 0 0 25 0 1 0 542243465 194740224 42207 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47544 42207 603 41 0 47503 0
vsize: 190176
[startup+500.125 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 47260 0 0 0 49885 129 0 0 25 0 1 0 542243465 195284992 42328 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47677 42328 603 41 0 47636 0
vsize: 190708
[startup+510.126 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20359
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 47406 0 0 0 50885 129 0 0 25 0 1 0 542243465 195825664 42474 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47809 42474 603 41 0 47768 0
vsize: 191236
[startup+520.126 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 47554 0 0 0 51884 131 0 0 25 0 1 0 542243465 196493312 42622 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47972 42622 603 41 0 47931 0
vsize: 191888
[startup+530.127 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 47723 0 0 0 52883 131 0 0 25 0 1 0 542243465 197210112 42791 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48147 42791 603 41 0 48106 0
vsize: 192588
[startup+540.127 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 47921 0 0 0 53883 132 0 0 25 0 1 0 542243465 198021120 42989 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48345 42989 603 41 0 48304 0
vsize: 193380
[startup+550.127 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 48123 0 0 0 54882 133 0 0 25 0 1 0 542243465 198832128 43191 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48543 43191 603 41 0 48502 0
vsize: 194172
[startup+560.128 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 48391 0 0 0 55881 134 0 0 25 0 1 0 542243465 199905280 43459 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48805 43459 603 41 0 48764 0
vsize: 195220
[startup+570.129 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 48492 0 0 0 56880 135 0 0 25 0 1 0 542243465 200310784 43560 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48904 43560 603 41 0 48863 0
vsize: 195616
[startup+580.128 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 48601 0 0 0 57880 135 0 0 25 0 1 0 542243465 200712192 43669 4294967295 134512640 134672761 3221224624 3221223808 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49002 43669 603 41 0 48961 0
vsize: 196008
[startup+590.13 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 48759 0 0 0 58879 136 0 0 25 0 1 0 542243465 201437184 43827 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49179 43827 603 41 0 49138 0
vsize: 196716
[startup+600.13 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 49060 0 0 0 59878 137 0 0 25 0 1 0 542243465 202661888 44128 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49478 44128 603 41 0 49437 0
vsize: 197912
[startup+610.13 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 49247 0 0 0 60878 138 0 0 25 0 1 0 542243465 203366400 44315 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49650 44315 603 41 0 49609 0
vsize: 198600
[startup+620.131 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 49421 0 0 0 61877 139 0 0 25 0 1 0 542243465 205213696 44489 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50101 44489 603 41 0 50060 0
vsize: 200404
[startup+630.131 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 49607 0 0 0 62876 140 0 0 25 0 1 0 542243465 205885440 44675 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50265 44675 603 41 0 50224 0
vsize: 201060
[startup+640.132 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 49794 0 0 0 63876 140 0 0 25 0 1 0 542243465 206737408 44862 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50473 44862 603 41 0 50432 0
vsize: 201892
[startup+650.132 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 49991 0 0 0 64875 141 0 0 25 0 1 0 542243465 207400960 45059 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50635 45059 603 41 0 50594 0
vsize: 202540
[startup+660.134 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 50188 0 0 0 65874 142 0 0 25 0 1 0 542243465 208224256 45256 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50836 45256 603 41 0 50795 0
vsize: 203344
[startup+670.134 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 50372 0 0 0 66874 143 0 0 25 0 1 0 542243465 209018880 45440 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51030 45440 603 41 0 50989 0
vsize: 204120
[startup+680.135 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 50570 0 0 0 67873 144 0 0 25 0 1 0 542243465 209821696 45638 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51226 45638 603 41 0 51185 0
vsize: 204904
[startup+690.135 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 50731 0 0 0 68872 145 0 0 25 0 1 0 542243465 210493440 45799 4294967295 134512640 134672761 3221224624 3221223792 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51390 45799 603 41 0 51349 0
vsize: 205560
[startup+700.136 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 50871 0 0 0 69871 146 0 0 25 0 1 0 542243465 211034112 45939 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51522 45939 603 41 0 51481 0
vsize: 206088
[startup+710.137 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 50988 0 0 0 70871 146 0 0 25 0 1 0 542243465 211574784 46056 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51654 46056 603 41 0 51613 0
vsize: 206616
[startup+720.138 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 51263 0 0 0 71869 148 0 0 25 0 1 0 542243465 212668416 46331 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51921 46331 603 41 0 51880 0
vsize: 207684
[startup+730.138 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 51573 0 0 0 72869 148 0 0 25 0 1 0 542243465 213880832 46641 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52217 46641 603 41 0 52176 0
vsize: 208868
[startup+740.138 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 51838 0 0 0 73868 149 0 0 25 0 1 0 542243465 214953984 46906 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52479 46906 603 41 0 52438 0
vsize: 209916
[startup+750.138 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 52121 0 0 0 74867 150 0 0 25 0 1 0 542243465 216182784 47189 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52779 47189 603 41 0 52738 0
vsize: 211116
[startup+760.138 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 52357 0 0 0 75866 152 0 0 25 0 1 0 542243465 217161728 47425 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53018 47425 603 41 0 52977 0
vsize: 212072
[startup+770.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 52636 0 0 0 76866 152 0 0 25 0 1 0 542243465 218238976 47704 4294967295 134512640 134672761 3221224624 3221223808 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53281 47704 603 41 0 53240 0
vsize: 213124
[startup+780.14 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 52942 0 0 0 77865 153 0 0 25 0 1 0 542243465 219594752 48010 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53612 48010 603 41 0 53571 0
vsize: 214448
[startup+790.141 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 53194 0 0 0 78864 154 0 0 25 0 1 0 542243465 220532736 48262 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53841 48262 603 41 0 53800 0
vsize: 215364
[startup+800.142 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 53464 0 0 0 79863 155 0 0 25 0 1 0 542243465 221634560 48532 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54110 48532 603 41 0 54069 0
vsize: 216440
[startup+810.143 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20361
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 53725 0 0 0 80862 156 0 0 25 0 1 0 542243465 222728192 48793 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54377 48793 603 41 0 54336 0
vsize: 217508
[startup+820.143 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 53938 0 0 0 81861 157 0 0 25 0 1 0 542243465 223531008 49006 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54573 49006 603 41 0 54532 0
vsize: 218292
[startup+830.144 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 54239 0 0 0 82861 158 0 0 25 0 1 0 542243465 224763904 49307 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54874 49307 603 41 0 54833 0
vsize: 219496
[startup+840.145 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 54590 0 0 0 83860 159 0 0 25 0 1 0 542243465 226238464 49658 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55234 49658 603 41 0 55193 0
vsize: 220936
[startup+850.145 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 54938 0 0 0 84859 160 0 0 25 0 1 0 542243465 227581952 50006 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55562 50006 603 41 0 55521 0
vsize: 222248
[startup+860.146 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 55129 0 0 0 85859 161 0 0 25 0 1 0 542243465 228450304 50197 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55774 50197 603 41 0 55733 0
vsize: 223096
[startup+870.147 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 55209 0 0 0 86859 161 0 0 25 0 1 0 542243465 228720640 50277 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55840 50277 603 41 0 55799 0
vsize: 223360
[startup+880.146 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 55320 0 0 0 87858 162 0 0 25 0 1 0 542243465 229298176 50388 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55981 50388 603 41 0 55940 0
vsize: 223924
[startup+890.146 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 55421 0 0 0 88857 162 0 0 25 0 1 0 542243465 229568512 50489 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56047 50489 603 41 0 56006 0
vsize: 224188
[startup+900.147 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 55541 0 0 0 89857 162 0 0 25 0 1 0 542243465 230105088 50609 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56178 50609 603 41 0 56137 0
vsize: 224712
[startup+910.148 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 55661 0 0 0 90857 163 0 0 25 0 1 0 542243465 230674432 50729 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56317 50729 603 41 0 56276 0
vsize: 225268
[startup+920.147 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 55786 0 0 0 91856 164 0 0 25 0 1 0 542243465 231079936 50854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56416 50854 603 41 0 56375 0
vsize: 225664
[startup+930.148 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 55913 0 0 0 92856 164 0 0 25 0 1 0 542243465 231616512 50981 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56547 50981 603 41 0 56506 0
vsize: 226188
[startup+940.148 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 56050 0 0 0 93856 165 0 0 25 0 1 0 542243465 232165376 51118 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56681 51118 603 41 0 56640 0
vsize: 226724
[startup+950.148 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 56197 0 0 0 94855 166 0 0 25 0 1 0 542243465 232693760 51265 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56810 51265 603 41 0 56769 0
vsize: 227240
[startup+960.149 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 56344 0 0 0 95854 166 0 0 25 0 1 0 542243465 233357312 51412 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56972 51412 603 41 0 56931 0
vsize: 227888
[startup+970.149 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 56467 0 0 0 96854 167 0 0 25 0 1 0 542243465 233897984 51535 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57104 51535 603 41 0 57063 0
vsize: 228416
[startup+980.149 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 56601 0 0 0 97853 168 0 0 25 0 1 0 542243465 234389504 51669 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57224 51669 603 41 0 57183 0
vsize: 228896
[startup+990.149 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 56748 0 0 0 98852 169 0 0 25 0 1 0 542243465 235065344 51816 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57389 51816 603 41 0 57348 0
vsize: 229556
[startup+1000.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 56906 0 0 0 99852 169 0 0 25 0 1 0 542243465 235700224 51974 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57544 51974 603 41 0 57503 0
vsize: 230176
[startup+1010.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 57058 0 0 0 100851 170 0 0 25 0 1 0 542243465 236363776 52126 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57706 52126 603 41 0 57665 0
vsize: 230824
[startup+1020.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 57201 0 0 0 101851 171 0 0 25 0 1 0 542243465 236896256 52269 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57836 52269 603 41 0 57795 0
vsize: 231344
[startup+1030.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 57352 0 0 0 102850 171 0 0 25 0 1 0 542243465 237432832 52420 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57967 52420 603 41 0 57926 0
vsize: 231868
[startup+1040.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 57509 0 0 0 103849 172 0 0 25 0 1 0 542243465 238104576 52577 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58131 52577 603 41 0 58090 0
vsize: 232524
[startup+1050.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 57657 0 0 0 104849 173 0 0 25 0 1 0 542243465 238792704 52725 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58299 52725 603 41 0 58258 0
vsize: 233196
[startup+1060.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 57802 0 0 0 105848 174 0 0 25 0 1 0 542243465 239333376 52870 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58431 52870 603 41 0 58390 0
vsize: 233724
[startup+1070.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 57941 0 0 0 106847 175 0 0 25 0 1 0 542243465 239874048 53009 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58563 53009 603 41 0 58522 0
vsize: 234252
[startup+1080.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 58066 0 0 0 107847 175 0 0 25 0 1 0 542243465 240381952 53134 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58687 53134 603 41 0 58646 0
vsize: 234748
[startup+1090.16 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 58191 0 0 0 108846 176 0 0 25 0 1 0 542243465 240922624 53259 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58819 53259 603 41 0 58778 0
vsize: 235276
[startup+1100.15 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 58321 0 0 0 109846 177 0 0 25 0 1 0 542243465 241491968 53389 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58958 53389 603 41 0 58917 0
vsize: 235832
[startup+1110.16 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20363
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 58445 0 0 0 110846 177 0 0 25 0 1 0 542243465 242028544 53513 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59089 53513 603 41 0 59048 0
vsize: 236356
[startup+1120.16 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20365
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 58584 0 0 0 111845 178 0 0 25 0 1 0 542243465 242561024 53652 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59219 53652 603 41 0 59178 0
vsize: 236876
[startup+1130.16 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20365
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 58732 0 0 0 112844 179 0 0 25 0 1 0 542243465 243154944 53800 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59364 53800 603 41 0 59323 0
vsize: 237456
[startup+1140.16 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20365
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 58867 0 0 0 113844 179 0 0 25 0 1 0 542243465 243703808 53935 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59498 53935 603 41 0 59457 0
vsize: 237992
[startup+1150.16 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20365
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 58998 0 0 0 114844 180 0 0 25 0 1 0 542243465 244244480 54066 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59630 54066 603 41 0 59589 0
vsize: 238520
[startup+1160.16 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20365
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 59112 0 0 0 115844 180 0 0 25 0 1 0 542243465 244781056 54180 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59761 54180 603 41 0 59720 0
vsize: 239044
[startup+1170.16 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20365
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 59250 0 0 0 116843 181 0 0 25 0 1 0 542243465 245383168 54318 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59908 54318 603 41 0 59867 0
vsize: 239632
[startup+1180.16 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20365
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 59396 0 0 0 117842 182 0 0 25 0 1 0 542243465 245923840 54464 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60040 54464 603 41 0 59999 0
vsize: 240160
[startup+1190.16 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20365
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 59557 0 0 0 118841 183 0 0 25 0 1 0 542243465 246595584 54625 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60204 54625 603 41 0 60163 0
vsize: 240816
[startup+1200.16 s]
Raw data (loadavg): 0.99 0.97 0.92 2/55 20365
Raw data (stat): 20357 (minisat+) R 20356 22929 22928 0 -1 0 59711 0 0 0 119841 183 0 0 25 0 1 0 542243465 247238656 54779 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60361 54779 603 41 0 60320 0
vsize: 241444
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.27 s]
Raw data (loadavg): 0.99 0.97 0.92 1/55 20365
Raw data (stat): 20357 (minisat+) Z 20356 22929 22928 0 -1 12 59713 0 0 0 119841 194 0 0 25 0 1 0 542243465 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.27
CPU time (s): 1200.36
CPU user time (s): 1198.41
CPU system time (s): 1.9437
CPU usage (%): 100.008
Max. virtual memory (Kb): 241444
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####