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 18308

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 14:22:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18250 boxname=wulflinc12 idbench=1404 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b4da9562dcd40afcc9afd9f695cf339d  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-cap6000.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-cap6000.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-cap6000.opb
IDLAUNCH: 18250
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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	: 2
cpu MHz		: 451.091
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        785732 kB
Buffers:         22732 kB
Cached:         204628 kB
SwapCached:        508 kB
Active:          46688 kB
Inactive:       182804 kB
HighTotal:      131008 kB
HighFree:        38080 kB
LowTotal:       903652 kB
LowFree:        747652 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            13836 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:42:34 (client local time) WITH STATUS 0 IN 1200.48 SECONDS
stats: 18250 7 1200.48 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  855145  3043372 |  256543       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/130273          
c   -- var.elim.:  2000/130273          
c   -- var.elim.:  3000/130273          
c   -- var.elim.:  4000/130273          
c   -- var.elim.:  5000/130273          
c   -- var.elim.:  6000/130273          
c   -- var.elim.:  7000/130273          
c   -- var.elim.:  8000/130273          
c   -- var.elim.:  9000/130273          
c   -- var.elim.:  10000/130273          
c   -- var.elim.:  11000/130273          
c   -- var.elim.:  12000/130273          
c   -- var.elim.:  13000/130273          
c   -- var.elim.:  14000/130273          
c   -- var.elim.:  15000/130273          
c   -- var.elim.:  16000/130273          
c   -- var.elim.:  17000/130273          
c   -- var.elim.:  18000/130273          
c   -- var.elim.:  19000/130273          
c   -- var.elim.:  20000/130273          
c   -- var.elim.:  21000/130273          
c   -- var.elim.:  22000/130273          
c   -- var.elim.:  23000/130273          
c   -- var.elim.:  24000/130273          
c   -- var.elim.:  25000/130273          
c   -- var.elim.:  26000/130273          
c   -- var.elim.:  27000/130273          
c   -- var.elim.:  28000/130273          
c   -- var.elim.:  29000/130273          
c   -- var.elim.:  30000/130273          
c   -- var.elim.:  31000/130273          
c   -- var.elim.:  32000/130273          
c   -- var.elim.:  33000/130273          
c   -- var.elim.:  34000/130273          
c   -- var.elim.:  35000/130273          
c   -- var.elim.:  36000/130273          
c   -- var.elim.:  37000/130273          
c   -- var.elim.:  38000/130273          
c   -- var.elim.:  39000/130273          
c   -- var.elim.:  40000/130273          
c   -- var.elim.:  41000/130273          
c   -- var.elim.:  42000/130273          
c   -- var.elim.:  43000/130273          
c   -- var.elim.:  44000/130273          
c   -- var.elim.:  45000/130273          
c   -- var.elim.:  46000/130273          
c   -- var.elim.:  47000/130273          
c   -- var.elim.:  48000/130273          
c   -- var.elim.:  49000/130273          
c   -- var.elim.:  50000/130273          
c   -- var.elim.:  51000/130273          
c   -- var.elim.:  52000/130273          
c   -- var.elim.:  53000/130273          
c   -- var.elim.:  54000/130273          
c   -- var.elim.:  55000/130273          
c   -- var.elim.:  56000/130273          
c   -- var.elim.:  57000/130273          
c   -- var.elim.:  58000/130273          
c   -- var.elim.:  59000/130273          
c   -- var.elim.:  60000/130273          
c   -- var.elim.:  61000/130273          
c   -- var.elim.:  62000/130273          
c   -- var.elim.:  63000/130273          
c   -- var.elim.:  64000/130273          
c   -- var.elim.:  65000/130273          
c   -- var.elim.:  66000/130273          
c   -- var.elim.:  67000/130273          
c   -- var.elim.:  68000/130273          
c   -- var.elim.:  69000/130273          
c   -- var.elim.:  70000/130273          
c   -- var.elim.:  71000/130273          
c   -- var.elim.:  72000/130273          
c   -- var.elim.:  73000/130273          
c   -- var.elim.:  74000/130273          
c   -- var.elim.:  75000/130273          
c   -- var.elim.:  76000/130273          
c   -- var.elim.:  77000/130273          
c   -- var.elim.:  78000/130273          
c   -- var.elim.:  79000/130273          
c   -- var.elim.:  80000/130273          
c   -- var.elim.:  81000/130273          
c   -- var.elim.:  82000/130273          
c   -- var.elim.:  83000/130273          
c   -- var.elim.:  84000/130273          
c   -- var.elim.:  85000/130273          
c   -- var.elim.:  86000/130273          
c   -- var.elim.:  87000/130273          
c   -- var.elim.:  88000/130273          
c   -- var.elim.:  89000/130273          
c   -- var.elim.:  90000/130273          
c   -- var.elim.:  91000/130273          
c   -- var.elim.:  92000/130273          
c   -- var.elim.:  93000/130273          
c   -- var.elim.:  94000/130273          
c   -- var.elim.:  95000/130273          
c   -- var.elim.:  96000/130273          
c   -- var.elim.:  97000/130273          
c   #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.94 2/54 30739
Raw data (stat): 30739 (runsolver) R 30738 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487540676 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.95 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 4034 0 0 0 988 10 0 0 25 0 1 0 487540676 12435456 2452 4294967295 134512640 134672761 3221224544 3221222672 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3036 2452 603 41 0 2995 0
vsize: 12144
[startup+20.0017 s]
Raw data (loadavg): 0.94 0.96 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 14288 0 0 0 1961 38 0 0 25 0 1 0 487540676 46768128 10119 4294967295 134512640 134672761 3221224544 3221222880 134522883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11418 10122 603 41 0 11377 0
vsize: 45672
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.96 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 15130 0 0 0 2958 40 0 0 25 0 1 0 487540676 47095808 10291 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11498 10291 603 41 0 11457 0
vsize: 45992
[startup+40.0021 s]
Raw data (loadavg): 0.95 0.96 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 40998 0 0 0 3897 101 0 0 25 0 1 0 487540676 163164160 36118 4294967295 134512640 134672761 3221224544 3221218800 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39835 36120 603 41 0 39794 0
vsize: 159340
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.96 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 47611 0 0 0 4880 118 0 0 25 0 1 0 487540676 185008128 37738 4294967295 134512640 134672761 3221224544 3221223668 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45168 37738 603 41 0 45127 0
vsize: 180672
[startup+60.0031 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 48177 0 0 0 5877 120 0 0 25 0 1 0 487540676 187404288 38304 4294967295 134512640 134672761 3221224544 3221223712 134564467 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45753 38304 603 41 0 45712 0
vsize: 183012
[startup+70.0036 s]
Raw data (loadavg): 0.97 0.96 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 48483 0 0 0 6876 122 0 0 25 0 1 0 487540676 188608512 38610 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46047 38610 603 41 0 46006 0
vsize: 184188
[startup+80.0041 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 48760 0 0 0 7876 122 0 0 25 0 1 0 487540676 189792256 38887 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46336 38887 603 41 0 46295 0
vsize: 185344
[startup+90.0046 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 49202 0 0 0 8874 124 0 0 25 0 1 0 487540676 191516672 39329 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46757 39329 603 41 0 46716 0
vsize: 187028
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 49739 0 0 0 9873 126 0 0 25 0 1 0 487540676 193904640 39866 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47340 39866 603 41 0 47299 0
vsize: 189360
[startup+110.005 s]
Raw data (loadavg): 0.98 0.96 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 50210 0 0 0 10871 127 0 0 25 0 1 0 487540676 195764224 40337 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47794 40337 603 41 0 47753 0
vsize: 191176
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 50854 0 0 0 11869 130 0 0 25 0 1 0 487540676 198414336 40981 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48441 40981 603 41 0 48400 0
vsize: 193764
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 51496 0 0 0 12867 132 0 0 25 0 1 0 487540676 200925184 41623 4294967295 134512640 134672761 3221224544 3221223680 134614670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49054 41623 603 41 0 49013 0
vsize: 196216
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 52114 0 0 0 13865 134 0 0 25 0 1 0 487540676 203444224 42241 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49669 42241 603 41 0 49628 0
vsize: 198676
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 52602 0 0 0 14864 135 0 0 25 0 1 0 487540676 205426688 42729 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50153 42729 603 41 0 50112 0
vsize: 200612
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 53189 0 0 0 15863 137 0 0 25 0 1 0 487540676 208072704 43316 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50799 43316 603 41 0 50758 0
vsize: 203196
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 53813 0 0 0 16860 140 0 0 25 0 1 0 487540676 210608128 43940 4294967295 134512640 134672761 3221224544 3221223728 134615585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51418 43940 603 41 0 51377 0
vsize: 205672
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 54408 0 0 0 17858 142 0 0 25 0 1 0 487540676 212979712 44535 4294967295 134512640 134672761 3221224544 3221223680 134614825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51997 44536 603 41 0 51956 0
vsize: 207988
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 55011 0 0 0 18857 143 0 0 25 0 1 0 487540676 215502848 45138 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52613 45138 603 41 0 52572 0
vsize: 210452
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 55625 0 0 0 19856 144 0 0 25 0 1 0 487540676 218021888 45752 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53228 45752 603 41 0 53187 0
vsize: 212912
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 56366 0 0 0 20854 146 0 0 25 0 1 0 487540676 220930048 46493 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53938 46493 603 41 0 53897 0
vsize: 215752
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 57052 0 0 0 21853 148 0 0 25 0 1 0 487540676 223830016 47179 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54646 47179 603 41 0 54605 0
vsize: 218584
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 57735 0 0 0 22850 151 0 0 25 0 1 0 487540676 226611200 47862 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55325 47862 603 41 0 55284 0
vsize: 221300
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 58304 0 0 0 23849 153 0 0 25 0 1 0 487540676 228855808 48431 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55873 48431 603 41 0 55832 0
vsize: 223492
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 58766 0 0 0 24848 154 0 0 25 0 1 0 487540676 230748160 48893 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56335 48893 603 41 0 56294 0
vsize: 225340
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 59392 0 0 0 25846 156 0 0 25 0 1 0 487540676 233414656 49519 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56986 49519 603 41 0 56945 0
vsize: 227944
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 60107 0 0 0 26843 159 0 0 25 0 1 0 487540676 236331008 50234 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57698 50234 603 41 0 57657 0
vsize: 230792
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 60600 0 0 0 27841 161 0 0 25 0 1 0 487540676 238325760 50727 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58185 50727 603 41 0 58144 0
vsize: 232740
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 61163 0 0 0 28840 163 0 0 25 0 1 0 487540676 240566272 51290 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58732 51290 603 41 0 58691 0
vsize: 234928
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 61480 0 0 0 29839 164 0 0 25 0 1 0 487540676 242454528 51607 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59193 51607 603 41 0 59152 0
vsize: 236772
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 61671 0 0 0 30839 164 0 0 25 0 1 0 487540676 243257344 51798 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59389 51798 603 41 0 59348 0
vsize: 237556
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 62065 0 0 0 31838 165 0 0 25 0 1 0 487540676 244838400 52192 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59775 52192 603 41 0 59734 0
vsize: 239100
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 62417 0 0 0 32837 166 0 0 25 0 1 0 487540676 246308864 52544 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60134 52544 603 41 0 60093 0
vsize: 240536
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 62905 0 0 0 33836 167 0 0 25 0 1 0 487540676 248156160 53032 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60585 53032 603 41 0 60544 0
vsize: 242340
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 63348 0 0 0 34835 169 0 0 25 0 1 0 487540676 250019840 53475 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61040 53475 603 41 0 60999 0
vsize: 244160
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 63761 0 0 0 35834 170 0 0 25 0 1 0 487540676 251736064 53888 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61459 53888 603 41 0 61418 0
vsize: 245836
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 64478 0 0 0 36832 172 0 0 25 0 1 0 487540676 254644224 54605 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62169 54605 603 41 0 62128 0
vsize: 248676
[startup+380.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 64950 0 0 0 37830 174 0 0 25 0 1 0 487540676 256499712 55077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62622 55077 603 41 0 62581 0
vsize: 250488
[startup+390.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 65351 0 0 0 38839 175 0 0 25 0 1 0 487540676 258093056 55478 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63011 55478 603 41 0 62970 0
vsize: 252044
[startup+400.119 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 65697 0 0 0 39838 176 0 0 25 0 1 0 487540676 259567616 55824 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63371 55824 603 41 0 63330 0
vsize: 253484
[startup+410.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 66315 0 0 0 40838 177 0 0 25 0 1 0 487540676 262066176 56442 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63981 56442 603 41 0 63940 0
vsize: 255924
[startup+420.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 66898 0 0 0 41836 179 0 0 25 0 1 0 487540676 264454144 57025 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64564 57025 603 41 0 64523 0
vsize: 258256
[startup+430.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 67369 0 0 0 42835 180 0 0 25 0 1 0 487540676 266448896 57496 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65051 57496 603 41 0 65010 0
vsize: 260204
[startup+440.12 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 67608 0 0 0 43835 181 0 0 25 0 1 0 487540676 267378688 57735 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65278 57735 603 41 0 65237 0
vsize: 261112
[startup+450.121 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 68000 0 0 0 44834 182 0 0 25 0 1 0 487540676 268955648 58127 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65663 58127 603 41 0 65622 0
vsize: 262652
[startup+460.121 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 68438 0 0 0 45832 184 0 0 25 0 1 0 487540676 270680064 58565 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66084 58565 603 41 0 66043 0
vsize: 264336
[startup+470.122 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 69068 0 0 0 46831 185 0 0 25 0 1 0 487540676 273321984 59195 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66729 59195 603 41 0 66688 0
vsize: 266916
[startup+480.121 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 69781 0 0 0 47830 187 0 0 25 0 1 0 487540676 276213760 59908 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67435 59908 603 41 0 67394 0
vsize: 269740
[startup+490.122 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 70131 0 0 0 48829 188 0 0 25 0 1 0 487540676 277671936 60258 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67791 60258 603 41 0 67750 0
vsize: 271164
[startup+500.122 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 70630 0 0 0 49827 189 0 0 25 0 1 0 487540676 279666688 60757 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68278 60757 603 41 0 68237 0
vsize: 273112
[startup+510.123 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 71043 0 0 0 50827 190 0 0 25 0 1 0 487540676 281255936 61170 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68666 61170 603 41 0 68625 0
vsize: 274664
[startup+520.122 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 71578 0 0 0 51825 192 0 0 25 0 1 0 487540676 283504640 61705 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69215 61705 603 41 0 69174 0
vsize: 276860
[startup+530.123 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 72009 0 0 0 52824 193 0 0 25 0 1 0 487540676 285241344 62136 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69639 62136 603 41 0 69598 0
vsize: 278556
[startup+540.123 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 72537 0 0 0 53823 194 0 0 25 0 1 0 487540676 287363072 62664 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70157 62664 603 41 0 70116 0
vsize: 280628
[startup+550.123 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 73073 0 0 0 54821 197 0 0 25 0 1 0 487540676 289619968 63200 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70708 63200 603 41 0 70667 0
vsize: 282832
[startup+560.124 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 73589 0 0 0 55821 197 0 0 25 0 1 0 487540676 291598336 63716 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71191 63716 603 41 0 71150 0
vsize: 284764
[startup+570.125 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 74118 0 0 0 56819 199 0 0 25 0 1 0 487540676 293842944 64245 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71739 64245 603 41 0 71698 0
vsize: 286956
[startup+580.125 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 74749 0 0 0 57818 201 0 0 25 0 1 0 487540676 296349696 64876 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72351 64876 603 41 0 72310 0
vsize: 289404
[startup+590.125 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 75311 0 0 0 58816 203 0 0 25 0 1 0 487540676 298729472 65438 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 72932 65438 603 41 0 72891 0
vsize: 291728
[startup+600.125 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 75851 0 0 0 59815 204 0 0 25 0 1 0 487540676 300834816 65978 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73446 65978 603 41 0 73405 0
vsize: 293784
[startup+610.126 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 76355 0 0 0 60813 206 0 0 25 0 1 0 487540676 302944256 66482 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 73961 66482 603 41 0 73920 0
vsize: 295844
[startup+620.126 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 76851 0 0 0 61812 207 0 0 25 0 1 0 487540676 305049600 66978 4294967295 134512640 134672761 3221224544 3221223680 134614800 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74475 66978 603 41 0 74434 0
vsize: 297900
[startup+630.126 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 77273 0 0 0 62811 209 0 0 25 0 1 0 487540676 306765824 67400 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 74894 67400 603 41 0 74853 0
vsize: 299576
[startup+640.126 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 77734 0 0 0 63809 210 0 0 25 0 1 0 487540676 308629504 67861 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75349 67861 603 41 0 75308 0
vsize: 301396
[startup+650.127 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 78210 0 0 0 64808 212 0 0 25 0 1 0 487540676 310480896 68337 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 75801 68337 603 41 0 75760 0
vsize: 303204
[startup+660.128 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 78628 0 0 0 65807 213 0 0 25 0 1 0 487540676 313257984 68755 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76479 68756 603 41 0 76438 0
vsize: 305916
[startup+670.128 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 79026 0 0 0 66806 214 0 0 25 0 1 0 487540676 314880000 69153 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 76875 69153 603 41 0 76834 0
vsize: 307500
[startup+680.129 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 79390 0 0 0 67804 216 0 0 25 0 1 0 487540676 316469248 69517 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77263 69517 603 41 0 77222 0
vsize: 309052
[startup+690.129 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 79780 0 0 0 68804 217 0 0 25 0 1 0 487540676 318058496 69907 4294967295 134512640 134672761 3221224544 3221223356 1075349943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 77651 69907 603 41 0 77610 0
vsize: 310604
[startup+700.129 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 80176 0 0 0 69803 218 0 0 25 0 1 0 487540676 319668224 70303 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78044 70303 603 41 0 78003 0
vsize: 312176
[startup+710.13 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 80507 0 0 0 70802 219 0 0 25 0 1 0 487540676 321138688 70634 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78403 70634 603 41 0 78362 0
vsize: 313612
[startup+720.131 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 80839 0 0 0 71801 220 0 0 25 0 1 0 487540676 322453504 70966 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78724 70966 603 41 0 78683 0
vsize: 314896
[startup+730.13 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 81205 0 0 0 72800 221 0 0 25 0 1 0 487540676 323895296 71332 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79076 71332 603 41 0 79035 0
vsize: 316304
[startup+740.132 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 81559 0 0 0 73799 222 0 0 25 0 1 0 487540676 325328896 71686 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79426 71686 603 41 0 79385 0
vsize: 317704
[startup+750.132 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 81889 0 0 0 74799 223 0 0 25 0 1 0 487540676 326787072 72016 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79782 72016 603 41 0 79741 0
vsize: 319128
[startup+760.133 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 82211 0 0 0 75798 224 0 0 25 0 1 0 487540676 328015872 72338 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80082 72338 603 41 0 80041 0
vsize: 320328
[startup+770.133 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 82529 0 0 0 76797 225 0 0 25 0 1 0 487540676 329355264 72656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80409 72656 603 41 0 80368 0
vsize: 321636
[startup+780.134 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 82905 0 0 0 77795 227 0 0 25 0 1 0 487540676 330956800 73032 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 80800 73032 603 41 0 80759 0
vsize: 323200
[startup+790.134 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 83218 0 0 0 78795 228 0 0 25 0 1 0 487540676 332288000 73345 4294967295 134512640 134672761 3221224544 3221223536 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81125 73345 603 41 0 81084 0
vsize: 324500
[startup+800.135 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 83536 0 0 0 79793 229 0 0 25 0 1 0 487540676 333606912 73663 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81447 73663 603 41 0 81406 0
vsize: 325788
[startup+810.136 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 83869 0 0 0 80793 230 0 0 25 0 1 0 487540676 334934016 73996 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 81771 73996 603 41 0 81730 0
vsize: 327084
[startup+820.136 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 84213 0 0 0 81792 231 0 0 25 0 1 0 487540676 336388096 74340 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82126 74340 603 41 0 82085 0
vsize: 328504
[startup+830.136 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 84478 0 0 0 82791 232 0 0 25 0 1 0 487540676 337448960 74605 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82385 74605 603 41 0 82344 0
vsize: 329540
[startup+840.137 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 84789 0 0 0 83791 233 0 0 25 0 1 0 487540676 338640896 74916 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 82676 74916 603 41 0 82635 0
vsize: 330704
[startup+850.137 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 85131 0 0 0 84790 234 0 0 25 0 1 0 487540676 340144128 75258 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83043 75258 603 41 0 83002 0
vsize: 332172
[startup+860.139 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 85443 0 0 0 85789 235 0 0 25 0 1 0 487540676 341336064 75570 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83334 75570 603 41 0 83293 0
vsize: 333336
[startup+870.139 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 85764 0 0 0 86789 236 0 0 25 0 1 0 487540676 342650880 75891 4294967295 134512640 134672761 3221224544 3221223728 134615835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83655 75891 603 41 0 83614 0
vsize: 334620
[startup+880.14 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 86073 0 0 0 87788 237 0 0 25 0 1 0 487540676 343969792 76200 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 83977 76200 603 41 0 83936 0
vsize: 335908
[startup+890.14 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 86343 0 0 0 88787 238 0 0 25 0 1 0 487540676 345169920 76470 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84270 76470 603 41 0 84229 0
vsize: 337080
[startup+900.14 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 86639 0 0 0 89786 239 0 0 25 0 1 0 487540676 346370048 76766 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84563 76766 603 41 0 84522 0
vsize: 338252
[startup+910.14 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 87011 0 0 0 90785 241 0 0 25 0 1 0 487540676 347828224 77138 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 84919 77138 603 41 0 84878 0
vsize: 339676
[startup+920.142 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 87326 0 0 0 91784 241 0 0 25 0 1 0 487540676 349159424 77453 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85244 77453 603 41 0 85203 0
vsize: 340976
[startup+930.141 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 87718 0 0 0 92783 242 0 0 25 0 1 0 487540676 350736384 77845 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 85629 77845 603 41 0 85588 0
vsize: 342516
[startup+940.142 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 88135 0 0 0 93782 244 0 0 25 0 1 0 487540676 352456704 78262 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86049 78262 603 41 0 86008 0
vsize: 344196
[startup+950.142 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 88462 0 0 0 94781 245 0 0 25 0 1 0 487540676 353775616 78589 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86371 78589 603 41 0 86330 0
vsize: 345484
[startup+960.143 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 88807 0 0 0 95780 246 0 0 25 0 1 0 487540676 355221504 78934 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 86724 78934 603 41 0 86683 0
vsize: 346896
[startup+970.143 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 89126 0 0 0 96780 247 0 0 25 0 1 0 487540676 356425728 79253 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87018 79253 603 41 0 86977 0
vsize: 348072
[startup+980.144 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 89567 0 0 0 97777 249 0 0 25 0 1 0 487540676 358268928 79694 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87468 79694 603 41 0 87427 0
vsize: 349872
[startup+990.144 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 89888 0 0 0 98776 251 0 0 25 0 1 0 487540676 359591936 80015 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 87791 80015 603 41 0 87750 0
vsize: 351164
[startup+1000.14 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 90212 0 0 0 99775 252 0 0 25 0 1 0 487540676 360910848 80339 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88113 80339 603 41 0 88072 0
vsize: 352452
[startup+1010.14 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 90501 0 0 0 100774 253 0 0 25 0 1 0 487540676 362094592 80628 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88402 80628 603 41 0 88361 0
vsize: 353608
[startup+1020.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 90859 0 0 0 101773 254 0 0 25 0 1 0 487540676 363540480 80986 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 88755 80986 603 41 0 88714 0
vsize: 355020
[startup+1030.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 91197 0 0 0 102772 255 0 0 25 0 1 0 487540676 364863488 81324 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89078 81324 603 41 0 89037 0
vsize: 356312
[startup+1040.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 91536 0 0 0 103771 257 0 0 25 0 1 0 487540676 366333952 81663 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89437 81663 603 41 0 89396 0
vsize: 357748
[startup+1050.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 91891 0 0 0 104771 257 0 0 25 0 1 0 487540676 367783936 82018 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 89791 82018 603 41 0 89750 0
vsize: 359164
[startup+1060.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 92249 0 0 0 105769 259 0 0 25 0 1 0 487540676 369233920 82376 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90145 82376 603 41 0 90104 0
vsize: 360580
[startup+1070.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 92609 0 0 0 106768 260 0 0 25 0 1 0 487540676 370700288 82736 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90503 82736 603 41 0 90462 0
vsize: 362012
[startup+1080.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 92908 0 0 0 107767 261 0 0 25 0 1 0 487540676 371924992 83035 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 90802 83035 603 41 0 90761 0
vsize: 363208
[startup+1090.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 93241 0 0 0 108766 262 0 0 25 0 1 0 487540676 373231616 83368 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91121 83368 603 41 0 91080 0
vsize: 364484
[startup+1100.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 93596 0 0 0 109766 263 0 0 25 0 1 0 487540676 374816768 83723 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91508 83723 603 41 0 91467 0
vsize: 366032
[startup+1110.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 93915 0 0 0 110766 263 0 0 25 0 1 0 487540676 376025088 84042 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 91803 84042 603 41 0 91762 0
vsize: 367212
[startup+1120.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 94273 0 0 0 111764 265 0 0 25 0 1 0 487540676 377602048 84400 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92188 84400 603 41 0 92147 0
vsize: 368752
[startup+1130.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 94602 0 0 0 112764 265 0 0 25 0 1 0 487540676 378908672 84729 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92507 84729 603 41 0 92466 0
vsize: 370028
[startup+1140.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 94977 0 0 0 113763 267 0 0 25 0 1 0 487540676 380358656 85104 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 92861 85104 603 41 0 92820 0
vsize: 371444
[startup+1150.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 95297 0 0 0 114762 267 0 0 25 0 1 0 487540676 381693952 85424 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 93187 85424 603 41 0 93146 0
vsize: 372748
[startup+1160.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 95622 0 0 0 115762 268 0 0 25 0 1 0 487540676 383008768 85749 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 93508 85749 603 41 0 93467 0
vsize: 374032
[startup+1170.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 95918 0 0 0 116761 269 0 0 25 0 1 0 487540676 384212992 86045 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 93802 86045 603 41 0 93761 0
vsize: 375208
[startup+1180.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 96258 0 0 0 117760 270 0 0 25 0 1 0 487540676 385740800 86385 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94175 86385 603 41 0 94134 0
vsize: 376700
[startup+1190.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 96524 0 0 0 118760 271 0 0 25 0 1 0 487540676 386809856 86651 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94436 86651 603 41 0 94395 0
vsize: 377744
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.94 2/54 30739
Raw data (stat): 30739 (minisat+) R 30738 25285 25284 0 -1 0 96813 0 0 0 119759 272 0 0 25 0 1 0 487540676 387989504 86940 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 94724 86940 603 41 0 94683 0
vsize: 378896
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.32 s]
Raw data (loadavg): 0.99 0.97 0.94 1/54 30739
Raw data (stat): 30739 (minisat+) Z 30738 25285 25284 0 -1 12 96813 0 0 0 119759 288 0 0 25 0 1 0 487540676 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.32
CPU time (s): 1200.48
CPU user time (s): 1197.59
CPU system time (s): 2.88456
CPU usage (%): 100.014
Max. virtual memory (Kb): 378896
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####