PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-cap6000.opb
MD5SUM	b4da9562dcd40afcc9afd9f695cf339d
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-249830
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.18
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 18312

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc30 THE 2005-04-21 14:23:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18244 boxname=wulflinc30 idbench=1404 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  b4da9562dcd40afcc9afd9f695cf339d  /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-cap6000.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-cap6000.opb
IDLAUNCH: 18244
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        862772 kB
Buffers:         13220 kB
Cached:         131072 kB
SwapCached:          4 kB
Active:          59948 kB
Inactive:        87152 kB
HighTotal:      131008 kB
HighFree:        29512 kB
LowTotal:       903652 kB
LowFree:        833260 kB
SwapTotal:     2097892 kB
SwapFree:      2097820 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6804 kB
Slab:            19124 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:43:11 (client local time) WITH STATUS 0 IN 1200.31 SECONDS
stats: 18244 7 1200.31 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2294 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###########################################################################################################################
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................
c ---[2293]---> Adder-cost: 61016   maxlim: 27161905   bits: 25/25
c ---[2292]---> BDD-cost:    3
c ---[2291]---> BDD-cost:    3
c ---[2290]---> BDD-cost:    3
c ---[2289]---> BDD-cost:    3
c ---[2288]---> BDD-cost:    3
c ---[2287]---> BDD-cost:    3
c ---[2286]---> BDD-cost:    3
c ---[2285]---> BDD-cost:    3
c ---[2284]---> BDD-cost:    3
c ---[2283]---> BDD-cost:    3
c ---[2282]---> BDD-cost:    3
c ---[2281]---> BDD-cost:    3
c ---[2280]---> BDD-cost:    3
c ---[2279]---> BDD-cost:    3
c ---[2278]---> BDD-cost:    3
c ---[2277]---> BDD-cost:    3
c ---[2276]---> BDD-cost:    3
c ---[2275]---> BDD-cost:    3
c ---[2274]---> BDD-cost:    3
c ---[2273]---> BDD-cost:    3
c ---[2272]---> BDD-cost:    3
c ---[2271]---> BDD-cost:    3
c ---[2270]---> BDD-cost:    3
c ---[2269]---> BDD-cost:    3
c ---[2268]---> BDD-cost:    3
c ---[2267]---> BDD-cost:    3
c ---[2266]---> BDD-cost:    3
c ---[2265]---> BDD-cost:    3
c ---[2264]---> BDD-cost:    3
c ---[2263]---> BDD-cost:    3
c ---[2262]---> BDD-cost:    3
c ---[2261]---> BDD-cost:    3
c ---[2260]---> BDD-cost:    3
c ---[2259]---> BDD-cost:    3
c ---[2258]---> BDD-cost:    3
c ---[2257]---> BDD-cost:    3
c ---[2256]---> BDD-cost:    3
c ---[2255]---> BDD-cost:    3
c ---[2254]---> BDD-cost:    3
c ---[2253]---> BDD-cost:    3
c ---[2252]---> BDD-cost:    3
c ---[2251]---> BDD-cost:    3
c ---[2250]---> BDD-cost:    3
c ---[2249]---> BDD-cost:    3
c ---[2248]---> BDD-cost:    3
c ---[2247]---> BDD-cost:    3
c ---[2246]---> BDD-cost:    3
c ---[2245]---> BDD-cost:    3
c ---[2244]---> BDD-cost:    3
c ---[2243]---> BDD-cost:    3
c ---[2242]---> BDD-cost:    3
c ---[2241]---> BDD-cost:    3
c ---[2240]---> BDD-cost:    3
c ---[2239]---> BDD-cost:    3
c ---[2238]---> BDD-cost:    3
c ---[2237]---> BDD-cost:    3
c ---[2236]---> BDD-cost:    3
c ---[2235]---> BDD-cost:    3
c ---[2234]---> BDD-cost:    3
c ---[2233]---> BDD-cost:    3
c ---[2232]---> BDD-cost:    3
c ---[2231]---> BDD-cost:    3
c ---[2230]---> BDD-cost:    3
c ---[2229]---> BDD-cost:    3
c ---[2228]---> BDD-cost:    3
c ---[2227]---> BDD-cost:    3
c ---[2226]---> BDD-cost:    3
c ---[2225]---> BDD-cost:    3
c ---[2224]---> BDD-cost:    3
c ---[2223]---> BDD-cost:    3
c ---[2222]---> BDD-cost:    3
c ---[2221]---> BDD-cost:    3
c ---[2220]---> BDD-cost:    3
c ---[2219]---> BDD-cost:    3
c ---[2218]---> BDD-cost:    3
c ---[2217]---> BDD-cost:    3
c ---[2216]---> BDD-cost:    3
c ---[2215]---> BDD-cost:    3
c ---[2214]---> BDD-cost:    3
c ---[2213]---> BDD-cost:    3
c ---[2212]---> BDD-cost:    3
c ---[2211]---> BDD-cost:    3
c ---[2210]---> BDD-cost:    3
c ---[2209]---> BDD-cost:    3
c ---[2208]---> BDD-cost:    3
c ---[2207]---> BDD-cost:    3
c ---[2206]---> BDD-cost:    3
c ---[2205]---> BDD-cost:    3
c ---[2204]---> BDD-cost:    3
c ---[2203]---> BDD-cost:    3
c ---[2202]---> BDD-cost:    3
c ---[2201]---> BDD-cost:    3
c ---[2200]---> BDD-cost:    3
c ---[2199]---> BDD-cost:    3
c ---[2198]---> BDD-cost:    3
c ---[2197]---> BDD-cost:    3
c ---[2196]---> BDD-cost:    3
c ---[2195]---> BDD-cost:    3
c ---[2194]---> BDD-cost:    3
c ---[2193]---> BDD-cost:    3
c ---[2192]---> BDD-cost:    3
c ---[2191]---> BDD-cost:    3
c ---[2190]---> BDD-cost:    3
c ---[2189]---> BDD-cost:    3
c ---[2188]---> BDD-cost:    3
c ---[2187]---> BDD-cost:    3
c ---[2186]---> BDD-cost:    3
c ---[2185]---> BDD-cost:    3
c ---[2184]---> BDD-cost:    3
c ---[2183]---> BDD-cost:    3
c ---[2182]---> BDD-cost:    3
c ---[2181]---> BDD-cost:    3
c ---[2180]---> BDD-cost:    3
c ---[2179]---> BDD-cost:    3
c ---[2178]---> BDD-cost:    3
c ---[2177]---> BDD-cost:    3
c ---[2176]---> BDD-cost:    3
c ---[2175]---> BDD-cost:    3
c ---[2174]---> BDD-cost:    3
c ---[2173]---> BDD-cost:    3
c ---[2172]---> BDD-cost:    3
c ---[2171]---> BDD-cost:    3
c ---[2170]---> BDD-cost:    3
c ---[2169]---> BDD-cost:    3
c ---[2168]---> BDD-cost:    3
c ---[2167]---> BDD-cost:    3
c ---[2166]---> BDD-cost:    3
c ---[2165]---> BDD-cost:    3
c ---[2164]---> BDD-cost:    3
c ---[2163]---> BDD-cost:    3
c ---[2162]---> BDD-cost:    3
c ---[2161]---> BDD-cost:    3
c ---[2160]---> BDD-cost:    3
c ---[2159]---> BDD-cost:    3
c ---[2158]---> BDD-cost:    3
c ---[2157]---> BDD-cost:    3
c ---[2156]---> BDD-cost:    3
c ---[2155]---> BDD-cost:    3
c ---[2154]---> BDD-cost:    3
c ---[2153]---> BDD-cost:    3
c ---[2152]---> BDD-cost:    3
c ---[2151]---> BDD-cost:    3
c ---[2150]---> BDD-cost:    3
c ---[2149]---> BDD-cost:    3
c ---[2148]---> BDD-cost:    3
c ---[2147]---> BDD-cost:    3
c ---[2146]---> BDD-cost:    3
c ---[2145]---> BDD-cost:    3
c ---[2144]---> BDD-cost:    3
c ---[2143]---> BDD-cost:    3
c ---[2142]---> BDD-cost:    3
c ---[2141]---> BDD-cost:    3
c ---[2140]---> BDD-cost:    3
c ---[2139]---> BDD-cost:    3
c ---[2138]---> BDD-cost:    3
c ---[2137]---> BDD-cost:    3
c ---[2136]---> BDD-cost:    3
c ---[2135]---> BDD-cost:    3
c ---[2134]---> BDD-cost:    3
c ---[2133]---> BDD-cost:    3
c ---[2132]---> BDD-cost:    3
c ---[2131]---> BDD-cost:    3
c ---[2130]---> BDD-cost:    3
c ---[2129]---> BDD-cost:    3
c ---[2128]---> BDD-cost:    3
c ---[2127]---> BDD-cost:    3
c ---[2126]---> BDD-cost:    3
c ---[2125]---> BDD-cost:    3
c ---[2124]---> BDD-cost:    3
c ---[2123]---> BDD-cost:    3
c ---[2122]---> BDD-cost:    3
c ---[2121]---> BDD-cost:    3
c ---[2120]---> BDD-cost:    3
c ---[2119]---> BDD-cost:    3
c ---[2118]---> BDD-cost:    3
c ---[2117]---> BDD-cost:    3
c ---[2116]---> BDD-cost:    3
c ---[2115]---> BDD-cost:    3
c ---[2114]---> BDD-cost:    3
c ---[2113]---> BDD-cost:    3
c ---[2112]---> BDD-cost:    3
c ---[2111]---> BDD-cost:    3
c ---[2110]---> BDD-cost:    3
c ---[2109]---> BDD-cost:    3
c ---[2108]---> BDD-cost:    3
c ---[2107]---> BDD-cost:    3
c ---[2106]---> BDD-cost:    3
c ---[2105]---> BDD-cost:    3
c ---[2104]---> BDD-cost:    3
c ---[2103]---> BDD-cost:    3
c ---[2102]---> BDD-cost:    3
c ---[2101]---> BDD-cost:    3
c ---[2100]---> BDD-cost:    3
c ---[2099]---> BDD-cost:    3
c ---[2098]---> BDD-cost:    3
c ---[2097]---> BDD-cost:    3
c ---[2096]---> BDD-cost:    3
c ---[2095]---> BDD-cost:    3
c ---[2094]---> BDD-cost:    3
c ---[2093]---> BDD-cost:    3
c ---[2092]---> BDD-cost:    3
c ---[2091]---> BDD-cost:    3
c ---[2090]---> BDD-cost:    3
c ---[2089]---> BDD-cost:    3
c ---[2088]---> BDD-cost:    3
c ---[2087]---> BDD-cost:    3
c ---[2086]---> BDD-cost:    3
c ---[2085]---> BDD-cost:    3
c ---[2084]---> BDD-cost:    3
c ---[2083]---> BDD-cost:    3
c ---[2082]---> BDD-cost:    3
c ---[2081]---> BDD-cost:    3
c ---[2080]---> BDD-cost:    3
c ---[2079]---> BDD-cost:    3
c ---[2078]---> BDD-cost:    3
c ---[2077]---> BDD-cost:    3
c ---[2076]---> BDD-cost:    3
c ---[2075]---> BDD-cost:    3
c ---[2074]---> BDD-cost:    3
c ---[2073]---> BDD-cost:    3
c ---[2072]---> BDD-cost:    3
c ---[2071]---> BDD-cost:    3
c ---[2070]---> BDD-cost:    3
c ---[2069]---> BDD-cost:    3
c ---[2068]---> BDD-cost:    3
c ---[2067]---> BDD-cost:    3
c ---[2066]---> BDD-cost:    3
c ---[2065]---> BDD-cost:    3
c ---[2064]---> BDD-cost:    3
c ---[2063]---> BDD-cost:    3
c ---[2062]---> BDD-cost:    3
c ---[2061]---> BDD-cost:    3
c ---[2060]---> BDD-cost:    3
c ---[2059]---> BDD-cost:    3
c ---[2058]---> BDD-cost:    3
c ---[2057]---> BDD-cost:    3
c ---[2056]---> BDD-cost:    3
c ---[2055]---> BDD-cost:    3
c ---[2054]---> BDD-cost:    3
c ---[2053]---> BDD-cost:    3
c ---[2052]---> BDD-cost:    3
c ---[2051]---> BDD-cost:    3
c ---[2050]---> BDD-cost:    3
c ---[2049]---> BDD-cost:    3
c ---[2048]---> BDD-cost:    3
c ---[2047]---> BDD-cost:    3
c ---[2046]---> BDD-cost:    3
c ---[2045]---> BDD-cost:    3
c ---[2044]---> BDD-cost:    3
c ---[2043]---> BDD-cost:    3
c ---[2042]---> BDD-cost:    3
c ---[2041]---> BDD-cost:    3
c ---[2040]---> BDD-cost:    3
c ---[2039]---> BDD-cost:    3
c ---[2038]---> BDD-cost:    3
c ---[2037]---> BDD-cost:    3
c ---[2036]---> BDD-cost:    3
c ---[2035]---> BDD-cost:    3
c ---[2034]---> BDD-cost:    3
c ---[2033]---> BDD-cost:    3
c ---[2032]---> BDD-cost:    3
c ---[2031]---> BDD-cost:    3
c ---[2030]---> BDD-cost:    3
c ---[2029]---> BDD-cost:    3
c ---[2028]---> BDD-cost:    3
c ---[2027]---> BDD-cost:    3
c ---[2026]---> BDD-cost:    3
c ---[2025]---> BDD-cost:    3
c ---[2024]---> BDD-cost:    3
c ---[2023]---> BDD-cost:    3
c ---[2022]---> BDD-cost:    3
c ---[2021]---> BDD-cost:    3
c ---[2020]---> BDD-cost:    3
c ---[2019]---> BDD-cost:    3
c ---[2018]---> BDD-cost:    3
c ---[2017]---> BDD-cost:    3
c ---[2016]---> BDD-cost:    3
c ---[2015]---> BDD-cost:    3
c ---[2014]---> BDD-cost:    3
c ---[2013]---> BDD-cost:    3
c ---[2012]---> BDD-cost:    3
c ---[2011]---> BDD-cost:    3
c ---[2010]---> BDD-cost:    3
c ---[2009]---> BDD-cost:    3
c ---[2008]---> BDD-cost:    3
c ---[2007]---> BDD-cost:    3
c ---[2006]---> BDD-cost:    3
c ---[2004]---> BDD-cost:    3
c ---[2002]---> BDD-cost:    3
c ---[2001]---> BDD-cost:    3
c ---[1999]---> BDD-cost:    3
c ---[1997]---> BDD-cost:    3
c ---[1995]---> BDD-cost:    3
c ---[1993]---> BDD-cost:    3
c ---[1991]---> BDD-cost:    3
c ---[1989]---> BDD-cost:    3
c ---[1987]---> BDD-cost:    3
c ---[1985]---> BDD-cost:    3
c ---[1983]---> BDD-cost:    3
c ---[1981]---> BDD-cost:    3
c ---[1980]---> BDD-cost:    3
c ---[1978]---> BDD-cost:    3
c ---[1976]---> BDD-cost:    3
c ---[1974]---> BDD-cost:    3
c ---[1972]---> BDD-cost:    3
c ---[1970]---> BDD-cost:    3
c ---[1968]---> BDD-cost:    3
c ---[1966]---> BDD-cost:    3
c ---[1964]---> BDD-cost:    3
c ---[1962]---> BDD-cost:    3
c ---[1960]---> BDD-cost:    3
c ---[1959]---> BDD-cost:    3
c ---[1957]---> BDD-cost:    3
c ---[1955]---> BDD-cost:    3
c ---[1953]---> BDD-cost:    3
c ---[1951]---> BDD-cost:    3
c ---[1949]---> BDD-cost:    3
c ---[1947]---> BDD-cost:    3
c ---[1945]---> BDD-cost:    3
c ---[1943]---> BDD-cost:    3
c ---[1941]---> BDD-cost:    3
c ---[1939]---> BDD-cost:    3
c ---[1938]---> BDD-cost:    3
c ---[1936]---> BDD-cost:    3
c ---[1934]---> BDD-cost:    3
c ---[1932]---> BDD-cost:    3
c ---[1930]---> BDD-cost:    3
c ---[1928]---> BDD-cost:    3
c ---[1926]---> BDD-cost:    3
c ---[1924]---> BDD-cost:    3
c ---[1922]---> BDD-cost:    3
c ---[1919]---> BDD-cost:    3
c ---[1918]---> BDD-cost:    3
c ---[1907]---> BDD-cost:    3
c ---[1896]---> BDD-cost:    3
c ---[1885]---> BDD-cost:    3
c ---[1874]---> BDD-cost:    3
c ---[1863]---> BDD-cost:    3
c ---[1852]---> BDD-cost:    3
c ---[1841]---> BDD-cost:    3
c ---[1830]---> BDD-cost:    1
c ---[1829]---> BDD-cost:    3
c ---[1827]---> BDD-cost:    1
c ---[1825]---> BDD-cost:    1
c ---[1823]---> BDD-cost:    1
c ---[1821]---> BDD-cost:    1
c ---[1819]---> BDD-cost:    1
c ---[1817]---> BDD-cost:    1
c ---[1815]---> BDD-cost:    1
c ---[1813]---> BDD-cost:    1
c ---[1811]---> BDD-cost:    1
c ---[1809]---> BDD-cost:    1
c ---[1808]---> BDD-cost:    3
c ---[1806]---> BDD-cost:    1
c ---[1804]---> BDD-cost:    1
c ---[1802]---> BDD-cost:    1
c ---[1800]---> BDD-cost:    1
c ---[1798]---> BDD-cost:    1
c ---[1796]---> BDD-cost:    1
c ---[1794]---> BDD-cost:    1
c ---[1792]---> BDD-cost:    1
c ---[1790]---> BDD-cost:    1
c ---[1788]---> BDD-cost:    1
c ---[1787]---> BDD-cost:    3
c ---[1786]---> BDD-cost:    3
c ---[1784]---> BDD-cost:    1
c ---[1782]---> BDD-cost:    1
c ---[1780]---> BDD-cost:    1
c ---[1778]---> BDD-cost:    1
c ---[1776]---> BDD-cost:    1
c ---[1774]---> BDD-cost:    1
c ---[1772]---> BDD-cost:    1
c ---[1770]---> BDD-cost:    1
c ---[1768]---> BDD-cost:    1
c ---[1766]---> BDD-cost:    1
c ---[1765]---> BDD-cost:    3
c ---[1763]---> BDD-cost:    1
c ---[1761]---> BDD-cost:    1
c ---[1759]---> BDD-cost:    1
c ---[1757]---> BDD-cost:    1
c ---[1755]---> BDD-cost:    1
c ---[1753]---> BDD-cost:    1
c ---[1751]---> BDD-cost:    1
c ---[1749]---> BDD-cost:    1
c ---[1747]---> BDD-cost:    1
c ---[1745]---> BDD-cost:    1
c ---[1744]---> BDD-cost:    3
c ---[1742]---> BDD-cost:    1
c ---[1741]---> BDD-cost:    5
c ---[1740]---> BDD-cost:    5
c ---[1739]---> BDD-cost:    5
c ---[1738]---> BDD-cost:    5
c ---[1737]---> BDD-cost:    5
c ---[1736]---> BDD-cost:    5
c ---[1735]---> BDD-cost:    5
c ---[1734]---> BDD-cost:    5
c ---[1733]---> BDD-cost:    5
c ---[1732]---> BDD-cost:    3
c ---[1731]---> BDD-cost:    5
c ---[1730]---> BDD-cost:    5
c ---[1729]---> BDD-cost:    5
c ---[1728]---> BDD-cost:    5
c ---[1727]---> BDD-cost:    5
c ---[1726]---> BDD-cost:    5
c ---[1725]---> BDD-cost:    5
c ---[1724]---> BDD-cost:    5
c ---[1723]---> BDD-cost:    5
c ---[1722]---> BDD-cost:    5
c ---[1721]---> BDD-cost:    3
c ---[1720]---> BDD-cost:    5
c ---[1719]---> BDD-cost:    5
c ---[1718]---> BDD-cost:    5
c ---[1717]---> BDD-cost:    5
c ---[1716]---> BDD-cost:    5
c ---[1715]---> BDD-cost:    5
c ---[1714]---> BDD-cost:    5
c ---[1713]---> BDD-cost:    5
c ---[1712]---> BDD-cost:    5
c ---[1711]---> BDD-cost:    5
c ---[1710]---> BDD-cost:    3
c ---[1709]---> BDD-cost:    5
c ---[1708]---> BDD-cost:    5
c ---[1707]---> BDD-cost:    5
c ---[1706]---> BDD-cost:    5
c ---[1705]---> BDD-cost:    5
c ---[1704]---> BDD-cost:    5
c ---[1703]---> BDD-cost:    5
c ---[1702]---> BDD-cost:    5
c ---[1700]---> BDD-cost:    5
c ---[1698]---> BDD-cost:    5
c ---[1697]---> BDD-cost:    3
c ---[1695]---> BDD-cost:    5
c ---[1694]---> BDD-cost:    3
c ---[1693]---> BDD-cost:    3
c ---[1692]---> BDD-cost:    3
c ---[1691]---> BDD-cost:    3
c ---[1690]---> BDD-cost:    3
c ---[1689]---> BDD-cost:    3
c ---[1688]---> BDD-cost:    3
c ---[1687]---> BDD-cost:    3
c ---[1686]---> BDD-cost:    3
c ---[1685]---> BDD-cost:    3
c ---[1684]---> BDD-cost:    3
c ---[1683]---> BDD-cost:    3
c ---[1682]---> BDD-cost:    3
c ---[1681]---> BDD-cost:    3
c ---[1680]---> BDD-cost:    3
c ---[1679]---> BDD-cost:    3
c ---[1678]---> BDD-cost:    3
c ---[1677]---> BDD-cost:    3
c ---[1676]---> BDD-cost:    3
c ---[1675]---> BDD-cost:    3
c ---[1674]---> BDD-cost:    3
c ---[1673]---> BDD-cost:    3
c ---[1672]---> BDD-cost:    3
c ---[1671]---> BDD-cost:    3
c ---[1670]---> BDD-cost:    3
c ---[1669]---> BDD-cost:    3
c ---[1668]---> BDD-cost:    3
c ---[1667]---> BDD-cost:    3
c ---[1666]---> BDD-cost:    3
c ---[1665]---> BDD-cost:    3
c ---[1664]---> BDD-cost:    3
c ---[1663]---> BDD-cost:    3
c ---[1662]---> BDD-cost:    3
c ---[1661]---> BDD-cost:    3
c ---[1660]---> BDD-cost:    3
c ---[1659]---> BDD-cost:    3
c ---[1658]---> BDD-cost:    3
c ---[1657]---> BDD-cost:    3
c ---[1656]---> BDD-cost:    3
c ---[1655]---> BDD-cost:    3
c ---[1654]---> BDD-cost:    3
c ---[1653]---> BDD-cost:    3
c ---[1652]---> BDD-cost:    3
c ---[1651]---> BDD-cost:    3
c ---[1650]---> BDD-cost:    3
c ---[1649]---> BDD-cost:    3
c ---[1648]---> BDD-cost:    3
c ---[1647]---> BDD-cost:    3
c ---[1646]---> BDD-cost:    3
c ---[1645]---> BDD-cost:    3
c ---[1644]---> BDD-cost:    3
c ---[1643]---> BDD-cost:    3
c ---[1642]---> BDD-cost:    3
c ---[1641]---> BDD-cost:    3
c ---[1640]---> BDD-cost:    3
c ---[1639]---> BDD-cost:    3
c ---[1638]---> BDD-cost:    3
c ---[1637]---> BDD-cost:    3
c ---[1636]---> BDD-cost:    3
c ---[1635]---> BDD-cost:    3
c ---[1634]---> BDD-cost:    3
c ---[1633]---> BDD-cost:    3
c ---[1632]---> BDD-cost:    3
c ---[1631]---> BDD-cost:    3
c ---[1630]---> BDD-cost:    3
c ---[1629]---> BDD-cost:    3
c ---[1628]---> BDD-cost:    3
c ---[1627]---> BDD-cost:    3
c ---[1626]---> BDD-cost:    3
c ---[1625]---> BDD-cost:    3
c ---[1624]---> BDD-cost:    3
c ---[1623]---> BDD-cost:    3
c ---[1622]---> BDD-cost:    3
c ---[1621]---> BDD-cost:    3
c ---[1620]---> BDD-cost:    3
c ---[1619]---> BDD-cost:    3
c ---[1618]---> BDD-cost:    3
c ---[1617]---> BDD-cost:    3
c ---[1616]---> BDD-cost:    3
c ---[1615]---> BDD-cost:    3
c ---[1614]---> BDD-cost:    3
c ---[1613]---> BDD-cost:    3
c ---[1612]---> BDD-cost:    3
c ---[1611]---> BDD-cost:    3
c ---[1610]---> BDD-cost:    3
c ---[1609]---> BDD-cost:    3
c ---[1608]---> BDD-cost:    3
c ---[1607]---> BDD-cost:    3
c ---[1606]---> BDD-cost:    3
c ---[1605]---> BDD-cost:    3
c ---[1604]---> BDD-cost:    3
c ---[1603]---> BDD-cost:    3
c ---[1602]---> BDD-cost:    3
c ---[1601]---> BDD-cost:    3
c ---[1600]---> BDD-cost:    3
c ---[1599]---> BDD-cost:    3
c ---[1598]---> BDD-cost:    3
c ---[1597]---> BDD-cost:    3
c ---[1596]---> BDD-cost:    3
c ---[1595]---> BDD-cost:    3
c ---[1594]---> BDD-cost:    3
c ---[1593]---> BDD-cost:    3
c ---[1592]---> BDD-cost:    3
c ---[1591]---> BDD-cost:    3
c ---[1590]---> BDD-cost:    3
c ---[1589]---> BDD-cost:    3
c ---[1588]---> BDD-cost:    3
c ---[1587]---> BDD-cost:    3
c ---[1586]---> BDD-cost:    3
c ---[1585]---> BDD-cost:    3
c ---[1584]---> BDD-cost:    3
c ---[1583]---> BDD-cost:    3
c ---[1582]---> BDD-cost:    3
c ---[1581]---> BDD-cost:    3
c ---[1580]---> BDD-cost:    3
c ---[1579]---> BDD-cost:    3
c ---[1578]---> BDD-cost:    3
c ---[1577]---> BDD-cost:    3
c ---[1576]---> BDD-cost:    3
c ---[1575]---> BDD-cost:    3
c ---[1574]---> BDD-cost:    3
c ---[1573]---> BDD-cost:    3
c ---[1572]---> BDD-cost:    3
c ---[1571]---> BDD-cost:    3
c ---[1570]---> BDD-cost:    3
c ---[1569]---> BDD-cost:    3
c ---[1568]---> BDD-cost:    3
c ---[1567]---> BDD-cost:    3
c ---[1566]---> BDD-cost:    3
c ---[1565]---> BDD-cost:    3
c ---[1564]---> BDD-cost:    3
c ---[1563]---> BDD-cost:    3
c ---[1562]---> BDD-cost:    3
c ---[1561]---> BDD-cost:    3
c ---[1560]---> BDD-cost:    3
c ---[1559]---> BDD-cost:    3
c ---[1558]---> BDD-cost:    3
c ---[1557]---> BDD-cost:    3
c ---[1556]---> BDD-cost:    3
c ---[1555]---> BDD-cost:    3
c ---[1554]---> BDD-cost:    3
c ---[1553]---> BDD-cost:    3
c ---[1552]---> BDD-cost:    3
c ---[1551]---> BDD-cost:    3
c ---[1550]---> BDD-cost:    3
c ---[1549]---> BDD-cost:    3
c ---[1548]---> BDD-cost:    3
c ---[1547]---> BDD-cost:    3
c ---[1546]---> BDD-cost:    3
c ---[1545]---> BDD-cost:    3
c ---[1544]---> BDD-cost:    3
c ---[1543]---> BDD-cost:    3
c ---[1542]---> BDD-cost:    3
c ---[1541]---> BDD-cost:    3
c ---[1540]---> BDD-cost:    3
c ---[1539]---> BDD-cost:    3
c ---[1538]---> BDD-cost:    3
c ---[1537]---> BDD-cost:    3
c ---[1536]---> BDD-cost:    3
c ---[1535]---> BDD-cost:    3
c ---[1534]---> BDD-cost:    3
c ---[1533]---> BDD-cost:    3
c ---[1532]---> BDD-cost:    3
c ---[1531]---> BDD-cost:    3
c ---[1530]---> BDD-cost:    3
c ---[1529]---> BDD-cost:    3
c ---[1528]---> BDD-cost:    3
c ---[1527]---> BDD-cost:    3
c ---[1526]---> BDD-cost:    3
c ---[1525]---> BDD-cost:    3
c ---[1524]---> BDD-cost:    3
c ---[1523]---> BDD-cost:    3
c ---[1522]---> BDD-cost:    3
c ---[1521]---> BDD-cost:    3
c ---[1520]---> BDD-cost:    3
c ---[1518]---> BDD-cost:    3
c ---[1517]---> BDD-cost:    3
c ---[1515]---> BDD-cost:    3
c ---[1513]---> BDD-cost:    3
c ---[1511]---> BDD-cost:    3
c ---[1509]---> BDD-cost:    1
c ---[1508]---> BDD-cost:    3
c ---[1507]---> BDD-cost:    3
c ---[1506]---> BDD-cost:    3
c ---[1505]---> BDD-cost:    3
c ---[1504]---> BDD-cost:    3
c ---[1503]---> BDD-cost:    3
c ---[1502]---> BDD-cost:    3
c ---[1501]---> BDD-cost:    3
c ---[1500]---> BDD-cost:    3
c ---[1499]---> BDD-cost:    3
c ---[1498]---> BDD-cost:    3
c ---[1497]---> BDD-cost:    3
c ---[1496]---> BDD-cost:    3
c ---[1495]---> BDD-cost:    3
c ---[1494]---> BDD-cost:    3
c ---[1493]---> BDD-cost:    3
c ---[1492]---> BDD-cost:    3
c ---[1491]---> BDD-cost:    3
c ---[1490]---> BDD-cost:    3
c ---[1489]---> BDD-cost:    3
c ---[1488]---> BDD-cost:    3
c ---[1487]---> BDD-cost:    3
c ---[1486]---> BDD-cost:    3
c ---[1485]---> BDD-cost:    3
c ---[1484]---> BDD-cost:    3
c ---[1483]---> BDD-cost:    3
c ---[1482]---> BDD-cost:    3
c ---[1481]---> BDD-cost:    3
c ---[1480]---> BDD-cost:    3
c ---[1479]---> BDD-cost:    3
c ---[1478]---> BDD-cost:    3
c ---[1477]---> BDD-cost:    3
c ---[1476]---> BDD-cost:    3
c ---[1475]---> BDD-cost:    3
c ---[1474]---> BDD-cost:    3
c ---[1473]---> BDD-cost:    3
c ---[1472]---> BDD-cost:    3
c ---[1471]---> BDD-cost:    3
c ---[1470]---> BDD-cost:    3
c ---[1469]---> BDD-cost:    3
c ---[1468]---> BDD-cost:    3
c ---[1467]---> BDD-cost:    3
c ---[1466]---> BDD-cost:    3
c ---[1465]---> BDD-cost:    3
c ---[1464]---> BDD-cost:    3
c ---[1463]---> BDD-cost:    3
c ---[1462]---> BDD-cost:    3
c ---[1461]---> BDD-cost:    3
c ---[1460]---> BDD-cost:    3
c ---[1459]---> BDD-cost:    3
c ---[1458]---> BDD-cost:    3
c ---[1457]---> BDD-cost:    3
c ---[1456]---> BDD-cost:    3
c ---[1455]---> BDD-cost:    3
c ---[1454]---> BDD-cost:    3
c ---[1453]---> BDD-cost:    3
c ---[1452]---> BDD-cost:    3
c ---[1451]---> BDD-cost:    3
c ---[1450]---> BDD-cost:    3
c ---[1449]---> BDD-cost:    3
c ---[1448]---> BDD-cost:    3
c ---[1447]---> BDD-cost:    3
c ---[1446]---> BDD-cost:    3
c ---[1445]---> BDD-cost:    3
c ---[1444]---> BDD-cost:    3
c ---[1443]---> BDD-cost:    3
c ---[1442]---> BDD-cost:    3
c ---[1441]---> BDD-cost:    3
c ---[1440]---> BDD-cost:    3
c ---[1439]---> BDD-cost:    3
c ---[1438]---> BDD-cost:    3
c ---[1437]---> BDD-cost:    3
c ---[1436]---> BDD-cost:    3
c ---[1435]---> BDD-cost:    3
c ---[1434]---> BDD-cost:    3
c ---[1433]---> BDD-cost:    3
c ---[1432]---> BDD-cost:    3
c ---[1431]---> BDD-cost:    3
c ---[1430]---> BDD-cost:    3
c ---[1429]---> BDD-cost:    3
c ---[1428]---> BDD-cost:    3
c ---[1427]---> BDD-cost:    3
c ---[1426]---> BDD-cost:    3
c ---[1425]---> BDD-cost:    3
c ---[1424]---> BDD-cost:    3
c ---[1423]---> BDD-cost:    3
c ---[1422]---> BDD-cost:    3
c ---[1421]---> BDD-cost:    3
c ---[1420]---> BDD-cost:    3
c ---[1419]---> BDD-cost:    3
c ---[1418]---> BDD-cost:    3
c ---[1417]---> BDD-cost:    3
c ---[1416]---> BDD-cost:    3
c ---[1415]---> BDD-cost:    3
c ---[1414]---> BDD-cost:    3
c ---[1413]---> BDD-cost:    3
c ---[1412]---> BDD-cost:    3
c ---[1411]---> BDD-cost:    3
c ---[1410]---> BDD-cost:    3
c ---[1409]---> BDD-cost:    3
c ---[1408]---> BDD-cost:    3
c ---[1407]---> BDD-cost:    3
c ---[1406]---> BDD-cost:    3
c ---[1405]---> BDD-cost:    3
c ---[1404]---> BDD-cost:    3
c ---[1403]---> BDD-cost:    3
c ---[1402]---> BDD-cost:    3
c ---[1401]---> BDD-cost:    3
c ---[1400]---> BDD-cost:    3
c ---[1399]---> BDD-cost:    3
c ---[1398]---> BDD-cost:    3
c ---[1397]---> BDD-cost:    3
c ---[1396]---> BDD-cost:    3
c ---[1395]---> BDD-cost:    3
c ---[1394]---> BDD-cost:    3
c ---[1393]---> BDD-cost:    3
c ---[1392]---> BDD-cost:    3
c ---[1391]---> BDD-cost:    3
c ---[1390]---> BDD-cost:    3
c ---[1389]---> BDD-cost:    3
c ---[1388]---> BDD-cost:    3
c ---[1387]---> BDD-cost:    3
c ---[1386]---> BDD-cost:    3
c ---[1385]---> BDD-cost:    3
c ---[1384]---> BDD-cost:    3
c ---[1383]---> BDD-cost:    3
c ---[1382]---> BDD-cost:    3
c ---[1381]---> BDD-cost:    3
c ---[1380]---> BDD-cost:    3
c ---[1379]---> BDD-cost:    3
c ---[1378]---> BDD-cost:    3
c ---[1377]---> BDD-cost:    3
c ---[1376]---> BDD-cost:    3
c ---[1375]---> BDD-cost:    3
c ---[1374]---> BDD-cost:    3
c ---[1373]---> BDD-cost:    3
c ---[1372]---> BDD-cost:    3
c ---[1371]---> BDD-cost:    3
c ---[1370]---> BDD-cost:    3
c ---[1369]---> BDD-cost:    3
c ---[1368]---> BDD-cost:    3
c ---[1367]---> BDD-cost:    3
c ---[1366]---> BDD-cost:    3
c ---[1365]---> BDD-cost:    3
c ---[1364]---> BDD-cost:    3
c ---[1363]---> BDD-cost:    3
c ---[1362]---> BDD-cost:    3
c ---[1361]---> BDD-cost:    3
c ---[1360]---> BDD-cost:    3
c ---[1359]---> BDD-cost:    3
c ---[1358]---> BDD-cost:    3
c ---[1357]---> BDD-cost:    3
c ---[1356]---> BDD-cost:    3
c ---[1355]---> BDD-cost:    3
c ---[1354]---> BDD-cost:    3
c ---[1353]---> BDD-cost:    3
c ---[1352]---> BDD-cost:    3
c ---[1351]---> BDD-cost:    3
c ---[1350]---> BDD-cost:    3
c ---[1349]---> BDD-cost:    3
c ---[1348]---> BDD-cost:    3
c ---[1347]---> BDD-cost:    3
c ---[1346]---> BDD-cost:    3
c ---[1345]---> BDD-cost:    3
c ---[1344]---> BDD-cost:    3
c ---[1343]---> BDD-cost:    3
c ---[1342]---> BDD-cost:    3
c ---[1341]---> BDD-cost:    3
c ---[1340]---> BDD-cost:    3
c ---[1339]---> BDD-cost:    3
c ---[1338]---> BDD-cost:    3
c ---[1337]---> BDD-cost:    3
c ---[1336]---> BDD-cost:    3
c ---[1335]---> BDD-cost:    3
c ---[1334]---> BDD-cost:    3
c ---[1333]---> BDD-cost:    3
c ---[1332]---> BDD-cost:    3
c ---[1331]---> BDD-cost:    3
c ---[1330]---> BDD-cost:    3
c ---[1329]---> BDD-cost:    3
c ---[1328]---> BDD-cost:    3
c ---[1327]---> BDD-cost:    3
c ---[1326]---> BDD-cost:    3
c ---[1325]---> BDD-cost:    3
c ---[1324]---> BDD-cost:    3
c ---[1323]---> BDD-cost:    3
c ---[1322]---> BDD-cost:    3
c ---[1321]---> BDD-cost:    3
c ---[1320]---> BDD-cost:    3
c ---[1319]---> BDD-cost:    3
c ---[1318]---> BDD-cost:    3
c ---[1317]---> BDD-cost:    3
c ---[1316]---> BDD-cost:    3
c ---[1315]---> BDD-cost:    3
c ---[1314]---> BDD-cost:    3
c ---[1313]---> BDD-cost:    3
c ---[1312]---> BDD-cost:    3
c ---[1311]---> BDD-cost:    3
c ---[1310]---> BDD-cost:    3
c ---[1309]---> BDD-cost:    3
c ---[1308]---> BDD-cost:    3
c ---[1307]---> BDD-cost:    3
c ---[1306]---> BDD-cost:    3
c ---[1305]---> BDD-cost:    3
c ---[1304]---> BDD-cost:    3
c ---[1303]---> BDD-cost:    3
c ---[1302]---> BDD-cost:    3
c ---[1301]---> BDD-cost:    3
c ---[1300]---> BDD-cost:    3
c ---[1299]---> BDD-cost:    3
c ---[1298]---> BDD-cost:    3
c ---[1297]---> BDD-cost:    3
c ---[1296]---> BDD-cost:    3
c ---[1295]---> BDD-cost:    3
c ---[1294]---> BDD-cost:    3
c ---[1293]---> BDD-cost:    3
c ---[1292]---> BDD-cost:    3
c ---[1291]---> BDD-cost:    3
c ---[1290]---> BDD-cost:    3
c ---[1289]---> BDD-cost:    3
c ---[1288]---> BDD-cost:    3
c ---[1287]---> BDD-cost:    3
c ---[1286]---> BDD-cost:    3
c ---[1285]---> BDD-cost:    3
c ---[1284]---> BDD-cost:    3
c ---[1283]---> BDD-cost:    3
c ---[1282]---> BDD-cost:    3
c ---[1281]---> BDD-cost:    3
c ---[1280]---> BDD-cost:    3
c ---[1279]---> BDD-cost:    3
c ---[1278]---> BDD-cost:    3
c ---[1277]---> BDD-cost:    3
c ---[1276]---> BDD-cost:    3
c ---[1275]---> BDD-cost:    3
c ---[1274]---> BDD-cost:    3
c ---[1273]---> BDD-cost:    3
c ---[1272]---> BDD-cost:    3
c ---[1271]---> BDD-cost:    3
c ---[1270]---> BDD-cost:    3
c ---[1269]---> BDD-cost:    3
c ---[1268]---> BDD-cost:    3
c ---[1267]---> BDD-cost:    3
c ---[1266]---> BDD-cost:    3
c ---[1265]---> BDD-cost:    3
c ---[1264]---> BDD-cost:    3
c ---[1263]---> BDD-cost:    3
c ---[1262]---> BDD-cost:    3
c ---[1261]---> BDD-cost:    3
c ---[1260]---> BDD-cost:    3
c ---[1259]---> BDD-cost:    3
c ---[1258]---> BDD-cost:    3
c ---[1257]---> BDD-cost:    3
c ---[1256]---> BDD-cost:    3
c ---[1255]---> BDD-cost:    3
c ---[1254]---> BDD-cost:    3
c ---[1253]---> BDD-cost:    3
c ---[1252]---> BDD-cost:    3
c ---[1251]---> BDD-cost:    3
c ---[1250]---> BDD-cost:    3
c ---[1249]---> BDD-cost:    3
c ---[1248]---> BDD-cost:    3
c ---[1247]---> BDD-cost:    3
c ---[1246]---> BDD-cost:    3
c ---[1245]---> BDD-cost:    3
c ---[1244]---> BDD-cost:    3
c ---[1243]---> BDD-cost:    3
c ---[1242]---> BDD-cost:    3
c ---[1241]---> BDD-cost:    3
c ---[1240]---> BDD-cost:    3
c ---[1239]---> BDD-cost:    3
c ---[1238]---> BDD-cost:    3
c ---[1237]---> BDD-cost:    3
c ---[1236]---> BDD-cost:    3
c ---[1235]---> BDD-cost:    3
c ---[1234]---> BDD-cost:    3
c ---[1233]---> BDD-cost:    3
c ---[1232]---> BDD-cost:    3
c ---[1231]---> BDD-cost:    3
c ---[1230]---> BDD-cost:    3
c ---[1229]---> BDD-cost:    3
c ---[1228]---> BDD-cost:    3
c ---[1227]---> BDD-cost:    3
c ---[1226]---> BDD-cost:    3
c ---[1225]---> BDD-cost:    3
c ---[1224]---> BDD-cost:    3
c ---[1223]---> BDD-cost:    3
c ---[1222]---> BDD-cost:    3
c ---[1221]---> BDD-cost:    3
c ---[1220]---> BDD-cost:    3
c ---[1219]---> BDD-cost:    3
c ---[1218]---> BDD-cost:    3
c ---[1217]---> BDD-cost:    3
c ---[1216]---> BDD-cost:    3
c ---[1215]---> BDD-cost:    3
c ---[1214]---> BDD-cost:    3
c ---[1213]---> BDD-cost:    3
c ---[1212]---> BDD-cost:    3
c ---[1211]---> BDD-cost:    3
c ---[1210]---> BDD-cost:    3
c ---[1209]---> BDD-cost:    3
c ---[1208]---> BDD-cost:    3
c ---[1207]---> BDD-cost:    3
c ---[1206]---> BDD-cost:    3
c ---[1205]---> BDD-cost:    3
c ---[1204]---> BDD-cost:    3
c ---[1203]---> BDD-cost:    3
c ---[1202]---> BDD-cost:    3
c ---[1201]---> BDD-cost:    3
c ---[1200]---> BDD-cost:    3
c ---[1199]---> BDD-cost:    3
c ---[1198]---> BDD-cost:    3
c ---[1197]---> BDD-cost:    3
c ---[1196]---> BDD-cost:    3
c ---[1195]---> BDD-cost:    3
c ---[1194]---> BDD-cost:    3
c ---[1193]---> BDD-cost:    3
c ---[1192]---> BDD-cost:    3
c ---[1191]---> BDD-cost:    3
c ---[1190]---> BDD-cost:    3
c ---[1189]---> BDD-cost:    3
c ---[1188]---> BDD-cost:    3
c ---[1187]---> BDD-cost:    3
c ---[1186]---> BDD-cost:    3
c ---[1185]---> BDD-cost:    3
c ---[1184]---> BDD-cost:    3
c ---[1183]---> BDD-cost:    3
c ---[1182]---> BDD-cost:    3
c ---[1181]---> BDD-cost:    3
c ---[1180]---> BDD-cost:    3
c ---[1179]---> BDD-cost:    3
c ---[1178]---> BDD-cost:    3
c ---[1177]---> BDD-cost:    3
c ---[1176]---> BDD-cost:    3
c ---[1175]---> BDD-cost:    3
c ---[1174]---> BDD-cost:    3
c ---[1173]---> BDD-cost:    3
c ---[1172]---> BDD-cost:    3
c ---[1171]---> BDD-cost:    3
c ---[1170]---> BDD-cost:    3
c ---[1169]---> BDD-cost:    3
c ---[1168]---> BDD-cost:    3
c ---[1167]---> BDD-cost:    3
c ---[1166]---> BDD-cost:    3
c ---[1165]---> BDD-cost:    3
c ---[1164]---> BDD-cost:    3
c ---[1163]---> BDD-cost:    3
c ---[1162]---> BDD-cost:    3
c ---[1161]---> BDD-cost:    3
c ---[1160]---> BDD-cost:    3
c ---[1159]---> BDD-cost:    3
c ---[1158]---> BDD-cost:    3
c ---[1157]---> BDD-cost:    3
c ---[1156]---> BDD-cost:    3
c ---[1155]---> BDD-cost:    3
c ---[1154]---> BDD-cost:    3
c ---[1153]---> BDD-cost:    3
c ---[1152]---> BDD-cost:    3
c ---[1151]---> BDD-cost:    3
c ---[1150]---> BDD-cost:    3
c ---[1149]---> BDD-cost:    3
c ---[1148]---> BDD-cost:    3
c ---[1147]---> BDD-cost:    3
c ---[1146]---> BDD-cost:    3
c ---[1145]---> BDD-cost:    3
c ---[1144]---> BDD-cost:    3
c ---[1143]---> BDD-cost:    3
c ---[1142]---> BDD-cost:    3
c ---[1141]---> BDD-cost:    3
c ---[1140]---> BDD-cost:    3
c ---[1139]---> BDD-cost:    3
c ---[1138]---> BDD-cost:    3
c ---[1137]---> BDD-cost:    3
c ---[1136]---> BDD-cost:    3
c ---[1135]---> BDD-cost:    3
c ---[1134]---> BDD-cost:    3
c ---[1133]---> BDD-cost:    3
c ---[1132]---> BDD-cost:    3
c ---[1131]---> BDD-cost:    3
c ---[1130]---> BDD-cost:    3
c ---[1129]---> BDD-cost:    3
c ---[1128]---> BDD-cost:    3
c ---[1127]---> BDD-cost:    3
c ---[1126]---> BDD-cost:    3
c ---[1125]---> BDD-cost:    3
c ---[1124]---> BDD-cost:    3
c ---[1123]---> BDD-cost:    3
c ---[1122]---> BDD-cost:    3
c ---[1121]---> BDD-cost:    3
c ---[1120]---> BDD-cost:    3
c ---[1119]---> BDD-cost:    3
c ---[1118]---> BDD-cost:    3
c ---[1117]---> BDD-cost:    3
c ---[1116]---> BDD-cost:    3
c ---[1115]---> BDD-cost:    3
c ---[1114]---> BDD-cost:    3
c ---[1113]---> BDD-cost:    3
c ---[1112]---> BDD-cost:    3
c ---[1111]---> BDD-cost:    3
c ---[1110]---> BDD-cost:    3
c ---[1109]---> BDD-cost:    3
c ---[1108]---> BDD-cost:    3
c ---[1107]---> BDD-cost:    3
c ---[1106]---> BDD-cost:    3
c ---[1105]---> BDD-cost:    3
c ---[1104]---> BDD-cost:    3
c ---[1103]---> BDD-cost:    3
c ---[1102]---> BDD-cost:    3
c ---[1101]---> BDD-cost:    3
c ---[1100]---> BDD-cost:    3
c ---[1099]---> BDD-cost:    3
c ---[1098]---> BDD-cost:    3
c ---[1097]---> BDD-cost:    3
c ---[1096]---> BDD-cost:    3
c ---[1095]---> BDD-cost:    3
c ---[1094]---> BDD-cost:    3
c ---[1093]---> BDD-cost:    3
c ---[1092]---> Adder-cost: 59486   maxlim: 14773890   bits: 24/24
c ---[1091]---> BDD-cost:    3
c ---[1090]---> BDD-cost:    3
c ---[1089]---> BDD-cost:    3
c ---[1088]---> BDD-cost:    3
c ---[1087]---> BDD-cost:    3
c ---[1085]---> BDD-cost:    1
c ---[1083]---> BDD-cost:    1
c ---[1081]---> BDD-cost:    1
c ---[1079]---> BDD-cost:    1
c ---[1077]---> BDD-cost:    1
c ---[1075]---> BDD-cost:    1
c ---[1073]---> BDD-cost:    1
c ---[1072]---> BDD-cost:    3
c ---[1070]---> BDD-cost:    1
c ---[1068]---> BDD-cost:    1
c ---[1066]---> BDD-cost:    1
c ---[1064]---> BDD-cost:    1
c ---[1062]---> BDD-cost:    1
c ---[1060]---> BDD-cost:    1
c ---[1058]---> BDD-cost:    1
c ---[1056]---> BDD-cost:    1
c ---[1054]---> BDD-cost:    1
c ---[1052]---> BDD-cost:    1
c ---[1051]---> BDD-cost:    3
c ---[1049]---> BDD-cost:    1
c ---[1047]---> BDD-cost:    1
c ---[1045]---> BDD-cost:    1
c ---[1037]---> BDD-cost:    3
c ---[1026]---> BDD-cost:    3
c ---[1015]---> BDD-cost:    3
c ---[1004]---> BDD-cost:    3
c ---[ 993]---> BDD-cost:    3
c ---[ 982]---> BDD-cost:    3
c ---[ 971]---> BDD-cost:    3
c ---[ 960]---> BDD-cost:    3
c ---[ 959]---> BDD-cost:    3
c ---[ 948]---> BDD-cost:    3
c ---[ 937]---> BDD-cost:    3
c ---[ 926]---> BDD-cost:    3
c ---[ 915]---> BDD-cost:    3
c ---[ 904]---> BDD-cost:    3
c ---[ 902]---> BDD-cost:    1
c ---[ 900]---> BDD-cost:    1
c ---[ 898]---> BDD-cost:    1
c ---[ 896]---> BDD-cost:    1
c ---[ 894]---> BDD-cost:    1
c ---[ 892]---> BDD-cost:    1
c ---[ 890]---> BDD-cost:    1
c ---[ 888]---> BDD-cost:    1
c ---[ 886]---> BDD-cost:    1
c ---[ 884]---> BDD-cost:    1
c ---[ 883]---> BDD-cost:    3
c ---[ 881]---> BDD-cost:    1
c ---[ 879]---> BDD-cost:    1
c ---[ 877]---> BDD-cost:    1
c ---[ 869]---> BDD-cost:    3
c ---[ 861]---> BDD-cost:    3
c ---[ 860]---> BDD-cost:    3
c ---[ 859]---> BDD-cost:    3
c ---[ 858]---> BDD-cost:    3
c ---[ 857]---> BDD-cost:    3
c ---[ 856]---> BDD-cost:    3
c ---[ 855]---> BDD-cost:    3
c ---[ 854]---> BDD-cost:    3
c ---[ 853]---> BDD-cost:    3
c ---[ 852]---> BDD-cost:    3
c ---[ 851]---> BDD-cost:    3
c ---[ 850]---> BDD-cost:    3
c ---[ 849]---> BDD-cost:    3
c ---[ 848]---> BDD-cost:    3
c ---[ 847]---> BDD-cost:    3
c ---[ 846]---> BDD-cost:    3
c ---[ 845]---> BDD-cost:    3
c ---[ 844]---> BDD-cost:    3
c ---[ 843]---> BDD-cost:    3
c ---[ 842]---> BDD-cost:    3
c ---[ 841]---> BDD-cost:    3
c ---[ 840]---> BDD-cost:    3
c ---[ 839]---> BDD-cost:    3
c ---[ 838]---> BDD-cost:    3
c ---[ 837]---> BDD-cost:    3
c ---[ 836]---> BDD-cost:    3
c ---[ 835]---> BDD-cost:    3
c ---[ 834]---> BDD-cost:    3
c ---[ 833]---> BDD-cost:    3
c ---[ 832]---> BDD-cost:    3
c ---[ 831]---> BDD-cost:    3
c ---[ 830]---> BDD-cost:    3
c ---[ 829]---> BDD-cost:    3
c ---[ 828]---> BDD-cost:    3
c ---[ 827]---> BDD-cost:    3
c ---[ 826]---> BDD-cost:    3
c ---[ 825]---> BDD-cost:    3
c ---[ 824]---> BDD-cost:    3
c ---[ 823]---> BDD-cost:    3
c ---[ 822]---> BDD-cost:    3
c ---[ 821]---> BDD-cost:    3
c ---[ 820]---> BDD-cost:    3
c ---[ 819]---> BDD-cost:    3
c ---[ 818]---> BDD-cost:    3
c ---[ 817]---> BDD-cost:    3
c ---[ 816]---> BDD-cost:    3
c ---[ 815]---> BDD-cost:    3
c ---[ 814]---> BDD-cost:    3
c ---[ 813]---> BDD-cost:    3
c ---[ 812]---> BDD-cost:    3
c ---[ 811]---> BDD-cost:    3
c ---[ 810]---> BDD-cost:    3
c ---[ 809]---> BDD-cost:    3
c ---[ 808]---> BDD-cost:    3
c ---[ 807]---> BDD-cost:    3
c ---[ 806]---> BDD-cost:    3
c ---[ 805]---> BDD-cost:    3
c ---[ 804]---> BDD-cost:    3
c ---[ 803]---> BDD-cost:    3
c ---[ 802]---> BDD-cost:    3
c ---[ 801]---> BDD-cost:    3
c ---[ 800]---> BDD-cost:    3
c ---[ 799]---> BDD-cost:    3
c ---[ 798]---> BDD-cost:    3
c ---[ 797]---> BDD-cost:    3
c ---[ 796]---> BDD-cost:    3
c ---[ 795]---> BDD-cost:    3
c ---[ 794]---> BDD-cost:    3
c ---[ 793]---> BDD-cost:    3
c ---[ 792]---> BDD-cost:    3
c ---[ 791]---> BDD-cost:    3
c ---[ 790]---> BDD-cost:    3
c ---[ 789]---> BDD-cost:    3
c ---[ 788]---> BDD-cost:    3
c ---[ 787]---> BDD-cost:    3
c ---[ 786]---> BDD-cost:    3
c ---[ 785]---> BDD-cost:    3
c ---[ 784]---> BDD-cost:    3
c ---[ 783]---> BDD-cost:    3
c ---[ 782]---> BDD-cost:    3
c ---[ 781]---> BDD-cost:    3
c ---[ 780]---> BDD-cost:    3
c ---[ 779]---> BDD-cost:    3
c ---[ 778]---> BDD-cost:    3
c ---[ 777]---> BDD-cost:    3
c ---[ 776]---> BDD-cost:    3
c ---[ 775]---> BDD-cost:    3
c ---[ 774]---> BDD-cost:    3
c ---[ 773]---> BDD-cost:    3
c ---[ 772]---> BDD-cost:    3
c ---[ 771]---> BDD-cost:    3
c ---[ 770]---> BDD-cost:    3
c ---[ 769]---> BDD-cost:    3
c ---[ 768]---> BDD-cost:    3
c ---[ 767]---> BDD-cost:    3
c ---[ 766]---> BDD-cost:    3
c ---[ 765]---> BDD-cost:    3
c ---[ 764]---> BDD-cost:    3
c ---[ 763]---> BDD-cost:    3
c ---[ 762]---> BDD-cost:    3
c ---[ 761]---> BDD-cost:    3
c ---[ 760]---> BDD-cost:    3
c ---[ 759]---> BDD-cost:    3
c ---[ 758]---> BDD-cost:    3
c ---[ 757]---> BDD-cost:    3
c ---[ 756]---> BDD-cost:    3
c ---[ 755]---> BDD-cost:    3
c ---[ 754]---> BDD-cost:    3
c ---[ 753]---> BDD-cost:    3
c ---[ 752]---> BDD-cost:    3
c ---[ 751]---> BDD-cost:    3
c ---[ 750]---> BDD-cost:    3
c ---[ 749]---> BDD-cost:    3
c ---[ 748]---> BDD-cost:    3
c ---[ 747]---> BDD-cost:    3
c ---[ 746]---> BDD-cost:    3
c ---[ 745]---> BDD-cost:    3
c ---[ 744]---> BDD-cost:    3
c ---[ 743]---> BDD-cost:    3
c ---[ 742]---> BDD-cost:    3
c ---[ 741]---> BDD-cost:    3
c ---[ 740]---> BDD-cost:    3
c ---[ 739]---> BDD-cost:    3
c ---[ 738]---> BDD-cost:    3
c ---[ 737]---> BDD-cost:    3
c ---[ 736]---> BDD-cost:    3
c ---[ 735]---> BDD-cost:    3
c ---[ 734]---> BDD-cost:    3
c ---[ 733]---> BDD-cost:    3
c ---[ 732]---> BDD-cost:    3
c ---[ 731]---> BDD-cost:    3
c ---[ 730]---> BDD-cost:    3
c ---[ 729]---> BDD-cost:    3
c ---[ 728]---> BDD-cost:    3
c ---[ 727]---> BDD-cost:    3
c ---[ 726]---> BDD-cost:    3
c ---[ 725]---> BDD-cost:    3
c ---[ 724]---> BDD-cost:    3
c ---[ 723]---> BDD-cost:    3
c ---[ 722]---> BDD-cost:    3
c ---[ 721]---> BDD-cost:    3
c ---[ 720]---> BDD-cost:    3
c ---[ 719]---> BDD-cost:    3
c ---[ 718]---> BDD-cost:    3
c ---[ 717]---> BDD-cost:    3
c ---[ 716]---> BDD-cost:    3
c ---[ 715]---> BDD-cost:    3
c ---[ 714]---> BDD-cost:    3
c ---[ 713]---> BDD-cost:    3
c ---[ 712]---> BDD-cost:    3
c ---[ 711]---> BDD-cost:    3
c ---[ 710]---> BDD-cost:    3
c ---[ 709]---> BDD-cost:    3
c ---[ 708]---> BDD-cost:    3
c ---[ 707]---> BDD-cost:    3
c ---[ 706]---> BDD-cost:    3
c ---[ 705]---> BDD-cost:    3
c ---[ 704]---> BDD-cost:    3
c ---[ 703]---> BDD-cost:    3
c ---[ 702]---> BDD-cost:    3
c ---[ 701]---> BDD-cost:    3
c ---[ 700]---> BDD-cost:    3
c ---[ 699]---> BDD-cost:    3
c ---[ 698]---> BDD-cost:    3
c ---[ 697]---> BDD-cost:    3
c ---[ 696]---> BDD-cost:    3
c ---[ 695]---> BDD-cost:    3
c ---[ 694]---> BDD-cost:    3
c ---[ 693]---> BDD-cost:    3
c ---[ 692]---> BDD-cost:    3
c ---[ 691]---> BDD-cost:    3
c ---[ 690]---> BDD-cost:    3
c ---[ 689]---> BDD-cost:    3
c ---[ 688]---> BDD-cost:    3
c ---[ 687]---> BDD-cost:    3
c ---[ 686]---> BDD-cost:    3
c ---[ 685]---> BDD-cost:    3
c ---[ 684]---> BDD-cost:    3
c ---[ 683]---> BDD-cost:    3
c ---[ 682]---> BDD-cost:    3
c ---[ 681]---> BDD-cost:    3
c ---[ 680]---> BDD-cost:    3
c ---[ 679]---> BDD-cost:    3
c ---[ 678]---> BDD-cost:    3
c ---[ 677]---> BDD-cost:    3
c ---[ 676]---> BDD-cost:    3
c ---[ 675]---> BDD-cost:    3
c ---[ 674]---> BDD-cost:    3
c ---[ 673]---> BDD-cost:    3
c ---[ 672]---> BDD-cost:    3
c ---[ 671]---> BDD-cost:    3
c ---[ 670]---> BDD-cost:    3
c ---[ 669]---> BDD-cost:    3
c ---[ 668]---> BDD-cost:    3
c ---[ 667]---> BDD-cost:    3
c ---[ 666]---> BDD-cost:    3
c ---[ 665]---> BDD-cost:    3
c ---[ 664]---> BDD-cost:    3
c ---[ 663]---> BDD-cost:    3
c ---[ 662]---> BDD-cost:    3
c ---[ 661]---> BDD-cost:    3
c ---[ 660]---> BDD-cost:    3
c ---[ 659]---> BDD-cost:    3
c ---[ 658]---> BDD-cost:    3
c ---[ 657]---> BDD-cost:    3
c ---[ 656]---> BDD-cost:    3
c ---[ 655]---> BDD-cost:    3
c ---[ 654]---> BDD-cost:    3
c ---[ 653]---> BDD-cost:    3
c ---[ 652]---> BDD-cost:    3
c ---[ 651]---> BDD-cost:    3
c ---[ 650]---> BDD-cost:    3
c ---[ 649]---> BDD-cost:    3
c ---[ 648]---> BDD-cost:    3
c ---[ 647]---> BDD-cost:    3
c ---[ 646]---> BDD-cost:    3
c ---[ 645]---> BDD-cost:    3
c ---[ 644]---> BDD-cost:    3
c ---[ 643]---> BDD-cost:    3
c ---[ 642]---> BDD-cost:    3
c ---[ 641]---> BDD-cost:    3
c ---[ 640]---> BDD-cost:    3
c ---[ 639]---> BDD-cost:    3
c ---[ 638]---> BDD-cost:    3
c ---[ 637]---> BDD-cost:    3
c ---[ 636]---> BDD-cost:    3
c ---[ 635]---> BDD-cost:    3
c ---[ 634]---> BDD-cost:    3
c ---[ 633]---> BDD-cost:    3
c ---[ 632]---> BDD-cost:    3
c ---[ 631]---> BDD-cost:    3
c ---[ 630]---> BDD-cost:    3
c ---[ 629]---> BDD-cost:    3
c ---[ 628]---> BDD-cost:    3
c ---[ 627]---> BDD-cost:    3
c ---[ 626]---> BDD-cost:    3
c ---[ 625]---> BDD-cost:    3
c ---[ 624]---> BDD-cost:    3
c ---[ 623]---> BDD-cost:    3
c ---[ 622]---> BDD-cost:    3
c ---[ 621]---> BDD-cost:    3
c ---[ 620]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    3
c ---[ 618]---> BDD-cost:    3
c ---[ 617]---> BDD-cost:    3
c ---[ 616]---> BDD-cost:    3
c ---[ 615]---> BDD-cost:    3
c ---[ 614]---> BDD-cost:    3
c ---[ 613]---> BDD-cost:    3
c ---[ 612]---> BDD-cost:    3
c ---[ 611]---> BDD-cost:    3
c ---[ 610]---> BDD-cost:    3
c ---[ 609]---> BDD-cost:    3
c ---[ 608]---> BDD-cost:    3
c ---[ 607]---> BDD-cost:    3
c ---[ 606]---> BDD-cost:    3
c ---[ 605]---> BDD-cost:    3
c ---[ 604]---> BDD-cost:    3
c ---[ 603]---> BDD-cost:    3
c ---[ 602]---> BDD-cost:    3
c ---[ 601]---> BDD-cost:    3
c ---[ 600]---> BDD-cost:    3
c ---[ 599]---> BDD-cost:    3
c ---[ 598]---> BDD-cost:    3
c ---[ 597]---> BDD-cost:    3
c ---[ 596]---> BDD-cost:    3
c ---[ 595]---> BDD-cost:    3
c ---[ 594]---> BDD-cost:    3
c ---[ 593]---> BDD-cost:    3
c ---[ 592]---> BDD-cost:    3
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:    3
c ---[ 589]---> BDD-cost:    3
c ---[ 588]---> BDD-cost:    3
c ---[ 587]---> BDD-cost:    3
c ---[ 586]---> BDD-cost:    3
c ---[ 585]---> BDD-cost:    3
c ---[ 584]---> BDD-cost:    3
c ---[ 583]---> BDD-cost:    3
c ---[ 582]---> BDD-cost:    3
c ---[ 581]---> BDD-cost:    3
c ---[ 580]---> BDD-cost:    3
c ---[ 579]---> BDD-cost:    3
c ---[ 578]---> BDD-cost:    3
c ---[ 577]---> BDD-cost:    3
c ---[ 576]---> BDD-cost:    3
c ---[ 575]---> BDD-cost:    3
c ---[ 574]---> BDD-cost:    3
c ---[ 573]---> BDD-cost:    3
c ---[ 572]---> BDD-cost:    3
c ---[ 571]---> BDD-cost:    3
c ---[ 570]---> BDD-cost:    3
c ---[ 569]---> BDD-cost:    3
c ---[ 568]---> BDD-cost:    3
c ---[ 567]---> BDD-cost:    3
c ---[ 566]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    3
c ---[ 564]---> BDD-cost:    3
c ---[ 563]---> BDD-cost:    3
c ---[ 562]---> BDD-cost:    3
c ---[ 561]---> BDD-cost:    3
c ---[ 560]---> BDD-cost:    3
c ---[ 559]---> BDD-cost:    3
c ---[ 558]---> BDD-cost:    3
c ---[ 557]---> BDD-cost:    3
c ---[ 556]---> BDD-cost:    3
c ---[ 555]---> BDD-cost:    3
c ---[ 554]---> BDD-cost:    3
c ---[ 553]---> BDD-cost:    3
c ---[ 552]---> BDD-cost:    3
c ---[ 551]---> BDD-cost:    3
c ---[ 550]---> BDD-cost:    3
c ---[ 549]---> BDD-cost:    3
c ---[ 548]---> BDD-cost:    3
c ---[ 547]---> BDD-cost:    3
c ---[ 546]---> BDD-cost:    3
c ---[ 545]---> BDD-cost:    3
c ---[ 544]---> BDD-cost:    3
c ---[ 543]---> BDD-cost:    3
c ---[ 542]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    3
c ---[ 540]---> BDD-cost:    3
c ---[ 539]---> BDD-cost:    3
c ---[ 538]---> BDD-cost:    3
c ---[ 537]---> BDD-cost:    3
c ---[ 536]---> BDD-cost:    3
c ---[ 535]---> BDD-cost:    3
c ---[ 534]---> BDD-cost:    3
c ---[ 533]---> BDD-cost:    3
c ---[ 532]---> BDD-cost:    3
c ---[ 531]---> BDD-cost:    3
c ---[ 530]---> BDD-cost:    3
c ---[ 529]---> BDD-cost:    3
c ---[ 528]---> BDD-cost:    3
c ---[ 527]---> BDD-cost:    3
c ---[ 526]---> BDD-cost:    3
c ---[ 525]---> BDD-cost:    3
c ---[ 524]---> BDD-cost:    3
c ---[ 523]---> BDD-cost:    3
c ---[ 522]---> BDD-cost:    3
c ---[ 521]---> BDD-cost:    3
c ---[ 520]---> BDD-cost:    3
c ---[ 519]---> BDD-cost:    3
c ---[ 518]---> BDD-cost:    3
c ---[ 517]---> BDD-cost:    3
c ---[ 516]---> BDD-cost:    3
c ---[ 515]---> BDD-cost:    3
c ---[ 514]---> BDD-cost:    3
c ---[ 513]---> BDD-cost:    3
c ---[ 512]---> BDD-cost:    3
c ---[ 511]---> BDD-cost:    3
c ---[ 510]---> BDD-cost:    3
c ---[ 509]---> BDD-cost:    3
c ---[ 508]---> BDD-cost:    3
c ---[ 507]---> BDD-cost:    3
c ---[ 506]---> BDD-cost:    3
c ---[ 505]---> BDD-cost:    3
c ---[ 504]---> BDD-cost:    3
c ---[ 503]---> BDD-cost:    3
c ---[ 502]---> BDD-cost:    3
c ---[ 501]---> BDD-cost:    3
c ---[ 500]---> BDD-cost:    3
c ---[ 499]---> BDD-cost:    3
c ---[ 498]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:    3
c ---[ 496]---> BDD-cost:    3
c ---[ 495]---> BDD-cost:    3
c ---[ 494]---> BDD-cost:    3
c ---[ 493]---> BDD-cost:    3
c ---[ 492]---> BDD-cost:    3
c ---[ 491]---> BDD-cost:    3
c ---[ 490]---> BDD-cost:    3
c ---[ 489]---> BDD-cost:    3
c ---[ 488]---> BDD-cost:    3
c ---[ 487]---> BDD-cost:    3
c ---[ 486]---> BDD-cost:    3
c ---[ 485]---> BDD-cost:    3
c ---[ 484]---> BDD-cost:    3
c ---[ 483]---> BDD-cost:    3
c ---[ 482]---> BDD-cost:    3
c ---[ 481]---> BDD-cost:    3
c ---[ 480]---> BDD-cost:    3
c ---[ 479]---> BDD-cost:    3
c ---[ 478]---> BDD-cost:    3
c ---[ 477]---> BDD-cost:    3
c ---[ 476]---> BDD-cost:    3
c ---[ 475]---> BDD-cost:    3
c ---[ 474]---> BDD-cost:    3
c ---[ 473]---> BDD-cost:    3
c ---[ 472]---> BDD-cost:    3
c ---[ 471]---> BDD-cost:    3
c ---[ 470]---> BDD-cost:    3
c ---[ 469]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:    3
c ---[ 467]---> BDD-cost:    3
c ---[ 466]---> BDD-cost:    3
c ---[ 465]---> BDD-cost:    3
c ---[ 464]---> BDD-cost:    3
c ---[ 463]---> BDD-cost:    3
c ---[ 462]---> BDD-cost:    3
c ---[ 461]---> BDD-cost:    3
c ---[ 460]---> BDD-cost:    3
c ---[ 459]---> BDD-cost:    3
c ---[ 458]---> BDD-cost:    3
c ---[ 457]---> BDD-cost:    3
c ---[ 456]---> BDD-cost:    3
c ---[ 455]---> BDD-cost:    3
c ---[ 454]---> BDD-cost:    3
c ---[ 453]---> BDD-cost:    3
c ---[ 452]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    3
c ---[ 450]---> BDD-cost:    3
c ---[ 449]---> BDD-cost:    3
c ---[ 448]---> BDD-cost:    3
c ---[ 447]---> BDD-cost:    3
c ---[ 446]---> BDD-cost:    3
c ---[ 445]---> BDD-cost:    3
c ---[ 444]---> BDD-cost:    3
c ---[ 443]---> BDD-cost:    3
c ---[ 442]---> BDD-cost:    3
c ---[ 441]---> BDD-cost:    3
c ---[ 440]---> BDD-cost:    3
c ---[ 439]---> BDD-cost:    3
c ---[ 438]---> BDD-cost:    3
c ---[ 437]---> BDD-cost:    3
c ---[ 436]---> BDD-cost:    3
c ---[ 435]---> BDD-cost:    3
c ---[ 434]---> BDD-cost:    3
c ---[ 433]---> BDD-cost:    3
c ---[ 432]---> BDD-cost:    3
c ---[ 431]---> BDD-cost:    3
c ---[ 430]---> BDD-cost:    3
c ---[ 429]---> BDD-cost:    3
c ---[ 428]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:    3
c ---[ 426]---> BDD-cost:    3
c ---[ 425]---> BDD-cost:    3
c ---[ 424]---> BDD-cost:    3
c ---[ 423]---> BDD-cost:    3
c ---[ 422]---> BDD-cost:    3
c ---[ 421]---> BDD-cost:    3
c ---[ 420]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    3
c ---[ 418]---> BDD-cost:    3
c ---[ 417]---> BDD-cost:    3
c ---[ 416]---> BDD-cost:    3
c ---[ 415]---> BDD-cost:    3
c ---[ 414]---> BDD-cost:    3
c ---[ 413]---> BDD-cost:    3
c ---[ 412]---> BDD-cost:    3
c ---[ 411]---> BDD-cost:    3
c ---[ 410]---> BDD-cost:    3
c ---[ 409]---> BDD-cost:    3
c ---[ 408]---> BDD-cost:    3
c ---[ 407]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:    3
c ---[ 405]---> BDD-cost:    3
c ---[ 404]---> BDD-cost:    3
c ---[ 403]---> BDD-cost:    3
c ---[ 402]---> BDD-cost:    3
c ---[ 401]---> BDD-cost:    3
c ---[ 400]---> BDD-cost:    3
c ---[ 399]---> BDD-cost:    3
c ---[ 398]---> BDD-cost:    3
c ---[ 397]---> BDD-cost:    3
c ---[ 396]---> BDD-cost:    3
c ---[ 395]---> BDD-cost:    3
c ---[ 394]---> BDD-cost:    3
c ---[ 393]---> BDD-cost:    3
c ---[ 392]---> BDD-cost:    3
c ---[ 391]---> BDD-cost:    3
c ---[ 390]---> BDD-cost:    3
c ---[ 389]---> BDD-cost:    3
c ---[ 388]---> BDD-cost:    3
c ---[ 387]---> BDD-cost:    3
c ---[ 386]---> BDD-cost:    3
c ---[ 385]---> BDD-cost:    3
c ---[ 384]---> BDD-cost:    3
c ---[ 383]---> BDD-cost:    3
c ---[ 382]---> BDD-cost:    3
c ---[ 381]---> BDD-cost:    3
c ---[ 380]---> BDD-cost:    3
c ---[ 379]---> BDD-cost:    3
c ---[ 378]---> BDD-cost:    3
c ---[ 377]---> BDD-cost:    3
c ---[ 376]---> BDD-cost:    3
c ---[ 375]---> BDD-cost:    3
c ---[ 374]---> BDD-cost:    3
c ---[ 373]---> BDD-cost:    3
c ---[ 372]---> BDD-cost:    3
c ---[ 371]---> BDD-cost:    3
c ---[ 370]---> BDD-cost:    3
c ---[ 369]---> BDD-cost:    3
c ---[ 368]---> BDD-cost:    3
c ---[ 367]---> BDD-cost:    3
c ---[ 366]---> BDD-cost:    3
c ---[ 365]---> BDD-cost:    3
c ---[ 364]---> BDD-cost:    3
c ---[ 363]---> BDD-cost:    3
c ---[ 362]---> BDD-cost:    3
c ---[ 361]---> BDD-cost:    3
c ---[ 360]---> BDD-cost:    3
c ---[ 359]---> BDD-cost:    3
c ---[ 358]---> BDD-cost:    3
c ---[ 357]---> BDD-cost:    3
c ---[ 356]---> BDD-cost:    3
c ---[ 355]---> BDD-cost:    3
c ---[ 354]---> BDD-cost:    3
c ---[ 353]---> BDD-cost:    3
c ---[ 352]---> BDD-cost:    3
c ---[ 351]---> BDD-cost:    3
c ---[ 350]---> BDD-cost:    3
c ---[ 349]---> BDD-cost:    3
c ---[ 348]---> BDD-cost:    3
c ---[ 347]---> BDD-cost:    3
c ---[ 346]---> BDD-cost:    3
c ---[ 345]---> BDD-cost:    3
c ---[ 344]---> BDD-cost:    3
c ---[ 343]---> BDD-cost:    3
c ---[ 342]---> BDD-cost:    3
c ---[ 341]---> BDD-cost:    3
c ---[ 340]---> BDD-cost:    3
c ---[ 339]---> BDD-cost:    3
c ---[ 338]---> BDD-cost:    3
c ---[ 337]---> BDD-cost:    3
c ---[ 336]---> BDD-cost:    3
c ---[ 335]---> BDD-cost:    3
c ---[ 334]---> BDD-cost:    3
c ---[ 333]---> BDD-cost:    3
c ---[ 332]---> BDD-cost:    3
c ---[ 331]---> BDD-cost:    3
c ---[ 330]---> BDD-cost:    3
c ---[ 329]---> BDD-cost:    3
c ---[ 328]---> BDD-cost:    3
c ---[ 327]---> BDD-cost:    3
c ---[ 326]---> BDD-cost:    3
c ---[ 325]---> BDD-cost:    3
c ---[ 324]---> BDD-cost:    3
c ---[ 323]---> BDD-cost:    3
c ---[ 322]---> BDD-cost:    3
c ---[ 321]---> BDD-cost:    3
c ---[ 320]---> BDD-cost:    3
c ---[ 319]---> BDD-cost:    3
c ---[ 318]---> BDD-cost:    3
c ---[ 317]---> BDD-cost:    3
c ---[ 316]---> BDD-cost:    3
c ---[ 315]---> BDD-cost:    3
c ---[ 314]---> BDD-cost:    3
c ---[ 313]---> BDD-cost:    3
c ---[ 312]---> BDD-cost:    3
c ---[ 311]---> BDD-cost:    3
c ---[ 310]---> BDD-cost:    3
c ---[ 309]---> BDD-cost:    3
c ---[ 308]---> BDD-cost:    3
c ---[ 307]---> BDD-cost:    3
c ---[ 306]---> BDD-cost:    3
c ---[ 305]---> BDD-cost:    3
c ---[ 304]---> BDD-cost:    3
c ---[ 303]---> BDD-cost:    3
c ---[ 302]---> BDD-cost:    3
c ---[ 301]---> BDD-cost:    3
c ---[ 300]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    3
c ---[ 298]---> BDD-cost:    3
c ---[ 297]---> BDD-cost:    3
c ---[ 296]---> BDD-cost:    3
c ---[ 295]---> BDD-cost:    3
c ---[ 294]---> BDD-cost:    3
c ---[ 293]---> BDD-cost:    3
c ---[ 292]---> BDD-cost:    3
c ---[ 291]---> BDD-cost:    3
c ---[ 290]---> BDD-cost:    3
c ---[ 289]---> BDD-cost:    3
c ---[ 288]---> BDD-cost:    3
c ---[ 287]---> BDD-cost:    3
c ---[ 286]---> BDD-cost:    3
c ---[ 285]---> BDD-cost:    3
c ---[ 284]---> BDD-cost:    3
c ---[ 283]---> BDD-cost:    3
c ---[ 282]---> BDD-cost:    3
c ---[ 281]---> BDD-cost:    3
c ---[ 280]---> BDD-cost:    3
c ---[ 279]---> BDD-cost:    3
c ---[ 278]---> BDD-cost:    3
c ---[ 277]---> BDD-cost:    3
c ---[ 276]---> BDD-cost:    3
c ---[ 275]---> BDD-cost:    3
c ---[ 274]---> BDD-cost:    3
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    3
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 268]---> BDD-cost:    3
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 263]---> BDD-cost:    3
c ---[ 262]---> BDD-cost:    3
c ---[ 261]---> BDD-cost:    3
c ---[ 260]---> BDD-cost:    3
c ---[ 259]---> BDD-cost:    3
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:    3
c ---[ 254]---> BDD-cost:    3
c ---[ 253]---> BDD-cost:    3
c ---[ 252]---> BDD-cost:    3
c ---[ 251]---> BDD-cost:    3
c ---[ 250]---> BDD-cost:    3
c ---[ 249]---> BDD-cost:    3
c ---[ 248]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    3
c ---[ 246]---> BDD-cost:    3
c ---[ 245]---> BDD-cost:    3
c ---[ 244]---> BDD-cost:    3
c ---[ 243]---> BDD-cost:    3
c ---[ 242]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    3
c ---[ 240]---> BDD-cost:    3
c ---[ 239]---> BDD-cost:    3
c ---[ 238]---> BDD-cost:    3
c ---[ 237]---> BDD-cost:    3
c ---[ 236]---> BDD-cost:    3
c ---[ 235]---> BDD-cost:    3
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    3
c ---[ 232]---> BDD-cost:    3
c ---[ 231]---> BDD-cost:    3
c ---[ 230]---> BDD-cost:    3
c ---[ 229]---> BDD-cost:    3
c ---[ 228]---> BDD-cost:    3
c ---[ 227]---> BDD-cost:    3
c ---[ 226]---> BDD-cost:    3
c ---[ 225]---> BDD-cost:    3
c ---[ 224]---> BDD-cost:    3
c ---[ 223]---> BDD-cost:    3
c ---[ 222]---> BDD-cost:    3
c ---[ 221]---> BDD-cost:    3
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:    3
c ---[ 218]---> BDD-cost:    3
c ---[ 217]---> BDD-cost:    3
c ---[ 216]---> BDD-cost:    3
c ---[ 215]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:    3
c ---[ 213]---> BDD-cost:    3
c ---[ 212]---> BDD-cost:    3
c ---[ 211]---> BDD-cost:    3
c ---[ 210]---> BDD-cost:    3
c ---[ 209]---> BDD-cost:    3
c ---[ 208]---> BDD-cost:    3
c ---[ 207]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    3
c ---[ 204]---> BDD-cost:    3
c ---[ 203]---> BDD-cost:    3
c ---[ 202]---> BDD-cost:    3
c ---[ 201]---> BDD-cost:    3
c ---[ 200]---> BDD-cost:    3
c ---[ 199]---> BDD-cost:    3
c ---[ 198]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    3
c ---[ 196]---> BDD-cost:    3
c ---[ 195]---> BDD-cost:    3
c ---[ 194]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    3
c ---[ 192]---> BDD-cost:    3
c ---[ 191]---> BDD-cost:    3
c ---[ 190]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:    3
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    3
c ---[ 186]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 184]---> BDD-cost:    3
c ---[ 183]---> BDD-cost:    3
c ---[ 182]---> BDD-cost:    3
c ---[ 181]---> BDD-cost:    3
c ---[ 180]---> BDD-cost:    3
c ---[ 179]---> BDD-cost:    3
c ---[ 178]---> BDD-cost:    3
c ---[ 177]---> BDD-cost:    3
c ---[ 176]---> BDD-cost:    3
c ---[ 175]---> BDD-cost:    3
c ---[ 174]---> BDD-cost:    3
c ---[ 173]---> BDD-cost:    3
c ---[ 172]---> BDD-cost:    3
c ---[ 171]---> BDD-cost:    3
c ---[ 170]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 168]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:    3
c ---[ 157]---> BDD-cost:    3
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    3
c ---[ 145]---> BDD-cost:    3
c ---[ 144]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 131]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 125]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    3
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    3
c ---[ 118]---> BDD-cost:    3
c ---[ 117]---> BDD-cost:    3
c ---[ 116]---> BDD-cost:    3
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:    3
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    3
c ---[ 110]---> BDD-cost:    3
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    3
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:    3
c ---[ 105]---> BDD-cost:    3
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    3
c ---[ 101]---> BDD-cost:    3
c ---[ 100]---> BDD-cost:    3
c ---[  99]---> BDD-cost:    3
c ---[  98]---> BDD-cost:    3
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    3
c ---[  95]---> BDD-cost:    3
c ---[  94]---> BDD-cost:    3
c ---[  93]---> BDD-cost:    3
c ---[  92]---> BDD-cost:    3
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  89]---> BDD-cost:    3
c ---[  88]---> BDD-cost:    3
c ---[  87]---> BDD-cost:    3
c ---[  86]---> BDD-cost:    3
c ---[  85]---> BDD-cost:    3
c ---[  84]---> BDD-cost:    3
c ---[  83]---> BDD-cost:    3
c ---[  82]---> BDD-cost:    3
c ---[  81]---> BDD-cost:    3
c ---[  80]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  77]---> BDD-cost:    3
c ---[  76]---> BDD-cost:    3
c ---[  75]---> BDD-cost:    3
c ---[  74]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  71]---> BDD-cost:    3
c ---[  70]---> BDD-cost:    3
c ---[  69]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  65]---> BDD-cost:    3
c ---[  64]---> BDD-cost:    3
c ---[  63]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  58]---> BDD-cost:    3
c ---[  57]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  53]---> BDD-cost:    3
c ---[  52]---> BDD-cost:    3
c ---[  51]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    3
c ---[  44]---> BDD-cost:    3
c ---[  43]---> BDD-cost:    3
c ---[  42]---> BDD-cost:    3
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:    3
c ---[  39]---> BDD-cost:    3
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    3
c ---[  36]---> BDD-cost:    3
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:    3
c ---[  33]---> BDD-cost:    3
c ---[  32]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    3
c ---[  26]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    3
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:    3
c ---[  12]---> BDD-cost:    3
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:    3
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    3
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    3
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  855124  3043296 |  285041       0        0     nan |  0.000 % |
c |       102 |  855100  3043214 |  313545      99      317     3.2 |  1.497 % |
c |       252 |  854948  3042698 |  344899     229      768     3.4 |  1.519 % |
c |       477 |  854948  3042698 |  379389     454     1640     3.6 |  1.519 % |
c |       814 |  854948  3042698 |  417328     791     6663     8.4 |  1.519 % |
c |      1320 |  854948  3042698 |  459061    1297     8773     6.8 |  1.519 % |
c |      2079 |  854859  3042384 |  504967    2053    13440     6.5 |  1.524 % |
c |      3218 |  854796  3042158 |  555464    3191    18905     5.9 |  1.525 % |
c |      4926 |  854488  3041062 |  611010    4892    28983     5.9 |  1.531 % |
c |      7488 |  854381  3040678 |  672111    7452    68033     9.1 |  1.532 % |
c |     11333 |  854288  3040342 |  739322   11296   169208    15.0 |  1.533 % |
c |     17099 |  854243  3040182 |  813255   17061   338731    19.9 |  1.534 % |
c |     25748 |  854180  3039956 |  894580   25709   583498    22.7 |  1.534 % |
c |     38726 |  854047  3039480 |  984038   38685  1117336    28.9 |  1.536 % |
c |     58188 |  853997  3039300 | 1082442   58146  2044607    35.2 |  1.537 % |
c |     87380 |  853997  3039300 | 1190686   87338  4944346    56.6 |  1.537 % |
c |    131170 |  853940  3039096 | 1309755  131127  6434703    49.1 |  1.537 % |
c |    196854 |  853865  3038826 | 1440731  196810 11033684    56.1 |  1.538 % |
c |    295380 |  853584  3037816 | 1584804  295331 16369076    55.4 |  1.542 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.89 0.95 0.93 2/54 21236
Raw data (stat): 21236 (runsolver) R 21235 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545766436 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.91 0.95 0.93 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 3989 0 0 0 988 11 0 0 25 0 1 0 545766436 12091392 2368 4294967295 134512640 134672761 3221224624 3221222752 134597191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2952 2368 603 41 0 2911 0
vsize: 11808
[startup+20.0002 s]
Raw data (loadavg): 0.92 0.96 0.93 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 14265 0 0 0 1963 36 0 0 25 0 1 0 545766436 46424064 10060 4294967295 134512640 134672761 3221224624 3221222808 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11334 10062 603 41 0 11293 0
vsize: 45336
[startup+29.9999 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 15087 0 0 0 2961 38 0 0 25 0 1 0 545766436 46755840 10212 4294967295 134512640 134672761 3221224624 3221222752 134597188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11415 10212 603 41 0 11374 0
vsize: 45660
[startup+39.9995 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 30847 0 0 0 3926 72 0 0 25 0 1 0 545766436 127377408 25915 4294967295 134512640 134672761 3221224624 3221223616 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31098 25915 603 41 0 31057 0
vsize: 124392
[startup+49.9998 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 31347 0 0 0 4925 74 0 0 25 0 1 0 545766436 129417216 26415 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31596 26415 603 41 0 31555 0
vsize: 126384
[startup+60.0003 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 31810 0 0 0 5923 76 0 0 25 0 1 0 545766436 131334144 26878 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32064 26878 603 41 0 32023 0
vsize: 128256
[startup+70.0008 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 32372 0 0 0 6921 78 0 0 25 0 1 0 545766436 133672960 27440 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32635 27440 603 41 0 32594 0
vsize: 130540
[startup+80.001 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 32966 0 0 0 7919 79 0 0 25 0 1 0 545766436 136085504 28034 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33224 28034 603 41 0 33183 0
vsize: 132896
[startup+90.002 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 33496 0 0 0 8918 81 0 0 25 0 1 0 545766436 138235904 28564 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33749 28564 603 41 0 33708 0
vsize: 134996
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 34081 0 0 0 9916 82 0 0 25 0 1 0 545766436 140660736 29149 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34341 29149 603 41 0 34300 0
vsize: 137364
[startup+110.003 s]
Raw data (loadavg): 1.06 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 34563 0 0 0 10915 83 0 0 25 0 1 0 545766436 142589952 29631 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34812 29631 603 41 0 34771 0
vsize: 139248
[startup+120.003 s]
Raw data (loadavg): 1.05 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 35251 0 0 0 11914 84 0 0 25 0 1 0 545766436 145678336 30319 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35566 30319 603 41 0 35525 0
vsize: 142264
[startup+130.003 s]
Raw data (loadavg): 1.04 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 35776 0 0 0 12913 86 0 0 25 0 1 0 545766436 147812352 30844 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36087 30844 603 41 0 36046 0
vsize: 144348
[startup+140.003 s]
Raw data (loadavg): 1.04 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 36377 0 0 0 13911 88 0 0 25 0 1 0 545766436 150228992 31445 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36677 31445 603 41 0 36636 0
vsize: 146708
[startup+150.004 s]
Raw data (loadavg): 1.03 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 36902 0 0 0 14909 90 0 0 25 0 1 0 545766436 152383488 31970 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37203 31970 603 41 0 37162 0
vsize: 148812
[startup+160.004 s]
Raw data (loadavg): 1.02 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 37359 0 0 0 15908 92 0 0 25 0 1 0 545766436 154271744 32427 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37664 32427 603 41 0 37623 0
vsize: 150656
[startup+170.004 s]
Raw data (loadavg): 1.02 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 37659 0 0 0 16907 93 0 0 25 0 1 0 545766436 155484160 32727 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37960 32727 603 41 0 37919 0
vsize: 151840
[startup+180.004 s]
Raw data (loadavg): 1.02 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 38076 0 0 0 17906 94 0 0 25 0 1 0 545766436 157097984 33144 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38354 33144 603 41 0 38313 0
vsize: 153416
[startup+190.004 s]
Raw data (loadavg): 1.01 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 38459 0 0 0 18905 95 0 0 25 0 1 0 545766436 158715904 33527 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38749 33527 603 41 0 38708 0
vsize: 154996
[startup+200.005 s]
Raw data (loadavg): 1.01 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 38734 0 0 0 19904 96 0 0 25 0 1 0 545766436 159797248 33802 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39013 33802 603 41 0 38972 0
vsize: 156052
[startup+210.005 s]
Raw data (loadavg): 1.01 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 38981 0 0 0 20904 96 0 0 25 0 1 0 545766436 160878592 34049 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39277 34049 603 41 0 39236 0
vsize: 157108
[startup+220.006 s]
Raw data (loadavg): 1.01 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 39241 0 0 0 21904 97 0 0 25 0 1 0 545766436 161878016 34309 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39521 34309 603 41 0 39480 0
vsize: 158084
[startup+230.006 s]
Raw data (loadavg): 1.01 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 39461 0 0 0 22903 98 0 0 25 0 1 0 545766436 163348480 34529 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39880 34529 603 41 0 39839 0
vsize: 159520
[startup+240.007 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 39715 0 0 0 23902 99 0 0 25 0 1 0 545766436 164278272 34783 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40107 34783 603 41 0 40066 0
vsize: 160428
[startup+250.006 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 40043 0 0 0 24902 99 0 0 25 0 1 0 545766436 165617664 35111 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40434 35111 603 41 0 40393 0
vsize: 161736
[startup+260.01 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 40345 0 0 0 25901 101 0 0 25 0 1 0 545766436 166948864 35413 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40759 35413 603 41 0 40718 0
vsize: 163036
[startup+270.01 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 40634 0 0 0 26900 102 0 0 25 0 1 0 545766436 168165376 35702 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41056 35702 603 41 0 41015 0
vsize: 164224
[startup+280.01 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 40866 0 0 0 27899 103 0 0 25 0 1 0 545766436 169111552 35934 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41287 35934 603 41 0 41246 0
vsize: 165148
[startup+290.011 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 41104 0 0 0 28899 103 0 0 25 0 1 0 545766436 170049536 36172 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41516 36172 603 41 0 41475 0
vsize: 166064
[startup+300.011 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 41346 0 0 0 29898 104 0 0 25 0 1 0 545766436 170995712 36414 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41747 36414 603 41 0 41706 0
vsize: 166988
[startup+310.011 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 41569 0 0 0 30897 105 0 0 25 0 1 0 545766436 171958272 36637 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41982 36637 603 41 0 41941 0
vsize: 167928
[startup+320.011 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 41782 0 0 0 31897 106 0 0 25 0 1 0 545766436 172896256 36850 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42211 36850 603 41 0 42170 0
vsize: 168844
[startup+330.011 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 41979 0 0 0 32896 107 0 0 25 0 1 0 545766436 173694976 37047 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42406 37047 603 41 0 42365 0
vsize: 169624
[startup+340.012 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 42150 0 0 0 33896 107 0 0 25 0 1 0 545766436 174358528 37218 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42568 37218 603 41 0 42527 0
vsize: 170272
[startup+350.011 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 42363 0 0 0 34896 108 0 0 25 0 1 0 545766436 175181824 37431 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42769 37431 603 41 0 42728 0
vsize: 171076
[startup+360.012 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 42827 0 0 0 35895 109 0 0 25 0 1 0 545766436 177201152 37895 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43262 37895 603 41 0 43221 0
vsize: 173048
[startup+370.012 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 43293 0 0 0 36893 110 0 0 25 0 1 0 545766436 179077120 38361 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43720 38361 603 41 0 43679 0
vsize: 174880
[startup+380.015 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 43670 0 0 0 37893 111 0 0 25 0 1 0 545766436 180555776 38738 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44081 38738 603 41 0 44040 0
vsize: 176324
[startup+390.016 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 44062 0 0 0 38892 113 0 0 25 0 1 0 545766436 182177792 39130 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44477 39130 603 41 0 44436 0
vsize: 177908
[startup+400.015 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 44431 0 0 0 39890 114 0 0 25 0 1 0 545766436 183668736 39499 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44841 39499 603 41 0 44800 0
vsize: 179364
[startup+410.016 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 44647 0 0 0 40890 115 0 0 25 0 1 0 545766436 184610816 39715 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45071 39715 603 41 0 45030 0
vsize: 180284
[startup+420.016 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 45009 0 0 0 41889 116 0 0 25 0 1 0 545766436 186081280 40077 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45430 40077 603 41 0 45389 0
vsize: 181720
[startup+430.016 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 45387 0 0 0 42888 117 0 0 25 0 1 0 545766436 187564032 40455 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45792 40455 603 41 0 45751 0
vsize: 183168
[startup+440.016 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 45680 0 0 0 43887 118 0 0 25 0 1 0 545766436 188776448 40748 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46088 40748 603 41 0 46047 0
vsize: 184352
[startup+450.016 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 46057 0 0 0 44886 119 0 0 25 0 1 0 545766436 190255104 41125 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46449 41125 603 41 0 46408 0
vsize: 185796
[startup+460.016 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 46371 0 0 0 45886 120 0 0 25 0 1 0 545766436 191602688 41439 4294967295 134512640 134672761 3221224624 3221223808 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46778 41439 603 41 0 46737 0
vsize: 187112
[startup+470.016 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 46706 0 0 0 46885 120 0 0 25 0 1 0 545766436 192954368 41774 4294967295 134512640 134672761 3221224624 3221223808 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47108 41774 603 41 0 47067 0
vsize: 188432
[startup+480.016 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 46973 0 0 0 47885 121 0 0 25 0 1 0 545766436 194048000 42041 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47375 42041 603 41 0 47334 0
vsize: 189500
[startup+490.02 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 47068 0 0 0 48885 121 0 0 25 0 1 0 545766436 194473984 42136 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47479 42136 603 41 0 47438 0
vsize: 189916
[startup+500.027 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 47184 0 0 0 49885 122 0 0 25 0 1 0 545766436 195022848 42252 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47613 42252 603 41 0 47572 0
vsize: 190452
[startup+510.027 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 47305 0 0 0 50885 122 0 0 25 0 1 0 545766436 195420160 42373 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47710 42373 603 41 0 47669 0
vsize: 190840
[startup+520.027 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 47456 0 0 0 51885 123 0 0 25 0 1 0 545766436 196091904 42524 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47874 42524 603 41 0 47833 0
vsize: 191496
[startup+530.027 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 47594 0 0 0 52884 123 0 0 25 0 1 0 545766436 196657152 42662 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48012 42662 603 41 0 47971 0
vsize: 192048
[startup+540.028 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 47789 0 0 0 53884 124 0 0 25 0 1 0 545766436 197480448 42857 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48213 42857 603 41 0 48172 0
vsize: 192852
[startup+550.028 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 47975 0 0 0 54883 125 0 0 25 0 1 0 545766436 198156288 43043 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48378 43043 603 41 0 48337 0
vsize: 193512
[startup+560.028 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 48182 0 0 0 55882 126 0 0 25 0 1 0 545766436 198967296 43250 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48576 43250 603 41 0 48535 0
vsize: 194304
[startup+570.028 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 48429 0 0 0 56882 126 0 0 25 0 1 0 545766436 200040448 43497 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48838 43497 603 41 0 48797 0
vsize: 195352
[startup+580.028 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 48514 0 0 0 57882 127 0 0 25 0 1 0 545766436 200310784 43582 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48904 43582 603 41 0 48863 0
vsize: 195616
[startup+590.029 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 48627 0 0 0 58882 127 0 0 25 0 1 0 545766436 200847360 43695 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49035 43695 603 41 0 48994 0
vsize: 196140
[startup+600.03 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 48813 0 0 0 59881 128 0 0 25 0 1 0 545766436 201576448 43881 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49213 43881 603 41 0 49172 0
vsize: 196852
[startup+610.03 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 49119 0 0 0 60881 129 0 0 25 0 1 0 545766436 202797056 44187 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49511 44187 603 41 0 49470 0
vsize: 198044
[startup+620.03 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 49271 0 0 0 61880 129 0 0 25 0 1 0 545766436 203497472 44339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49682 44339 603 41 0 49641 0
vsize: 198728
[startup+630.03 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 49450 0 0 0 62880 129 0 0 25 0 1 0 545766436 205213696 44518 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50101 44518 603 41 0 50060 0
vsize: 200404
[startup+640.031 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 49629 0 0 0 63880 130 0 0 25 0 1 0 545766436 206020608 44697 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50298 44697 603 41 0 50257 0
vsize: 201192
[startup+650.031 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 49819 0 0 0 64880 130 0 0 25 0 1 0 545766436 206737408 44887 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50473 44887 603 41 0 50432 0
vsize: 201892
[startup+660.031 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 50012 0 0 0 65879 131 0 0 25 0 1 0 545766436 207536128 45080 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50668 45080 603 41 0 50627 0
vsize: 202672
[startup+670.032 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 50206 0 0 0 66879 132 0 0 25 0 1 0 545766436 208355328 45274 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50868 45274 603 41 0 50827 0
vsize: 203472
[startup+680.032 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 50383 0 0 0 67878 133 0 0 25 0 1 0 545766436 209018880 45451 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51030 45451 603 41 0 50989 0
vsize: 204120
[startup+690.032 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 50576 0 0 0 68877 134 0 0 25 0 1 0 545766436 209821696 45644 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51226 45644 603 41 0 51185 0
vsize: 204904
[startup+700.033 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 50738 0 0 0 69877 134 0 0 25 0 1 0 545766436 210493440 45806 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51390 45806 603 41 0 51349 0
vsize: 205560
[startup+710.033 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 50876 0 0 0 70877 134 0 0 25 0 1 0 545766436 211034112 45944 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51522 45944 603 41 0 51481 0
vsize: 206088
[startup+720.033 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 50991 0 0 0 71876 135 0 0 25 0 1 0 545766436 211574784 46059 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51654 46059 603 41 0 51613 0
vsize: 206616
[startup+730.033 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 51263 0 0 0 72876 135 0 0 25 0 1 0 545766436 212668416 46331 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51921 46331 603 41 0 51880 0
vsize: 207684
[startup+740.034 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 51573 0 0 0 73875 136 0 0 25 0 1 0 545766436 213880832 46641 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52217 46641 603 41 0 52176 0
vsize: 208868
[startup+750.034 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 51829 0 0 0 74874 137 0 0 25 0 1 0 545766436 214953984 46897 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52479 46897 603 41 0 52438 0
vsize: 209916
[startup+760.034 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 52103 0 0 0 75873 138 0 0 25 0 1 0 545766436 216047616 47171 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52746 47171 603 41 0 52705 0
vsize: 210984
[startup+770.034 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 52342 0 0 0 76873 139 0 0 25 0 1 0 545766436 217161728 47410 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53018 47410 603 41 0 52977 0
vsize: 212072
[startup+780.034 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 52615 0 0 0 77872 140 0 0 25 0 1 0 545766436 218238976 47683 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53281 47683 603 41 0 53240 0
vsize: 213124
[startup+790.035 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 52909 0 0 0 78872 140 0 0 25 0 1 0 545766436 219459584 47977 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53579 47977 603 41 0 53538 0
vsize: 214316
[startup+800.034 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 53162 0 0 0 79871 141 0 0 25 0 1 0 545766436 220393472 48230 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53807 48230 603 41 0 53766 0
vsize: 215228
[startup+810.034 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 53427 0 0 0 80871 142 0 0 25 0 1 0 545766436 221499392 48495 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54077 48495 603 41 0 54036 0
vsize: 216308
[startup+820.035 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 53683 0 0 0 81870 143 0 0 25 0 1 0 545766436 222593024 48751 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54344 48751 603 41 0 54303 0
vsize: 217376
[startup+830.035 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 53880 0 0 0 82870 143 0 0 25 0 1 0 545766436 223395840 48948 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54540 48948 603 41 0 54499 0
vsize: 218160
[startup+840.036 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 54194 0 0 0 83869 144 0 0 25 0 1 0 545766436 224628736 49262 4294967295 134512640 134672761 3221224624 3221223748 134566115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54841 49262 603 41 0 54800 0
vsize: 219364
[startup+850.037 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 54504 0 0 0 84868 145 0 0 25 0 1 0 545766436 225837056 49572 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55136 49572 603 41 0 55095 0
vsize: 220544
[startup+860.037 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 54867 0 0 0 85867 147 0 0 25 0 1 0 545766436 227315712 49935 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55497 49935 603 41 0 55456 0
vsize: 221988
[startup+870.037 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 55081 0 0 0 86867 147 0 0 25 0 1 0 545766436 228253696 50149 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55726 50149 603 41 0 55685 0
vsize: 222904
[startup+880.037 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 55188 0 0 0 87867 147 0 0 25 0 1 0 545766436 228720640 50256 4294967295 134512640 134672761 3221224624 3221223624 1075349771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55840 50256 603 41 0 55799 0
vsize: 223360
[startup+890.038 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 55279 0 0 0 88867 147 0 0 25 0 1 0 545766436 228990976 50347 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55906 50347 603 41 0 55865 0
vsize: 223624
[startup+900.038 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 55391 0 0 0 89866 148 0 0 25 0 1 0 545766436 229568512 50459 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56047 50459 603 41 0 56006 0
vsize: 224188
[startup+910.038 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 55503 0 0 0 90866 148 0 0 25 0 1 0 545766436 229974016 50571 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56146 50571 603 41 0 56105 0
vsize: 224584
[startup+920.038 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 55616 0 0 0 91866 149 0 0 25 0 1 0 545766436 230375424 50684 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56244 50684 603 41 0 56203 0
vsize: 224976
[startup+930.038 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 55743 0 0 0 92866 149 0 0 25 0 1 0 545766436 230948864 50811 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56384 50811 603 41 0 56343 0
vsize: 225536
[startup+940.039 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 55865 0 0 0 93865 150 0 0 25 0 1 0 545766436 231350272 50933 4294967295 134512640 134672761 3221224624 3221223808 134559492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56482 50933 603 41 0 56441 0
vsize: 225928
[startup+950.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 55994 0 0 0 94865 150 0 0 25 0 1 0 545766436 231899136 51062 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56616 51062 603 41 0 56575 0
vsize: 226464
[startup+960.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 56135 0 0 0 95865 150 0 0 25 0 1 0 545766436 232562688 51203 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56778 51203 603 41 0 56737 0
vsize: 227112
[startup+970.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 56290 0 0 0 96865 151 0 0 25 0 1 0 545766436 233091072 51358 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56907 51358 603 41 0 56866 0
vsize: 227628
[startup+980.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 56409 0 0 0 97865 151 0 0 25 0 1 0 545766436 233627648 51477 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57038 51477 603 41 0 56997 0
vsize: 228152
[startup+990.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 56535 0 0 0 98864 152 0 0 25 0 1 0 545766436 234242048 51603 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57188 51603 603 41 0 57147 0
vsize: 228752
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 56682 0 0 0 99864 152 0 0 25 0 1 0 545766436 234795008 51750 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57323 51750 603 41 0 57282 0
vsize: 229292
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 56832 0 0 0 100864 153 0 0 25 0 1 0 545766436 235376640 51900 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57465 51900 603 41 0 57424 0
vsize: 229860
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 56982 0 0 0 101864 153 0 0 25 0 1 0 545766436 235962368 52050 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57608 52050 603 41 0 57567 0
vsize: 230432
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 57128 0 0 0 102863 153 0 0 25 0 1 0 545766436 236630016 52196 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57771 52196 603 41 0 57730 0
vsize: 231084
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 57266 0 0 0 103864 153 0 0 25 0 1 0 545766436 237166592 52334 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57902 52334 603 41 0 57861 0
vsize: 231608
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 57424 0 0 0 104863 154 0 0 25 0 1 0 545766436 237834240 52492 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58065 52492 603 41 0 58024 0
vsize: 232260
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 57569 0 0 0 105863 154 0 0 25 0 1 0 545766436 238387200 52637 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58200 52637 603 41 0 58159 0
vsize: 232800
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 57718 0 0 0 106863 154 0 0 25 0 1 0 545766436 239063040 52786 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58365 52786 603 41 0 58324 0
vsize: 233460
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 57859 0 0 0 107863 155 0 0 25 0 1 0 545766436 239603712 52927 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58497 52927 603 41 0 58456 0
vsize: 233988
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 57991 0 0 0 108862 155 0 0 25 0 1 0 545766436 240164864 53059 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58634 53059 603 41 0 58593 0
vsize: 234536
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 58109 0 0 0 109862 156 0 0 25 0 1 0 545766436 240652288 53177 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58753 53177 603 41 0 58712 0
vsize: 235012
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 58230 0 0 0 110862 156 0 0 25 0 1 0 545766436 241053696 53298 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58851 53298 603 41 0 58810 0
vsize: 235404
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 58359 0 0 0 111862 156 0 0 25 0 1 0 545766436 241627136 53427 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58991 53427 603 41 0 58950 0
vsize: 235964
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 58485 0 0 0 112862 156 0 0 25 0 1 0 545766436 242159616 53553 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59121 53553 603 41 0 59080 0
vsize: 236484
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 58628 0 0 0 113862 157 0 0 25 0 1 0 545766436 242696192 53696 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59252 53696 603 41 0 59211 0
vsize: 237008
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 58772 0 0 0 114862 157 0 0 25 0 1 0 545766436 243290112 53840 4294967295 134512640 134672761 3221224624 3221223764 134560629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59397 53840 603 41 0 59356 0
vsize: 237588
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 58898 0 0 0 115861 158 0 0 25 0 1 0 545766436 243838976 53966 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59531 53966 603 41 0 59490 0
vsize: 238124
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 59024 0 0 0 116861 158 0 0 25 0 1 0 545766436 244379648 54092 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59663 54092 603 41 0 59622 0
vsize: 238652
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 59135 0 0 0 117861 158 0 0 25 0 1 0 545766436 244781056 54203 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59761 54203 603 41 0 59720 0
vsize: 239044
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 59282 0 0 0 118861 159 0 0 25 0 1 0 545766436 245518336 54350 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59941 54350 603 41 0 59900 0
vsize: 239764
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 21236
Raw data (stat): 21236 (minisat+) R 21235 11931 11930 0 -1 0 59423 0 0 0 119860 160 0 0 25 0 1 0 545766436 246059008 54491 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60073 54491 603 41 0 60032 0
vsize: 240292
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.98 0.94 1/54 21236
Raw data (stat): 21236 (minisat+) Z 21235 11931 11930 0 -1 12 59425 0 0 0 119860 170 0 0 23 0 1 0 545766436 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.17
CPU time (s): 1200.31
CPU user time (s): 1198.61
CPU system time (s): 1.70274
CPU usage (%): 100.012
Max. virtual memory (Kb): 240292
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####