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/submitted/een/normalized-cap6000.opb
MD5SUM	e584a5264af1e9b64f6a152de988bbbe
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-1384839
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.14
Number of variables	6000
Total number of constraints	2294
Number of constraints which are clauses	421
Number of constraints which are cardinality constraints (but not clauses)	1871
Number of constraints which are nor clauses,nor cardinality constraints	2
Minimum length of a constraint	2
Maximum length of a constraint	5998
Trace number 7035

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-14 20:54:32 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5081 boxname=wulflinc20 idbench=391 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  e584a5264af1e9b64f6a152de988bbbe  /oldhome/oroussel/tmp/wulflinc20/normalized-cap6000.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc20/normalized-cap6000.opb /oldhome/oroussel/tmp/wulflinc20/normalized-cap6000.opb
IDLAUNCH: 5081
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        808960 kB
Buffers:         36212 kB
Cached:         153600 kB
SwapCached:       2628 kB
Active:          58928 kB
Inactive:       136428 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        808708 kB
SwapTotal:     2097892 kB
SwapFree:      2095264 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24636 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:14:35 (client local time) WITH STATUS 0 IN 1200.32 SECONDS
stats: 5081 7 1200.32 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 ---[1919]---> BDD-cost:    3
c ---[1918]---> BDD-cost:    3
c ---[1917]---> BDD-cost:    3
c ---[1916]---> BDD-cost:    3
c ---[1915]---> BDD-cost:    3
c ---[1914]---> BDD-cost:    3
c ---[1913]---> BDD-cost:    3
c ---[1912]---> BDD-cost:    3
c ---[1911]---> BDD-cost:    3
c ---[1910]---> BDD-cost:    3
c ---[1909]---> BDD-cost:    3
c ---[1908]---> BDD-cost:    3
c ---[1907]---> BDD-cost:    3
c ---[1906]---> BDD-cost:    3
c ---[1905]---> BDD-cost:    3
c ---[1904]---> BDD-cost:    3
c ---[1903]---> BDD-cost:    3
c ---[1902]---> BDD-cost:    3
c ---[1901]---> BDD-cost:    3
c ---[1900]---> BDD-cost:    3
c ---[1899]---> BDD-cost:    3
c ---[1898]---> BDD-cost:    3
c ---[1897]---> BDD-cost:    3
c ---[1896]---> BDD-cost:    3
c ---[1895]---> BDD-cost:    3
c ---[1894]---> BDD-cost:    3
c ---[1893]---> BDD-cost:    3
c ---[1892]---> BDD-cost:    3
c ---[1891]---> BDD-cost:    3
c ---[1890]---> BDD-cost:    3
c ---[1889]---> BDD-cost:    3
c ---[1888]---> BDD-cost:    3
c ---[1887]---> BDD-cost:    3
c ---[1886]---> BDD-cost:    3
c ---[1885]---> BDD-cost:    3
c ---[1884]---> BDD-cost:    3
c ---[1883]---> BDD-cost:    3
c ---[1882]---> BDD-cost:    3
c ---[1881]---> BDD-cost:    3
c ---[1880]---> BDD-cost:    3
c ---[1879]---> BDD-cost:    3
c ---[1878]---> BDD-cost:    3
c ---[1877]---> BDD-cost:    3
c ---[1876]---> BDD-cost:    3
c ---[1875]---> BDD-cost:    3
c ---[1874]---> BDD-cost:    3
c ---[1873]---> BDD-cost:    3
c ---[1872]---> BDD-cost:    3
c ---[1871]---> BDD-cost:    3
c ---[1870]---> BDD-cost:    3
c ---[1869]---> BDD-cost:    3
c ---[1868]---> BDD-cost:    3
c ---[1867]---> BDD-cost:    3
c ---[1866]---> BDD-cost:    3
c ---[1865]---> BDD-cost:    3
c ---[1864]---> BDD-cost:    3
c ---[1863]---> BDD-cost:    3
c ---[1862]---> BDD-cost:    3
c ---[1861]---> BDD-cost:    3
c ---[1860]---> BDD-cost:    3
c ---[1859]---> BDD-cost:    3
c ---[1858]---> BDD-cost:    3
c ---[1857]---> BDD-cost:    3
c ---[1856]---> BDD-cost:    3
c ---[1855]---> BDD-cost:    3
c ---[1854]---> BDD-cost:    3
c ---[1853]---> BDD-cost:    3
c ---[1852]---> BDD-cost:    3
c ---[1851]---> BDD-cost:    3
c ---[1850]---> BDD-cost:    3
c ---[1849]---> BDD-cost:    3
c ---[1848]---> BDD-cost:    3
c ---[1847]---> BDD-cost:    3
c ---[1846]---> BDD-cost:    3
c ---[1845]---> BDD-cost:    3
c ---[1844]---> BDD-cost:    3
c ---[1843]---> BDD-cost:    3
c ---[1842]---> BDD-cost:    3
c ---[1841]---> BDD-cost:    3
c ---[1840]---> BDD-cost:    3
c ---[1839]---> BDD-cost:    3
c ---[1838]---> BDD-cost:    3
c ---[1837]---> BDD-cost:    3
c ---[1836]---> BDD-cost:    3
c ---[1835]---> BDD-cost:    3
c ---[1834]---> BDD-cost:    3
c ---[1833]---> BDD-cost:    3
c ---[1832]---> BDD-cost:    3
c ---[1831]---> BDD-cost:    3
c ---[1830]---> BDD-cost:    3
c ---[1829]---> BDD-cost:    3
c ---[1828]---> BDD-cost:    3
c ---[1827]---> BDD-cost:    3
c ---[1826]---> BDD-cost:    3
c ---[1825]---> BDD-cost:    3
c ---[1824]---> BDD-cost:    3
c ---[1823]---> BDD-cost:    3
c ---[1822]---> BDD-cost:    3
c ---[1821]---> BDD-cost:    3
c ---[1820]---> BDD-cost:    3
c ---[1819]---> BDD-cost:    3
c ---[1818]---> BDD-cost:    3
c ---[1817]---> BDD-cost:    3
c ---[1816]---> BDD-cost:    3
c ---[1815]---> BDD-cost:    3
c ---[1814]---> BDD-cost:    3
c ---[1813]---> BDD-cost:    3
c ---[1812]---> BDD-cost:    3
c ---[1811]---> BDD-cost:    3
c ---[1810]---> BDD-cost:    3
c ---[1809]---> BDD-cost:    3
c ---[1808]---> BDD-cost:    3
c ---[1807]---> BDD-cost:    3
c ---[1806]---> BDD-cost:    3
c ---[1805]---> BDD-cost:    3
c ---[1804]---> BDD-cost:    3
c ---[1803]---> BDD-cost:    3
c ---[1802]---> BDD-cost:    3
c ---[1801]---> BDD-cost:    3
c ---[1800]---> BDD-cost:    3
c ---[1799]---> BDD-cost:    3
c ---[1798]---> BDD-cost:    3
c ---[1797]---> BDD-cost:    3
c ---[1796]---> BDD-cost:    3
c ---[1795]---> BDD-cost:    3
c ---[1794]---> BDD-cost:    3
c ---[1793]---> BDD-cost:    3
c ---[1792]---> BDD-cost:    3
c ---[1791]---> BDD-cost:    3
c ---[1790]---> BDD-cost:    3
c ---[1789]---> BDD-cost:    3
c ---[1788]---> BDD-cost:    3
c ---[1787]---> BDD-cost:    3
c ---[1786]---> BDD-cost:    3
c ---[1785]---> BDD-cost:    3
c ---[1784]---> BDD-cost:    3
c ---[1783]---> BDD-cost:    3
c ---[1782]---> BDD-cost:    3
c ---[1781]---> BDD-cost:    3
c ---[1780]---> BDD-cost:    3
c ---[1779]---> BDD-cost:    3
c ---[1778]---> BDD-cost:    3
c ---[1777]---> BDD-cost:    3
c ---[1776]---> BDD-cost:    3
c ---[1775]---> BDD-cost:    3
c ---[1774]---> BDD-cost:    3
c ---[1773]---> BDD-cost:    3
c ---[1772]---> BDD-cost:    3
c ---[1771]---> BDD-cost:    3
c ---[1770]---> BDD-cost:    3
c ---[1769]---> BDD-cost:    3
c ---[1768]---> BDD-cost:    3
c ---[1767]---> BDD-cost:    3
c ---[1766]---> BDD-cost:    3
c ---[1765]---> BDD-cost:    3
c ---[1764]---> BDD-cost:    3
c ---[1763]---> BDD-cost:    3
c ---[1762]---> BDD-cost:    3
c ---[1761]---> BDD-cost:    3
c ---[1760]---> BDD-cost:    3
c ---[1759]---> BDD-cost:    3
c ---[1758]---> BDD-cost:    3
c ---[1757]---> BDD-cost:    3
c ---[1756]---> BDD-cost:    3
c ---[1755]---> BDD-cost:    3
c ---[1754]---> BDD-cost:    3
c ---[1753]---> BDD-cost:    3
c ---[1752]---> BDD-cost:    3
c ---[1751]---> BDD-cost:    3
c ---[1750]---> BDD-cost:    3
c ---[1749]---> BDD-cost:    3
c ---[1748]---> BDD-cost:    3
c ---[1747]---> BDD-cost:    3
c ---[1746]---> BDD-cost:    3
c ---[1745]---> BDD-cost:    3
c ---[1744]---> BDD-cost:    3
c ---[1743]---> BDD-cost:    3
c ---[1742]---> BDD-cost:    3
c ---[1741]---> BDD-cost:    3
c ---[1740]---> BDD-cost:    3
c ---[1739]---> BDD-cost:    3
c ---[1738]---> BDD-cost:    3
c ---[1737]---> BDD-cost:    3
c ---[1736]---> BDD-cost:    3
c ---[1735]---> BDD-cost:    3
c ---[1734]---> BDD-cost:    3
c ---[1733]---> BDD-cost:    3
c ---[1732]---> BDD-cost:    3
c ---[1731]---> BDD-cost:    3
c ---[1730]---> BDD-cost:    3
c ---[1729]---> BDD-cost:    3
c ---[1728]---> BDD-cost:    3
c ---[1727]---> BDD-cost:    3
c ---[1726]---> BDD-cost:    3
c ---[1725]---> BDD-cost:    3
c ---[1724]---> BDD-cost:    3
c ---[1723]---> BDD-cost:    3
c ---[1722]---> BDD-cost:    3
c ---[1721]---> BDD-cost:    3
c ---[1720]---> BDD-cost:    3
c ---[1719]---> BDD-cost:    3
c ---[1718]---> BDD-cost:    3
c ---[1717]---> BDD-cost:    3
c ---[1716]---> BDD-cost:    3
c ---[1715]---> BDD-cost:    3
c ---[1714]---> BDD-cost:    3
c ---[1713]---> BDD-cost:    3
c ---[1712]---> BDD-cost:    3
c ---[1711]---> BDD-cost:    3
c ---[1710]---> BDD-cost:    3
c ---[1709]---> BDD-cost:    3
c ---[1708]---> BDD-cost:    3
c ---[1707]---> BDD-cost:    3
c ---[1706]---> BDD-cost:    3
c ---[1705]---> BDD-cost:    3
c ---[1704]---> BDD-cost:    3
c ---[1703]---> BDD-cost:    3
c ---[1702]---> BDD-cost:    3
c ---[1701]---> BDD-cost:    3
c ---[1700]---> BDD-cost:    3
c ---[1699]---> BDD-cost:    3
c ---[1698]---> BDD-cost:    3
c ---[1697]---> BDD-cost:    3
c ---[1696]---> BDD-cost:    3
c ---[1695]---> BDD-cost:    3
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 ---[1519]---> BDD-cost:    3
c ---[1518]---> BDD-cost:    3
c ---[1517]---> BDD-cost:    3
c ---[1516]---> BDD-cost:    3
c ---[1515]---> BDD-cost:    3
c ---[1514]---> BDD-cost:    3
c ---[1513]---> BDD-cost:    3
c ---[1512]---> BDD-cost:    3
c ---[1511]---> BDD-cost:    3
c ---[1510]---> BDD-cost:    3
c ---[1509]---> BDD-cost:    3
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]---> BDD-cost:    3
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 ---[1086]---> BDD-cost:    3
c ---[1085]---> BDD-cost:    3
c ---[1084]---> BDD-cost:    3
c ---[1083]---> BDD-cost:    3
c ---[1082]---> BDD-cost:    3
c ---[1081]---> BDD-cost:    3
c ---[1080]---> BDD-cost:    3
c ---[1079]---> BDD-cost:    3
c ---[1078]---> BDD-cost:    3
c ---[1077]---> BDD-cost:    3
c ---[1076]---> BDD-cost:    3
c ---[1075]---> BDD-cost:    3
c ---[1074]---> BDD-cost:    3
c ---[1073]---> BDD-cost:    3
c ---[1072]---> BDD-cost:    3
c ---[1071]---> BDD-cost:    3
c ---[1070]---> BDD-cost:    3
c ---[1069]---> BDD-cost:    3
c ---[1068]---> BDD-cost:    3
c ---[1067]---> BDD-cost:    3
c ---[1066]---> BDD-cost:    3
c ---[1065]---> BDD-cost:    3
c ---[1064]---> BDD-cost:    3
c ---[1063]---> BDD-cost:    3
c ---[1062]---> BDD-cost:    3
c ---[1061]---> BDD-cost:    3
c ---[1060]---> BDD-cost:    3
c ---[1059]---> BDD-cost:    3
c ---[1058]---> BDD-cost:    3
c ---[1057]---> BDD-cost:    3
c ---[1056]---> BDD-cost:    3
c ---[1055]---> BDD-cost:    3
c ---[1054]---> BDD-cost:    3
c ---[1053]---> BDD-cost:    3
c ---[1052]---> BDD-cost:    3
c ---[1051]---> BDD-cost:    3
c ---[1050]---> BDD-cost:    3
c ---[1049]---> BDD-cost:    3
c ---[1048]---> BDD-cost:    3
c ---[1047]---> BDD-cost:    3
c ---[1046]---> BDD-cost:    3
c ---[1045]---> BDD-cost:    3
c ---[1044]---> BDD-cost:    3
c ---[1043]---> BDD-cost:    3
c ---[1042]---> BDD-cost:    3
c ---[1041]---> BDD-cost:    3
c ---[1040]---> BDD-cost:    3
c ---[1039]---> BDD-cost:    3
c ---[1038]---> BDD-cost:    3
c ---[1037]---> BDD-cost:    3
c ---[1036]---> BDD-cost:    3
c ---[1035]---> BDD-cost:    3
c ---[1034]---> BDD-cost:    3
c ---[1033]---> BDD-cost:    3
c ---[1032]---> BDD-cost:    3
c ---[1031]---> BDD-cost:    3
c ---[1030]---> BDD-cost:    3
c ---[1029]---> BDD-cost:    3
c ---[1028]---> BDD-cost:    3
c ---[1027]---> BDD-cost:    3
c ---[1026]---> BDD-cost:    3
c ---[1025]---> BDD-cost:    3
c ---[1024]---> BDD-cost:    3
c ---[1023]---> BDD-cost:    3
c ---[1022]---> BDD-cost:    3
c ---[1021]---> BDD-cost:    3
c ---[1020]---> BDD-cost:    3
c ---[1019]---> BDD-cost:    3
c ---[1018]---> BDD-cost:    3
c ---[1017]---> BDD-cost:    3
c ---[1016]---> BDD-cost:    3
c ---[1015]---> BDD-cost:    3
c ---[1014]---> BDD-cost:    3
c ---[1013]---> BDD-cost:    3
c ---[1012]---> BDD-cost:    3
c ---[1011]---> BDD-cost:    3
c ---[1010]---> BDD-cost:    3
c ---[1009]---> BDD-cost:    3
c ---[1008]---> BDD-cost:    3
c ---[1007]---> BDD-cost:    3
c ---[1006]---> BDD-cost:    3
c ---[1005]---> BDD-cost:    3
c ---[1004]---> BDD-cost:    3
c ---[1003]---> BDD-cost:    3
c ---[1002]---> BDD-cost:    3
c ---[1001]---> BDD-cost:    3
c ---[1000]---> BDD-cost:    3
c ---[ 999]---> BDD-cost:    3
c ---[ 998]---> BDD-cost:    3
c ---[ 997]---> BDD-cost:    3
c ---[ 996]---> BDD-cost:    3
c ---[ 995]---> BDD-cost:    3
c ---[ 994]---> BDD-cost:    3
c ---[ 993]---> BDD-cost:    3
c ---[ 992]---> BDD-cost:    3
c ---[ 991]---> BDD-cost:    3
c ---[ 990]---> BDD-cost:    3
c ---[ 989]---> BDD-cost:    3
c ---[ 988]---> BDD-cost:    3
c ---[ 987]---> BDD-cost:    3
c ---[ 986]---> BDD-cost:    3
c ---[ 985]---> BDD-cost:    3
c ---[ 984]---> BDD-cost:    3
c ---[ 983]---> BDD-cost:    3
c ---[ 982]---> BDD-cost:    3
c ---[ 981]---> BDD-cost:    3
c ---[ 980]---> BDD-cost:    3
c ---[ 979]---> BDD-cost:    3
c ---[ 978]---> BDD-cost:    3
c ---[ 977]---> BDD-cost:    3
c ---[ 976]---> BDD-cost:    3
c ---[ 975]---> BDD-cost:    3
c ---[ 974]---> BDD-cost:    3
c ---[ 973]---> BDD-cost:    3
c ---[ 972]---> BDD-cost:    3
c ---[ 971]---> BDD-cost:    3
c ---[ 970]---> BDD-cost:    3
c ---[ 969]---> BDD-cost:    3
c ---[ 968]---> BDD-cost:    3
c ---[ 967]---> BDD-cost:    3
c ---[ 966]---> BDD-cost:    3
c ---[ 965]---> BDD-cost:    3
c ---[ 964]---> BDD-cost:    3
c ---[ 963]---> BDD-cost:    3
c ---[ 962]---> BDD-cost:    3
c ---[ 961]---> BDD-cost:    3
c ---[ 960]---> BDD-cost:    3
c ---[ 959]---> BDD-cost:    3
c ---[ 958]---> BDD-cost:    3
c ---[ 957]---> BDD-cost:    3
c ---[ 956]---> BDD-cost:    3
c ---[ 955]---> BDD-cost:    3
c ---[ 954]---> BDD-cost:    3
c ---[ 953]---> BDD-cost:    3
c ---[ 952]---> BDD-cost:    3
c ---[ 951]---> BDD-cost:    3
c ---[ 950]---> BDD-cost:    3
c ---[ 949]---> BDD-cost:    3
c ---[ 948]---> BDD-cost:    3
c ---[ 947]---> BDD-cost:    3
c ---[ 946]---> BDD-cost:    3
c ---[ 945]---> BDD-cost:    3
c ---[ 944]---> BDD-cost:    3
c ---[ 943]---> BDD-cost:    3
c ---[ 942]---> BDD-cost:    3
c ---[ 941]---> BDD-cost:    3
c ---[ 940]---> BDD-cost:    3
c ---[ 939]---> BDD-cost:    3
c ---[ 938]---> BDD-cost:    3
c ---[ 937]---> BDD-cost:    3
c ---[ 936]---> BDD-cost:    3
c ---[ 935]---> BDD-cost:    3
c ---[ 934]---> BDD-cost:    3
c ---[ 933]---> BDD-cost:    3
c ---[ 932]---> BDD-cost:    3
c ---[ 931]---> BDD-cost:    3
c ---[ 930]---> BDD-cost:    3
c ---[ 929]---> BDD-cost:    3
c ---[ 928]---> BDD-cost:    3
c ---[ 927]---> BDD-cost:    3
c ---[ 926]---> BDD-cost:    3
c ---[ 925]---> BDD-cost:    3
c ---[ 924]---> BDD-cost:    3
c ---[ 923]---> BDD-cost:    3
c ---[ 922]---> BDD-cost:    3
c ---[ 921]---> BDD-cost:    3
c ---[ 920]---> BDD-cost:    3
c ---[ 919]---> BDD-cost:    3
c ---[ 918]---> BDD-cost:    3
c ---[ 917]---> BDD-cost:    3
c ---[ 916]---> BDD-cost:    3
c ---[ 915]---> BDD-cost:    3
c ---[ 914]---> BDD-cost:    3
c ---[ 913]---> BDD-cost:    3
c ---[ 912]---> BDD-cost:    3
c ---[ 911]---> BDD-cost:    3
c ---[ 910]---> BDD-cost:    3
c ---[ 909]---> BDD-cost:    3
c ---[ 908]---> BDD-cost:    3
c ---[ 907]---> BDD-cost:    3
c ---[ 906]---> BDD-cost:    3
c ---[ 905]---> BDD-cost:    3
c ---[ 904]---> BDD-cost:    3
c ---[ 903]---> BDD-cost:    3
c ---[ 902]---> BDD-cost:    3
c ---[ 901]---> BDD-cost:    3
c ---[ 900]---> BDD-cost:    3
c ---[ 899]---> BDD-cost:    3
c ---[ 898]---> BDD-cost:    3
c ---[ 897]---> BDD-cost:    3
c ---[ 896]---> BDD-cost:    3
c ---[ 895]---> BDD-cost:    3
c ---[ 894]---> BDD-cost:    3
c ---[ 893]---> BDD-cost:    3
c ---[ 892]---> BDD-cost:    3
c ---[ 891]---> BDD-cost:    3
c ---[ 890]---> BDD-cost:    3
c ---[ 889]---> BDD-cost:    3
c ---[ 888]---> BDD-cost:    3
c ---[ 887]---> BDD-cost:    3
c ---[ 886]---> BDD-cost:    3
c ---[ 885]---> BDD-cost:    3
c ---[ 884]---> BDD-cost:    3
c ---[ 883]---> BDD-cost:    3
c ---[ 882]---> BDD-cost:    3
c ---[ 881]---> BDD-cost:    3
c ---[ 880]---> BDD-cost:    3
c ---[ 879]---> BDD-cost:    3
c ---[ 878]---> BDD-cost:    3
c ---[ 877]---> BDD-cost:    3
c ---[ 876]---> BDD-cost:    3
c ---[ 875]---> BDD-cost:    3
c ---[ 874]---> BDD-cost:    3
c ---[ 873]---> BDD-cost:    3
c ---[ 872]---> BDD-cost:    3
c ---[ 871]---> BDD-cost:    3
c ---[ 870]---> BDD-cost:    3
c ---[ 869]---> BDD-cost:    3
c ---[ 868]---> BDD-cost:    3
c ---[ 867]---> BDD-cost:    3
c ---[ 866]---> BDD-cost:    3
c ---[ 865]---> BDD-cost:    3
c ---[ 864]---> BDD-cost:    3
c ---[ 863]---> BDD-cost:    3
c ---[ 862]---> 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 ---[ 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 ---[ 675]---> BDD-cost:    3
c ---[ 673]---> BDD-cost:    3
c ---[ 671]---> BDD-cost:    3
c ---[ 669]---> BDD-cost:    3
c ---[ 667]---> BDD-cost:    3
c ---[ 665]---> BDD-cost:    3
c ---[ 663]---> 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 ---[ 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 ---[ 629]---> BDD-cost:    3
c ---[ 627]---> BDD-cost:    3
c ---[ 624]---> BDD-cost:    3
c ---[ 622]---> BDD-cost:    3
c ---[ 620]---> BDD-cost:    3
c ---[ 618]---> BDD-cost:    3
c ---[ 616]---> BDD-cost:    3
c ---[ 614]---> BDD-cost:    3
c ---[ 612]---> BDD-cost:    3
c ---[ 610]---> BDD-cost:    3
c ---[ 609]---> BDD-cost:    3
c ---[ 608]---> BDD-cost:    3
c ---[ 606]---> 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 ---[ 584]---> BDD-cost:    3
c ---[ 582]---> BDD-cost:    3
c ---[ 580]---> BDD-cost:    3
c ---[ 578]---> BDD-cost:    3
c ---[ 576]---> 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 ---[ 530]---> BDD-cost:    3
c ---[ 529]---> BDD-cost:    3
c ---[ 527]---> BDD-cost:    3
c ---[ 525]---> BDD-cost:    3
c ---[ 523]---> BDD-cost:    3
c ---[ 521]---> BDD-cost:    3
c ---[ 519]---> BDD-cost:    3
c ---[ 517]---> BDD-cost:    3
c ---[ 515]---> 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 ---[ 257]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:    3
c ---[ 253]---> 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:    5
c ---[  43]---> BDD-cost:    5
c ---[  42]---> BDD-cost:    5
c ---[  41]---> BDD-cost:    5
c ---[  40]---> BDD-cost:    5
c ---[  39]---> BDD-cost:    5
c ---[  38]---> BDD-cost:    5
c ---[  37]---> BDD-cost:    5
c ---[  36]---> BDD-cost:    5
c ---[  35]---> BDD-cost:    5
c ---[  34]---> BDD-cost:    5
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    5
c ---[  28]---> BDD-cost:    5
c ---[  26]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    5
c ---[  23]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    5
c ---[  21]---> BDD-cost:    5
c ---[  20]---> BDD-cost:    5
c ---[  19]---> BDD-cost:    5
c ---[  18]---> BDD-cost:    5
c ---[  17]---> BDD-cost:    5
c ---[  15]---> BDD-cost:    5
c ---[  14]---> BDD-cost:    5
c ---[  13]---> BDD-cost:    5
c ---[  12]---> BDD-cost:    5
c ---[  11]---> BDD-cost:    5
c ---[  10]---> BDD-cost:    5
c ---[   9]---> BDD-cost:    5
c ---[   8]---> BDD-cost:    5
c ---[   7]---> BDD-cost:    5
c ---[   6]---> BDD-cost:    5
c ---[   5]---> BDD-cost:    5
c ---[   4]---> BDD-cost:    5
c ---[   3]---> BDD-cost:    5
c ---[   2]---> BDD-cost:    5
c ---[   1]---> Adder-cost: 61016   maxlim: 27161905   bits: 25/25
c ---[   0]---> Adder-cost: 59486   maxlim: 14773890   bits: 24/24
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  855062  3043014 |  256518       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/130227          
c   -- var.elim.:  2000/130227          
c   -- var.elim.:  3000/130227          
c   -- var.elim.:  4000/130227          
c   -- var.elim.:  5000/130227          
c   -- var.elim.:  6000/130227          
c   -- var.elim.:  7000/130227          
c   -- var.elim.:  8000/130227          
c   -- var.elim.:  9000/130227          
c   -- var.elim.:  10000/130227          
c   -- var.elim.:  11000/130227          
c   -- var.elim.:  12000/130227          
c   -- var.elim.:  13000/130227          
c   -- var.elim.:  14000/130227          
c   -- var.elim.:  15000/130227          
c   -- var.elim.:  16000/130227          
c   -- var.elim.:  17000/130227          
c   -- var.elim.:  18000/130227          
c   -- var.elim.:  19000/130227          
c   -- var.elim.:  20000/130227          
c   -- var.elim.:  21000/130227          
c   -- var.elim.:  22000/130227          
c   -- var.elim.:  23000/130227          
c   -- var.elim.:  24000/130227          
c   -- var.elim.:  25000/130227          
c   -- var.elim.:  26000/130227          
c   -- var.elim.:  27000/130227          
c   -- var.elim.:  28000/130227          
c   -- var.elim.:  29000/130227          
c   -- var.elim.:  30000/130227          
c   -- var.elim.:  31000/130227          
c   -- var.elim.:  32000/130227          
c   -- var.elim.:  33000/130227          
c   -- var.elim.:  34000/130227          
c   -- var.elim.:  35000/130227          
c   -- var.elim.:  36000/130227          
c   -- var.elim.:  37000/130227          
c   -- var.elim.:  38000/130227          
c   -- var.elim.:  39000/130227          
c   -- var.elim.:  40000/130227          
c   -- var.elim.:  41000/130227          
c   -- var.elim.:  42000/130227          
c   -- var.elim.:  43000/130227          
c   -- var.elim.:  44000/130227          
c   -- var.elim.:  45000/130227          
c   -- var.elim.:  46000/130227          
c   -- var.elim.:  47000/130227          
c   -- var.elim.:  48000/130227          
c   -- var.elim.:  49000/130227          
c   -- var.elim.:  50000/130227          
c   -- var.elim.:  51000/130227          
c   -- var.elim.:  52000/130227          
c   -- var.elim.:  53000/130227          
c   -- var.elim.:  54000/130227          
c   -- var.elim.:  55000/130227          
c   -- var.elim.:  56000/130227          
c   -- var.elim.:  57000/130227          
c   -- var.elim.:  58000/130227          
c   -- var.elim.:  59000/130227          
c   -- var.elim.:  60000/130227          
c   -- var.elim.:  61000/130227          
c   -- var.elim.:  62000/130227          
c   -- var.elim.:  63000/130227          
c   -- var.elim.:  64000/130227          
c   -- var.elim.:  65000/130227          
c   -- var.elim.:  66000/130227          
c   -- var.elim.:  67000/130227          
c   -- var.elim.:  68000/130227          
c   -- var.elim.:  69000/130227          
c   -- var.elim.:  70000/130227          
c   -- var.elim.:  71000/130227          
c   -- var.elim.:  72000/130227          
c   -- var.elim.:  73000/130227          
c   -- var.elim.:  74000/130227          
c   -- var.elim.:  75000/130227          
c   -- var.elim.:  76000/130227          
c   -- var.elim.:  77000/130227          
c   -- var.elim.:  78000/130227          
c   -- var.elim.:  79000/130227          
c   -- var.elim.:  80000/130227          
c   -- var.elim.:  81000/130227          
c   -- var.elim.:  82000/130227          
c   -- var.elim.:  83000/130227          
c   -- var.elim.:  84000/130227          
c   -- var.elim.:  85000/130227          
c   -- var.elim.:  86000/130227          
c   -- var.elim.:  87000/130227          
c   -- var.elim.:  88000/130227          
c   -- var.elim.:  89000/130227          
c   -- var.elim.:  90000/130227          
c   -- var.elim.:  91000/130227          
c   -- var.elim.:  92000/130227          
c   -- var.elim.:  93000/130227          
c   -- var.elim.:  94000/130227          
c   -- var.elim.:  95000/130227          
c   -- var.elim.:  96000/130227          
c   -- var.elim.:  97000/130227          
c   -- var.elim.:  98000/130227          
c   -- var.elim.:  99000/130227          
c   -- var.elim.:  100000/130227          
c   -- var.elim.:  101000/130227          
c   -- var.elim.:  102000/130227          
c   -- var.elim.:  103000/130227          
c   -- var.elim.:  104000/130227          
c   -- var.elim.:  105000/130227          
c   -- var.elim.:  106000/130227          
c   -- var.elim.:  107000/130227          
c   -- var.elim.:  108000/130227          
c   -- var.elim.:  109000/130227          
c   -- var.elim.:  110000/130227          
c   -- var.elim.:  111000/130227          
c   -- var.elim.:  112000/130227          
c   -- var.elim.:  113000/130227          
c   -- var.elim.:  114000/130227          
c   -- var.elim.:  115000/130227          
c   -- var.elim.:  116000/130227          
c   -- var.elim.:  117000/130227          
c   -- var.elim.:  118000/130227          
c   -- var.elim.:  119000/130227          
c   -- var.elim.:  120000/130227          
c   -- var.elim.:  121000/130227          
c   -- var.elim.:  122000/130227          
c   -- var.elim.:  123000/130227          
c   -- var.elim.:  124000/130227          
c   -- var.elim.:  125000/130227          
c   -- var.elim.:  126000/130227          
c   -- var.elim.:  127000/130227          
c   -- var.elim.:  128000/130227          
c   -- var.elim.:  129000/130227          
c   -- var.elim.:  130000/130227          
c   -- var.elim.:  130227/130227          
c   -- var.elim.:  1000/5867          
c   -- var.elim.:  2000/5867          
c   -- var.elim.:  3000/5867          
c   -- var.elim.:  4000/5867          
c   -- var.elim.:  5000/5867          
c   -- var.elim.:  5867/5867          
c   -- var.elim.:  26/26          
c   -- subsuming                       
c   -- var.elim.:  289/289          
c   -- var.elim.:  200/200          
c   -- subsuming                       
c   -- var.elim.:  203/203          
c   -- var.elim.:  160/160          
c   -- subsuming                       
c |         0 |  846954  3013725 |      --       0       --      -- |     --   | -8085/-23504
c |         0 |  846954  3013725 |  338781       0        0     nan |  0.000 % |
c |       100 |  846954  3013725 |  372659     100      335     3.4 |  1.541 % |
c |       251 |  846954  301372#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.81 2/54 9737
Raw data (stat): 9737 (runsolver) R 9736 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487629076 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.95 0.81 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 3828 0 0 0 989 10 0 0 25 0 1 0 487629076 12623872 2529 4294967295 134512640 134672761 3221224560 3221222832 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3082 2529 603 41 0 3041 0
vsize: 12328
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.81 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 14171 0 0 0 1967 32 0 0 25 0 1 0 487629076 47288320 10338 4294967295 134512640 134672761 3221224560 3221223744 134593685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11545 10338 603 41 0 11504 0
vsize: 46180
[startup+30.0011 s]
Raw data (loadavg): 0.95 0.96 0.81 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 14875 0 0 0 2966 33 0 0 25 0 1 0 487629076 47349760 10372 4294967295 134512640 134672761 3221224560 3221222832 134597191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11560 10372 603 41 0 11519 0
vsize: 46240
[startup+40.0009 s]
Raw data (loadavg): 0.95 0.96 0.82 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 42243 0 0 0 3899 99 0 0 25 0 1 0 487629076 182636544 37681 4294967295 134512640 134672761 3221224560 3221223068 1075349669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44589 37681 603 41 0 44548 0
vsize: 178356
[startup+50.0004 s]
Raw data (loadavg): 0.96 0.96 0.82 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 46486 0 0 0 4887 111 0 0 25 0 1 0 487629076 183070720 37790 4294967295 134512640 134672761 3221224560 3221223568 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44695 37790 603 41 0 44654 0
vsize: 178780
[startup+60.0004 s]
Raw data (loadavg): 0.97 0.96 0.82 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 46955 0 0 0 5886 112 0 0 25 0 1 0 487629076 184995840 38259 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45165 38259 603 41 0 45124 0
vsize: 180660
[startup+70.0001 s]
Raw data (loadavg): 0.97 0.96 0.82 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 47564 0 0 0 6885 114 0 0 25 0 1 0 487629076 187621376 38868 4294967295 134512640 134672761 3221224560 3221223600 134612632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45806 38868 603 41 0 45765 0
vsize: 183224
[startup+80.0005 s]
Raw data (loadavg): 0.98 0.96 0.82 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 48250 0 0 0 7883 115 0 0 25 0 1 0 487629076 190296064 39554 4294967295 134512640 134672761 3221224560 3221223392 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46459 39555 603 41 0 46418 0
vsize: 185836
[startup+90.0005 s]
Raw data (loadavg): 0.98 0.96 0.82 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 49135 0 0 0 8881 117 0 0 25 0 1 0 487629076 193998848 40439 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47363 40439 603 41 0 47322 0
vsize: 189452
[startup+100 s]
Raw data (loadavg): 0.98 0.96 0.82 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 49694 0 0 0 9880 119 0 0 25 0 1 0 487629076 196268032 40998 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47917 40998 603 41 0 47876 0
vsize: 191668
[startup+110.001 s]
Raw data (loadavg): 0.98 0.96 0.82 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 50120 0 0 0 10879 120 0 0 25 0 1 0 487629076 198123520 41424 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48370 41424 603 41 0 48329 0
vsize: 193480
[startup+120.001 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 50556 0 0 0 11879 121 0 0 25 0 1 0 487629076 199860224 41860 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48794 41860 603 41 0 48753 0
vsize: 195176
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 51055 0 0 0 12878 121 0 0 25 0 1 0 487629076 202125312 42359 4294967295 134512640 134672761 3221224560 3221223744 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49347 42360 603 41 0 49306 0
vsize: 197388
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 51500 0 0 0 13877 123 0 0 25 0 1 0 487629076 203988992 42804 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49802 42804 603 41 0 49761 0
vsize: 199208
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 51887 0 0 0 14876 124 0 0 25 0 1 0 487629076 205475840 43191 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50165 43191 603 41 0 50124 0
vsize: 200660
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 52279 0 0 0 15875 125 0 0 25 0 1 0 487629076 207130624 43583 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50569 43583 603 41 0 50528 0
vsize: 202276
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 52643 0 0 0 16874 126 0 0 25 0 1 0 487629076 208588800 43947 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50925 43947 603 41 0 50884 0
vsize: 203700
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 53016 0 0 0 17874 126 0 0 25 0 1 0 487629076 210182144 44320 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51314 44320 603 41 0 51273 0
vsize: 205256
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 53357 0 0 0 18873 128 0 0 25 0 1 0 487629076 211505152 44661 4294967295 134512640 134672761 3221224560 3221223372 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51637 44661 603 41 0 51596 0
vsize: 206548
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 53665 0 0 0 19871 129 0 0 25 0 1 0 487629076 212828160 44969 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51960 44969 603 41 0 51919 0
vsize: 207840
[startup+210.001 s]
Raw data (loadavg): 0.99 0.97 0.83 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 53938 0 0 0 20871 130 0 0 25 0 1 0 487629076 213893120 45242 4294967295 134512640 134672761 3221224560 3221223744 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52220 45242 603 41 0 52179 0
vsize: 208880
[startup+220.001 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 54153 0 0 0 21870 131 0 0 25 0 1 0 487629076 214687744 45457 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52414 45457 603 41 0 52373 0
vsize: 209656
[startup+230.001 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 54393 0 0 0 22870 132 0 0 25 0 1 0 487629076 215805952 45697 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52687 45697 603 41 0 52646 0
vsize: 210748
[startup+240.001 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 54631 0 0 0 23869 132 0 0 25 0 1 0 487629076 216768512 45935 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52922 45935 603 41 0 52881 0
vsize: 211688
[startup+250.001 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 54843 0 0 0 24869 133 0 0 25 0 1 0 487629076 217567232 46147 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53117 46147 603 41 0 53076 0
vsize: 212468
[startup+260.002 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 55088 0 0 0 25868 133 0 0 25 0 1 0 487629076 218779648 46392 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53413 46392 603 41 0 53372 0
vsize: 213652
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 55329 0 0 0 26868 134 0 0 25 0 1 0 487629076 219701248 46633 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53638 46633 603 41 0 53597 0
vsize: 214552
[startup+280.002 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 55545 0 0 0 27867 135 0 0 25 0 1 0 487629076 220631040 46849 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53865 46849 603 41 0 53824 0
vsize: 215460
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 55822 0 0 0 28867 135 0 0 25 0 1 0 487629076 222257152 47126 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54262 47126 603 41 0 54221 0
vsize: 217048
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 56184 0 0 0 29866 136 0 0 25 0 1 0 487629076 223711232 47488 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54617 47488 603 41 0 54576 0
vsize: 218468
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.84 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 56510 0 0 0 30865 138 0 0 25 0 1 0 487629076 225165312 47814 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54972 47814 603 41 0 54931 0
vsize: 219888
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 56839 0 0 0 31865 138 0 0 25 0 1 0 487629076 226484224 48143 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55294 48143 603 41 0 55253 0
vsize: 221176
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.85 2/54 9737
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 57159 0 0 0 32864 139 0 0 25 0 1 0 487629076 227794944 48463 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55614 48463 603 41 0 55573 0
vsize: 222456
[startup+340.005 s]
Raw data (loadavg): 1.15 1.00 0.86 2/54 9790
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 57441 0 0 0 33863 140 0 0 25 0 1 0 487629076 228872192 48745 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55877 48745 603 41 0 55836 0
vsize: 223508
[startup+350.004 s]
Raw data (loadavg): 1.12 1.00 0.86 2/54 9790
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 57726 0 0 0 34863 140 0 0 25 0 1 0 487629076 230060032 49030 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56167 49030 603 41 0 56126 0
vsize: 224668
[startup+360.005 s]
Raw data (loadavg): 1.10 1.00 0.86 2/54 9790
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 58007 0 0 0 35862 141 0 0 25 0 1 0 487629076 231174144 49311 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56439 49311 603 41 0 56398 0
vsize: 225756
[startup+370.005 s]
Raw data (loadavg): 1.09 1.00 0.86 2/54 9790
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 58276 0 0 0 36862 142 0 0 25 0 1 0 487629076 232267776 49580 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56706 49580 603 41 0 56665 0
vsize: 226824
[startup+380.005 s]
Raw data (loadavg): 1.07 1.00 0.86 2/54 9790
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 58517 0 0 0 37862 143 0 0 25 0 1 0 487629076 233345024 49821 4294967295 134512640 134672761 3221224560 3221223744 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56969 49821 603 41 0 56928 0
vsize: 227876
[startup+390.006 s]
Raw data (loadavg): 1.06 1.00 0.86 2/54 9790
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 58790 0 0 0 38861 143 0 0 25 0 1 0 487629076 234409984 50094 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57229 50094 603 41 0 57188 0
vsize: 228916
[startup+400.005 s]
Raw data (loadavg): 1.05 1.00 0.86 2/54 9790
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 59071 0 0 0 39861 144 0 0 25 0 1 0 487629076 235577344 50375 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57514 50375 603 41 0 57473 0
vsize: 230056
[startup+410.006 s]
Raw data (loadavg): 1.04 1.00 0.86 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 59361 0 0 0 40860 145 0 0 25 0 1 0 487629076 236900352 50665 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57837 50665 603 41 0 57796 0
vsize: 231348
[startup+420.006 s]
Raw data (loadavg): 1.04 1.00 0.87 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 59633 0 0 0 41859 146 0 0 25 0 1 0 487629076 237989888 50937 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58103 50937 603 41 0 58062 0
vsize: 232412
[startup+430.006 s]
Raw data (loadavg): 1.03 1.00 0.87 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 59853 0 0 0 42859 146 0 0 25 0 1 0 487629076 238833664 51157 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58309 51157 603 41 0 58268 0
vsize: 233236
[startup+440.006 s]
Raw data (loadavg): 1.03 1.00 0.87 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 60109 0 0 0 43858 147 0 0 25 0 1 0 487629076 239890432 51413 4294967295 134512640 134672761 3221224560 3221223372 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58567 51413 603 41 0 58526 0
vsize: 234268
[startup+450.006 s]
Raw data (loadavg): 1.02 1.00 0.87 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 60323 0 0 0 44858 147 0 0 25 0 1 0 487629076 240721920 51627 4294967295 134512640 134672761 3221224560 3221223744 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58770 51627 603 41 0 58729 0
vsize: 235080
[startup+460.006 s]
Raw data (loadavg): 1.02 1.00 0.87 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 60556 0 0 0 45858 148 0 0 25 0 1 0 487629076 241668096 51860 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59001 51860 603 41 0 58960 0
vsize: 236004
[startup+470.006 s]
Raw data (loadavg): 1.01 1.00 0.87 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 60783 0 0 0 46857 149 0 0 25 0 1 0 487629076 242655232 52087 4294967295 134512640 134672761 3221224560 3221223744 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59242 52087 603 41 0 59201 0
vsize: 236968
[startup+480.006 s]
Raw data (loadavg): 1.01 1.00 0.87 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 61031 0 0 0 47856 150 0 0 25 0 1 0 487629076 243675136 52335 4294967295 134512640 134672761 3221224560 3221223576 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59491 52335 603 41 0 59450 0
vsize: 237964
[startup+490.005 s]
Raw data (loadavg): 1.01 1.00 0.87 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 61339 0 0 0 48856 150 0 0 25 0 1 0 487629076 245018624 52643 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59819 52643 603 41 0 59778 0
vsize: 239276
[startup+500.005 s]
Raw data (loadavg): 1.01 1.00 0.87 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 61617 0 0 0 49855 151 0 0 25 0 1 0 487629076 246095872 52921 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60082 52921 603 41 0 60041 0
vsize: 240328
[startup+510.005 s]
Raw data (loadavg): 1.01 1.00 0.87 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 61852 0 0 0 50854 152 0 0 25 0 1 0 487629076 247169024 53156 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60344 53156 603 41 0 60303 0
vsize: 241376
[startup+520.004 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 62093 0 0 0 51854 153 0 0 25 0 1 0 487629076 248094720 53397 4294967295 134512640 134672761 3221224560 3221223732 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60570 53397 603 41 0 60529 0
vsize: 242280
[startup+530.005 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 62331 0 0 0 52853 154 0 0 25 0 1 0 487629076 249024512 53635 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60797 53635 603 41 0 60756 0
vsize: 243188
[startup+540.005 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 62568 0 0 0 53853 154 0 0 25 0 1 0 487629076 250130432 53872 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61067 53872 603 41 0 61026 0
vsize: 244268
[startup+550.005 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 62803 0 0 0 54852 155 0 0 25 0 1 0 487629076 251121664 54107 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61309 54107 603 41 0 61268 0
vsize: 245236
[startup+560.004 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 62990 0 0 0 55851 156 0 0 25 0 1 0 487629076 251777024 54294 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61469 54294 603 41 0 61428 0
vsize: 245876
[startup+570.005 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 63201 0 0 0 56850 157 0 0 25 0 1 0 487629076 252702720 54505 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61695 54505 603 41 0 61654 0
vsize: 246780
[startup+580.005 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 63390 0 0 0 57850 158 0 0 25 0 1 0 487629076 253517824 54694 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61894 54694 603 41 0 61853 0
vsize: 247576
[startup+590.005 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 63571 0 0 0 58849 158 0 0 25 0 1 0 487629076 254316544 54875 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62089 54875 603 41 0 62048 0
vsize: 248356
[startup+600.005 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 63733 0 0 0 59849 159 0 0 25 0 1 0 487629076 254849024 55037 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62219 55037 603 41 0 62178 0
vsize: 248876
[startup+610.005 s]
Raw data (loadavg): 1.00 1.00 0.88 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 63927 0 0 0 60849 159 0 0 25 0 1 0 487629076 255770624 55231 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62444 55231 603 41 0 62403 0
vsize: 249776
[startup+620.005 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 64147 0 0 0 61848 160 0 0 25 0 1 0 487629076 256565248 55451 4294967295 134512640 134672761 3221224560 3221223744 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62638 55451 603 41 0 62597 0
vsize: 250552
[startup+630.005 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 64341 0 0 0 62848 161 0 0 25 0 1 0 487629076 257384448 55645 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62838 55645 603 41 0 62797 0
vsize: 251352
[startup+640.005 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 64523 0 0 0 63847 161 0 0 25 0 1 0 487629076 258207744 55827 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63039 55827 603 41 0 62998 0
vsize: 252156
[startup+650.005 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 9792
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 64685 0 0 0 64847 161 0 0 25 0 1 0 487629076 258875392 55989 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63202 55989 603 41 0 63161 0
vsize: 252808
[startup+660.005 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 64838 0 0 0 65847 162 0 0 25 0 1 0 487629076 259399680 56142 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63330 56142 603 41 0 63289 0
vsize: 253320
[startup+670.005 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 65016 0 0 0 66847 162 0 0 25 0 1 0 487629076 260186112 56320 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63522 56320 603 41 0 63481 0
vsize: 254088
[startup+680.005 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 65202 0 0 0 67846 163 0 0 25 0 1 0 487629076 261042176 56506 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63731 56506 603 41 0 63690 0
vsize: 254924
[startup+690.005 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 65374 0 0 0 68846 163 0 0 25 0 1 0 487629076 261726208 56678 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63898 56678 603 41 0 63857 0
vsize: 255592
[startup+700.005 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 65523 0 0 0 69845 164 0 0 25 0 1 0 487629076 262389760 56827 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64060 56827 603 41 0 64019 0
vsize: 256240
[startup+710.005 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 65697 0 0 0 70845 165 0 0 25 0 1 0 487629076 263053312 57001 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64222 57001 603 41 0 64181 0
vsize: 256888
[startup+720.005 s]
Raw data (loadavg): 1.00 1.00 0.89 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 65846 0 0 0 71844 165 0 0 25 0 1 0 487629076 263884800 57150 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64425 57150 603 41 0 64384 0
vsize: 257700
[startup+730.006 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 65960 0 0 0 72844 166 0 0 25 0 1 0 487629076 264282112 57264 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64522 57264 603 41 0 64481 0
vsize: 258088
[startup+740.005 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 66106 0 0 0 73844 166 0 0 25 0 1 0 487629076 264810496 57410 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64651 57410 603 41 0 64610 0
vsize: 258604
[startup+750.006 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 66239 0 0 0 74843 167 0 0 25 0 1 0 487629076 265359360 57543 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64785 57543 603 41 0 64744 0
vsize: 259140
[startup+760.006 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 66413 0 0 0 75843 167 0 0 25 0 1 0 487629076 266018816 57717 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64946 57717 603 41 0 64905 0
vsize: 259784
[startup+770.006 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 66525 0 0 0 76843 168 0 0 25 0 1 0 487629076 267595776 57829 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65331 57829 603 41 0 65290 0
vsize: 261324
[startup+780.007 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 66664 0 0 0 77842 169 0 0 25 0 1 0 487629076 268267520 57968 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65495 57968 603 41 0 65454 0
vsize: 261980
[startup+790.006 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 66800 0 0 0 78842 169 0 0 25 0 1 0 487629076 268800000 58104 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65625 58104 603 41 0 65584 0
vsize: 262500
[startup+800.006 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 66926 0 0 0 79842 169 0 0 25 0 1 0 487629076 269377536 58230 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65766 58230 603 41 0 65725 0
vsize: 263064
[startup+810.007 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 67060 0 0 0 80841 170 0 0 25 0 1 0 487629076 269824000 58364 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65875 58364 603 41 0 65834 0
vsize: 263500
[startup+820.006 s]
Raw data (loadavg): 1.00 1.00 0.90 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 67226 0 0 0 81841 170 0 0 25 0 1 0 487629076 270610432 58530 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66067 58530 603 41 0 66026 0
vsize: 264268
[startup+830.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 67385 0 0 0 82841 171 0 0 25 0 1 0 487629076 271142912 58689 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66197 58689 603 41 0 66156 0
vsize: 264788
[startup+840.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 67539 0 0 0 83841 171 0 0 25 0 1 0 487629076 271876096 58843 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66376 58843 603 41 0 66335 0
vsize: 265504
[startup+850.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 67697 0 0 0 84841 171 0 0 25 0 1 0 487629076 272535552 59001 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66537 59001 603 41 0 66496 0
vsize: 266148
[startup+860.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 67896 0 0 0 85840 172 0 0 25 0 1 0 487629076 273354752 59200 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66737 59200 603 41 0 66696 0
vsize: 266948
[startup+870.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 68069 0 0 0 86840 172 0 0 25 0 1 0 487629076 274014208 59373 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66898 59373 603 41 0 66857 0
vsize: 267592
[startup+880.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 68241 0 0 0 87840 173 0 0 25 0 1 0 487629076 274702336 59545 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67066 59545 603 41 0 67025 0
vsize: 268264
[startup+890.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 68392 0 0 0 88839 173 0 0 25 0 1 0 487629076 275374080 59696 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67230 59696 603 41 0 67189 0
vsize: 268920
[startup+900.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 68547 0 0 0 89839 174 0 0 25 0 1 0 487629076 276049920 59851 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67395 59851 603 41 0 67354 0
vsize: 269580
[startup+910.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 68663 0 0 0 90839 174 0 0 25 0 1 0 487629076 276443136 59967 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67491 59967 603 41 0 67450 0
vsize: 269964
[startup+920.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 68785 0 0 0 91838 175 0 0 25 0 1 0 487629076 276975616 60089 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67621 60089 603 41 0 67580 0
vsize: 270484
[startup+930.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 68926 0 0 0 92838 175 0 0 25 0 1 0 487629076 277499904 60230 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67749 60230 603 41 0 67708 0
vsize: 270996
[startup+940.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 69074 0 0 0 93837 176 0 0 25 0 1 0 487629076 278155264 60378 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67909 60378 603 41 0 67868 0
vsize: 271636
[startup+950.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 69215 0 0 0 94837 177 0 0 25 0 1 0 487629076 278843392 60519 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68077 60519 603 41 0 68036 0
vsize: 272308
[startup+960.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 69304 0 0 0 95837 177 0 0 25 0 1 0 487629076 279105536 60608 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68141 60608 603 41 0 68100 0
vsize: 272564
[startup+970.005 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 69423 0 0 0 96837 177 0 0 25 0 1 0 487629076 279633920 60727 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68270 60727 603 41 0 68229 0
vsize: 273080
[startup+980.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 69553 0 0 0 97837 177 0 0 25 0 1 0 487629076 280162304 60857 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68399 60857 603 41 0 68358 0
vsize: 273596
[startup+990.006 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 69657 0 0 0 98837 178 0 0 25 0 1 0 487629076 280555520 60961 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68495 60961 603 41 0 68454 0
vsize: 273980
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 69902 0 0 0 99836 178 0 0 25 0 1 0 487629076 281489408 61206 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68723 61206 603 41 0 68682 0
vsize: 274892
[startup+1010 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 70116 0 0 0 100836 179 0 0 25 0 1 0 487629076 282415104 61420 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68949 61420 603 41 0 68908 0
vsize: 275796
[startup+1020 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 70410 0 0 0 101835 180 0 0 25 0 1 0 487629076 283615232 61714 4294967295 134512640 134672761 3221224560 3221223760 134610711 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69242 61714 603 41 0 69201 0
vsize: 276968
[startup+1030.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 70485 0 0 0 102835 180 0 0 25 0 1 0 487629076 283881472 61789 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69307 61789 603 41 0 69266 0
vsize: 277228
[startup+1040.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 70603 0 0 0 103835 180 0 0 25 0 1 0 487629076 284438528 61907 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69443 61907 603 41 0 69402 0
vsize: 277772
[startup+1050.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 70685 0 0 0 104835 181 0 0 25 0 1 0 487629076 284700672 61989 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69507 61989 603 41 0 69466 0
vsize: 278028
[startup+1060.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 70791 0 0 0 105835 181 0 0 25 0 1 0 487629076 285126656 62095 4294967295 134512640 134672761 3221224560 3221223724 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69611 62095 603 41 0 69570 0
vsize: 278444
[startup+1070.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 70902 0 0 0 106835 181 0 0 25 0 1 0 487629076 285704192 62206 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69752 62206 603 41 0 69711 0
vsize: 279008
[startup+1080.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 71014 0 0 0 107835 181 0 0 25 0 1 0 487629076 286101504 62318 4294967295 134512640 134672761 3221224560 3221223744 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69849 62318 603 41 0 69808 0
vsize: 279396
[startup+1090.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 71139 0 0 0 108835 181 0 0 25 0 1 0 487629076 286633984 62443 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69979 62443 603 41 0 69938 0
vsize: 279916
[startup+1100.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 71244 0 0 0 109835 182 0 0 25 0 1 0 487629076 287162368 62548 4294967295 134512640 134672761 3221224560 3221223512 1075347141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70108 62548 603 41 0 70067 0
vsize: 280432
[startup+1110.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 71375 0 0 0 110834 182 0 0 25 0 1 0 487629076 287559680 62679 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70205 62679 603 41 0 70164 0
vsize: 280820
[startup+1120.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 71497 0 0 0 111834 182 0 0 25 0 1 0 487629076 288092160 62801 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70335 62801 603 41 0 70294 0
vsize: 281340
[startup+1130.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 71629 0 0 0 112834 183 0 0 25 0 1 0 487629076 288616448 62933 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70463 62933 603 41 0 70422 0
vsize: 281852
[startup+1140.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 71762 0 0 0 113834 183 0 0 25 0 1 0 487629076 289148928 63066 4294967295 134512640 134672761 3221224560 3221223744 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70593 63066 603 41 0 70552 0
vsize: 282372
[startup+1150.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 71910 0 0 0 114834 183 0 0 25 0 1 0 487629076 289816576 63214 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70756 63214 603 41 0 70715 0
vsize: 283024
[startup+1160.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 72041 0 0 0 115834 184 0 0 25 0 1 0 487629076 290344960 63345 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70885 63345 603 41 0 70844 0
vsize: 283540
[startup+1170.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 72161 0 0 0 116834 184 0 0 25 0 1 0 487629076 290742272 63465 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70982 63465 603 41 0 70941 0
vsize: 283928
[startup+1180.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 72297 0 0 0 117834 184 0 0 25 0 1 0 487629076 291397632 63601 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71142 63601 603 41 0 71101 0
vsize: 284568
[startup+1190.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 72434 0 0 0 118834 184 0 0 25 0 1 0 487629076 291921920 63738 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71270 63738 603 41 0 71229 0
vsize: 285080
[startup+1200.01 s]
Raw data (loadavg): 1.00 1.00 0.91 2/54 9794
Raw data (stat): 9737 (minisat+) R 9736 27565 27564 0 -1 0 72565 0 0 0 119833 185 0 0 25 0 1 0 487629076 292450304 63869 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71399 63869 603 41 0 71358 0
vsize: 285596
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.00 1.00 0.91 1/54 9794
Raw data (stat): 9737 (minisat+) Z 9736 27565 27564 0 -1 12 72565 0 0 0 119833 197 0 0 25 0 1 0 487629076 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.13
CPU time (s): 1200.32
CPU user time (s): 1198.34
CPU system time (s): 1.9767
CPU usage (%): 100.015
Max. virtual memory (Kb): 285596
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####