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 18306

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        838780 kB
Buffers:         21144 kB
Cached:         152640 kB
SwapCached:        364 kB
Active:          10112 kB
Inactive:       166200 kB
HighTotal:      131008 kB
HighFree:       114296 kB
LowTotal:       903652 kB
LowFree:        724484 kB
SwapTotal:     2097136 kB
SwapFree:      2096356 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6372 kB
Slab:            13828 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 14:42:04 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 18252 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2294 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###########################################################################################################################
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................
c ---[2293]---> Adder-cost: 61016   maxlim: 27161905   bits: 25/25
c ---[2292]---> BDD-cost:    3
c ---[2291]---> BDD-cost:    3
c ---[2290]---> BDD-cost:    3
c ---[2289]---> BDD-cost:    3
c ---[2288]---> BDD-cost:    3
c ---[2287]---> BDD-cost:    3
c ---[2286]---> BDD-cost:    3
c ---[2285]---> BDD-cost:    3
c ---[2284]---> BDD-cost:    3
c ---[2283]---> BDD-cost:    3
c ---[2282]---> BDD-cost:    3
c ---[2281]---> BDD-cost:    3
c ---[2280]---> BDD-cost:    3
c ---[2279]---> BDD-cost:    3
c ---[2278]---> BDD-cost:    3
c ---[2277]---> BDD-cost:    3
c ---[2276]---> BDD-cost:    3
c ---[2275]---> BDD-cost:    3
c ---[2274]---> BDD-cost:    3
c ---[2273]---> BDD-cost:    3
c ---[2272]---> BDD-cost:    3
c ---[2271]---> BDD-cost:    3
c ---[2270]---> BDD-cost:    3
c ---[2269]---> BDD-cost:    3
c ---[2268]---> BDD-cost:    3
c ---[2267]---> BDD-cost:    3
c ---[2266]---> BDD-cost:    3
c ---[2265]---> BDD-cost:    3
c ---[2264]---> BDD-cost:    3
c ---[2263]---> BDD-cost:    3
c ---[2262]---> BDD-cost:    3
c ---[2261]---> BDD-cost:    3
c ---[2260]---> BDD-cost:    3
c ---[2259]---> BDD-cost:    3
c ---[2258]---> BDD-cost:    3
c ---[2257]---> BDD-cost:    3
c ---[2256]---> BDD-cost:    3
c ---[2255]---> BDD-cost:    3
c ---[2254]---> BDD-cost:    3
c ---[2253]---> BDD-cost:    3
c ---[2252]---> BDD-cost:    3
c ---[2251]---> BDD-cost:    3
c ---[2250]---> BDD-cost:    3
c ---[2249]---> BDD-cost:    3
c ---[2248]---> BDD-cost:    3
c ---[2247]---> BDD-cost:    3
c ---[2246]---> BDD-cost:    3
c ---[2245]---> BDD-cost:    3
c ---[2244]---> BDD-cost:    3
c ---[2243]---> BDD-cost:    3
c ---[2242]---> BDD-cost:    3
c ---[2241]---> BDD-cost:    3
c ---[2240]---> BDD-cost:    3
c ---[2239]---> BDD-cost:    3
c ---[2238]---> BDD-cost:    3
c ---[2237]---> BDD-cost:    3
c ---[2236]---> BDD-cost:    3
c ---[2235]---> BDD-cost:    3
c ---[2234]---> BDD-cost:    3
c ---[2233]---> BDD-cost:    3
c ---[2232]---> BDD-cost:    3
c ---[2231]---> BDD-cost:    3
c ---[2230]---> BDD-cost:    3
c ---[2229]---> BDD-cost:    3
c ---[2228]---> BDD-cost:    3
c ---[2227]---> BDD-cost:    3
c ---[2226]---> BDD-cost:    3
c ---[2225]---> BDD-cost:    3
c ---[2224]---> BDD-cost:    3
c ---[2223]---> BDD-cost:    3
c ---[2222]---> BDD-cost:    3
c ---[2221]---> BDD-cost:    3
c ---[2220]---> BDD-cost:    3
c ---[2219]---> BDD-cost:    3
c ---[2218]---> BDD-cost:    3
c ---[2217]---> BDD-cost:    3
c ---[2216]---> BDD-cost:    3
c ---[2215]---> BDD-cost:    3
c ---[2214]---> BDD-cost:    3
c ---[2213]---> BDD-cost:    3
c ---[2212]---> BDD-cost:    3
c ---[2211]---> BDD-cost:    3
c ---[2210]---> BDD-cost:    3
c ---[2209]---> BDD-cost:    3
c ---[2208]---> BDD-cost:    3
c ---[2207]---> BDD-cost:    3
c ---[2206]---> BDD-cost:    3
c ---[2205]---> BDD-cost:    3
c ---[2204]---> BDD-cost:    3
c ---[2203]---> BDD-cost:    3
c ---[2202]---> BDD-cost:    3
c ---[2201]---> BDD-cost:    3
c ---[2200]---> BDD-cost:    3
c ---[2199]---> BDD-cost:    3
c ---[2198]---> BDD-cost:    3
c ---[2197]---> BDD-cost:    3
c ---[2196]---> BDD-cost:    3
c ---[2195]---> BDD-cost:    3
c ---[2194]---> BDD-cost:    3
c ---[2193]---> BDD-cost:    3
c ---[2192]---> BDD-cost:    3
c ---[2191]---> BDD-cost:    3
c ---[2190]---> BDD-cost:    3
c ---[2189]---> BDD-cost:    3
c ---[2188]---> BDD-cost:    3
c ---[2187]---> BDD-cost:    3
c ---[2186]---> BDD-cost:    3
c ---[2185]---> BDD-cost:    3
c ---[2184]---> BDD-cost:    3
c ---[2183]---> BDD-cost:    3
c ---[2182]---> BDD-cost:    3
c ---[2181]---> BDD-cost:    3
c ---[2180]---> BDD-cost:    3
c ---[2179]---> BDD-cost:    3
c ---[2178]---> BDD-cost:    3
c ---[2177]---> BDD-cost:    3
c ---[2176]---> BDD-cost:    3
c ---[2175]---> BDD-cost:    3
c ---[2174]---> BDD-cost:    3
c ---[2173]---> BDD-cost:    3
c ---[2172]---> BDD-cost:    3
c ---[2171]---> BDD-cost:    3
c ---[2170]---> BDD-cost:    3
c ---[2169]---> BDD-cost:    3
c ---[2168]---> BDD-cost:    3
c ---[2167]---> BDD-cost:    3
c ---[2166]---> BDD-cost:    3
c ---[2165]---> BDD-cost:    3
c ---[2164]---> BDD-cost:    3
c ---[2163]---> BDD-cost:    3
c ---[2162]---> BDD-cost:    3
c ---[2161]---> BDD-cost:    3
c ---[2160]---> BDD-cost:    3
c ---[2159]---> BDD-cost:    3
c ---[2158]---> BDD-cost:    3
c ---[2157]---> BDD-cost:    3
c ---[2156]---> BDD-cost:    3
c ---[2155]---> BDD-cost:    3
c ---[2154]---> BDD-cost:    3
c ---[2153]---> BDD-cost:    3
c ---[2152]---> BDD-cost:    3
c ---[2151]---> BDD-cost:    3
c ---[2150]---> BDD-cost:    3
c ---[2149]---> BDD-cost:    3
c ---[2148]---> BDD-cost:    3
c ---[2147]---> BDD-cost:    3
c ---[2146]---> BDD-cost:    3
c ---[2145]---> BDD-cost:    3
c ---[2144]---> BDD-cost:    3
c ---[2143]---> BDD-cost:    3
c ---[2142]---> BDD-cost:    3
c ---[2141]---> BDD-cost:    3
c ---[2140]---> BDD-cost:    3
c ---[2139]---> BDD-cost:    3
c ---[2138]---> BDD-cost:    3
c ---[2137]---> BDD-cost:    3
c ---[2136]---> BDD-cost:    3
c ---[2135]---> BDD-cost:    3
c ---[2134]---> BDD-cost:    3
c ---[2133]---> BDD-cost:    3
c ---[2132]---> BDD-cost:    3
c ---[2131]---> BDD-cost:    3
c ---[2130]---> BDD-cost:    3
c ---[2129]---> BDD-cost:    3
c ---[2128]---> BDD-cost:    3
c ---[2127]---> BDD-cost:    3
c ---[2126]---> BDD-cost:    3
c ---[2125]---> BDD-cost:    3
c ---[2124]---> BDD-cost:    3
c ---[2123]---> BDD-cost:    3
c ---[2122]---> BDD-cost:    3
c ---[2121]---> BDD-cost:    3
c ---[2120]---> BDD-cost:    3
c ---[2119]---> BDD-cost:    3
c ---[2118]---> BDD-cost:    3
c ---[2117]---> BDD-cost:    3
c ---[2116]---> BDD-cost:    3
c ---[2115]---> BDD-cost:    3
c ---[2114]---> BDD-cost:    3
c ---[2113]---> BDD-cost:    3
c ---[2112]---> BDD-cost:    3
c ---[2111]---> BDD-cost:    3
c ---[2110]---> BDD-cost:    3
c ---[2109]---> BDD-cost:    3
c ---[2108]---> BDD-cost:    3
c ---[2107]---> BDD-cost:    3
c ---[2106]---> BDD-cost:    3
c ---[2105]---> BDD-cost:    3
c ---[2104]---> BDD-cost:    3
c ---[2103]---> BDD-cost:    3
c ---[2102]---> BDD-cost:    3
c ---[2101]---> BDD-cost:    3
c ---[2100]---> BDD-cost:    3
c ---[2099]---> BDD-cost:    3
c ---[2098]---> BDD-cost:    3
c ---[2097]---> BDD-cost:    3
c ---[2096]---> BDD-cost:    3
c ---[2095]---> BDD-cost:    3
c ---[2094]---> BDD-cost:    3
c ---[2093]---> BDD-cost:    3
c ---[2092]---> BDD-cost:    3
c ---[2091]---> BDD-cost:    3
c ---[2090]---> BDD-cost:    3
c ---[2089]---> BDD-cost:    3
c ---[2088]---> BDD-cost:    3
c ---[2087]---> BDD-cost:    3
c ---[2086]---> BDD-cost:    3
c ---[2085]---> BDD-cost:    3
c ---[2084]---> BDD-cost:    3
c ---[2083]---> BDD-cost:    3
c ---[2082]---> BDD-cost:    3
c ---[2081]---> BDD-cost:    3
c ---[2080]---> BDD-cost:    3
c ---[2079]---> BDD-cost:    3
c ---[2078]---> BDD-cost:    3
c ---[2077]---> BDD-cost:    3
c ---[2076]---> BDD-cost:    3
c ---[2075]---> BDD-cost:    3
c ---[2074]---> BDD-cost:    3
c ---[2073]---> BDD-cost:    3
c ---[2072]---> BDD-cost:    3
c ---[2071]---> BDD-cost:    3
c ---[2070]---> BDD-cost:    3
c ---[2069]---> BDD-cost:    3
c ---[2068]---> BDD-cost:    3
c ---[2067]---> BDD-cost:    3
c ---[2066]---> BDD-cost:    3
c ---[2065]---> BDD-cost:    3
c ---[2064]---> BDD-cost:    3
c ---[2063]---> BDD-cost:    3
c ---[2062]---> BDD-cost:    3
c ---[2061]---> BDD-cost:    3
c ---[2060]---> BDD-cost:    3
c ---[2059]---> BDD-cost:    3
c ---[2058]---> BDD-cost:    3
c ---[2057]---> BDD-cost:    3
c ---[2056]---> BDD-cost:    3
c ---[2055]---> BDD-cost:    3
c ---[2054]---> BDD-cost:    3
c ---[2053]---> BDD-cost:    3
c ---[2052]---> BDD-cost:    3
c ---[2051]---> BDD-cost:    3
c ---[2050]---> BDD-cost:    3
c ---[2049]---> BDD-cost:    3
c ---[2048]---> BDD-cost:    3
c ---[2047]---> BDD-cost:    3
c ---[2046]---> BDD-cost:    3
c ---[2045]---> BDD-cost:    3
c ---[2044]---> BDD-cost:    3
c ---[2043]---> BDD-cost:    3
c ---[2042]---> BDD-cost:    3
c ---[2041]---> BDD-cost:    3
c ---[2040]---> BDD-cost:    3
c ---[2039]---> BDD-cost:    3
c ---[2038]---> BDD-cost:    3
c ---[2037]---> BDD-cost:    3
c ---[2036]---> BDD-cost:    3
c ---[2035]---> BDD-cost:    3
c ---[2034]---> BDD-cost:    3
c ---[2033]---> BDD-cost:    3
c ---[2032]---> BDD-cost:    3
c ---[2031]---> BDD-cost:    3
c ---[2030]---> BDD-cost:    3
c ---[2029]---> BDD-cost:    3
c ---[2028]---> BDD-cost:    3
c ---[2027]---> BDD-cost:    3
c ---[2026]---> BDD-cost:    3
c ---[2025]---> BDD-cost:    3
c ---[2024]---> BDD-cost:    3
c ---[2023]---> BDD-cost:    3
c ---[2022]---> BDD-cost:    3
c ---[2021]---> BDD-cost:    3
c ---[2020]---> BDD-cost:    3
c ---[2019]---> BDD-cost:    3
c ---[2018]---> BDD-cost:    3
c ---[2017]---> BDD-cost:    3
c ---[2016]---> BDD-cost:    3
c ---[2015]---> BDD-cost:    3
c ---[2014]---> BDD-cost:    3
c ---[2013]---> BDD-cost:    3
c ---[2012]---> BDD-cost:    3
c ---[2011]---> BDD-cost:    3
c ---[2010]---> BDD-cost:    3
c ---[2009]---> BDD-cost:    3
c ---[2008]---> BDD-cost:    3
c ---[2007]---> BDD-cost:    3
c ---[2006]---> BDD-cost:    3
c ---[2004]---> BDD-cost:    3
c ---[2002]---> BDD-cost:    3
c ---[2001]---> BDD-cost:    3
c ---[1999]---> BDD-cost:    3
c ---[1997]---> BDD-cost:    3
c ---[1995]---> BDD-cost:    3
c ---[1993]---> BDD-cost:    3
c ---[1991]---> BDD-cost:    3
c ---[1989]---> BDD-cost:    3
c ---[1987]---> BDD-cost:    3
c ---[1985]---> BDD-cost:    3
c ---[1983]---> BDD-cost:    3
c ---[1981]---> BDD-cost:    3
c ---[1980]---> BDD-cost:    3
c ---[1978]---> BDD-cost:    3
c ---[1976]---> BDD-cost:    3
c ---[1974]---> BDD-cost:    3
c ---[1972]---> BDD-cost:    3
c ---[1970]---> BDD-cost:    3
c ---[1968]---> BDD-cost:    3
c ---[1966]---> BDD-cost:    3
c ---[1964]---> BDD-cost:    3
c ---[1962]---> BDD-cost:    3
c ---[1960]---> BDD-cost:    3
c ---[1959]---> BDD-cost:    3
c ---[1957]---> BDD-cost:    3
c ---[1955]---> BDD-cost:    3
c ---[1953]---> BDD-cost:    3
c ---[1951]---> BDD-cost:    3
c ---[1949]---> BDD-cost:    3
c ---[1947]---> BDD-cost:    3
c ---[1945]---> BDD-cost:    3
c ---[1943]---> BDD-cost:    3
c ---[1941]---> BDD-cost:    3
c ---[1939]---> BDD-cost:    3
c ---[1938]---> BDD-cost:    3
c ---[1936]---> BDD-cost:    3
c ---[1934]---> BDD-cost:    3
c ---[1932]---> BDD-cost:    3
c ---[1930]---> BDD-cost:    3
c ---[1928]---> BDD-cost:    3
c ---[1926]---> BDD-cost:    3
c ---[1924]---> BDD-cost:    3
c ---[1922]---> BDD-cost:    3
c ---[1919]---> BDD-cost:    3
c ---[1918]---> BDD-cost:    3
c ---[1907]---> BDD-cost:    3
c ---[1896]---> BDD-cost:    3
c ---[1885]---> BDD-cost:    3
c ---[1874]---> BDD-cost:    3
c ---[1863]---> BDD-cost:    3
c ---[1852]---> BDD-cost:    3
c ---[1841]---> BDD-cost:    3
c ---[1830]---> BDD-cost:    1
c ---[1829]---> BDD-cost:    3
c ---[1827]---> BDD-cost:    1
c ---[1825]---> BDD-cost:    1
c ---[1823]---> BDD-cost:    1
c ---[1821]---> BDD-cost:    1
c ---[1819]---> BDD-cost:    1
c ---[1817]---> BDD-cost:    1
c ---[1815]---> BDD-cost:    1
c ---[1813]---> BDD-cost:    1
c ---[1811]---> BDD-cost:    1
c ---[1809]---> BDD-cost:    1
c ---[1808]---> BDD-cost:    3
c ---[1806]---> BDD-cost:    1
c ---[1804]---> BDD-cost:    1
c ---[1802]---> BDD-cost:    1
c ---[1800]---> BDD-cost:    1
c ---[1798]---> BDD-cost:    1
c ---[1796]---> BDD-cost:    1
c ---[1794]---> BDD-cost:    1
c ---[1792]---> BDD-cost:    1
c ---[1790]---> BDD-cost:    1
c ---[1788]---> BDD-cost:    1
c ---[1787]---> BDD-cost:    3
c ---[1786]---> BDD-cost:    3
c ---[1784]---> BDD-cost:    1
c ---[1782]---> BDD-cost:    1
c ---[1780]---> BDD-cost:    1
c ---[1778]---> BDD-cost:    1
c ---[1776]---> BDD-cost:    1
c ---[1774]---> BDD-cost:    1
c ---[1772]---> BDD-cost:    1
c ---[1770]---> BDD-cost:    1
c ---[1768]---> BDD-cost:    1
c ---[1766]---> BDD-cost:    1
c ---[1765]---> BDD-cost:    3
c ---[1763]---> BDD-cost:    1
c ---[1761]---> BDD-cost:    1
c ---[1759]---> BDD-cost:    1
c ---[1757]---> BDD-cost:    1
c ---[1755]---> BDD-cost:    1
c ---[1753]---> BDD-cost:    1
c ---[1751]---> BDD-cost:    1
c ---[1749]---> BDD-cost:    1
c ---[1747]---> BDD-cost:    1
c ---[1745]---> BDD-cost:    1
c ---[1744]---> BDD-cost:    3
c ---[1742]---> BDD-cost:    1
c ---[1741]---> BDD-cost:    5
c ---[1740]---> BDD-cost:    5
c ---[1739]---> BDD-cost:    5
c ---[1738]---> BDD-cost:    5
c ---[1737]---> BDD-cost:    5
c ---[1736]---> BDD-cost:    5
c ---[1735]---> BDD-cost:    5
c ---[1734]---> BDD-cost:    5
c ---[1733]---> BDD-cost:    5
c ---[1732]---> BDD-cost:    3
c ---[1731]---> BDD-cost:    5
c ---[1730]---> BDD-cost:    5
c ---[1729]---> BDD-cost:    5
c ---[1728]---> BDD-cost:    5
c ---[1727]---> BDD-cost:    5
c ---[1726]---> BDD-cost:    5
c ---[1725]---> BDD-cost:    5
c ---[1724]---> BDD-cost:    5
c ---[1723]---> BDD-cost:    5
c ---[1722]---> BDD-cost:    5
c ---[1721]---> BDD-cost:    3
c ---[1720]---> BDD-cost:    5
c ---[1719]---> BDD-cost:    5
c ---[1718]---> BDD-cost:    5
c ---[1717]---> BDD-cost:    5
c ---[1716]---> BDD-cost:    5
c ---[1715]---> BDD-cost:    5
c ---[1714]---> BDD-cost:    5
c ---[1713]---> BDD-cost:    5
c ---[1712]---> BDD-cost:    5
c ---[1711]---> BDD-cost:    5
c ---[1710]---> BDD-cost:    3
c ---[1709]---> BDD-cost:    5
c ---[1708]---> BDD-cost:    5
c ---[1707]---> BDD-cost:    5
c ---[1706]---> BDD-cost:    5
c ---[1705]---> BDD-cost:    5
c ---[1704]---> BDD-cost:    5
c ---[1703]---> BDD-cost:    5
c ---[1702]---> BDD-cost:    5
c ---[1700]---> BDD-cost:    5
c ---[1698]---> BDD-cost:    5
c ---[1697]---> BDD-cost:    3
c ---[1695]---> BDD-cost:    5
c ---[1694]---> BDD-cost:    3
c ---[1693]---> BDD-cost:    3
c ---[1692]---> BDD-cost:    3
c ---[1691]---> BDD-cost:    3
c ---[1690]---> BDD-cost:    3
c ---[1689]---> BDD-cost:    3
c ---[1688]---> BDD-cost:    3
c ---[1687]---> BDD-cost:    3
c ---[1686]---> BDD-cost:    3
c ---[1685]---> BDD-cost:    3
c ---[1684]---> BDD-cost:    3
c ---[1683]---> BDD-cost:    3
c ---[1682]---> BDD-cost:    3
c ---[1681]---> BDD-cost:    3
c ---[1680]---> BDD-cost:    3
c ---[1679]---> BDD-cost:    3
c ---[1678]---> BDD-cost:    3
c ---[1677]---> BDD-cost:    3
c ---[1676]---> BDD-cost:    3
c ---[1675]---> BDD-cost:    3
c ---[1674]---> BDD-cost:    3
c ---[1673]---> BDD-cost:    3
c ---[1672]---> BDD-cost:    3
c ---[1671]---> BDD-cost:    3
c ---[1670]---> BDD-cost:    3
c ---[1669]---> BDD-cost:    3
c ---[1668]---> BDD-cost:    3
c ---[1667]---> BDD-cost:    3
c ---[1666]---> BDD-cost:    3
c ---[1665]---> BDD-cost:    3
c ---[1664]---> BDD-cost:    3
c ---[1663]---> BDD-cost:    3
c ---[1662]---> BDD-cost:    3
c ---[1661]---> BDD-cost:    3
c ---[1660]---> BDD-cost:    3
c ---[1659]---> BDD-cost:    3
c ---[1658]---> BDD-cost:    3
c ---[1657]---> BDD-cost:    3
c ---[1656]---> BDD-cost:    3
c ---[1655]---> BDD-cost:    3
c ---[1654]---> BDD-cost:    3
c ---[1653]---> BDD-cost:    3
c ---[1652]---> BDD-cost:    3
c ---[1651]---> BDD-cost:    3
c ---[1650]---> BDD-cost:    3
c ---[1649]---> BDD-cost:    3
c ---[1648]---> BDD-cost:    3
c ---[1647]---> BDD-cost:    3
c ---[1646]---> BDD-cost:    3
c ---[1645]---> BDD-cost:    3
c ---[1644]---> BDD-cost:    3
c ---[1643]---> BDD-cost:    3
c ---[1642]---> BDD-cost:    3
c ---[1641]---> BDD-cost:    3
c ---[1640]---> BDD-cost:    3
c ---[1639]---> BDD-cost:    3
c ---[1638]---> BDD-cost:    3
c ---[1637]---> BDD-cost:    3
c ---[1636]---> BDD-cost:    3
c ---[1635]---> BDD-cost:    3
c ---[1634]---> BDD-cost:    3
c ---[1633]---> BDD-cost:    3
c ---[1632]---> BDD-cost:    3
c ---[1631]---> BDD-cost:    3
c ---[1630]---> BDD-cost:    3
c ---[1629]---> BDD-cost:    3
c ---[1628]---> BDD-cost:    3
c ---[1627]---> BDD-cost:    3
c ---[1626]---> BDD-cost:    3
c ---[1625]---> BDD-cost:    3
c ---[1624]---> BDD-cost:    3
c ---[1623]---> BDD-cost:    3
c ---[1622]---> BDD-cost:    3
c ---[1621]---> BDD-cost:    3
c ---[1620]---> BDD-cost:    3
c ---[1619]---> BDD-cost:    3
c ---[1618]---> BDD-cost:    3
c ---[1617]---> BDD-cost:    3
c ---[1616]---> BDD-cost:    3
c ---[1615]---> BDD-cost:    3
c ---[1614]---> BDD-cost:    3
c ---[1613]---> BDD-cost:    3
c ---[1612]---> BDD-cost:    3
c ---[1611]---> BDD-cost:    3
c ---[1610]---> BDD-cost:    3
c ---[1609]---> BDD-cost:    3
c ---[1608]---> BDD-cost:    3
c ---[1607]---> BDD-cost:    3
c ---[1606]---> BDD-cost:    3
c ---[1605]---> BDD-cost:    3
c ---[1604]---> BDD-cost:    3
c ---[1603]---> BDD-cost:    3
c ---[1602]---> BDD-cost:    3
c ---[1601]---> BDD-cost:    3
c ---[1600]---> BDD-cost:    3
c ---[1599]---> BDD-cost:    3
c ---[1598]---> BDD-cost:    3
c ---[1597]---> BDD-cost:    3
c ---[1596]---> BDD-cost:    3
c ---[1595]---> BDD-cost:    3
c ---[1594]---> BDD-cost:    3
c ---[1593]---> BDD-cost:    3
c ---[1592]---> BDD-cost:    3
c ---[1591]---> BDD-cost:    3
c ---[1590]---> BDD-cost:    3
c ---[1589]---> BDD-cost:    3
c ---[1588]---> BDD-cost:    3
c ---[1587]---> BDD-cost:    3
c ---[1586]---> BDD-cost:    3
c ---[1585]---> BDD-cost:    3
c ---[1584]---> BDD-cost:    3
c ---[1583]---> BDD-cost:    3
c ---[1582]---> BDD-cost:    3
c ---[1581]---> BDD-cost:    3
c ---[1580]---> BDD-cost:    3
c ---[1579]---> BDD-cost:    3
c ---[1578]---> BDD-cost:    3
c ---[1577]---> BDD-cost:    3
c ---[1576]---> BDD-cost:    3
c ---[1575]---> BDD-cost:    3
c ---[1574]---> BDD-cost:    3
c ---[1573]---> BDD-cost:    3
c ---[1572]---> BDD-cost:    3
c ---[1571]---> BDD-cost:    3
c ---[1570]---> BDD-cost:    3
c ---[1569]---> BDD-cost:    3
c ---[1568]---> BDD-cost:    3
c ---[1567]---> BDD-cost:    3
c ---[1566]---> BDD-cost:    3
c ---[1565]---> BDD-cost:    3
c ---[1564]---> BDD-cost:    3
c ---[1563]---> BDD-cost:    3
c ---[1562]---> BDD-cost:    3
c ---[1561]---> BDD-cost:    3
c ---[1560]---> BDD-cost:    3
c ---[1559]---> BDD-cost:    3
c ---[1558]---> BDD-cost:    3
c ---[1557]---> BDD-cost:    3
c ---[1556]---> BDD-cost:    3
c ---[1555]---> BDD-cost:    3
c ---[1554]---> BDD-cost:    3
c ---[1553]---> BDD-cost:    3
c ---[1552]---> BDD-cost:    3
c ---[1551]---> BDD-cost:    3
c ---[1550]---> BDD-cost:    3
c ---[1549]---> BDD-cost:    3
c ---[1548]---> BDD-cost:    3
c ---[1547]---> BDD-cost:    3
c ---[1546]---> BDD-cost:    3
c ---[1545]---> BDD-cost:    3
c ---[1544]---> BDD-cost:    3
c ---[1543]---> BDD-cost:    3
c ---[1542]---> BDD-cost:    3
c ---[1541]---> BDD-cost:    3
c ---[1540]---> BDD-cost:    3
c ---[1539]---> BDD-cost:    3
c ---[1538]---> BDD-cost:    3
c ---[1537]---> BDD-cost:    3
c ---[1536]---> BDD-cost:    3
c ---[1535]---> BDD-cost:    3
c ---[1534]---> BDD-cost:    3
c ---[1533]---> BDD-cost:    3
c ---[1532]---> BDD-cost:    3
c ---[1531]---> BDD-cost:    3
c ---[1530]---> BDD-cost:    3
c ---[1529]---> BDD-cost:    3
c ---[1528]---> BDD-cost:    3
c ---[1527]---> BDD-cost:    3
c ---[1526]---> BDD-cost:    3
c ---[1525]---> BDD-cost:    3
c ---[1524]---> BDD-cost:    3
c ---[1523]---> BDD-cost:    3
c ---[1522]---> BDD-cost:    3
c ---[1521]---> BDD-cost:    3
c ---[1520]---> BDD-cost:    3
c ---[1518]---> BDD-cost:    3
c ---[1517]---> BDD-cost:    3
c ---[1515]---> BDD-cost:    3
c ---[1513]---> BDD-cost:    3
c ---[1511]---> BDD-cost:    3
c ---[1509]---> BDD-cost:    1
c ---[1508]---> BDD-cost:    3
c ---[1507]---> BDD-cost:    3
c ---[1506]---> BDD-cost:    3
c ---[1505]---> BDD-cost:    3
c ---[1504]---> BDD-cost:    3
c ---[1503]---> BDD-cost:    3
c ---[1502]---> BDD-cost:    3
c ---[1501]---> BDD-cost:    3
c ---[1500]---> BDD-cost:    3
c ---[1499]---> BDD-cost:    3
c ---[1498]---> BDD-cost:    3
c ---[1497]---> BDD-cost:    3
c ---[1496]---> BDD-cost:    3
c ---[1495]---> BDD-cost:    3
c ---[1494]---> BDD-cost:    3
c ---[1493]---> BDD-cost:    3
c ---[1492]---> BDD-cost:    3
c ---[1491]---> BDD-cost:    3
c ---[1490]---> BDD-cost:    3
c ---[1489]---> BDD-cost:    3
c ---[1488]---> BDD-cost:    3
c ---[1487]---> BDD-cost:    3
c ---[1486]---> BDD-cost:    3
c ---[1485]---> BDD-cost:    3
c ---[1484]---> BDD-cost:    3
c ---[1483]---> BDD-cost:    3
c ---[1482]---> BDD-cost:    3
c ---[1481]---> BDD-cost:    3
c ---[1480]---> BDD-cost:    3
c ---[1479]---> BDD-cost:    3
c ---[1478]---> BDD-cost:    3
c ---[1477]---> BDD-cost:    3
c ---[1476]---> BDD-cost:    3
c ---[1475]---> BDD-cost:    3
c ---[1474]---> BDD-cost:    3
c ---[1473]---> BDD-cost:    3
c ---[1472]---> BDD-cost:    3
c ---[1471]---> BDD-cost:    3
c ---[1470]---> BDD-cost:    3
c ---[1469]---> BDD-cost:    3
c ---[1468]---> BDD-cost:    3
c ---[1467]---> BDD-cost:    3
c ---[1466]---> BDD-cost:    3
c ---[1465]---> BDD-cost:    3
c ---[1464]---> BDD-cost:    3
c ---[1463]---> BDD-cost:    3
c ---[1462]---> BDD-cost:    3
c ---[1461]---> BDD-cost:    3
c ---[1460]---> BDD-cost:    3
c ---[1459]---> BDD-cost:    3
c ---[1458]---> BDD-cost:    3
c ---[1457]---> BDD-cost:    3
c ---[1456]---> BDD-cost:    3
c ---[1455]---> BDD-cost:    3
c ---[1454]---> BDD-cost:    3
c ---[1453]---> BDD-cost:    3
c ---[1452]---> BDD-cost:    3
c ---[1451]---> BDD-cost:    3
c ---[1450]---> BDD-cost:    3
c ---[1449]---> BDD-cost:    3
c ---[1448]---> BDD-cost:    3
c ---[1447]---> BDD-cost:    3
c ---[1446]---> BDD-cost:    3
c ---[1445]---> BDD-cost:    3
c ---[1444]---> BDD-cost:    3
c ---[1443]---> BDD-cost:    3
c ---[1442]---> BDD-cost:    3
c ---[1441]---> BDD-cost:    3
c ---[1440]---> BDD-cost:    3
c ---[1439]---> BDD-cost:    3
c ---[1438]---> BDD-cost:    3
c ---[1437]---> BDD-cost:    3
c ---[1436]---> BDD-cost:    3
c ---[1435]---> BDD-cost:    3
c ---[1434]---> BDD-cost:    3
c ---[1433]---> BDD-cost:    3
c ---[1432]---> BDD-cost:    3
c ---[1431]---> BDD-cost:    3
c ---[1430]---> BDD-cost:    3
c ---[1429]---> BDD-cost:    3
c ---[1428]---> BDD-cost:    3
c ---[1427]---> BDD-cost:    3
c ---[1426]---> BDD-cost:    3
c ---[1425]---> BDD-cost:    3
c ---[1424]---> BDD-cost:    3
c ---[1423]---> BDD-cost:    3
c ---[1422]---> BDD-cost:    3
c ---[1421]---> BDD-cost:    3
c ---[1420]---> BDD-cost:    3
c ---[1419]---> BDD-cost:    3
c ---[1418]---> BDD-cost:    3
c ---[1417]---> BDD-cost:    3
c ---[1416]---> BDD-cost:    3
c ---[1415]---> BDD-cost:    3
c ---[1414]---> BDD-cost:    3
c ---[1413]---> BDD-cost:    3
c ---[1412]---> BDD-cost:    3
c ---[1411]---> BDD-cost:    3
c ---[1410]---> BDD-cost:    3
c ---[1409]---> BDD-cost:    3
c ---[1408]---> BDD-cost:    3
c ---[1407]---> BDD-cost:    3
c ---[1406]---> BDD-cost:    3
c ---[1405]---> BDD-cost:    3
c ---[1404]---> BDD-cost:    3
c ---[1403]---> BDD-cost:    3
c ---[1402]---> BDD-cost:    3
c ---[1401]---> BDD-cost:    3
c ---[1400]---> BDD-cost:    3
c ---[1399]---> BDD-cost:    3
c ---[1398]---> BDD-cost:    3
c ---[1397]---> BDD-cost:    3
c ---[1396]---> BDD-cost:    3
c ---[1395]---> BDD-cost:    3
c ---[1394]---> BDD-cost:    3
c ---[1393]---> BDD-cost:    3
c ---[1392]---> BDD-cost:    3
c ---[1391]---> BDD-cost:    3
c ---[1390]---> BDD-cost:    3
c ---[1389]---> BDD-cost:    3
c ---[1388]---> BDD-cost:    3
c ---[1387]---> BDD-cost:    3
c ---[1386]---> BDD-cost:    3
c ---[1385]---> BDD-cost:    3
c ---[1384]---> BDD-cost:    3
c ---[1383]---> BDD-cost:    3
c ---[1382]---> BDD-cost:    3
c ---[1381]---> BDD-cost:    3
c ---[1380]---> BDD-cost:    3
c ---[1379]---> BDD-cost:    3
c ---[1378]---> BDD-cost:    3
c ---[1377]---> BDD-cost:    3
c ---[1376]---> BDD-cost:    3
c ---[1375]---> BDD-cost:    3
c ---[1374]---> BDD-cost:    3
c ---[1373]---> BDD-cost:    3
c ---[1372]---> BDD-cost:    3
c ---[1371]---> BDD-cost:    3
c ---[1370]---> BDD-cost:    3
c ---[1369]---> BDD-cost:    3
c ---[1368]---> BDD-cost:    3
c ---[1367]---> BDD-cost:    3
c ---[1366]---> BDD-cost:    3
c ---[1365]---> BDD-cost:    3
c ---[1364]---> BDD-cost:    3
c ---[1363]---> BDD-cost:    3
c ---[1362]---> BDD-cost:    3
c ---[1361]---> BDD-cost:    3
c ---[1360]---> BDD-cost:    3
c ---[1359]---> BDD-cost:    3
c ---[1358]---> BDD-cost:    3
c ---[1357]---> BDD-cost:    3
c ---[1356]---> BDD-cost:    3
c ---[1355]---> BDD-cost:    3
c ---[1354]---> BDD-cost:    3
c ---[1353]---> BDD-cost:    3
c ---[1352]---> BDD-cost:    3
c ---[1351]---> BDD-cost:    3
c ---[1350]---> BDD-cost:    3
c ---[1349]---> BDD-cost:    3
c ---[1348]---> BDD-cost:    3
c ---[1347]---> BDD-cost:    3
c ---[1346]---> BDD-cost:    3
c ---[1345]---> BDD-cost:    3
c ---[1344]---> BDD-cost:    3
c ---[1343]---> BDD-cost:    3
c ---[1342]---> BDD-cost:    3
c ---[1341]---> BDD-cost:    3
c ---[1340]---> BDD-cost:    3
c ---[1339]---> BDD-cost:    3
c ---[1338]---> BDD-cost:    3
c ---[1337]---> BDD-cost:    3
c ---[1336]---> BDD-cost:    3
c ---[1335]---> BDD-cost:    3
c ---[1334]---> BDD-cost:    3
c ---[1333]---> BDD-cost:    3
c ---[1332]---> BDD-cost:    3
c ---[1331]---> BDD-cost:    3
c ---[1330]---> BDD-cost:    3
c ---[1329]---> BDD-cost:    3
c ---[1328]---> BDD-cost:    3
c ---[1327]---> BDD-cost:    3
c ---[1326]---> BDD-cost:    3
c ---[1325]---> BDD-cost:    3
c ---[1324]---> BDD-cost:    3
c ---[1323]---> BDD-cost:    3
c ---[1322]---> BDD-cost:    3
c ---[1321]---> BDD-cost:    3
c ---[1320]---> BDD-cost:    3
c ---[1319]---> BDD-cost:    3
c ---[1318]---> BDD-cost:    3
c ---[1317]---> BDD-cost:    3
c ---[1316]---> BDD-cost:    3
c ---[1315]---> BDD-cost:    3
c ---[1314]---> BDD-cost:    3
c ---[1313]---> BDD-cost:    3
c ---[1312]---> BDD-cost:    3
c ---[1311]---> BDD-cost:    3
c ---[1310]---> BDD-cost:    3
c ---[1309]---> BDD-cost:    3
c ---[1308]---> BDD-cost:    3
c ---[1307]---> BDD-cost:    3
c ---[1306]---> BDD-cost:    3
c ---[1305]---> BDD-cost:    3
c ---[1304]---> BDD-cost:    3
c ---[1303]---> BDD-cost:    3
c ---[1302]---> BDD-cost:    3
c ---[1301]---> BDD-cost:    3
c ---[1300]---> BDD-cost:    3
c ---[1299]---> BDD-cost:    3
c ---[1298]---> BDD-cost:    3
c ---[1297]---> BDD-cost:    3
c ---[1296]---> BDD-cost:    3
c ---[1295]---> BDD-cost:    3
c ---[1294]---> BDD-cost:    3
c ---[1293]---> BDD-cost:    3
c ---[1292]---> BDD-cost:    3
c ---[1291]---> BDD-cost:    3
c ---[1290]---> BDD-cost:    3
c ---[1289]---> BDD-cost:    3
c ---[1288]---> BDD-cost:    3
c ---[1287]---> BDD-cost:    3
c ---[1286]---> BDD-cost:    3
c ---[1285]---> BDD-cost:    3
c ---[1284]---> BDD-cost:    3
c ---[1283]---> BDD-cost:    3
c ---[1282]---> BDD-cost:    3
c ---[1281]---> BDD-cost:    3
c ---[1280]---> BDD-cost:    3
c ---[1279]---> BDD-cost:    3
c ---[1278]---> BDD-cost:    3
c ---[1277]---> BDD-cost:    3
c ---[1276]---> BDD-cost:    3
c ---[1275]---> BDD-cost:    3
c ---[1274]---> BDD-cost:    3
c ---[1273]---> BDD-cost:    3
c ---[1272]---> BDD-cost:    3
c ---[1271]---> BDD-cost:    3
c ---[1270]---> BDD-cost:    3
c ---[1269]---> BDD-cost:    3
c ---[1268]---> BDD-cost:    3
c ---[1267]---> BDD-cost:    3
c ---[1266]---> BDD-cost:    3
c ---[1265]---> BDD-cost:    3
c ---[1264]---> BDD-cost:    3
c ---[1263]---> BDD-cost:    3
c ---[1262]---> BDD-cost:    3
c ---[1261]---> BDD-cost:    3
c ---[1260]---> BDD-cost:    3
c ---[1259]---> BDD-cost:    3
c ---[1258]---> BDD-cost:    3
c ---[1257]---> BDD-cost:    3
c ---[1256]---> BDD-cost:    3
c ---[1255]---> BDD-cost:    3
c ---[1254]---> BDD-cost:    3
c ---[1253]---> BDD-cost:    3
c ---[1252]---> BDD-cost:    3
c ---[1251]---> BDD-cost:    3
c ---[1250]---> BDD-cost:    3
c ---[1249]---> BDD-cost:    3
c ---[1248]---> BDD-cost:    3
c ---[1247]---> BDD-cost:    3
c ---[1246]---> BDD-cost:    3
c ---[1245]---> BDD-cost:    3
c ---[1244]---> BDD-cost:    3
c ---[1243]---> BDD-cost:    3
c ---[1242]---> BDD-cost:    3
c ---[1241]---> BDD-cost:    3
c ---[1240]---> BDD-cost:    3
c ---[1239]---> BDD-cost:    3
c ---[1238]---> BDD-cost:    3
c ---[1237]---> BDD-cost:    3
c ---[1236]---> BDD-cost:    3
c ---[1235]---> BDD-cost:    3
c ---[1234]---> BDD-cost:    3
c ---[1233]---> BDD-cost:    3
c ---[1232]---> BDD-cost:    3
c ---[1231]---> BDD-cost:    3
c ---[1230]---> BDD-cost:    3
c ---[1229]---> BDD-cost:    3
c ---[1228]---> BDD-cost:    3
c ---[1227]---> BDD-cost:    3
c ---[1226]---> BDD-cost:    3
c ---[1225]---> BDD-cost:    3
c ---[1224]---> BDD-cost:    3
c ---[1223]---> BDD-cost:    3
c ---[1222]---> BDD-cost:    3
c ---[1221]---> BDD-cost:    3
c ---[1220]---> BDD-cost:    3
c ---[1219]---> BDD-cost:    3
c ---[1218]---> BDD-cost:    3
c ---[1217]---> BDD-cost:    3
c ---[1216]---> BDD-cost:    3
c ---[1215]---> BDD-cost:    3
c ---[1214]---> BDD-cost:    3
c ---[1213]---> BDD-cost:    3
c ---[1212]---> BDD-cost:    3
c ---[1211]---> BDD-cost:    3
c ---[1210]---> BDD-cost:    3
c ---[1209]---> BDD-cost:    3
c ---[1208]---> BDD-cost:    3
c ---[1207]---> BDD-cost:    3
c ---[1206]---> BDD-cost:    3
c ---[1205]---> BDD-cost:    3
c ---[1204]---> BDD-cost:    3
c ---[1203]---> BDD-cost:    3
c ---[1202]---> BDD-cost:    3
c ---[1201]---> BDD-cost:    3
c ---[1200]---> BDD-cost:    3
c ---[1199]---> BDD-cost:    3
c ---[1198]---> BDD-cost:    3
c ---[1197]---> BDD-cost:    3
c ---[1196]---> BDD-cost:    3
c ---[1195]---> BDD-cost:    3
c ---[1194]---> BDD-cost:    3
c ---[1193]---> BDD-cost:    3
c ---[1192]---> BDD-cost:    3
c ---[1191]---> BDD-cost:    3
c ---[1190]---> BDD-cost:    3
c ---[1189]---> BDD-cost:    3
c ---[1188]---> BDD-cost:    3
c ---[1187]---> BDD-cost:    3
c ---[1186]---> BDD-cost:    3
c ---[1185]---> BDD-cost:    3
c ---[1184]---> BDD-cost:    3
c ---[1183]---> BDD-cost:    3
c ---[1182]---> BDD-cost:    3
c ---[1181]---> BDD-cost:    3
c ---[1180]---> BDD-cost:    3
c ---[1179]---> BDD-cost:    3
c ---[1178]---> BDD-cost:    3
c ---[1177]---> BDD-cost:    3
c ---[1176]---> BDD-cost:    3
c ---[1175]---> BDD-cost:    3
c ---[1174]---> BDD-cost:    3
c ---[1173]---> BDD-cost:    3
c ---[1172]---> BDD-cost:    3
c ---[1171]---> BDD-cost:    3
c ---[1170]---> BDD-cost:    3
c ---[1169]---> BDD-cost:    3
c ---[1168]---> BDD-cost:    3
c ---[1167]---> BDD-cost:    3
c ---[1166]---> BDD-cost:    3
c ---[1165]---> BDD-cost:    3
c ---[1164]---> BDD-cost:    3
c ---[1163]---> BDD-cost:    3
c ---[1162]---> BDD-cost:    3
c ---[1161]---> BDD-cost:    3
c ---[1160]---> BDD-cost:    3
c ---[1159]---> BDD-cost:    3
c ---[1158]---> BDD-cost:    3
c ---[1157]---> BDD-cost:    3
c ---[1156]---> BDD-cost:    3
c ---[1155]---> BDD-cost:    3
c ---[1154]---> BDD-cost:    3
c ---[1153]---> BDD-cost:    3
c ---[1152]---> BDD-cost:    3
c ---[1151]---> BDD-cost:    3
c ---[1150]---> BDD-cost:    3
c ---[1149]---> BDD-cost:    3
c ---[1148]---> BDD-cost:    3
c ---[1147]---> BDD-cost:    3
c ---[1146]---> BDD-cost:    3
c ---[1145]---> BDD-cost:    3
c ---[1144]---> BDD-cost:    3
c ---[1143]---> BDD-cost:    3
c ---[1142]---> BDD-cost:    3
c ---[1141]---> BDD-cost:    3
c ---[1140]---> BDD-cost:    3
c ---[1139]---> BDD-cost:    3
c ---[1138]---> BDD-cost:    3
c ---[1137]---> BDD-cost:    3
c ---[1136]---> BDD-cost:    3
c ---[1135]---> BDD-cost:    3
c ---[1134]---> BDD-cost:    3
c ---[1133]---> BDD-cost:    3
c ---[1132]---> BDD-cost:    3
c ---[1131]---> BDD-cost:    3
c ---[1130]---> BDD-cost:    3
c ---[1129]---> BDD-cost:    3
c ---[1128]---> BDD-cost:    3
c ---[1127]---> BDD-cost:    3
c ---[1126]---> BDD-cost:    3
c ---[1125]---> BDD-cost:    3
c ---[1124]---> BDD-cost:    3
c ---[1123]---> BDD-cost:    3
c ---[1122]---> BDD-cost:    3
c ---[1121]---> BDD-cost:    3
c ---[1120]---> BDD-cost:    3
c ---[1119]---> BDD-cost:    3
c ---[1118]---> BDD-cost:    3
c ---[1117]---> BDD-cost:    3
c ---[1116]---> BDD-cost:    3
c ---[1115]---> BDD-cost:    3
c ---[1114]---> BDD-cost:    3
c ---[1113]---> BDD-cost:    3
c ---[1112]---> BDD-cost:    3
c ---[1111]---> BDD-cost:    3
c ---[1110]---> BDD-cost:    3
c ---[1109]---> BDD-cost:    3
c ---[1108]---> BDD-cost:    3
c ---[1107]---> BDD-cost:    3
c ---[1106]---> BDD-cost:    3
c ---[1105]---> BDD-cost:    3
c ---[1104]---> BDD-cost:    3
c ---[1103]---> BDD-cost:    3
c ---[1102]---> BDD-cost:    3
c ---[1101]---> BDD-cost:    3
c ---[1100]---> BDD-cost:    3
c ---[1099]---> BDD-cost:    3
c ---[1098]---> BDD-cost:    3
c ---[1097]---> BDD-cost:    3
c ---[1096]---> BDD-cost:    3
c ---[1095]---> BDD-cost:    3
c ---[1094]---> BDD-cost:    3
c ---[1093]---> BDD-cost:    3
c ---[1092]---> Adder-cost: 59486   maxlim: 14773890   bits: 24/24
c ---[1091]---> BDD-cost:    3
c ---[1090]---> BDD-cost:    3
c ---[1089]---> BDD-cost:    3
c ---[1088]---> BDD-cost:    3
c ---[1087]---> BDD-cost:    3
c ---[1085]---> BDD-cost:    1
c ---[1083]---> BDD-cost:    1
c ---[1081]---> BDD-cost:    1
c ---[1079]---> BDD-cost:    1
c ---[1077]---> BDD-cost:    1
c ---[1075]---> BDD-cost:    1
c ---[1073]---> BDD-cost:    1
c ---[1072]---> BDD-cost:    3
c ---[1070]---> BDD-cost:    1
c ---[1068]---> BDD-cost:    1
c ---[1066]---> BDD-cost:    1
c ---[1064]---> BDD-cost:    1
c ---[1062]---> BDD-cost:    1
c ---[1060]---> BDD-cost:    1
c ---[1058]---> BDD-cost:    1
c ---[1056]---> BDD-cost:    1
c ---[1054]---> BDD-cost:    1
c ---[1052]---> BDD-cost:    1
c ---[1051]---> BDD-cost:    3
c ---[1049]---> BDD-cost:    1
c ---[1047]---> BDD-cost:    1
c ---[1045]---> BDD-cost:    1
c ---[1037]---> BDD-cost:    3
c ---[1026]---> BDD-cost:    3
c ---[1015]---> BDD-cost:    3
c ---[1004]---> BDD-cost:    3
c ---[ 993]---> BDD-cost:    3
c ---[ 982]---> BDD-cost:    3
c ---[ 971]---> BDD-cost:    3
c ---[ 960]---> BDD-cost:    3
c ---[ 959]---> BDD-cost:    3
c ---[ 948]---> BDD-cost:    3
c ---[ 937]---> BDD-cost:    3
c ---[ 926]---> BDD-cost:    3
c ---[ 915]---> BDD-cost:    3
c ---[ 904]---> BDD-cost:    3
c ---[ 902]---> BDD-cost:    1
c ---[ 900]---> BDD-cost:    1
c ---[ 898]---> BDD-cost:    1
c ---[ 896]---> BDD-cost:    1
c ---[ 894]---> BDD-cost:    1
c ---[ 892]---> BDD-cost:    1
c ---[ 890]---> BDD-cost:    1
c ---[ 888]---> BDD-cost:    1
c ---[ 886]---> BDD-cost:    1
c ---[ 884]---> BDD-cost:    1
c ---[ 883]---> BDD-cost:    3
c ---[ 881]---> BDD-cost:    1
c ---[ 879]---> BDD-cost:    1
c ---[ 877]---> BDD-cost:    1
c ---[ 869]---> BDD-cost:    3
c ---[ 861]---> BDD-cost:    3
c ---[ 860]---> BDD-cost:    3
c ---[ 859]---> BDD-cost:    3
c ---[ 858]---> BDD-cost:    3
c ---[ 857]---> BDD-cost:    3
c ---[ 856]---> BDD-cost:    3
c ---[ 855]---> BDD-cost:    3
c ---[ 854]---> BDD-cost:    3
c ---[ 853]---> BDD-cost:    3
c ---[ 852]---> BDD-cost:    3
c ---[ 851]---> BDD-cost:    3
c ---[ 850]---> BDD-cost:    3
c ---[ 849]---> BDD-cost:    3
c ---[ 848]---> BDD-cost:    3
c ---[ 847]---> BDD-cost:    3
c ---[ 846]---> BDD-cost:    3
c ---[ 845]---> BDD-cost:    3
c ---[ 844]---> BDD-cost:    3
c ---[ 843]---> BDD-cost:    3
c ---[ 842]---> BDD-cost:    3
c ---[ 841]---> BDD-cost:    3
c ---[ 840]---> BDD-cost:    3
c ---[ 839]---> BDD-cost:    3
c ---[ 838]---> BDD-cost:    3
c ---[ 837]---> BDD-cost:    3
c ---[ 836]---> BDD-cost:    3
c ---[ 835]---> BDD-cost:    3
c ---[ 834]---> BDD-cost:    3
c ---[ 833]---> BDD-cost:    3
c ---[ 832]---> BDD-cost:    3
c ---[ 831]---> BDD-cost:    3
c ---[ 830]---> BDD-cost:    3
c ---[ 829]---> BDD-cost:    3
c ---[ 828]---> BDD-cost:    3
c ---[ 827]---> BDD-cost:    3
c ---[ 826]---> BDD-cost:    3
c ---[ 825]---> BDD-cost:    3
c ---[ 824]---> BDD-cost:    3
c ---[ 823]---> BDD-cost:    3
c ---[ 822]---> BDD-cost:    3
c ---[ 821]---> BDD-cost:    3
c ---[ 820]---> BDD-cost:    3
c ---[ 819]---> BDD-cost:    3
c ---[ 818]---> BDD-cost:    3
c ---[ 817]---> BDD-cost:    3
c ---[ 816]---> BDD-cost:    3
c ---[ 815]---> BDD-cost:    3
c ---[ 814]---> BDD-cost:    3
c ---[ 813]---> BDD-cost:    3
c ---[ 812]---> BDD-cost:    3
c ---[ 811]---> BDD-cost:    3
c ---[ 810]---> BDD-cost:    3
c ---[ 809]---> BDD-cost:    3
c ---[ 808]---> BDD-cost:    3
c ---[ 807]---> BDD-cost:    3
c ---[ 806]---> BDD-cost:    3
c ---[ 805]---> BDD-cost:    3
c ---[ 804]---> BDD-cost:    3
c ---[ 803]---> BDD-cost:    3
c ---[ 802]---> BDD-cost:    3
c ---[ 801]---> BDD-cost:    3
c ---[ 800]---> BDD-cost:    3
c ---[ 799]---> BDD-cost:    3
c ---[ 798]---> BDD-cost:    3
c ---[ 797]---> BDD-cost:    3
c ---[ 796]---> BDD-cost:    3
c ---[ 795]---> BDD-cost:    3
c ---[ 794]---> BDD-cost:    3
c ---[ 793]---> BDD-cost:    3
c ---[ 792]---> BDD-cost:    3
c ---[ 791]---> BDD-cost:    3
c ---[ 790]---> BDD-cost:    3
c ---[ 789]---> BDD-cost:    3
c ---[ 788]---> BDD-cost:    3
c ---[ 787]---> BDD-cost:    3
c ---[ 786]---> BDD-cost:    3
c ---[ 785]---> BDD-cost:    3
c ---[ 784]---> BDD-cost:    3
c ---[ 783]---> BDD-cost:    3
c ---[ 782]---> BDD-cost:    3
c ---[ 781]---> BDD-cost:    3
c ---[ 780]---> BDD-cost:    3
c ---[ 779]---> BDD-cost:    3
c ---[ 778]---> BDD-cost:    3
c ---[ 777]---> BDD-cost:    3
c ---[ 776]---> BDD-cost:    3
c ---[ 775]---> BDD-cost:    3
c ---[ 774]---> BDD-cost:    3
c ---[ 773]---> BDD-cost:    3
c ---[ 772]---> BDD-cost:    3
c ---[ 771]---> BDD-cost:    3
c ---[ 770]---> BDD-cost:    3
c ---[ 769]---> BDD-cost:    3
c ---[ 768]---> BDD-cost:    3
c ---[ 767]---> BDD-cost:    3
c ---[ 766]---> BDD-cost:    3
c ---[ 765]---> BDD-cost:    3
c ---[ 764]---> BDD-cost:    3
c ---[ 763]---> BDD-cost:    3
c ---[ 762]---> BDD-cost:    3
c ---[ 761]---> BDD-cost:    3
c ---[ 760]---> BDD-cost:    3
c ---[ 759]---> BDD-cost:    3
c ---[ 758]---> BDD-cost:    3
c ---[ 757]---> BDD-cost:    3
c ---[ 756]---> BDD-cost:    3
c ---[ 755]---> BDD-cost:    3
c ---[ 754]---> BDD-cost:    3
c ---[ 753]---> BDD-cost:    3
c ---[ 752]---> BDD-cost:    3
c ---[ 751]---> BDD-cost:    3
c ---[ 750]---> BDD-cost:    3
c ---[ 749]---> BDD-cost:    3
c ---[ 748]---> BDD-cost:    3
c ---[ 747]---> BDD-cost:    3
c ---[ 746]---> BDD-cost:    3
c ---[ 745]---> BDD-cost:    3
c ---[ 744]---> BDD-cost:    3
c ---[ 743]---> BDD-cost:    3
c ---[ 742]---> BDD-cost:    3
c ---[ 741]---> BDD-cost:    3
c ---[ 740]---> BDD-cost:    3
c ---[ 739]---> BDD-cost:    3
c ---[ 738]---> BDD-cost:    3
c ---[ 737]---> BDD-cost:    3
c ---[ 736]---> BDD-cost:    3
c ---[ 735]---> BDD-cost:    3
c ---[ 734]---> BDD-cost:    3
c ---[ 733]---> BDD-cost:    3
c ---[ 732]---> BDD-cost:    3
c ---[ 731]---> BDD-cost:    3
c ---[ 730]---> BDD-cost:    3
c ---[ 729]---> BDD-cost:    3
c ---[ 728]---> BDD-cost:    3
c ---[ 727]---> BDD-cost:    3
c ---[ 726]---> BDD-cost:    3
c ---[ 725]---> BDD-cost:    3
c ---[ 724]---> BDD-cost:    3
c ---[ 723]---> BDD-cost:    3
c ---[ 722]---> BDD-cost:    3
c ---[ 721]---> BDD-cost:    3
c ---[ 720]---> BDD-cost:    3
c ---[ 719]---> BDD-cost:    3
c ---[ 718]---> BDD-cost:    3
c ---[ 717]---> BDD-cost:    3
c ---[ 716]---> BDD-cost:    3
c ---[ 715]---> BDD-cost:    3
c ---[ 714]---> BDD-cost:    3
c ---[ 713]---> BDD-cost:    3
c ---[ 712]---> BDD-cost:    3
c ---[ 711]---> BDD-cost:    3
c ---[ 710]---> BDD-cost:    3
c ---[ 709]---> BDD-cost:    3
c ---[ 708]---> BDD-cost:    3
c ---[ 707]---> BDD-cost:    3
c ---[ 706]---> BDD-cost:    3
c ---[ 705]---> BDD-cost:    3
c ---[ 704]---> BDD-cost:    3
c ---[ 703]---> BDD-cost:    3
c ---[ 702]---> BDD-cost:    3
c ---[ 701]---> BDD-cost:    3
c ---[ 700]---> BDD-cost:    3
c ---[ 699]---> BDD-cost:    3
c ---[ 698]---> BDD-cost:    3
c ---[ 697]---> BDD-cost:    3
c ---[ 696]---> BDD-cost:    3
c ---[ 695]---> BDD-cost:    3
c ---[ 694]---> BDD-cost:    3
c ---[ 693]---> BDD-cost:    3
c ---[ 692]---> BDD-cost:    3
c ---[ 691]---> BDD-cost:    3
c ---[ 690]---> BDD-cost:    3
c ---[ 689]---> BDD-cost:    3
c ---[ 688]---> BDD-cost:    3
c ---[ 687]---> BDD-cost:    3
c ---[ 686]---> BDD-cost:    3
c ---[ 685]---> BDD-cost:    3
c ---[ 684]---> BDD-cost:    3
c ---[ 683]---> BDD-cost:    3
c ---[ 682]---> BDD-cost:    3
c ---[ 681]---> BDD-cost:    3
c ---[ 680]---> BDD-cost:    3
c ---[ 679]---> BDD-cost:    3
c ---[ 678]---> BDD-cost:    3
c ---[ 677]---> BDD-cost:    3
c ---[ 676]---> BDD-cost:    3
c ---[ 675]---> BDD-cost:    3
c ---[ 674]---> BDD-cost:    3
c ---[ 673]---> BDD-cost:    3
c ---[ 672]---> BDD-cost:    3
c ---[ 671]---> BDD-cost:    3
c ---[ 670]---> BDD-cost:    3
c ---[ 669]---> BDD-cost:    3
c ---[ 668]---> BDD-cost:    3
c ---[ 667]---> BDD-cost:    3
c ---[ 666]---> BDD-cost:    3
c ---[ 665]---> BDD-cost:    3
c ---[ 664]---> BDD-cost:    3
c ---[ 663]---> BDD-cost:    3
c ---[ 662]---> BDD-cost:    3
c ---[ 661]---> BDD-cost:    3
c ---[ 660]---> BDD-cost:    3
c ---[ 659]---> BDD-cost:    3
c ---[ 658]---> BDD-cost:    3
c ---[ 657]---> BDD-cost:    3
c ---[ 656]---> BDD-cost:    3
c ---[ 655]---> BDD-cost:    3
c ---[ 654]---> BDD-cost:    3
c ---[ 653]---> BDD-cost:    3
c ---[ 652]---> BDD-cost:    3
c ---[ 651]---> BDD-cost:    3
c ---[ 650]---> BDD-cost:    3
c ---[ 649]---> BDD-cost:    3
c ---[ 648]---> BDD-cost:    3
c ---[ 647]---> BDD-cost:    3
c ---[ 646]---> BDD-cost:    3
c ---[ 645]---> BDD-cost:    3
c ---[ 644]---> BDD-cost:    3
c ---[ 643]---> BDD-cost:    3
c ---[ 642]---> BDD-cost:    3
c ---[ 641]---> BDD-cost:    3
c ---[ 640]---> BDD-cost:    3
c ---[ 639]---> BDD-cost:    3
c ---[ 638]---> BDD-cost:    3
c ---[ 637]---> BDD-cost:    3
c ---[ 636]---> BDD-cost:    3
c ---[ 635]---> BDD-cost:    3
c ---[ 634]---> BDD-cost:    3
c ---[ 633]---> BDD-cost:    3
c ---[ 632]---> BDD-cost:    3
c ---[ 631]---> BDD-cost:    3
c ---[ 630]---> BDD-cost:    3
c ---[ 629]---> BDD-cost:    3
c ---[ 628]---> BDD-cost:    3
c ---[ 627]---> BDD-cost:    3
c ---[ 626]---> BDD-cost:    3
c ---[ 625]---> BDD-cost:    3
c ---[ 624]---> BDD-cost:    3
c ---[ 623]---> BDD-cost:    3
c ---[ 622]---> BDD-cost:    3
c ---[ 621]---> BDD-cost:    3
c ---[ 620]---> BDD-cost:    3
c ---[ 619]---> BDD-cost:    3
c ---[ 618]---> BDD-cost:    3
c ---[ 617]---> BDD-cost:    3
c ---[ 616]---> BDD-cost:    3
c ---[ 615]---> BDD-cost:    3
c ---[ 614]---> BDD-cost:    3
c ---[ 613]---> BDD-cost:    3
c ---[ 612]---> BDD-cost:    3
c ---[ 611]---> BDD-cost:    3
c ---[ 610]---> BDD-cost:    3
c ---[ 609]---> BDD-cost:    3
c ---[ 608]---> BDD-cost:    3
c ---[ 607]---> BDD-cost:    3
c ---[ 606]---> BDD-cost:    3
c ---[ 605]---> BDD-cost:    3
c ---[ 604]---> BDD-cost:    3
c ---[ 603]---> BDD-cost:    3
c ---[ 602]---> BDD-cost:    3
c ---[ 601]---> BDD-cost:    3
c ---[ 600]---> BDD-cost:    3
c ---[ 599]---> BDD-cost:    3
c ---[ 598]---> BDD-cost:    3
c ---[ 597]---> BDD-cost:    3
c ---[ 596]---> BDD-cost:    3
c ---[ 595]---> BDD-cost:    3
c ---[ 594]---> BDD-cost:    3
c ---[ 593]---> BDD-cost:    3
c ---[ 592]---> BDD-cost:    3
c ---[ 591]---> BDD-cost:    3
c ---[ 590]---> BDD-cost:    3
c ---[ 589]---> BDD-cost:    3
c ---[ 588]---> BDD-cost:    3
c ---[ 587]---> BDD-cost:    3
c ---[ 586]---> BDD-cost:    3
c ---[ 585]---> BDD-cost:    3
c ---[ 584]---> BDD-cost:    3
c ---[ 583]---> BDD-cost:    3
c ---[ 582]---> BDD-cost:    3
c ---[ 581]---> BDD-cost:    3
c ---[ 580]---> BDD-cost:    3
c ---[ 579]---> BDD-cost:    3
c ---[ 578]---> BDD-cost:    3
c ---[ 577]---> BDD-cost:    3
c ---[ 576]---> BDD-cost:    3
c ---[ 575]---> BDD-cost:    3
c ---[ 574]---> BDD-cost:    3
c ---[ 573]---> BDD-cost:    3
c ---[ 572]---> BDD-cost:    3
c ---[ 571]---> BDD-cost:    3
c ---[ 570]---> BDD-cost:    3
c ---[ 569]---> BDD-cost:    3
c ---[ 568]---> BDD-cost:    3
c ---[ 567]---> BDD-cost:    3
c ---[ 566]---> BDD-cost:    3
c ---[ 565]---> BDD-cost:    3
c ---[ 564]---> BDD-cost:    3
c ---[ 563]---> BDD-cost:    3
c ---[ 562]---> BDD-cost:    3
c ---[ 561]---> BDD-cost:    3
c ---[ 560]---> BDD-cost:    3
c ---[ 559]---> BDD-cost:    3
c ---[ 558]---> BDD-cost:    3
c ---[ 557]---> BDD-cost:    3
c ---[ 556]---> BDD-cost:    3
c ---[ 555]---> BDD-cost:    3
c ---[ 554]---> BDD-cost:    3
c ---[ 553]---> BDD-cost:    3
c ---[ 552]---> BDD-cost:    3
c ---[ 551]---> BDD-cost:    3
c ---[ 550]---> BDD-cost:    3
c ---[ 549]---> BDD-cost:    3
c ---[ 548]---> BDD-cost:    3
c ---[ 547]---> BDD-cost:    3
c ---[ 546]---> BDD-cost:    3
c ---[ 545]---> BDD-cost:    3
c ---[ 544]---> BDD-cost:    3
c ---[ 543]---> BDD-cost:    3
c ---[ 542]---> BDD-cost:    3
c ---[ 541]---> BDD-cost:    3
c ---[ 540]---> BDD-cost:    3
c ---[ 539]---> BDD-cost:    3
c ---[ 538]---> BDD-cost:    3
c ---[ 537]---> BDD-cost:    3
c ---[ 536]---> BDD-cost:    3
c ---[ 535]---> BDD-cost:    3
c ---[ 534]---> BDD-cost:    3
c ---[ 533]---> BDD-cost:    3
c ---[ 532]---> BDD-cost:    3
c ---[ 531]---> BDD-cost:    3
c ---[ 530]---> BDD-cost:    3
c ---[ 529]---> BDD-cost:    3
c ---[ 528]---> BDD-cost:    3
c ---[ 527]---> BDD-cost:    3
c ---[ 526]---> BDD-cost:    3
c ---[ 525]---> BDD-cost:    3
c ---[ 524]---> BDD-cost:    3
c ---[ 523]---> BDD-cost:    3
c ---[ 522]---> BDD-cost:    3
c ---[ 521]---> BDD-cost:    3
c ---[ 520]---> BDD-cost:    3
c ---[ 519]---> BDD-cost:    3
c ---[ 518]---> BDD-cost:    3
c ---[ 517]---> BDD-cost:    3
c ---[ 516]---> BDD-cost:    3
c ---[ 515]---> BDD-cost:    3
c ---[ 514]---> BDD-cost:    3
c ---[ 513]---> BDD-cost:    3
c ---[ 512]---> BDD-cost:    3
c ---[ 511]---> BDD-cost:    3
c ---[ 510]---> BDD-cost:    3
c ---[ 509]---> BDD-cost:    3
c ---[ 508]---> BDD-cost:    3
c ---[ 507]---> BDD-cost:    3
c ---[ 506]---> BDD-cost:    3
c ---[ 505]---> BDD-cost:    3
c ---[ 504]---> BDD-cost:    3
c ---[ 503]---> BDD-cost:    3
c ---[ 502]---> BDD-cost:    3
c ---[ 501]---> BDD-cost:    3
c ---[ 500]---> BDD-cost:    3
c ---[ 499]---> BDD-cost:    3
c ---[ 498]---> BDD-cost:    3
c ---[ 497]---> BDD-cost:    3
c ---[ 496]---> BDD-cost:    3
c ---[ 495]---> BDD-cost:    3
c ---[ 494]---> BDD-cost:    3
c ---[ 493]---> BDD-cost:    3
c ---[ 492]---> BDD-cost:    3
c ---[ 491]---> BDD-cost:    3
c ---[ 490]---> BDD-cost:    3
c ---[ 489]---> BDD-cost:    3
c ---[ 488]---> BDD-cost:    3
c ---[ 487]---> BDD-cost:    3
c ---[ 486]---> BDD-cost:    3
c ---[ 485]---> BDD-cost:    3
c ---[ 484]---> BDD-cost:    3
c ---[ 483]---> BDD-cost:    3
c ---[ 482]---> BDD-cost:    3
c ---[ 481]---> BDD-cost:    3
c ---[ 480]---> BDD-cost:    3
c ---[ 479]---> BDD-cost:    3
c ---[ 478]---> BDD-cost:    3
c ---[ 477]---> BDD-cost:    3
c ---[ 476]---> BDD-cost:    3
c ---[ 475]---> BDD-cost:    3
c ---[ 474]---> BDD-cost:    3
c ---[ 473]---> BDD-cost:    3
c ---[ 472]---> BDD-cost:    3
c ---[ 471]---> BDD-cost:    3
c ---[ 470]---> BDD-cost:    3
c ---[ 469]---> BDD-cost:    3
c ---[ 468]---> BDD-cost:    3
c ---[ 467]---> BDD-cost:    3
c ---[ 466]---> BDD-cost:    3
c ---[ 465]---> BDD-cost:    3
c ---[ 464]---> BDD-cost:    3
c ---[ 463]---> BDD-cost:    3
c ---[ 462]---> BDD-cost:    3
c ---[ 461]---> BDD-cost:    3
c ---[ 460]---> BDD-cost:    3
c ---[ 459]---> BDD-cost:    3
c ---[ 458]---> BDD-cost:    3
c ---[ 457]---> BDD-cost:    3
c ---[ 456]---> BDD-cost:    3
c ---[ 455]---> BDD-cost:    3
c ---[ 454]---> BDD-cost:    3
c ---[ 453]---> BDD-cost:    3
c ---[ 452]---> BDD-cost:    3
c ---[ 451]---> BDD-cost:    3
c ---[ 450]---> BDD-cost:    3
c ---[ 449]---> BDD-cost:    3
c ---[ 448]---> BDD-cost:    3
c ---[ 447]---> BDD-cost:    3
c ---[ 446]---> BDD-cost:    3
c ---[ 445]---> BDD-cost:    3
c ---[ 444]---> BDD-cost:    3
c ---[ 443]---> BDD-cost:    3
c ---[ 442]---> BDD-cost:    3
c ---[ 441]---> BDD-cost:    3
c ---[ 440]---> BDD-cost:    3
c ---[ 439]---> BDD-cost:    3
c ---[ 438]---> BDD-cost:    3
c ---[ 437]---> BDD-cost:    3
c ---[ 436]---> BDD-cost:    3
c ---[ 435]---> BDD-cost:    3
c ---[ 434]---> BDD-cost:    3
c ---[ 433]---> BDD-cost:    3
c ---[ 432]---> BDD-cost:    3
c ---[ 431]---> BDD-cost:    3
c ---[ 430]---> BDD-cost:    3
c ---[ 429]---> BDD-cost:    3
c ---[ 428]---> BDD-cost:    3
c ---[ 427]---> BDD-cost:    3
c ---[ 426]---> BDD-cost:    3
c ---[ 425]---> BDD-cost:    3
c ---[ 424]---> BDD-cost:    3
c ---[ 423]---> BDD-cost:    3
c ---[ 422]---> BDD-cost:    3
c ---[ 421]---> BDD-cost:    3
c ---[ 420]---> BDD-cost:    3
c ---[ 419]---> BDD-cost:    3
c ---[ 418]---> BDD-cost:    3
c ---[ 417]---> BDD-cost:    3
c ---[ 416]---> BDD-cost:    3
c ---[ 415]---> BDD-cost:    3
c ---[ 414]---> BDD-cost:    3
c ---[ 413]---> BDD-cost:    3
c ---[ 412]---> BDD-cost:    3
c ---[ 411]---> BDD-cost:    3
c ---[ 410]---> BDD-cost:    3
c ---[ 409]---> BDD-cost:    3
c ---[ 408]---> BDD-cost:    3
c ---[ 407]---> BDD-cost:    3
c ---[ 406]---> BDD-cost:    3
c ---[ 405]---> BDD-cost:    3
c ---[ 404]---> BDD-cost:    3
c ---[ 403]---> BDD-cost:    3
c ---[ 402]---> BDD-cost:    3
c ---[ 401]---> BDD-cost:    3
c ---[ 400]---> BDD-cost:    3
c ---[ 399]---> BDD-cost:    3
c ---[ 398]---> BDD-cost:    3
c ---[ 397]---> BDD-cost:    3
c ---[ 396]---> BDD-cost:    3
c ---[ 395]---> BDD-cost:    3
c ---[ 394]---> BDD-cost:    3
c ---[ 393]---> BDD-cost:    3
c ---[ 392]---> BDD-cost:    3
c ---[ 391]---> BDD-cost:    3
c ---[ 390]---> BDD-cost:    3
c ---[ 389]---> BDD-cost:    3
c ---[ 388]---> BDD-cost:    3
c ---[ 387]---> BDD-cost:    3
c ---[ 386]---> BDD-cost:    3
c ---[ 385]---> BDD-cost:    3
c ---[ 384]---> BDD-cost:    3
c ---[ 383]---> BDD-cost:    3
c ---[ 382]---> BDD-cost:    3
c ---[ 381]---> BDD-cost:    3
c ---[ 380]---> BDD-cost:    3
c ---[ 379]---> BDD-cost:    3
c ---[ 378]---> BDD-cost:    3
c ---[ 377]---> BDD-cost:    3
c ---[ 376]---> BDD-cost:    3
c ---[ 375]---> BDD-cost:    3
c ---[ 374]---> BDD-cost:    3
c ---[ 373]---> BDD-cost:    3
c ---[ 372]---> BDD-cost:    3
c ---[ 371]---> BDD-cost:    3
c ---[ 370]---> BDD-cost:    3
c ---[ 369]---> BDD-cost:    3
c ---[ 368]---> BDD-cost:    3
c ---[ 367]---> BDD-cost:    3
c ---[ 366]---> BDD-cost:    3
c ---[ 365]---> BDD-cost:    3
c ---[ 364]---> BDD-cost:    3
c ---[ 363]---> BDD-cost:    3
c ---[ 362]---> BDD-cost:    3
c ---[ 361]---> BDD-cost:    3
c ---[ 360]---> BDD-cost:    3
c ---[ 359]---> BDD-cost:    3
c ---[ 358]---> BDD-cost:    3
c ---[ 357]---> BDD-cost:    3
c ---[ 356]---> BDD-cost:    3
c ---[ 355]---> BDD-cost:    3
c ---[ 354]---> BDD-cost:    3
c ---[ 353]---> BDD-cost:    3
c ---[ 352]---> BDD-cost:    3
c ---[ 351]---> BDD-cost:    3
c ---[ 350]---> BDD-cost:    3
c ---[ 349]---> BDD-cost:    3
c ---[ 348]---> BDD-cost:    3
c ---[ 347]---> BDD-cost:    3
c ---[ 346]---> BDD-cost:    3
c ---[ 345]---> BDD-cost:    3
c ---[ 344]---> BDD-cost:    3
c ---[ 343]---> BDD-cost:    3
c ---[ 342]---> BDD-cost:    3
c ---[ 341]---> BDD-cost:    3
c ---[ 340]---> BDD-cost:    3
c ---[ 339]---> BDD-cost:    3
c ---[ 338]---> BDD-cost:    3
c ---[ 337]---> BDD-cost:    3
c ---[ 336]---> BDD-cost:    3
c ---[ 335]---> BDD-cost:    3
c ---[ 334]---> BDD-cost:    3
c ---[ 333]---> BDD-cost:    3
c ---[ 332]---> BDD-cost:    3
c ---[ 331]---> BDD-cost:    3
c ---[ 330]---> BDD-cost:    3
c ---[ 329]---> BDD-cost:    3
c ---[ 328]---> BDD-cost:    3
c ---[ 327]---> BDD-cost:    3
c ---[ 326]---> BDD-cost:    3
c ---[ 325]---> BDD-cost:    3
c ---[ 324]---> BDD-cost:    3
c ---[ 323]---> BDD-cost:    3
c ---[ 322]---> BDD-cost:    3
c ---[ 321]---> BDD-cost:    3
c ---[ 320]---> BDD-cost:    3
c ---[ 319]---> BDD-cost:    3
c ---[ 318]---> BDD-cost:    3
c ---[ 317]---> BDD-cost:    3
c ---[ 316]---> BDD-cost:    3
c ---[ 315]---> BDD-cost:    3
c ---[ 314]---> BDD-cost:    3
c ---[ 313]---> BDD-cost:    3
c ---[ 312]---> BDD-cost:    3
c ---[ 311]---> BDD-cost:    3
c ---[ 310]---> BDD-cost:    3
c ---[ 309]---> BDD-cost:    3
c ---[ 308]---> BDD-cost:    3
c ---[ 307]---> BDD-cost:    3
c ---[ 306]---> BDD-cost:    3
c ---[ 305]---> BDD-cost:    3
c ---[ 304]---> BDD-cost:    3
c ---[ 303]---> BDD-cost:    3
c ---[ 302]---> BDD-cost:    3
c ---[ 301]---> BDD-cost:    3
c ---[ 300]---> BDD-cost:    3
c ---[ 299]---> BDD-cost:    3
c ---[ 298]---> BDD-cost:    3
c ---[ 297]---> BDD-cost:    3
c ---[ 296]---> BDD-cost:    3
c ---[ 295]---> BDD-cost:    3
c ---[ 294]---> BDD-cost:    3
c ---[ 293]---> BDD-cost:    3
c ---[ 292]---> BDD-cost:    3
c ---[ 291]---> BDD-cost:    3
c ---[ 290]---> BDD-cost:    3
c ---[ 289]---> BDD-cost:    3
c ---[ 288]---> BDD-cost:    3
c ---[ 287]---> BDD-cost:    3
c ---[ 286]---> BDD-cost:    3
c ---[ 285]---> BDD-cost:    3
c ---[ 284]---> BDD-cost:    3
c ---[ 283]---> BDD-cost:    3
c ---[ 282]---> BDD-cost:    3
c ---[ 281]---> BDD-cost:    3
c ---[ 280]---> BDD-cost:    3
c ---[ 279]---> BDD-cost:    3
c ---[ 278]---> BDD-cost:    3
c ---[ 277]---> BDD-cost:    3
c ---[ 276]---> BDD-cost:    3
c ---[ 275]---> BDD-cost:    3
c ---[ 274]---> BDD-cost:    3
c ---[ 273]---> BDD-cost:    3
c ---[ 272]---> BDD-cost:    3
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 268]---> BDD-cost:    3
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 263]---> BDD-cost:    3
c ---[ 262]---> BDD-cost:    3
c ---[ 261]---> BDD-cost:    3
c ---[ 260]---> BDD-cost:    3
c ---[ 259]---> BDD-cost:    3
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:    3
c ---[ 254]---> BDD-cost:    3
c ---[ 253]---> BDD-cost:    3
c ---[ 252]---> BDD-cost:    3
c ---[ 251]---> BDD-cost:    3
c ---[ 250]---> BDD-cost:    3
c ---[ 249]---> BDD-cost:    3
c ---[ 248]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    3
c ---[ 246]---> BDD-cost:    3
c ---[ 245]---> BDD-cost:    3
c ---[ 244]---> BDD-cost:    3
c ---[ 243]---> BDD-cost:    3
c ---[ 242]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    3
c ---[ 240]---> BDD-cost:    3
c ---[ 239]---> BDD-cost:    3
c ---[ 238]---> BDD-cost:    3
c ---[ 237]---> BDD-cost:    3
c ---[ 236]---> BDD-cost:    3
c ---[ 235]---> BDD-cost:    3
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    3
c ---[ 232]---> BDD-cost:    3
c ---[ 231]---> BDD-cost:    3
c ---[ 230]---> BDD-cost:    3
c ---[ 229]---> BDD-cost:    3
c ---[ 228]---> BDD-cost:    3
c ---[ 227]---> BDD-cost:    3
c ---[ 226]---> BDD-cost:    3
c ---[ 225]---> BDD-cost:    3
c ---[ 224]---> BDD-cost:    3
c ---[ 223]---> BDD-cost:    3
c ---[ 222]---> BDD-cost:    3
c ---[ 221]---> BDD-cost:    3
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:    3
c ---[ 218]---> BDD-cost:    3
c ---[ 217]---> BDD-cost:    3
c ---[ 216]---> BDD-cost:    3
c ---[ 215]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:    3
c ---[ 213]---> BDD-cost:    3
c ---[ 212]---> BDD-cost:    3
c ---[ 211]---> BDD-cost:    3
c ---[ 210]---> BDD-cost:    3
c ---[ 209]---> BDD-cost:    3
c ---[ 208]---> BDD-cost:    3
c ---[ 207]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    3
c ---[ 204]---> BDD-cost:    3
c ---[ 203]---> BDD-cost:    3
c ---[ 202]---> BDD-cost:    3
c ---[ 201]---> BDD-cost:    3
c ---[ 200]---> BDD-cost:    3
c ---[ 199]---> BDD-cost:    3
c ---[ 198]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    3
c ---[ 196]---> BDD-cost:    3
c ---[ 195]---> BDD-cost:    3
c ---[ 194]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    3
c ---[ 192]---> BDD-cost:    3
c ---[ 191]---> BDD-cost:    3
c ---[ 190]---> BDD-cost:    3
c ---[ 189]---> BDD-cost:    3
c ---[ 188]---> BDD-cost:    3
c ---[ 187]---> BDD-cost:    3
c ---[ 186]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 184]---> BDD-cost:    3
c ---[ 183]---> BDD-cost:    3
c ---[ 182]---> BDD-cost:    3
c ---[ 181]---> BDD-cost:    3
c ---[ 180]---> BDD-cost:    3
c ---[ 179]---> BDD-cost:    3
c ---[ 178]---> BDD-cost:    3
c ---[ 177]---> BDD-cost:    3
c ---[ 176]---> BDD-cost:    3
c ---[ 175]---> BDD-cost:    3
c ---[ 174]---> BDD-cost:    3
c ---[ 173]---> BDD-cost:    3
c ---[ 172]---> BDD-cost:    3
c ---[ 171]---> BDD-cost:    3
c ---[ 170]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 168]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:    3
c ---[ 157]---> BDD-cost:    3
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    3
c ---[ 145]---> BDD-cost:    3
c ---[ 144]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:    3
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    3
c ---[ 137]---> BDD-cost:    3
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 131]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 125]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    3
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    3
c ---[ 118]---> BDD-cost:    3
c ---[ 117]---> BDD-cost:    3
c ---[ 116]---> BDD-cost:    3
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:    3
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    3
c ---[ 110]---> BDD-cost:    3
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    3
c ---[ 107]---> BDD-cost:    3
c ---[ 106]---> BDD-cost:    3
c ---[ 105]---> BDD-cost:    3
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    3
c ---[ 101]---> BDD-cost:    3
c ---[ 100]---> BDD-cost:    3
c ---[  99]---> BDD-cost:    3
c ---[  98]---> BDD-cost:    3
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    3
c ---[  95]---> BDD-cost:    3
c ---[  94]---> BDD-cost:    3
c ---[  93]---> BDD-cost:    3
c ---[  92]---> BDD-cost:    3
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  89]---> BDD-cost:    3
c ---[  88]---> BDD-cost:    3
c ---[  87]---> BDD-cost:    3
c ---[  86]---> BDD-cost:    3
c ---[  85]---> BDD-cost:    3
c ---[  84]---> BDD-cost:    3
c ---[  83]---> BDD-cost:    3
c ---[  82]---> BDD-cost:    3
c ---[  81]---> BDD-cost:    3
c ---[  80]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  77]---> BDD-cost:    3
c ---[  76]---> BDD-cost:    3
c ---[  75]---> BDD-cost:    3
c ---[  74]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  71]---> BDD-cost:    3
c ---[  70]---> BDD-cost:    3
c ---[  69]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  65]---> BDD-cost:    3
c ---[  64]---> BDD-cost:    3
c ---[  63]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  59]---> BDD-cost:    3
c ---[  58]---> BDD-cost:    3
c ---[  57]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  53]---> BDD-cost:    3
c ---[  52]---> BDD-cost:    3
c ---[  51]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    3
c ---[  44]---> BDD-cost:    3
c ---[  43]---> BDD-cost:    3
c ---[  42]---> BDD-cost:    3
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:    3
c ---[  39]---> BDD-cost:    3
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    3
c ---[  36]---> BDD-cost:    3
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:    3
c ---[  33]---> BDD-cost:    3
c ---[  32]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    3
c ---[  26]---> BDD-cost:    3
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    3
c ---[  22]---> BDD-cost:    3
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  19]---> BDD-cost:    3
c ---[  18]---> BDD-cost:    3
c ---[  17]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:    3
c ---[  12]---> BDD-cost:    3
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:    3
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    3
c ---[   7]---> BDD-cost:    3
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    3
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  860965  3057211 |  286988       0        0     nan |  0.000 % |
c |       100 |  860939  3057123 |  315686      97      309     3.2 |  1.497 % |
c |       250 |  860796  3056636 |  347255     227      782     3.4 |  1.517 % |
c |       475 |  860782  3056592 |  381981     450     2074     4.6 |  1.519 % |
c |       812 |  860777  3056577 |  420179     786     3295     4.2 |  1.520 % |
c |      1318 |  860777  3056577 |  462197    1292     6676     5.2 |  1.520 % |
c |      2077 |  860695  3056286 |  508416    2049    12208     6.0 |  1.524 % |
c |      3216 |  860608  3055986 |  559258    3183    19915     6.3 |  1.528 % |
c |      4924 |  860598  3055956 |  615184    4888    36355     7.4 |  1.530 % |
c |      7486 |  860577  3055889 |  676702    7447    86375    11.6 |  1.533 % |
c |     11330 |  860577  3055889 |  744372   11291   199376    17.7 |  1.533 % |
c |     17096 |  860528  3055721 |  818810   17054   338104    19.8 |  1.535 % |
c |     25746 |  860518  3055691 |  900691   25701   637267    24.8 |  1.537 % |
c |     38721 |  860450  3055445 |  990760   38675  1045820    27.0 |  1.537 % |
c |     58182 |  860156  3054397 | 1089836   58130  1864825    32.1 |  1.542 % |
c |     87376 |  860098  3054191 | 1198820   87323  2880877    33.0 |  1.543 % |
c |    131167 |  860093  3054176 | 1318702  131112  4505005    34.4 |  1.544 % |
c |    196852 |  859963  3053711 | 1450572  196794  7271619    37.0 |  1.546 % |
c |    295378 |  859850  3053310 | 1595629  295317 17207349    58.3 |  1.548 % |
#### 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.96 1.01 0.94 2/54 9464
Raw data (stat): 9464 (runsolver) R 9463 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487536879 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.96 1.01 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 3990 0 0 0 989 9 0 0 25 0 1 0 487536879 12062720 2369 4294967295 134512640 134672761 3221224544 3221222528 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2945 2369 603 41 0 2904 0
vsize: 11780
[startup+20.0008 s]
Raw data (loadavg): 0.97 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 14376 0 4 0 1960 36 0 0 24 0 1 0 487536879 46698496 10175 4294967295 134512640 134672761 3221224544 3221223728 134593677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11401 10175 603 41 0 11360 0
vsize: 45604
[startup+30.0012 s]
Raw data (loadavg): 0.97 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 15083 0 4 0 2958 38 0 0 25 0 1 0 487536879 46755840 10212 4294967295 134512640 134672761 3221224544 3221222960 134597184 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11415 10212 603 41 0 11374 0
vsize: 45660
[startup+40.0011 s]
Raw data (loadavg): 0.98 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 30827 0 4 0 3919 77 0 0 25 0 1 0 487536879 126926848 25899 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30988 25899 603 41 0 30947 0
vsize: 123952
[startup+50.0024 s]
Raw data (loadavg): 0.98 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 31310 0 4 0 4917 79 0 0 25 0 1 0 487536879 128827392 26382 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31452 26382 603 41 0 31411 0
vsize: 125808
[startup+60.0028 s]
Raw data (loadavg): 0.98 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 31798 0 4 0 5915 81 0 0 25 0 1 0 487536879 130895872 26870 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31957 26870 603 41 0 31916 0
vsize: 127828
[startup+70.0027 s]
Raw data (loadavg): 0.98 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 32486 0 4 0 6912 84 0 0 25 0 1 0 487536879 133844992 27558 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32677 27558 603 41 0 32636 0
vsize: 130708
[startup+80.004 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 33003 0 4 0 7911 86 0 0 25 0 1 0 487536879 135864320 28075 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33170 28075 603 41 0 33129 0
vsize: 132680
[startup+90.0034 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 33504 0 4 0 8909 87 0 0 25 0 1 0 487536879 137883648 28576 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33663 28576 603 41 0 33622 0
vsize: 134652
[startup+100.004 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 33937 0 4 0 9907 89 0 0 25 0 1 0 487536879 139624448 29009 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34088 29009 603 41 0 34047 0
vsize: 136352
[startup+110.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 34411 0 4 0 10906 91 0 0 25 0 1 0 487536879 141770752 29483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34612 29483 603 41 0 34571 0
vsize: 138448
[startup+120.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 34786 0 4 0 11904 93 0 0 25 0 1 0 487536879 143478784 29858 4294967295 134512640 134672761 3221224544 3221223648 134559818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35029 29858 603 41 0 34988 0
vsize: 140116
[startup+130.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 35161 0 4 0 12903 94 0 0 25 0 1 0 487536879 144879616 30233 4294967295 134512640 134672761 3221224544 3221223544 1075349774 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35371 30233 603 41 0 35330 0
vsize: 141484
[startup+140.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 35516 0 4 0 13902 95 0 0 25 0 1 0 487536879 146366464 30588 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35734 30588 603 41 0 35693 0
vsize: 142936
[startup+150.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 35894 0 4 0 14901 96 0 0 25 0 1 0 487536879 147853312 30966 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36097 30966 603 41 0 36056 0
vsize: 144388
[startup+160.006 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 36260 0 4 0 15900 98 0 0 25 0 1 0 487536879 149352448 31332 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36463 31332 603 41 0 36422 0
vsize: 145852
[startup+170.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 36603 0 4 0 16899 99 0 0 25 0 1 0 487536879 150831104 31675 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36824 31675 603 41 0 36783 0
vsize: 147296
[startup+180.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 36903 0 4 0 17898 99 0 0 25 0 1 0 487536879 152055808 31975 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37123 31975 603 41 0 37082 0
vsize: 148492
[startup+190.007 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 37207 0 4 0 18897 100 0 0 25 0 1 0 487536879 153305088 32279 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37428 32279 603 41 0 37387 0
vsize: 149712
[startup+200.008 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 37563 0 4 0 19896 102 0 0 25 0 1 0 487536879 155389952 32635 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37937 32635 603 41 0 37896 0
vsize: 151748
[startup+210.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 37896 0 4 0 20895 103 0 0 25 0 1 0 487536879 156639232 32968 4294967295 134512640 134672761 3221224544 3221223648 134560373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38242 32968 603 41 0 38201 0
vsize: 152968
[startup+220.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 38204 0 4 0 21894 104 0 0 25 0 1 0 487536879 157855744 33276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38539 33276 603 41 0 38498 0
vsize: 154156
[startup+230.01 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 38506 0 4 0 22893 105 0 0 25 0 1 0 487536879 159109120 33578 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38845 33578 603 41 0 38804 0
vsize: 155380
[startup+240.009 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 38861 0 4 0 23892 107 0 0 25 0 1 0 487536879 160567296 33933 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39201 33933 603 41 0 39160 0
vsize: 156804
[startup+250.01 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 39085 0 4 0 24891 107 0 0 25 0 1 0 487536879 161517568 34157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39433 34157 603 41 0 39392 0
vsize: 157732
[startup+260.011 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 39258 0 4 0 25891 108 0 0 25 0 1 0 487536879 162185216 34330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39596 34330 603 41 0 39555 0
vsize: 158384
[startup+270.011 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 39462 0 4 0 26890 109 0 0 25 0 1 0 487536879 162988032 34534 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39792 34534 603 41 0 39751 0
vsize: 159168
[startup+280.011 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 39707 0 4 0 27889 110 0 0 25 0 1 0 487536879 164061184 34779 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40054 34779 603 41 0 40013 0
vsize: 160216
[startup+290.012 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 39977 0 4 0 28889 110 0 0 25 0 1 0 487536879 165134336 35049 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40316 35049 603 41 0 40275 0
vsize: 161264
[startup+300.012 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 40228 0 4 0 29888 111 0 0 25 0 1 0 487536879 166121472 35300 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40557 35300 603 41 0 40516 0
vsize: 162228
[startup+310.012 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 40464 0 4 0 30888 112 0 0 25 0 1 0 487536879 167157760 35536 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40810 35536 603 41 0 40769 0
vsize: 163240
[startup+320.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 40690 0 4 0 31887 113 0 0 25 0 1 0 487536879 168157184 35762 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41054 35762 603 41 0 41013 0
vsize: 164216
[startup+330.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 40943 0 4 0 32885 114 0 0 25 0 1 0 487536879 169144320 36015 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41295 36015 603 41 0 41254 0
vsize: 165180
[startup+340.013 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 41331 0 4 0 33884 116 0 0 25 0 1 0 487536879 170762240 36403 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41690 36403 603 41 0 41649 0
vsize: 166760
[startup+350.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 41729 0 4 0 34883 117 0 0 25 0 1 0 487536879 172371968 36801 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42083 36801 603 41 0 42042 0
vsize: 168332
[startup+360.015 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 42147 0 4 0 35881 119 0 0 25 0 1 0 487536879 174125056 37219 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42511 37219 603 41 0 42470 0
vsize: 170044
[startup+370.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 42501 0 4 0 36880 120 0 0 25 0 1 0 487536879 175460352 37573 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42837 37573 603 41 0 42796 0
vsize: 171348
[startup+380.015 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 42845 0 4 0 37879 121 0 0 25 0 1 0 487536879 176943104 37917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43199 37917 603 41 0 43158 0
vsize: 172796
[startup+390.014 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 43187 0 4 0 38878 122 0 0 25 0 1 0 487536879 178294784 38259 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43529 38259 603 41 0 43488 0
vsize: 174116
[startup+400.015 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 43479 0 4 0 39877 124 0 0 25 0 1 0 487536879 179503104 38551 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43824 38551 603 41 0 43783 0
vsize: 175296
[startup+410.016 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 43765 0 4 0 40876 125 0 0 25 0 1 0 487536879 180715520 38837 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44120 38837 603 41 0 44079 0
vsize: 176480
[startup+420.016 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 44043 0 4 0 41875 126 0 0 25 0 1 0 487536879 181846016 39115 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44396 39115 603 41 0 44355 0
vsize: 177584
[startup+430.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 44268 0 4 0 42874 127 0 0 25 0 1 0 487536879 182784000 39340 4294967295 134512640 134672761 3221224544 3221223648 134560306 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44625 39340 603 41 0 44584 0
vsize: 178500
[startup+440.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 44473 0 4 0 43873 128 0 0 25 0 1 0 487536879 183590912 39545 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44822 39545 603 41 0 44781 0
vsize: 179288
[startup+450.017 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 44732 0 4 0 44872 129 0 0 25 0 1 0 487536879 184668160 39804 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45085 39804 603 41 0 45044 0
vsize: 180340
[startup+460.018 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 44988 0 4 0 45871 130 0 0 25 0 1 0 487536879 185741312 40060 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45347 40060 603 41 0 45306 0
vsize: 181388
[startup+470.019 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 45211 0 4 0 46871 130 0 0 25 0 1 0 487536879 186683392 40283 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45577 40283 603 41 0 45536 0
vsize: 182308
[startup+480.019 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 45456 0 4 0 47870 131 0 0 25 0 1 0 487536879 187654144 40528 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45814 40528 603 41 0 45773 0
vsize: 183256
[startup+490.019 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 45691 0 4 0 48868 133 0 0 25 0 1 0 487536879 188620800 40763 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46050 40763 603 41 0 46009 0
vsize: 184200
[startup+500.02 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 45957 0 4 0 49868 133 0 0 25 0 1 0 487536879 189702144 41029 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46314 41029 603 41 0 46273 0
vsize: 185256
[startup+510.021 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 46209 0 4 0 50867 135 0 0 25 0 1 0 487536879 190771200 41281 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46575 41281 603 41 0 46534 0
vsize: 186300
[startup+520.021 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 46454 0 4 0 51866 136 0 0 25 0 1 0 487536879 191713280 41526 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46805 41526 603 41 0 46764 0
vsize: 187220
[startup+530.022 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 46688 0 4 0 52866 136 0 0 25 0 1 0 487536879 192786432 41760 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47067 41760 603 41 0 47026 0
vsize: 188268
[startup+540.022 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 46910 0 4 0 53865 137 0 0 25 0 1 0 487536879 193585152 41982 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47262 41982 603 41 0 47221 0
vsize: 189048
[startup+550.023 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 47145 0 4 0 54864 138 0 0 25 0 1 0 487536879 194519040 42217 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47490 42217 603 41 0 47449 0
vsize: 189960
[startup+560.023 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 47403 0 4 0 55863 140 0 0 25 0 1 0 487536879 195596288 42475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47753 42475 603 41 0 47712 0
vsize: 191012
[startup+570.023 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 47625 0 4 0 56862 141 0 0 25 0 1 0 487536879 196550656 42697 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47986 42697 603 41 0 47945 0
vsize: 191944
[startup+580.024 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 47847 0 4 0 57861 142 0 0 25 0 1 0 487536879 197488640 42919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48215 42919 603 41 0 48174 0
vsize: 192860
[startup+590.023 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 48063 0 4 0 58860 143 0 0 25 0 1 0 487536879 199344128 43135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48668 43135 603 41 0 48627 0
vsize: 194672
[startup+600.025 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 48298 0 4 0 59859 144 0 0 25 0 1 0 487536879 200273920 43370 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48895 43370 603 41 0 48854 0
vsize: 195580
[startup+610.025 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 48509 0 4 0 60859 145 0 0 25 0 1 0 487536879 201207808 43581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49123 43581 603 41 0 49082 0
vsize: 196492
[startup+620.025 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 48698 0 4 0 61858 145 0 0 25 0 1 0 487536879 202014720 43770 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49320 43770 603 41 0 49279 0
vsize: 197280
[startup+630.025 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 48888 0 4 0 62857 146 0 0 25 0 1 0 487536879 202678272 43960 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49482 43960 603 41 0 49441 0
vsize: 197928
[startup+640.026 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 49092 0 4 0 63857 147 0 0 25 0 1 0 487536879 203493376 44164 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49681 44164 603 41 0 49640 0
vsize: 198724
[startup+650.027 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 49373 0 4 0 64857 147 0 0 25 0 1 0 487536879 204726272 44445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49982 44445 603 41 0 49941 0
vsize: 199928
[startup+660.027 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 49644 0 4 0 65856 148 0 0 25 0 1 0 487536879 205807616 44716 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50246 44716 603 41 0 50205 0
vsize: 200984
[startup+670.026 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 49931 0 4 0 66855 149 0 0 25 0 1 0 487536879 207020032 45003 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50542 45003 603 41 0 50501 0
vsize: 202168
[startup+680.027 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 50201 0 4 0 67853 151 0 0 25 0 1 0 487536879 208093184 45273 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50804 45273 603 41 0 50763 0
vsize: 203216
[startup+690.027 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 50483 0 4 0 68852 153 0 0 25 0 1 0 487536879 209166336 45555 4294967295 134512640 134672761 3221224544 3221223728 134558856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51066 45555 603 41 0 51025 0
vsize: 204264
[startup+700.028 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 50745 0 4 0 69851 153 0 0 25 0 1 0 487536879 210243584 45817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51329 45817 603 41 0 51288 0
vsize: 205316
[startup+710.029 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 51001 0 4 0 70850 154 0 0 25 0 1 0 487536879 211378176 46073 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51606 46073 603 41 0 51565 0
vsize: 206424
[startup+720.029 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 51097 0 4 0 71850 155 0 0 25 0 1 0 487536879 211787776 46169 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51706 46169 603 41 0 51665 0
vsize: 206824
[startup+730.029 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 51583 0 4 0 72848 157 0 0 25 0 1 0 487536879 213819392 46655 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52202 46655 603 41 0 52161 0
vsize: 208808
[startup+740.029 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 51668 0 4 0 73848 157 0 0 25 0 1 0 487536879 214085632 46740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52267 46740 603 41 0 52226 0
vsize: 209068
[startup+750.031 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 51817 0 4 0 74847 158 0 0 25 0 1 0 487536879 214769664 46889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52434 46889 603 41 0 52393 0
vsize: 209736
[startup+760.032 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 51913 0 4 0 75847 158 0 0 25 0 1 0 487536879 215166976 46985 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52531 46985 603 41 0 52490 0
vsize: 210124
[startup+770.031 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 52042 0 4 0 76847 159 0 0 25 0 1 0 487536879 215568384 47114 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52629 47114 603 41 0 52588 0
vsize: 210516
[startup+780.032 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 52168 0 4 0 77847 159 0 0 25 0 1 0 487536879 216104960 47240 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52760 47240 603 41 0 52719 0
vsize: 211040
[startup+790.032 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 52289 0 4 0 78846 159 0 0 25 0 1 0 487536879 216653824 47361 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52894 47361 603 41 0 52853 0
vsize: 211576
[startup+800.033 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 52418 0 4 0 79846 160 0 0 25 0 1 0 487536879 217190400 47490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53025 47490 603 41 0 52984 0
vsize: 212100
[startup+810.033 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 52547 0 4 0 80845 161 0 0 25 0 1 0 487536879 217731072 47619 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53157 47619 603 41 0 53116 0
vsize: 212628
[startup+820.034 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 52675 0 4 0 81845 162 0 0 25 0 1 0 487536879 218132480 47747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53255 47747 603 41 0 53214 0
vsize: 213020
[startup+830.034 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 52797 0 4 0 82845 162 0 0 25 0 1 0 487536879 218664960 47869 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53385 47869 603 41 0 53344 0
vsize: 213540
[startup+840.034 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 52930 0 4 0 83844 162 0 0 25 0 1 0 487536879 219222016 48002 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53521 48002 603 41 0 53480 0
vsize: 214084
[startup+850.035 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 53068 0 4 0 84844 163 0 0 25 0 1 0 487536879 219779072 48140 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53657 48140 603 41 0 53616 0
vsize: 214628
[startup+860.035 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 53230 0 4 0 85843 164 0 0 25 0 1 0 487536879 220463104 48302 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53824 48302 603 41 0 53783 0
vsize: 215296
[startup+870.035 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 53382 0 4 0 86843 164 0 0 25 0 1 0 487536879 221155328 48454 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53993 48454 603 41 0 53952 0
vsize: 215972
[startup+880.036 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 53531 0 4 0 87843 164 0 0 25 0 1 0 487536879 221753344 48603 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54139 48603 603 41 0 54098 0
vsize: 216556
[startup+890.036 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 53694 0 4 0 88842 165 0 0 25 0 1 0 487536879 222314496 48766 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54276 48766 603 41 0 54235 0
vsize: 217104
[startup+900.038 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 53884 0 4 0 89842 166 0 0 25 0 1 0 487536879 223113216 48956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54471 48956 603 41 0 54430 0
vsize: 217884
[startup+910.038 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 54063 0 4 0 90841 166 0 0 25 0 1 0 487536879 223969280 49135 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54680 49135 603 41 0 54639 0
vsize: 218720
[startup+920.038 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 54231 0 4 0 91840 167 0 0 25 0 1 0 487536879 224636928 49303 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54843 49303 603 41 0 54802 0
vsize: 219372
[startup+930.038 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 54390 0 4 0 92840 168 0 0 25 0 1 0 487536879 225234944 49462 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54989 49462 603 41 0 54948 0
vsize: 219956
[startup+940.038 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 54540 0 4 0 93839 169 0 0 25 0 1 0 487536879 225894400 49612 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55150 49612 603 41 0 55109 0
vsize: 220600
[startup+950.038 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 54696 0 4 0 94839 169 0 0 25 0 1 0 487536879 226430976 49768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55281 49768 603 41 0 55240 0
vsize: 221124
[startup+960.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 54851 0 4 0 95839 170 0 0 25 0 1 0 487536879 227131392 49923 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55452 49923 603 41 0 55411 0
vsize: 221808
[startup+970.039 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 54995 0 4 0 96838 170 0 0 25 0 1 0 487536879 227667968 50067 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55583 50067 603 41 0 55542 0
vsize: 222332
[startup+980.039 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 55145 0 4 0 97837 171 0 0 25 0 1 0 487536879 228380672 50217 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55757 50217 603 41 0 55716 0
vsize: 223028
[startup+990.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 55295 0 4 0 98837 172 0 0 25 0 1 0 487536879 228921344 50367 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55889 50367 603 41 0 55848 0
vsize: 223556
[startup+1000.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 55448 0 4 0 99837 172 0 0 25 0 1 0 487536879 229646336 50520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56066 50520 603 41 0 56025 0
vsize: 224264
[startup+1010.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 55595 0 4 0 100836 173 0 0 25 0 1 0 487536879 230182912 50667 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56197 50667 603 41 0 56156 0
vsize: 224788
[startup+1020.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 55746 0 4 0 101836 173 0 0 25 0 1 0 487536879 230715392 50818 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56327 50818 603 41 0 56286 0
vsize: 225308
[startup+1030.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 55883 0 4 0 102835 174 0 0 25 0 1 0 487536879 231342080 50955 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56480 50955 603 41 0 56439 0
vsize: 225920
[startup+1040.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 56017 0 4 0 103836 174 0 0 25 0 1 0 487536879 231874560 51089 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56610 51089 603 41 0 56569 0
vsize: 226440
[startup+1050.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 56174 0 4 0 104835 175 0 0 25 0 1 0 487536879 232558592 51246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56777 51246 603 41 0 56736 0
vsize: 227108
[startup+1060.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 56315 0 4 0 105834 176 0 0 25 0 1 0 487536879 233095168 51387 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56908 51387 603 41 0 56867 0
vsize: 227632
[startup+1070.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 56456 0 4 0 106833 176 0 0 25 0 1 0 487536879 233738240 51528 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57065 51528 603 41 0 57024 0
vsize: 228260
[startup+1080.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 56613 0 4 0 107833 177 0 0 25 0 1 0 487536879 234409984 51685 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57229 51685 603 41 0 57188 0
vsize: 228916
[startup+1090.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 56737 0 4 0 108833 177 0 0 25 0 1 0 487536879 234946560 51809 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57360 51809 603 41 0 57319 0
vsize: 229440
[startup+1100.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 56864 0 4 0 109832 178 0 0 25 0 1 0 487536879 235495424 51936 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57494 51936 603 41 0 57453 0
vsize: 229976
[startup+1110.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 56998 0 4 0 110831 179 0 0 25 0 1 0 487536879 235905024 52070 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57594 52070 603 41 0 57553 0
vsize: 230376
[startup+1120.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 57215 0 4 0 111830 180 0 0 25 0 1 0 487536879 236904448 52287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57838 52287 603 41 0 57797 0
vsize: 231352
[startup+1130.04 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 57396 0 4 0 112830 181 0 0 25 0 1 0 487536879 237809664 52468 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58059 52468 603 41 0 58018 0
vsize: 232236
[startup+1140.05 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 57520 0 4 0 113829 181 0 0 25 0 1 0 487536879 238391296 52592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58201 52592 603 41 0 58160 0
vsize: 232804
[startup+1150.05 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 57644 0 4 0 114829 182 0 0 25 0 1 0 487536879 238817280 52716 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58305 52716 603 41 0 58264 0
vsize: 233220
[startup+1160.05 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 57931 0 4 0 115828 183 0 0 25 0 1 0 487536879 239886336 53003 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58566 53003 603 41 0 58525 0
vsize: 234264
[startup+1170.05 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 58038 0 4 0 116827 184 0 0 25 0 1 0 487536879 240480256 53110 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58711 53110 603 41 0 58670 0
vsize: 234844
[startup+1180.05 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 58203 0 4 0 117827 184 0 0 25 0 1 0 487536879 241152000 53275 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58875 53275 603 41 0 58834 0
vsize: 235500
[startup+1190.05 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 58662 0 4 0 118826 186 0 0 25 0 1 0 487536879 242896896 53734 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59301 53734 603 41 0 59260 0
vsize: 237204
[startup+1200.05 s]
Raw data (loadavg): 0.99 1.00 0.94 2/54 9464
Raw data (stat): 9464 (minisat+) R 9463 5897 5896 0 -1 0 58728 0 4 0 119825 186 0 0 25 0 1 0 487536879 243326976 53800 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59406 53800 603 41 0 59365 0
vsize: 237624
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 1.00 0.94 1/54 9464
Raw data (stat): 9464 (minisat+) Z 9463 5897 5896 0 -1 12 58730 0 4 0 119825 196 0 0 25 0 1 0 487536879 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.15
CPU time (s): 1200.23
CPU user time (s): 1198.26
CPU system time (s): 1.9687
CPU usage (%): 100.006
Max. virtual memory (Kb): 237624
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####