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 7038

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        838024 kB
Buffers:         35756 kB
Cached:         124880 kB
SwapCached:        320 kB
Active:          60808 kB
Inactive:       103004 kB
HighTotal:      131008 kB
HighFree:         2128 kB
LowTotal:       903652 kB
LowFree:        835896 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27280 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 21:16:56 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 5083 7 1200.26 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  860884  3056763 |  286961       0        0     nan |  0.000 % |
c |       100 |  860849  3056646 |  315657      96      298     3.1 |  1.442 % |
c |       250 |  860631  3055899 |  347222     227      744     3.3 |  1.467 % |
c |       475 |  860622  3055870 |  381945     451     2393     5.3 |  1.468 % |
c |       812 |  860583  3055732 |  420139     787     3989     5.1 |  1.469 % |
c |      1318 |  860539  3055581 |  462153    1292     5758     4.5 |  1.470 % |
c |      2077 |  860306  3054750 |  508368    2045     8405     4.1 |  1.475 % |
c |      3216 |  860218  3054446 |  559205    3181    13211     4.2 |  1.478 % |
c |      4924 |  859759  3052817 |  615126    4879    21952     4.5 |  1.487 % |
c |      7487 |  858945  3049932 |  676639    7423    35730     4.8 |  1.503 % |
c |     11331 |  858667  3048933 |  744302   11262    88137     7.8 |  1.507 % |
c |     17100 |  858662  3048918 |  818733   17030   219855    12.9 |  1.508 % |
c |     25749 |  858600  3048694 |  900606   25678   423396    16.5 |  1.509 % |
c |     38723 |  858556  3048536 |  990667   38651   953197    24.7 |  1.510 % |
c |     58184 |  858556  3048536 | 1089733   58112  3038664    52.3 |  1.510 % |
c |     87377 |  858340  3047768 | 1198707   87300  4372939    50.1 |  1.515 % |
c |    131166 |  858335  3047753 | 1318578  131088  6092405    46.5 |  1.516 % |
c |    196850 |  858128  3047025 | 1450435  196767 10160334    51.6 |  1.521 % |
c |    295376 |  858004  3046584 | 1595479  295291 13810327    46.8 |  1.523 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.89 0.94 0.82 2/55 2569
Raw data (stat): 2569 (runsolver) R 2568 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487636269 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 s]
Raw data (loadavg): 0.90 0.94 0.82 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 3732 0 0 0 990 8 0 0 25 0 1 0 487636269 12267520 2442 4294967295 134512640 134672761 3221224560 3221222832 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2995 2442 603 41 0 2954 0
vsize: 11980
[startup+20.0009 s]
Raw data (loadavg): 0.92 0.95 0.82 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 14075 0 0 0 1966 32 0 0 25 0 1 0 487636269 46931968 10253 4294967295 134512640 134672761 3221224560 3221223744 134593677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11458 10253 603 41 0 11417 0
vsize: 45832
[startup+30.0018 s]
Raw data (loadavg): 0.93 0.95 0.82 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 14778 0 0 0 2965 34 0 0 25 0 1 0 487636269 46993408 10286 4294967295 134512640 134672761 3221224560 3221223120 134597188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11473 10286 603 41 0 11432 0
vsize: 45892
[startup+40.003 s]
Raw data (loadavg): 0.94 0.95 0.82 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 30420 0 0 0 3931 68 0 0 25 0 1 0 487636269 125960192 25866 4294967295 134512640 134672761 3221224560 3221223812 134562288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30752 25866 603 41 0 30711 0
vsize: 123008
[startup+50.0039 s]
Raw data (loadavg): 0.95 0.95 0.82 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 30930 0 0 0 4928 70 0 0 25 0 1 0 487636269 128000000 26376 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31250 26376 603 41 0 31209 0
vsize: 125000
[startup+60.0039 s]
Raw data (loadavg): 0.96 0.95 0.82 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 31105 0 0 0 5927 71 0 0 25 0 1 0 487636269 128819200 26551 4294967295 134512640 134672761 3221224560 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31450 26551 603 41 0 31409 0
vsize: 125800
[startup+70.0048 s]
Raw data (loadavg): 0.96 0.95 0.82 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 31234 0 0 0 6926 71 0 0 25 0 1 0 487636269 129372160 26680 4294967295 134512640 134672761 3221224560 3221223684 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31585 26680 603 41 0 31544 0
vsize: 126340
[startup+80.0057 s]
Raw data (loadavg): 0.97 0.95 0.83 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 31588 0 0 0 7924 73 0 0 25 0 1 0 487636269 130711552 27034 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31912 27034 603 41 0 31871 0
vsize: 127648
[startup+90.0064 s]
Raw data (loadavg): 0.97 0.95 0.83 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 32267 0 0 0 8922 75 0 0 25 0 1 0 487636269 133677056 27713 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32636 27713 603 41 0 32595 0
vsize: 130544
[startup+100.006 s]
Raw data (loadavg): 0.98 0.95 0.83 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 32961 0 0 0 9920 77 0 0 25 0 1 0 487636269 136491008 28407 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33323 28407 603 41 0 33282 0
vsize: 133292
[startup+110.006 s]
Raw data (loadavg): 0.98 0.95 0.83 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 33702 0 0 0 10919 79 0 0 25 0 1 0 487636269 139452416 29148 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34046 29148 603 41 0 34005 0
vsize: 136184
[startup+120.007 s]
Raw data (loadavg): 0.98 0.95 0.83 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 34327 0 0 0 11917 80 0 0 25 0 1 0 487636269 142020608 29773 4294967295 134512640 134672761 3221224560 3221223728 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34673 29773 603 41 0 34632 0
vsize: 138692
[startup+130.007 s]
Raw data (loadavg): 0.98 0.96 0.83 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 34849 0 0 0 12916 81 0 0 25 0 1 0 487636269 144183296 30295 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35201 30295 603 41 0 35160 0
vsize: 140804
[startup+140.008 s]
Raw data (loadavg): 0.99 0.96 0.83 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 35127 0 0 0 13914 82 0 0 25 0 1 0 487636269 145260544 30573 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35464 30573 603 41 0 35423 0
vsize: 141856
[startup+150.009 s]
Raw data (loadavg): 0.99 0.96 0.83 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 35659 0 0 0 14912 85 0 0 25 0 1 0 487636269 147677184 31105 4294967295 134512640 134672761 3221224560 3221223696 134560726 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36054 31105 603 41 0 36013 0
vsize: 144216
[startup+160.009 s]
Raw data (loadavg): 0.99 0.96 0.83 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 36167 0 0 0 15910 87 0 0 25 0 1 0 487636269 149827584 31613 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36579 31613 603 41 0 36538 0
vsize: 146316
[startup+170.01 s]
Raw data (loadavg): 0.99 0.96 0.83 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 36590 0 0 0 16909 88 0 0 25 0 1 0 487636269 151445504 32036 4294967295 134512640 134672761 3221224560 3221223796 134557472 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36974 32036 603 41 0 36933 0
vsize: 147896
[startup+180.01 s]
Raw data (loadavg): 0.99 0.96 0.83 2/55 2569
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 36952 0 0 0 17908 89 0 0 25 0 1 0 487636269 152915968 32398 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37333 32398 603 41 0 37292 0
vsize: 149332
[startup+190.014 s]
Raw data (loadavg): 0.99 0.96 0.84 2/56 2570
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 37306 0 0 0 18908 90 0 0 25 0 1 0 487636269 154394624 32752 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37694 32752 603 41 0 37653 0
vsize: 150776
[startup+200.015 s]
Raw data (loadavg): 1.22 1.01 0.85 2/55 2622
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 37572 0 0 0 19907 91 0 0 25 0 1 0 487636269 155463680 33018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37955 33018 603 41 0 37914 0
vsize: 151820
[startup+210.014 s]
Raw data (loadavg): 1.19 1.01 0.85 2/55 2622
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 37834 0 0 0 20907 91 0 0 25 0 1 0 487636269 156528640 33280 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38215 33280 603 41 0 38174 0
vsize: 152860
[startup+220.015 s]
Raw data (loadavg): 1.16 1.01 0.85 2/55 2622
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 38083 0 0 0 21906 92 0 0 25 0 1 0 487636269 157478912 33529 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38447 33529 603 41 0 38406 0
vsize: 153788
[startup+230.015 s]
Raw data (loadavg): 1.13 1.01 0.86 2/55 2622
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 38288 0 0 0 22906 92 0 0 25 0 1 0 487636269 158285824 33734 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38644 33734 603 41 0 38603 0
vsize: 154576
[startup+240.016 s]
Raw data (loadavg): 1.11 1.01 0.86 2/55 2622
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 38477 0 0 0 23905 93 0 0 25 0 1 0 487636269 159088640 33923 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38840 33923 603 41 0 38799 0
vsize: 155360
[startup+250.016 s]
Raw data (loadavg): 1.09 1.01 0.86 2/55 2622
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 38715 0 0 0 24905 94 0 0 25 0 1 0 487636269 160600064 34161 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39209 34161 603 41 0 39168 0
vsize: 156836
[startup+260.016 s]
Raw data (loadavg): 1.08 1.01 0.86 2/55 2622
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 38881 0 0 0 25905 94 0 0 25 0 1 0 487636269 161271808 34327 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39373 34327 603 41 0 39332 0
vsize: 157492
[startup+270.017 s]
Raw data (loadavg): 1.07 1.01 0.86 2/55 2624
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 39100 0 0 0 26905 95 0 0 25 0 1 0 487636269 162263040 34546 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39615 34546 603 41 0 39574 0
vsize: 158460
[startup+280.017 s]
Raw data (loadavg): 1.06 1.00 0.86 2/55 2624
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 39341 0 0 0 27904 95 0 0 25 0 1 0 487636269 163209216 34787 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39846 34787 603 41 0 39805 0
vsize: 159384
[startup+290.018 s]
Raw data (loadavg): 1.05 1.00 0.86 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 39563 0 0 0 28904 96 0 0 25 0 1 0 487636269 164044800 35009 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40050 35009 603 41 0 40009 0
vsize: 160200
[startup+300.017 s]
Raw data (loadavg): 1.04 1.00 0.86 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 39795 0 0 0 29903 96 0 0 25 0 1 0 487636269 164990976 35241 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40281 35241 603 41 0 40240 0
vsize: 161124
[startup+310.017 s]
Raw data (loadavg): 1.03 1.00 0.86 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 40008 0 0 0 30903 97 0 0 25 0 1 0 487636269 165957632 35454 4294967295 134512640 134672761 3221224560 3221223696 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40517 35454 603 41 0 40476 0
vsize: 162068
[startup+320.018 s]
Raw data (loadavg): 1.03 1.00 0.86 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 40199 0 0 0 31903 98 0 0 25 0 1 0 487636269 166625280 35645 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40680 35645 603 41 0 40639 0
vsize: 162720
[startup+330.018 s]
Raw data (loadavg): 1.02 1.00 0.87 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 40375 0 0 0 32902 98 0 0 25 0 1 0 487636269 167497728 35821 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40893 35821 603 41 0 40852 0
vsize: 163572
[startup+340.019 s]
Raw data (loadavg): 1.02 1.00 0.87 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 40676 0 0 0 33902 99 0 0 25 0 1 0 487636269 168677376 36122 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41181 36122 603 41 0 41140 0
vsize: 164724
[startup+350.019 s]
Raw data (loadavg): 1.02 1.00 0.87 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 41028 0 0 0 34901 99 0 0 25 0 1 0 487636269 170164224 36474 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41544 36474 603 41 0 41503 0
vsize: 166176
[startup+360.019 s]
Raw data (loadavg): 1.01 1.00 0.87 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 41468 0 0 0 35900 101 0 0 25 0 1 0 487636269 171921408 36914 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41973 36914 603 41 0 41932 0
vsize: 167892
[startup+370.019 s]
Raw data (loadavg): 1.01 1.00 0.87 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 42073 0 0 0 36899 102 0 0 25 0 1 0 487636269 174456832 37519 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42592 37519 603 41 0 42551 0
vsize: 170368
[startup+380.019 s]
Raw data (loadavg): 1.01 1.00 0.87 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 42620 0 0 0 37897 104 0 0 25 0 1 0 487636269 176611328 38066 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43118 38066 603 41 0 43077 0
vsize: 172472
[startup+390.02 s]
Raw data (loadavg): 1.01 1.00 0.87 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 43173 0 0 0 38896 106 0 0 25 0 1 0 487636269 178896896 38619 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43676 38619 603 41 0 43635 0
vsize: 174704
[startup+400.021 s]
Raw data (loadavg): 1.00 1.00 0.87 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 43476 0 0 0 39895 107 0 0 25 0 1 0 487636269 180125696 38922 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43976 38922 603 41 0 43935 0
vsize: 175904
[startup+410.021 s]
Raw data (loadavg): 1.00 1.00 0.87 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 43636 0 0 0 40894 108 0 0 25 0 1 0 487636269 180797440 39082 4294967295 134512640 134672761 3221224560 3221223712 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44140 39082 603 41 0 44099 0
vsize: 176560
[startup+420.02 s]
Raw data (loadavg): 1.00 1.00 0.87 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 43807 0 0 0 41894 108 0 0 25 0 1 0 487636269 181481472 39253 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44307 39253 603 41 0 44266 0
vsize: 177228
[startup+430.02 s]
Raw data (loadavg): 1.00 1.00 0.88 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 44004 0 0 0 42894 108 0 0 25 0 1 0 487636269 182304768 39450 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44508 39450 603 41 0 44467 0
vsize: 178032
[startup+440.022 s]
Raw data (loadavg): 1.00 1.00 0.88 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 44268 0 0 0 43893 109 0 0 25 0 1 0 487636269 183382016 39714 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44771 39714 603 41 0 44730 0
vsize: 179084
[startup+450.021 s]
Raw data (loadavg): 1.00 1.00 0.88 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 44471 0 0 0 44892 110 0 0 25 0 1 0 487636269 184193024 39917 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44969 39917 603 41 0 44928 0
vsize: 179876
[startup+460.021 s]
Raw data (loadavg): 1.00 1.00 0.88 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 44654 0 0 0 45893 110 0 0 25 0 1 0 487636269 184864768 40100 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45133 40100 603 41 0 45092 0
vsize: 180532
[startup+470.022 s]
Raw data (loadavg): 1.00 1.00 0.88 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 44824 0 0 0 46892 110 0 0 25 0 1 0 487636269 185540608 40270 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45298 40270 603 41 0 45257 0
vsize: 181192
[startup+480.022 s]
Raw data (loadavg): 1.00 1.00 0.88 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 44982 0 0 0 47892 111 0 0 25 0 1 0 487636269 186253312 40428 4294967295 134512640 134672761 3221224560 3221223664 134555164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45472 40428 603 41 0 45431 0
vsize: 181888
[startup+490.023 s]
Raw data (loadavg): 1.00 1.00 0.88 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 45122 0 0 0 48892 111 0 0 25 0 1 0 487636269 186826752 40568 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45612 40568 603 41 0 45571 0
vsize: 182448
[startup+500.024 s]
Raw data (loadavg): 1.00 1.00 0.88 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 45275 0 0 0 49892 111 0 0 25 0 1 0 487636269 187498496 40721 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45776 40721 603 41 0 45735 0
vsize: 183104
[startup+510.024 s]
Raw data (loadavg): 1.00 1.00 0.88 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 45404 0 0 0 50892 112 0 0 25 0 1 0 487636269 188080128 40850 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45918 40850 603 41 0 45877 0
vsize: 183672
[startup+520.024 s]
Raw data (loadavg): 1.00 1.00 0.88 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 45568 0 0 0 51891 112 0 0 25 0 1 0 487636269 188821504 41014 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46099 41014 603 41 0 46058 0
vsize: 184396
[startup+530.024 s]
Raw data (loadavg): 1.00 1.00 0.89 2/55 2626
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 45672 0 0 0 52891 113 0 0 25 0 1 0 487636269 189239296 41118 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46201 41118 603 41 0 46160 0
vsize: 184804
[startup+540.024 s]
Raw data (loadavg): 1.00 1.00 0.89 2/55 2628
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 45782 0 0 0 53891 113 0 0 25 0 1 0 487636269 189640704 41228 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46299 41228 603 41 0 46258 0
vsize: 185196
[startup+550.024 s]
Raw data (loadavg): 1.00 1.00 0.89 2/55 2628
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 45899 0 0 0 54891 113 0 0 25 0 1 0 487636269 190173184 41345 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46429 41345 603 41 0 46388 0
vsize: 185716
[startup+560.025 s]
Raw data (loadavg): 1.00 1.00 0.89 2/55 2628
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 46019 0 0 0 55891 114 0 0 25 0 1 0 487636269 190590976 41465 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46531 41465 603 41 0 46490 0
vsize: 186124
[startup+570.026 s]
Raw data (loadavg): 1.00 1.00 0.89 2/55 2628
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 46134 0 0 0 56891 114 0 0 25 0 1 0 487636269 191127552 41580 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46662 41580 603 41 0 46621 0
vsize: 186648
[startup+580.026 s]
Raw data (loadavg): 1.00 1.00 0.89 2/55 2628
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 46270 0 0 0 57891 114 0 0 25 0 1 0 487636269 192712704 41716 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47049 41716 603 41 0 47008 0
vsize: 188196
[startup+590.027 s]
Raw data (loadavg): 1.00 1.00 0.89 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 46387 0 0 0 58891 114 0 0 25 0 1 0 487636269 193122304 41833 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47149 41833 603 41 0 47108 0
vsize: 188596
[startup+600.027 s]
Raw data (loadavg): 1.00 1.00 0.89 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 46508 0 0 0 59890 115 0 0 25 0 1 0 487636269 193658880 41954 4294967295 134512640 134672761 3221224560 3221223744 134558754 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47280 41954 603 41 0 47239 0
vsize: 189120
[startup+610.027 s]
Raw data (loadavg): 1.00 1.00 0.89 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 46640 0 0 0 60890 115 0 0 25 0 1 0 487636269 194199552 42086 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47412 42086 603 41 0 47371 0
vsize: 189648
[startup+620.028 s]
Raw data (loadavg): 1.00 1.00 0.89 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 46757 0 0 0 61890 116 0 0 25 0 1 0 487636269 194600960 42203 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47510 42203 603 41 0 47469 0
vsize: 190040
[startup+630.028 s]
Raw data (loadavg): 1.00 1.00 0.89 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 46872 0 0 0 62890 116 0 0 25 0 1 0 487636269 195137536 42318 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47641 42318 603 41 0 47600 0
vsize: 190564
[startup+640.029 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 46997 0 0 0 63890 116 0 0 25 0 1 0 487636269 195543040 42443 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47740 42443 603 41 0 47699 0
vsize: 190960
[startup+650.03 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 47123 0 0 0 64890 117 0 0 25 0 1 0 487636269 196079616 42569 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47871 42569 603 41 0 47830 0
vsize: 191484
[startup+660.029 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 47249 0 0 0 65889 117 0 0 25 0 1 0 487636269 196681728 42695 4294967295 134512640 134672761 3221224560 3221223744 134559342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48018 42695 603 41 0 47977 0
vsize: 192072
[startup+670.03 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 47379 0 0 0 66889 117 0 0 25 0 1 0 487636269 197222400 42825 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48150 42825 603 41 0 48109 0
vsize: 192600
[startup+680.031 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 47501 0 0 0 67889 117 0 0 25 0 1 0 487636269 197627904 42947 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48249 42947 603 41 0 48208 0
vsize: 192996
[startup+690.031 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 47644 0 0 0 68890 117 0 0 25 0 1 0 487636269 198356992 43090 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48427 43090 603 41 0 48386 0
vsize: 193708
[startup+700.032 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 47776 0 0 0 69889 118 0 0 25 0 1 0 487636269 198893568 43222 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48558 43222 603 41 0 48517 0
vsize: 194232
[startup+710.031 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 47979 0 0 0 70889 118 0 0 25 0 1 0 487636269 199696384 43425 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48754 43425 603 41 0 48713 0
vsize: 195016
[startup+720.031 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 48309 0 0 0 71887 120 0 0 25 0 1 0 487636269 201048064 43755 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49084 43755 603 41 0 49043 0
vsize: 196336
[startup+730.031 s]
Raw data (loadavg): 1.00 1.00 0.90 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 48558 0 0 0 72887 121 0 0 25 0 1 0 487636269 202014720 44004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49320 44004 603 41 0 49279 0
vsize: 197280
[startup+740.032 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 48853 0 0 0 73886 122 0 0 25 0 1 0 487636269 203374592 44299 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49652 44299 603 41 0 49611 0
vsize: 198608
[startup+750.033 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 48993 0 0 0 74886 122 0 0 25 0 1 0 487636269 203911168 44439 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49783 44439 603 41 0 49742 0
vsize: 199132
[startup+760.033 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 49161 0 0 0 75886 123 0 0 25 0 1 0 487636269 204578816 44607 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49946 44607 603 41 0 49905 0
vsize: 199784
[startup+770.034 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 49372 0 0 0 76885 123 0 0 25 0 1 0 487636269 205418496 44818 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50151 44818 603 41 0 50110 0
vsize: 200604
[startup+780.034 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 49608 0 0 0 77884 124 0 0 25 0 1 0 487636269 206356480 45054 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50380 45054 603 41 0 50339 0
vsize: 201520
[startup+790.034 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 49822 0 0 0 78884 125 0 0 25 0 1 0 487636269 207159296 45268 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50576 45268 603 41 0 50535 0
vsize: 202304
[startup+800.035 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 50023 0 0 0 79883 126 0 0 25 0 1 0 487636269 207958016 45469 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50771 45469 603 41 0 50730 0
vsize: 203084
[startup+810.034 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 50242 0 0 0 80883 126 0 0 25 0 1 0 487636269 208891904 45688 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50999 45688 603 41 0 50958 0
vsize: 203996
[startup+820.036 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 50463 0 0 0 81882 127 0 0 25 0 1 0 487636269 209825792 45909 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51227 45909 603 41 0 51186 0
vsize: 204908
[startup+830.035 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 50671 0 0 0 82882 128 0 0 25 0 1 0 487636269 210632704 46117 4294967295 134512640 134672761 3221224560 3221223728 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51424 46117 603 41 0 51383 0
vsize: 205696
[startup+840.035 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 50873 0 0 0 83881 128 0 0 25 0 1 0 487636269 211468288 46319 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51628 46319 603 41 0 51587 0
vsize: 206512
[startup+850.036 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 51069 0 0 0 84880 129 0 0 25 0 1 0 487636269 212271104 46515 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51824 46515 603 41 0 51783 0
vsize: 207296
[startup+860.036 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 51263 0 0 0 85880 130 0 0 25 0 1 0 487636269 213073920 46709 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52020 46709 603 41 0 51979 0
vsize: 208080
[startup+870.037 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 51469 0 0 0 86879 131 0 0 25 0 1 0 487636269 213901312 46915 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52222 46915 603 41 0 52181 0
vsize: 208888
[startup+880.037 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2630
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 51591 0 0 0 87879 131 0 0 25 0 1 0 487636269 214446080 47037 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52355 47037 603 41 0 52314 0
vsize: 209420
[startup+890.037 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 51713 0 0 0 88878 132 0 0 25 0 1 0 487636269 214990848 47159 4294967295 134512640 134672761 3221224560 3221223728 134561121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52488 47159 603 41 0 52447 0
vsize: 209952
[startup+900.037 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 51821 0 0 0 89878 132 0 0 25 0 1 0 487636269 215388160 47267 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52585 47267 603 41 0 52544 0
vsize: 210340
[startup+910.037 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 51907 0 0 0 90878 133 0 0 25 0 1 0 487636269 215785472 47353 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52682 47353 603 41 0 52641 0
vsize: 210728
[startup+920.038 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 51991 0 0 0 91878 133 0 0 25 0 1 0 487636269 216051712 47437 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52747 47437 603 41 0 52706 0
vsize: 210988
[startup+930.037 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 52092 0 0 0 92878 133 0 0 25 0 1 0 487636269 216461312 47538 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52847 47538 603 41 0 52806 0
vsize: 211388
[startup+940.037 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 52186 0 0 0 93878 133 0 0 25 0 1 0 487636269 216862720 47632 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52945 47632 603 41 0 52904 0
vsize: 211780
[startup+950.037 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 52278 0 0 0 94878 133 0 0 25 0 1 0 487636269 217260032 47724 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53042 47724 603 41 0 53001 0
vsize: 212168
[startup+960.037 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 52385 0 0 0 95878 134 0 0 25 0 1 0 487636269 217657344 47831 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53139 47831 603 41 0 53098 0
vsize: 212556
[startup+970.037 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 52500 0 0 0 96878 134 0 0 25 0 1 0 487636269 218066944 47946 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53239 47946 603 41 0 53198 0
vsize: 212956
[startup+980.037 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 52609 0 0 0 97878 134 0 0 25 0 1 0 487636269 218550272 48055 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53357 48055 603 41 0 53316 0
vsize: 213428
[startup+990.037 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 52711 0 0 0 98877 135 0 0 25 0 1 0 487636269 219078656 48157 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53486 48157 603 41 0 53445 0
vsize: 213944
[startup+1000.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 52812 0 0 0 99877 135 0 0 25 0 1 0 487636269 219484160 48258 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53585 48258 603 41 0 53544 0
vsize: 214340
[startup+1010.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 52904 0 0 0 100877 135 0 0 25 0 1 0 487636269 219881472 48350 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53682 48350 603 41 0 53641 0
vsize: 214728
[startup+1020.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 53004 0 0 0 101877 135 0 0 25 0 1 0 487636269 220282880 48450 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53780 48450 603 41 0 53739 0
vsize: 215120
[startup+1030.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 53107 0 0 0 102877 135 0 0 25 0 1 0 487636269 220684288 48553 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53878 48553 603 41 0 53837 0
vsize: 215512
[startup+1040.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 53205 0 0 0 103877 136 0 0 25 0 1 0 487636269 221081600 48651 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53975 48651 603 41 0 53934 0
vsize: 215900
[startup+1050.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 53303 0 0 0 104877 136 0 0 25 0 1 0 487636269 221483008 48749 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54073 48749 603 41 0 54032 0
vsize: 216292
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 53405 0 0 0 105877 136 0 0 25 0 1 0 487636269 221880320 48851 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54170 48851 603 41 0 54129 0
vsize: 216680
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 53527 0 0 0 106877 136 0 0 25 0 1 0 487636269 222433280 48973 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54305 48973 603 41 0 54264 0
vsize: 217220
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 53640 0 0 0 107877 137 0 0 25 0 1 0 487636269 222834688 49086 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54403 49086 603 41 0 54362 0
vsize: 217612
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 53763 0 0 0 108877 137 0 0 25 0 1 0 487636269 223502336 49209 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54566 49209 603 41 0 54525 0
vsize: 218264
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 53902 0 0 0 109876 138 0 0 25 0 1 0 487636269 224034816 49348 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54696 49348 603 41 0 54655 0
vsize: 218784
[startup+1110.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 54048 0 0 0 110875 139 0 0 25 0 1 0 487636269 224571392 49494 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54827 49494 603 41 0 54786 0
vsize: 219308
[startup+1120.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 54165 0 0 0 111875 139 0 0 25 0 1 0 487636269 225120256 49611 4294967295 134512640 134672761 3221224560 3221223696 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54961 49611 603 41 0 54920 0
vsize: 219844
[startup+1130.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 54284 0 0 0 112875 139 0 0 25 0 1 0 487636269 225693696 49730 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55101 49730 603 41 0 55060 0
vsize: 220404
[startup+1140.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 54422 0 0 0 113875 140 0 0 25 0 1 0 487636269 226226176 49868 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55231 49868 603 41 0 55190 0
vsize: 220924
[startup+1150.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 54558 0 0 0 114874 140 0 0 25 0 1 0 487636269 226766848 50004 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55363 50004 603 41 0 55322 0
vsize: 221452
[startup+1160.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 54676 0 0 0 115874 141 0 0 25 0 1 0 487636269 227196928 50122 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55468 50122 603 41 0 55427 0
vsize: 221872
[startup+1170.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 54812 0 0 0 116874 141 0 0 25 0 1 0 487636269 227737600 50258 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55600 50258 603 41 0 55559 0
vsize: 222400
[startup+1180.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2632
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 54944 0 0 0 117874 141 0 0 25 0 1 0 487636269 228274176 50390 4294967295 134512640 134672761 3221224560 3221223744 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55731 50390 603 41 0 55690 0
vsize: 222924
[startup+1190.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2634
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 55095 0 0 0 118873 142 0 0 25 0 1 0 487636269 228810752 50541 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55862 50541 603 41 0 55821 0
vsize: 223448
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.91 2/55 2634
Raw data (stat): 2569 (minisat+) R 2568 20024 20023 0 -1 0 55224 0 0 0 119873 142 0 0 25 0 1 0 487636269 229363712 50670 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55997 50670 603 41 0 55956 0
vsize: 223988
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.91 1/55 2634
Raw data (stat): 2569 (minisat+) Z 2568 20024 20023 0 -1 12 55226 0 0 0 119873 152 0 0 25 0 1 0 487636269 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.14
CPU time (s): 1200.26
CPU user time (s): 1198.74
CPU system time (s): 1.52377
CPU usage (%): 100.01
Max. virtual memory (Kb): 223988
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####