PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-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	-285037
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.16
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 21978

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        306672 kB
Buffers:         15932 kB
Cached:         687084 kB
SwapCached:        104 kB
Active:          42768 kB
Inactive:       662660 kB
HighTotal:      131008 kB
HighFree:        29316 kB
LowTotal:       903652 kB
LowFree:        277356 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            17012 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:01:49 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 12485 7 1200.29 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): 1.14 1.03 1.01 2/54 4128
Raw data (stat): 4128 (runsolver) R 4127 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549846611 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): 1.12 1.03 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 3989 0 0 0 989 9 0 0 25 0 1 0 549846611 12091392 2368 4294967295 134512640 134672761 3221224624 3221222608 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2952 2368 603 41 0 2911 0
vsize: 11808
[startup+20.001 s]
Raw data (loadavg): 1.10 1.03 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 14138 0 0 0 1965 33 0 0 25 0 1 0 549846611 46153728 9933 4294967295 134512640 134672761 3221224624 3221222496 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11268 9933 603 41 0 11227 0
vsize: 45072
[startup+30.001 s]
Raw data (loadavg): 1.08 1.03 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 15087 0 0 0 2963 35 0 0 25 0 1 0 549846611 46755840 10212 4294967295 134512640 134672761 3221224624 3221222608 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11415 10212 603 41 0 11374 0
vsize: 45660
[startup+40.0019 s]
Raw data (loadavg): 1.07 1.03 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 30834 0 0 0 3926 72 0 0 25 0 1 0 549846611 127242240 25902 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31065 25902 603 41 0 31024 0
vsize: 124260
[startup+50.002 s]
Raw data (loadavg): 1.06 1.03 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 31346 0 0 0 4925 73 0 0 25 0 1 0 549846611 129417216 26414 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31596 26414 603 41 0 31555 0
vsize: 126384
[startup+60.0053 s]
Raw data (loadavg): 1.05 1.02 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 31778 0 0 0 5924 74 0 0 25 0 1 0 549846611 131198976 26846 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32031 26846 603 41 0 31990 0
vsize: 128124
[startup+70.0087 s]
Raw data (loadavg): 1.04 1.02 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 32334 0 0 0 6923 75 0 0 25 0 1 0 549846611 133402624 27402 4294967295 134512640 134672761 3221224624 3221223872 134562294 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32569 27402 603 41 0 32528 0
vsize: 130276
[startup+80.008 s]
Raw data (loadavg): 1.04 1.02 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 32923 0 0 0 7921 77 0 0 25 0 1 0 549846611 135954432 27991 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33192 27991 603 41 0 33151 0
vsize: 132768
[startup+90.008 s]
Raw data (loadavg): 1.03 1.02 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 33414 0 0 0 8920 79 0 0 25 0 1 0 549846611 137969664 28482 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33684 28482 603 41 0 33643 0
vsize: 134736
[startup+100.012 s]
Raw data (loadavg): 1.02 1.02 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 34023 0 0 0 9919 80 0 0 25 0 1 0 549846611 140390400 29091 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34275 29091 603 41 0 34234 0
vsize: 137100
[startup+110.012 s]
Raw data (loadavg): 1.02 1.02 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 34452 0 0 0 10917 82 0 0 25 0 1 0 549846611 142188544 29520 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34714 29520 603 41 0 34673 0
vsize: 138856
[startup+120.012 s]
Raw data (loadavg): 1.02 1.02 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 35150 0 0 0 11915 84 0 0 25 0 1 0 549846611 145272832 30218 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35467 30218 603 41 0 35426 0
vsize: 141868
[startup+130.012 s]
Raw data (loadavg): 1.01 1.02 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 35699 0 0 0 12913 86 0 0 25 0 1 0 549846611 147542016 30767 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36021 30767 603 41 0 35980 0
vsize: 144084
[startup+140.012 s]
Raw data (loadavg): 1.01 1.02 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 36256 0 0 0 13911 88 0 0 25 0 1 0 549846611 149819392 31324 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36577 31324 603 41 0 36536 0
vsize: 146308
[startup+150.012 s]
Raw data (loadavg): 1.01 1.02 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 36855 0 0 0 14909 90 0 0 25 0 1 0 549846611 152248320 31923 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37170 31923 603 41 0 37129 0
vsize: 148680
[startup+160.013 s]
Raw data (loadavg): 1.01 1.02 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 37250 0 0 0 15909 91 0 0 25 0 1 0 549846611 153866240 32318 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37565 32318 603 41 0 37524 0
vsize: 150260
[startup+170.013 s]
Raw data (loadavg): 1.01 1.01 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 37575 0 0 0 16908 92 0 0 25 0 1 0 549846611 155082752 32643 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37862 32643 603 41 0 37821 0
vsize: 151448
[startup+180.013 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 37977 0 0 0 17906 94 0 0 25 0 1 0 549846611 156692480 33045 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38255 33045 603 41 0 38214 0
vsize: 153020
[startup+190.014 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 38367 0 0 0 18905 96 0 0 25 0 1 0 549846611 158306304 33435 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38649 33435 603 41 0 38608 0
vsize: 154596
[startup+200.013 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 38668 0 0 0 19904 96 0 0 25 0 1 0 549846611 159526912 33736 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38947 33736 603 41 0 38906 0
vsize: 155788
[startup+210.013 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 38912 0 0 0 20904 97 0 0 25 0 1 0 549846611 160468992 33980 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39177 33980 603 41 0 39136 0
vsize: 156708
[startup+220.014 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 39165 0 0 0 21904 98 0 0 25 0 1 0 549846611 161583104 34233 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39449 34233 603 41 0 39408 0
vsize: 157796
[startup+230.013 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 39397 0 0 0 22902 99 0 0 25 0 1 0 549846611 163078144 34465 4294967295 134512640 134672761 3221224624 3221223808 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39814 34465 603 41 0 39773 0
vsize: 159256
[startup+240.013 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 39647 0 0 0 23902 100 0 0 25 0 1 0 549846611 164012032 34715 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40042 34715 603 41 0 40001 0
vsize: 160168
[startup+250.013 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 39957 0 0 0 24901 100 0 0 25 0 1 0 549846611 165347328 35025 4294967295 134512640 134672761 3221224624 3221223808 134559356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40368 35025 603 41 0 40327 0
vsize: 161472
[startup+260.013 s]
Raw data (loadavg): 1.00 1.01 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 40268 0 0 0 25900 101 0 0 25 0 1 0 549846611 166555648 35336 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40663 35336 603 41 0 40622 0
vsize: 162652
[startup+270.013 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 40558 0 0 0 26899 103 0 0 25 0 1 0 549846611 167759872 35626 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40957 35626 603 41 0 40916 0
vsize: 163828
[startup+280.013 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 40812 0 0 0 27898 103 0 0 25 0 1 0 549846611 168845312 35880 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41222 35880 603 41 0 41181 0
vsize: 164888
[startup+290.013 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 41039 0 0 0 28898 104 0 0 25 0 1 0 549846611 169779200 36107 4294967295 134512640 134672761 3221224624 3221223728 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41450 36107 603 41 0 41409 0
vsize: 165800
[startup+300.013 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 41289 0 0 0 29897 105 0 0 25 0 1 0 549846611 170860544 36357 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41714 36357 603 41 0 41673 0
vsize: 166856
[startup+310.014 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 41518 0 0 0 30896 106 0 0 25 0 1 0 549846611 171687936 36586 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41916 36586 603 41 0 41875 0
vsize: 167664
[startup+320.014 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 41734 0 0 0 31896 107 0 0 25 0 1 0 549846611 172625920 36802 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42145 36802 603 41 0 42104 0
vsize: 168580
[startup+330.014 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 41932 0 0 0 32896 107 0 0 25 0 1 0 549846611 173428736 37000 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42341 37000 603 41 0 42300 0
vsize: 169364
[startup+340.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 42107 0 0 0 33895 108 0 0 25 0 1 0 549846611 174227456 37175 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42536 37175 603 41 0 42495 0
vsize: 170144
[startup+350.014 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 42278 0 0 0 34895 108 0 0 25 0 1 0 549846611 174895104 37346 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42699 37346 603 41 0 42658 0
vsize: 170796
[startup+360.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 42718 0 0 0 35894 109 0 0 25 0 1 0 549846611 176660480 37786 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43130 37786 603 41 0 43089 0
vsize: 172520
[startup+370.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 43188 0 0 0 36892 111 0 0 25 0 1 0 549846611 178679808 38256 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43623 38256 603 41 0 43582 0
vsize: 174492
[startup+380.014 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 43581 0 0 0 37892 112 0 0 25 0 1 0 549846611 180285440 38649 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44015 38649 603 41 0 43974 0
vsize: 176060
[startup+390.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 43969 0 0 0 38891 113 0 0 25 0 1 0 549846611 181776384 39037 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44379 39037 603 41 0 44338 0
vsize: 177516
[startup+400.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 44371 0 0 0 39890 115 0 0 25 0 1 0 549846611 183525376 39439 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44806 39439 603 41 0 44765 0
vsize: 179224
[startup+410.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 44584 0 0 0 40890 115 0 0 25 0 1 0 549846611 184340480 39652 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45005 39652 603 41 0 44964 0
vsize: 180020
[startup+420.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 44909 0 0 0 41888 116 0 0 25 0 1 0 549846611 185679872 39977 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45332 39977 603 41 0 45291 0
vsize: 181328
[startup+430.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 45297 0 0 0 42887 117 0 0 25 0 1 0 549846611 187158528 40365 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45693 40365 603 41 0 45652 0
vsize: 182772
[startup+440.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 45603 0 0 0 43886 119 0 0 25 0 1 0 549846611 188375040 40671 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45990 40671 603 41 0 45949 0
vsize: 183960
[startup+450.015 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 45963 0 0 0 44885 119 0 0 25 0 1 0 549846611 189984768 41031 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46383 41031 603 41 0 46342 0
vsize: 185532
[startup+460.016 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 46305 0 0 0 45885 121 0 0 25 0 1 0 549846611 191332352 41373 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46712 41373 603 41 0 46671 0
vsize: 186848
[startup+470.016 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 46630 0 0 0 46884 122 0 0 25 0 1 0 549846611 192684032 41698 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47042 41698 603 41 0 47001 0
vsize: 188168
[startup+480.016 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 46921 0 0 0 47883 123 0 0 25 0 1 0 549846611 193900544 41989 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47339 41989 603 41 0 47298 0
vsize: 189356
[startup+490.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 47044 0 0 0 48883 123 0 0 25 0 1 0 549846611 194342912 42112 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47447 42112 603 41 0 47406 0
vsize: 189788
[startup+500.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 47158 0 0 0 49883 123 0 0 25 0 1 0 549846611 194875392 42226 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47577 42226 603 41 0 47536 0
vsize: 190308
[startup+510.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 47273 0 0 0 50883 123 0 0 25 0 1 0 549846611 195284992 42341 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47677 42341 603 41 0 47636 0
vsize: 190708
[startup+520.017 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 47424 0 0 0 51883 124 0 0 25 0 1 0 549846611 195956736 42492 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47841 42492 603 41 0 47800 0
vsize: 191364
[startup+530.018 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 47566 0 0 0 52882 124 0 0 25 0 1 0 549846611 196493312 42634 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47972 42634 603 41 0 47931 0
vsize: 191888
[startup+540.018 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 47744 0 0 0 53882 125 0 0 25 0 1 0 549846611 197345280 42812 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48180 42812 603 41 0 48139 0
vsize: 192720
[startup+550.018 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 47931 0 0 0 54882 125 0 0 25 0 1 0 549846611 198021120 42999 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48345 42999 603 41 0 48304 0
vsize: 193380
[startup+560.019 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 48141 0 0 0 55881 126 0 0 25 0 1 0 549846611 198832128 43209 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48543 43209 603 41 0 48502 0
vsize: 194172
[startup+570.019 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 48412 0 0 0 56880 127 0 0 25 0 1 0 549846611 199905280 43480 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48805 43480 603 41 0 48764 0
vsize: 195220
[startup+580.019 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 48496 0 0 0 57880 128 0 0 25 0 1 0 549846611 200310784 43564 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48904 43564 603 41 0 48863 0
vsize: 195616
[startup+590.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 48605 0 0 0 58880 128 0 0 25 0 1 0 549846611 200712192 43673 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49002 43673 603 41 0 48961 0
vsize: 196008
[startup+600.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 48763 0 0 0 59879 129 0 0 25 0 1 0 549846611 201437184 43831 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49179 43831 603 41 0 49138 0
vsize: 196716
[startup+610.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 49063 0 0 0 60878 130 0 0 25 0 1 0 549846611 202661888 44131 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49478 44131 603 41 0 49437 0
vsize: 197912
[startup+620.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 49247 0 0 0 61878 130 0 0 25 0 1 0 549846611 203366400 44315 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49650 44315 603 41 0 49609 0
vsize: 198600
[startup+630.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 49416 0 0 0 62878 131 0 0 25 0 1 0 549846611 205082624 44484 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50069 44484 603 41 0 50028 0
vsize: 200276
[startup+640.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 49601 0 0 0 63877 132 0 0 25 0 1 0 549846611 205885440 44669 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50265 44669 603 41 0 50224 0
vsize: 201060
[startup+650.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 49785 0 0 0 64877 132 0 0 25 0 1 0 549846611 206589952 44853 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50437 44853 603 41 0 50396 0
vsize: 201748
[startup+660.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 49977 0 0 0 65876 133 0 0 25 0 1 0 549846611 207400960 45045 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50635 45045 603 41 0 50594 0
vsize: 202540
[startup+670.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 50174 0 0 0 66876 134 0 0 25 0 1 0 549846611 208224256 45242 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50836 45242 603 41 0 50795 0
vsize: 203344
[startup+680.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 50356 0 0 0 67875 135 0 0 25 0 1 0 549846611 208887808 45424 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50998 45424 603 41 0 50957 0
vsize: 203992
[startup+690.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 50551 0 0 0 68875 135 0 0 25 0 1 0 549846611 209686528 45619 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51193 45619 603 41 0 51152 0
vsize: 204772
[startup+700.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 50718 0 0 0 69874 136 0 0 25 0 1 0 549846611 210358272 45786 4294967295 134512640 134672761 3221224624 3221223776 134565083 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51357 45786 603 41 0 51316 0
vsize: 205428
[startup+710.022 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 50855 0 0 0 70874 136 0 0 25 0 1 0 549846611 211034112 45923 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51522 45923 603 41 0 51481 0
vsize: 206088
[startup+720.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 50965 0 0 0 71873 137 0 0 25 0 1 0 549846611 211439616 46033 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51621 46033 603 41 0 51580 0
vsize: 206484
[startup+730.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 51216 0 0 0 72873 138 0 0 25 0 1 0 549846611 212533248 46284 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51888 46284 603 41 0 51847 0
vsize: 207552
[startup+740.022 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 51527 0 0 0 73871 139 0 0 25 0 1 0 549846611 213745664 46595 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52184 46595 603 41 0 52143 0
vsize: 208736
[startup+750.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 51795 0 0 0 74871 139 0 0 25 0 1 0 549846611 214818816 46863 4294967295 134512640 134672761 3221224624 3221223808 134558977 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52446 46863 603 41 0 52405 0
vsize: 209784
[startup+760.022 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 52065 0 0 0 75870 140 0 0 25 0 1 0 549846611 215912448 47133 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52713 47133 603 41 0 52672 0
vsize: 210852
[startup+770.022 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 52324 0 0 0 76870 141 0 0 25 0 1 0 549846611 217026560 47392 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52985 47392 603 41 0 52944 0
vsize: 211940
[startup+780.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 52577 0 0 0 77869 142 0 0 25 0 1 0 549846611 218107904 47645 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53249 47645 603 41 0 53208 0
vsize: 212996
[startup+790.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 52878 0 0 0 78869 142 0 0 25 0 1 0 549846611 219324416 47946 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53546 47946 603 41 0 53505 0
vsize: 214184
[startup+800.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 53140 0 0 0 79868 143 0 0 25 0 1 0 549846611 220262400 48208 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53775 48208 603 41 0 53734 0
vsize: 215100
[startup+810.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 53409 0 0 0 80868 144 0 0 25 0 1 0 549846611 221499392 48477 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54077 48477 603 41 0 54036 0
vsize: 216308
[startup+820.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 53668 0 0 0 81867 145 0 0 25 0 1 0 549846611 222457856 48736 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54311 48736 603 41 0 54270 0
vsize: 217244
[startup+830.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 53865 0 0 0 82867 145 0 0 25 0 1 0 549846611 223260672 48933 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54507 48933 603 41 0 54466 0
vsize: 218028
[startup+840.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 54190 0 0 0 83866 146 0 0 25 0 1 0 549846611 224628736 49258 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54841 49258 603 41 0 54800 0
vsize: 219364
[startup+850.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 54483 0 0 0 84866 147 0 0 25 0 1 0 549846611 225837056 49551 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55136 49551 603 41 0 55095 0
vsize: 220544
[startup+860.022 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 54848 0 0 0 85864 148 0 0 25 0 1 0 549846611 227315712 49916 4294967295 134512640 134672761 3221224624 3221223728 134560408 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55497 49916 603 41 0 55456 0
vsize: 221988
[startup+870.022 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 55081 0 0 0 86863 149 0 0 25 0 1 0 549846611 228253696 50149 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55726 50149 603 41 0 55685 0
vsize: 222904
[startup+880.021 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 55183 0 0 0 87863 149 0 0 25 0 1 0 549846611 228585472 50251 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55807 50251 603 41 0 55766 0
vsize: 223228
[startup+890.022 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 55275 0 0 0 88863 150 0 0 25 0 1 0 549846611 228990976 50343 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55906 50343 603 41 0 55865 0
vsize: 223624
[startup+900.022 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 55387 0 0 0 89863 150 0 0 25 0 1 0 549846611 229433344 50455 4294967295 134512640 134672761 3221224624 3221223792 134561133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56014 50455 603 41 0 55973 0
vsize: 224056
[startup+910.022 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 55500 0 0 0 90863 150 0 0 25 0 1 0 549846611 229974016 50568 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56146 50568 603 41 0 56105 0
vsize: 224584
[startup+920.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 55614 0 0 0 91862 151 0 0 25 0 1 0 549846611 230375424 50682 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56244 50682 603 41 0 56203 0
vsize: 224976
[startup+930.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 55741 0 0 0 92862 152 0 0 25 0 1 0 549846611 230948864 50809 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56384 50809 603 41 0 56343 0
vsize: 225536
[startup+940.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 55864 0 0 0 93862 152 0 0 25 0 1 0 549846611 231350272 50932 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56482 50932 603 41 0 56441 0
vsize: 225928
[startup+950.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 55992 0 0 0 94861 153 0 0 25 0 1 0 549846611 231899136 51060 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56616 51060 603 41 0 56575 0
vsize: 226464
[startup+960.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 56134 0 0 0 95861 153 0 0 25 0 1 0 549846611 232562688 51202 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56778 51202 603 41 0 56737 0
vsize: 227112
[startup+970.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 56290 0 0 0 96860 154 0 0 25 0 1 0 549846611 233091072 51358 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56907 51358 603 41 0 56866 0
vsize: 227628
[startup+980.023 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 56409 0 0 0 97860 154 0 0 25 0 1 0 549846611 233627648 51477 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57038 51477 603 41 0 56997 0
vsize: 228152
[startup+990.024 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 56536 0 0 0 98860 154 0 0 25 0 1 0 549846611 234242048 51604 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57188 51604 603 41 0 57147 0
vsize: 228752
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 56685 0 0 0 99860 155 0 0 25 0 1 0 549846611 234795008 51753 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57323 51753 603 41 0 57282 0
vsize: 229292
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 56836 0 0 0 100859 156 0 0 25 0 1 0 549846611 235376640 51904 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57465 51904 603 41 0 57424 0
vsize: 229860
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 56987 0 0 0 101859 156 0 0 25 0 1 0 549846611 236093440 52055 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57640 52055 603 41 0 57599 0
vsize: 230560
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 57135 0 0 0 102859 157 0 0 25 0 1 0 549846611 236630016 52203 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57771 52203 603 41 0 57730 0
vsize: 231084
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 57273 0 0 0 103858 158 0 0 25 0 1 0 549846611 237166592 52341 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57902 52341 603 41 0 57861 0
vsize: 231608
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 57430 0 0 0 104858 158 0 0 25 0 1 0 549846611 237834240 52498 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58065 52498 603 41 0 58024 0
vsize: 232260
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 57577 0 0 0 105858 159 0 0 25 0 1 0 549846611 238387200 52645 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58200 52645 603 41 0 58159 0
vsize: 232800
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 57724 0 0 0 106857 159 0 0 25 0 1 0 549846611 239063040 52792 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58365 52792 603 41 0 58324 0
vsize: 233460
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 57869 0 0 0 107857 159 0 0 25 0 1 0 549846611 239603712 52937 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58497 52937 603 41 0 58456 0
vsize: 233988
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 1.00 2/54 4128
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 57997 0 0 0 108857 160 0 0 25 0 1 0 549846611 240164864 53065 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58634 53065 603 41 0 58593 0
vsize: 234536
[startup+1100.02 s]
Raw data (loadavg): 1.08 1.02 1.01 2/57 4180
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 58117 0 0 0 109852 164 0 0 25 0 1 0 549846611 240652288 53185 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58753 53185 603 41 0 58712 0
vsize: 235012
[startup+1110.03 s]
Raw data (loadavg): 1.07 1.02 1.00 2/54 4181
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 58239 0 0 0 110852 164 0 0 25 0 1 0 549846611 241053696 53307 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58851 53307 603 41 0 58810 0
vsize: 235404
[startup+1120.03 s]
Raw data (loadavg): 1.06 1.01 1.00 2/54 4181
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 58368 0 0 0 111851 165 0 0 25 0 1 0 549846611 241627136 53436 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58991 53436 603 41 0 58950 0
vsize: 235964
[startup+1130.03 s]
Raw data (loadavg): 1.05 1.01 1.00 2/54 4181
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 58493 0 0 0 112851 166 0 0 25 0 1 0 549846611 242159616 53561 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59121 53561 603 41 0 59080 0
vsize: 236484
[startup+1140.03 s]
Raw data (loadavg): 1.04 1.01 1.00 2/54 4181
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 58639 0 0 0 113850 166 0 0 25 0 1 0 549846611 242696192 53707 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59252 53707 603 41 0 59211 0
vsize: 237008
[startup+1150.02 s]
Raw data (loadavg): 1.03 1.01 1.00 2/54 4181
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 58801 0 0 0 114850 167 0 0 25 0 1 0 549846611 243437568 53869 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59433 53869 603 41 0 59392 0
vsize: 237732
[startup+1160.03 s]
Raw data (loadavg): 1.03 1.01 1.00 2/54 4181
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 58910 0 0 0 115849 168 0 0 25 0 1 0 549846611 243974144 53978 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59564 53978 603 41 0 59523 0
vsize: 238256
[startup+1170.03 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 4181
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 59032 0 0 0 116848 169 0 0 25 0 1 0 549846611 244379648 54100 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59663 54100 603 41 0 59622 0
vsize: 238652
[startup+1180.03 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 4183
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 59144 0 0 0 117847 171 0 0 25 0 1 0 549846611 244916224 54212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59794 54212 603 41 0 59753 0
vsize: 239176
[startup+1190.03 s]
Raw data (loadavg): 1.02 1.01 1.00 2/54 4183
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 59296 0 0 0 118847 171 0 0 25 0 1 0 549846611 245518336 54364 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59941 54364 603 41 0 59900 0
vsize: 239764
[startup+1200.03 s]
Raw data (loadavg): 1.01 1.01 1.00 2/54 4183
Raw data (stat): 4128 (minisat+) R 4127 10614 10613 0 -1 0 59437 0 0 0 119847 171 0 0 25 0 1 0 549846611 246059008 54505 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60073 54505 603 41 0 60032 0
vsize: 240292
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.01 1.01 1.00 1/54 4183
Raw data (stat): 4128 (minisat+) Z 4127 10614 10613 0 -1 12 59439 0 0 0 119847 181 0 0 25 0 1 0 549846611 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.13
CPU time (s): 1200.29
CPU user time (s): 1198.47
CPU system time (s): 1.81972
CPU usage (%): 100.014
Max. virtual memory (Kb): 240292
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####