Name | mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-grow22.opb |
MD5SUM | c03619cd7187044150b0404ea204a73a |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 0 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1760 |
Biggest coefficient in the objective function | 469762048 |
Number of bits for the biggest coefficient in the objective function | 29 |
Sum of the numbers in the objective function | 29326573307 |
Number of bits of the sum of numbers in the objective function | 35 |
Biggest number in a constraint | 109773592723456 |
Number of bits of the biggest number in a constraint | 47 |
Biggest sum of numbers in a constraint | 511403730649348 |
Number of bits of the biggest sum of numbers | 49 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1258.38 |
Number of variables | 21824 |
Total number of constraints | 1320 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 1320 |
Minimum length of a constraint | 19 |
Maximum length of a constraint | 416 |
LAUNCH ON wulflinc28 THE 2005-09-20 02:47:45 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3165 boxname=wulflinc28 idbench=821 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: c03619cd7187044150b0404ea204a73a /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-grow22.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-grow22.opb IDLAUNCH: 3165 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 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.077 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: 891104 kB Buffers: 21820 kB Cached: 92440 kB SwapCached: 660 kB Active: 29760 kB Inactive: 87012 kB HighTotal: 131008 kB HighFree: 34972 kB LowTotal: 903652 kB LowFree: 856132 kB SwapTotal: 2097640 kB SwapFree: 2096408 kB Dirty: 40 kB Writeback: 0 kB Mapped: 5816 kB Slab: 21020 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 03:07:55 (client local time) WITH STATUS 0 IN 1209.42 SECONDS stats: 3165 7 1209.42 0
c Parsing PB file... c PARSE ERROR! [line 1831] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 1760 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ######################################################################################################################################################################################################################################################################################################################################################################################################################################################## c -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss c ---[2039]---> BDD-cost: 20 c ---[2038]---> BDD-cost: 24 c ---[2036]---> BDD-cost: 23 c ---[2032]---> BDD-cost: 22 c ---[2030]---> BDD-cost: 24 c ---[2029]---> BDD-cost: 25 c ---[2028]---> BDD-cost: 19 c ---[2027]---> BDD-cost: 21 c ---[2025]---> BDD-cost: 22 c ---[2024]---> BDD-cost: 21 c ---[2023]---> BDD-cost: 27 c ---[2022]---> BDD-cost: 20 c ---[2021]---> BDD-cost: 24 c ---[2019]---> BDD-cost: 23 c ---[2016]---> BDD-cost: 22 c ---[2015]---> BDD-cost: 22 c ---[2013]---> BDD-cost: 24 c ---[2012]---> BDD-cost: 25 c ---[2011]---> BDD-cost: 19 c ---[2010]---> BDD-cost: 21 c ---[2008]---> BDD-cost: 22 c ---[2007]---> BDD-cost: 21 c ---[2006]---> BDD-cost: 27 c ---[2005]---> BDD-cost: 20 c ---[2004]---> BDD-cost: 24 c ---[2002]---> BDD-cost: 23 c ---[1999]---> BDD-cost: 22 c ---[1998]---> BDD-cost: 22 c ---[1996]---> BDD-cost: 24 c ---[1995]---> BDD-cost: 25 c ---[1994]---> BDD-cost: 19 c ---[1993]---> BDD-cost: 21 c ---[1991]---> BDD-cost: 22 c ---[1990]---> BDD-cost: 21 c ---[1989]---> BDD-cost: 27 c ---[1988]---> BDD-cost: 20 c ---[1987]---> BDD-cost: 24 c ---[1985]---> BDD-cost: 23 c ---[1982]---> BDD-cost: 22 c ---[1981]---> BDD-cost: 22 c ---[1979]---> BDD-cost: 24 c ---[1978]---> BDD-cost: 25 c ---[1977]---> BDD-cost: 19 c ---[1976]---> BDD-cost: 21 c ---[1974]---> BDD-cost: 22 c ---[1973]---> BDD-cost: 21 c ---[1972]---> BDD-cost: 27 c ---[1971]---> BDD-cost: 20 c ---[1970]---> BDD-cost: 24 c ---[1968]---> BDD-cost: 23 c ---[1965]---> BDD-cost: 22 c ---[1964]---> BDD-cost: 22 c ---[1962]---> BDD-cost: 24 c ---[1961]---> BDD-cost: 25 c ---[1960]---> BDD-cost: 19 c ---[1959]---> BDD-cost: 21 c ---[1957]---> BDD-cost: 22 c ---[1956]---> BDD-cost: 21 c ---[1955]---> BDD-cost: 27 c ---[1954]---> BDD-cost: 20 c ---[1953]---> BDD-cost: 24 c ---[1951]---> BDD-cost: 23 c ---[1948]---> BDD-cost: 22 c ---[1947]---> BDD-cost: 22 c ---[1945]---> BDD-cost: 24 c ---[1944]---> BDD-cost: 25 c ---[1943]---> BDD-cost: 19 c ---[1942]---> BDD-cost: 21 c ---[1940]---> BDD-cost: 22 c ---[1939]---> BDD-cost: 21 c ---[1938]---> BDD-cost: 27 c ---[1937]---> BDD-cost: 20 c ---[1936]---> BDD-cost: 24 c ---[1934]---> BDD-cost: 23 c ---[1931]---> BDD-cost: 22 c ---[1930]---> BDD-cost: 22 c ---[1928]---> BDD-cost: 24 c ---[1927]---> BDD-cost: 25 c ---[1926]---> BDD-cost: 19 c ---[1925]---> BDD-cost: 21 c ---[1923]---> BDD-cost: 22 c ---[1922]---> BDD-cost: 21 c ---[1921]---> BDD-cost: 27 c ---[1920]---> BDD-cost: 20 c ---[1919]---> BDD-cost: 24 c ---[1917]---> BDD-cost: 23 c ---[1914]---> BDD-cost: 22 c ---[1913]---> BDD-cost: 22 c ---[1911]---> BDD-cost: 24 c ---[1910]---> BDD-cost: 25 c ---[1909]---> BDD-cost: 19 c ---[1908]---> BDD-cost: 21 c ---[1906]---> BDD-cost: 22 c ---[1905]---> BDD-cost: 21 c ---[1904]---> BDD-cost: 27 c ---[1903]---> BDD-cost: 20 c ---[1902]---> BDD-cost: 24 c ---[1900]---> BDD-cost: 23 c ---[1897]---> BDD-cost: 22 c ---[1896]---> BDD-cost: 22 c ---[1894]---> BDD-cost: 24 c ---[1893]---> BDD-cost: 25 c ---[1892]---> BDD-cost: 19 c ---[1891]---> BDD-cost: 21 c ---[1889]---> BDD-cost: 22 c ---[1888]---> BDD-cost: 21 c ---[1887]---> BDD-cost: 27 c ---[1886]---> BDD-cost: 20 c ---[1885]---> BDD-cost: 24 c ---[1883]---> BDD-cost: 23 c ---[1880]---> BDD-cost: 22 c ---[1879]---> BDD-cost: 22 c ---[1877]---> BDD-cost: 24 c ---[1876]---> BDD-cost: 25 c ---[1875]---> BDD-cost: 19 c ---[1874]---> BDD-cost: 21 c ---[1872]---> BDD-cost: 22 c ---[1871]---> BDD-cost: 21 c ---[1870]---> BDD-cost: 27 c ---[1869]---> BDD-cost: 20 c ---[1868]---> BDD-cost: 24 c ---[1866]---> BDD-cost: 23 c ---[1863]---> BDD-cost: 22 c ---[1862]---> BDD-cost: 22 c ---[1860]---> BDD-cost: 24 c ---[1859]---> BDD-cost: 25 c ---[1858]---> BDD-cost: 19 c ---[1857]---> BDD-cost: 21 c ---[1855]---> BDD-cost: 22 c ---[1854]---> BDD-cost: 21 c ---[1853]---> BDD-cost: 27 c ---[1852]---> BDD-cost: 20 c ---[1851]---> BDD-cost: 24 c ---[1849]---> BDD-cost: 23 c ---[1846]---> BDD-cost: 22 c ---[1845]---> BDD-cost: 22 c ---[1843]---> BDD-cost: 24 c ---[1842]---> BDD-cost: 25 c ---[1841]---> BDD-cost: 19 c ---[1840]---> BDD-cost: 21 c ---[1838]---> BDD-cost: 22 c ---[1837]---> BDD-cost: 21 c ---[1836]---> BDD-cost: 27 c ---[1835]---> BDD-cost: 20 c ---[1834]---> BDD-cost: 24 c ---[1832]---> BDD-cost: 23 c ---[1829]---> BDD-cost: 22 c ---[1828]---> BDD-cost: 22 c ---[1826]---> BDD-cost: 24 c ---[1825]---> BDD-cost: 25 c ---[1824]---> BDD-cost: 19 c ---[1823]---> BDD-cost: 21 c ---[1821]---> BDD-cost: 22 c ---[1820]---> BDD-cost: 21 c ---[1819]---> BDD-cost: 27 c ---[1818]---> BDD-cost: 20 c ---[1817]---> BDD-cost: 24 c ---[1815]---> BDD-cost: 23 c ---[1812]---> BDD-cost: 22 c ---[1811]---> BDD-cost: 22 c ---[1809]---> BDD-cost: 24 c ---[1808]---> BDD-cost: 25 c ---[1807]---> BDD-cost: 19 c ---[1806]---> BDD-cost: 21 c ---[1804]---> BDD-cost: 22 c ---[1803]---> BDD-cost: 21 c ---[1802]---> BDD-cost: 27 c ---[1801]---> BDD-cost: 20 c ---[1800]---> BDD-cost: 24 c ---[1798]---> BDD-cost: 23 c ---[1795]---> BDD-cost: 22 c ---[1794]---> BDD-cost: 22 c ---[1792]---> BDD-cost: 24 c ---[1791]---> BDD-cost: 25 c ---[1790]---> BDD-cost: 19 c ---[1789]---> BDD-cost: 21 c ---[1787]---> BDD-cost: 22 c ---[1786]---> BDD-cost: 21 c ---[1785]---> BDD-cost: 27 c ---[1784]---> BDD-cost: 20 c ---[1783]---> BDD-cost: 24 c ---[1781]---> BDD-cost: 23 c ---[1778]---> BDD-cost: 22 c ---[1777]---> BDD-cost: 22 c ---[1775]---> BDD-cost: 24 c ---[1774]---> BDD-cost: 25 c ---[1773]---> BDD-cost: 19 c ---[1772]---> BDD-cost: 21 c ---[1770]---> BDD-cost: 22 c ---[1769]---> BDD-cost: 21 c ---[1768]---> BDD-cost: 27 c ---[1767]---> BDD-cost: 20 c ---[1766]---> BDD-cost: 24 c ---[1764]---> BDD-cost: 23 c ---[1761]---> BDD-cost: 22 c ---[1760]---> BDD-cost: 22 c ---[1758]---> BDD-cost: 24 c ---[1757]---> BDD-cost: 25 c ---[1756]---> BDD-cost: 19 c ---[1755]---> BDD-cost: 21 c ---[1753]---> BDD-cost: 22 c ---[1752]---> BDD-cost: 21 c ---[1751]---> BDD-cost: 27 c ---[1750]---> BDD-cost: 20 c ---[1749]---> BDD-cost: 24 c ---[1747]---> BDD-cost: 23 c ---[1744]---> BDD-cost: 22 c ---[1743]---> BDD-cost: 22 c ---[1741]---> BDD-cost: 24 c ---[1740]---> BDD-cost: 25 c ---[1739]---> BDD-cost: 19 c ---[1738]---> BDD-cost: 21 c ---[1736]---> BDD-cost: 22 c ---[1735]---> BDD-cost: 21 c ---[1734]---> BDD-cost: 27 c ---[1733]---> BDD-cost: 20 c ---[1732]---> BDD-cost: 24 c ---[1730]---> BDD-cost: 23 c ---[1727]---> BDD-cost: 22 c ---[1726]---> BDD-cost: 22 c ---[1724]---> BDD-cost: 24 c ---[1723]---> BDD-cost: 25 c ---[1722]---> BDD-cost: 19 c ---[1721]---> BDD-cost: 21 c ---[1719]---> BDD-cost: 22 c ---[1718]---> BDD-cost: 21 c ---[1717]---> BDD-cost: 27 c ---[1716]---> BDD-cost: 20 c ---[1715]---> BDD-cost: 24 c ---[1713]---> BDD-cost: 23 c ---[1710]---> BDD-cost: 22 c ---[1709]---> BDD-cost: 22 c ---[1707]---> BDD-cost: 24 c ---[1706]---> BDD-cost: 25 c ---[1705]---> BDD-cost: 19 c ---[1704]---> BDD-cost: 21 c ---[1702]---> BDD-cost: 22 c ---[1701]---> BDD-cost: 21 c ---[1700]---> BDD-cost: 27 c ---[1699]---> BDD-cost: 20 c ---[1698]---> BDD-cost: 24 c ---[1696]---> BDD-cost: 23 c ---[1693]---> BDD-cost: 22 c ---[1692]---> BDD-cost: 22 c ---[1690]---> BDD-cost: 24 c ---[1689]---> BDD-cost: 25 c ---[1688]---> BDD-cost: 19 c ---[1687]---> BDD-cost: 21 c ---[1685]---> BDD-cost: 22 c ---[1684]---> BDD-cost: 21 c ---[1683]---> BDD-cost: 27 c ---[1682]---> BDD-cost: 20 c ---[1681]---> BDD-cost: 24 c ---[1679]---> BDD-cost: 23 c ---[1676]---> BDD-cost: 22 c ---[1675]---> BDD-cost: 22 c ---[1673]---> BDD-cost: 24 c ---[1672]---> BDD-cost: 25 c ---[1671]---> BDD-cost: 19 c ---[1670]---> BDD-cost: 21 c ---[1668]---> BDD-cost: 22 c ---[1667]---> BDD-cost: 21 c ---[1666]---> BDD-cost: 27 c ---[1644]---> BDD-cost: 26 c ---[1641]---> BDD-cost: 26 c ---[1638]---> BDD-cost: 26 c ---[1635]---> BDD-cost: 26 c ---[1632]---> BDD-cost: 26 c ---[1629]---> BDD-cost: 26 c ---[1626]---> BDD-cost: 26 c ---[1623]---> BDD-cost: 26 c ---[1620]---> BDD-cost: 26 c ---[1617]---> BDD-cost: 26 c ---[1614]---> BDD-cost: 26 c ---[1611]---> BDD-cost: 26 c ---[1608]---> BDD-cost: 26 c ---[1605]---> BDD-cost: 26 c ---[1602]---> BDD-cost: 26 c ---[1599]---> BDD-cost: 19 c ---[1598]---> BDD-cost: 23 c ---[1596]---> BDD-cost: 22 c ---[1593]---> BDD-cost: 21 c ---[1592]---> BDD-cost: 21 c ---[1590]---> BDD-cost: 23 c ---[1589]---> BDD-cost: 24 c ---[1588]---> BDD-cost: 18 c ---[1587]---> BDD-cost: 20 c ---[1585]---> BDD-cost: 21 c ---[1584]---> BDD-cost: 20 c ---[1583]---> BDD-cost: 26 c ---[1582]---> BDD-cost: 19 c ---[1581]---> BDD-cost: 23 c ---[1579]---> BDD-cost: 22 c ---[1576]---> BDD-cost: 21 c ---[1575]---> BDD-cost: 21 c ---[1573]---> BDD-cost: 23 c ---[1572]---> BDD-cost: 24 c ---[1571]---> BDD-cost: 18 c ---[1570]---> BDD-cost: 20 c ---[1568]---> BDD-cost: 21 c ---[1567]---> BDD-cost: 20 c ---[1566]---> BDD-cost: 26 c ---[1565]---> BDD-cost: 19 c ---[1564]---> BDD-cost: 23 c ---[1562]---> BDD-cost: 22 c ---[1559]---> BDD-cost: 21 c ---[1558]---> BDD-cost: 21 c ---[1556]---> BDD-cost: 23 c ---[1555]---> BDD-cost: 24 c ---[1554]---> BDD-cost: 18 c ---[1553]---> BDD-cost: 20 c ---[1551]---> BDD-cost: 21 c ---[1550]---> BDD-cost: 20 c ---[1549]---> BDD-cost: 26 c ---[1548]---> BDD-cost: 19 c ---[1547]---> BDD-cost: 23 c ---[1545]---> BDD-cost: 22 c ---[1542]---> BDD-cost: 21 c ---[1541]---> BDD-cost: 21 c ---[1539]---> BDD-cost: 23 c ---[1538]---> BDD-cost: 24 c ---[1537]---> BDD-cost: 18 c ---[1536]---> BDD-cost: 20 c ---[1534]---> BDD-cost: 21 c ---[1533]---> BDD-cost: 20 c ---[1532]---> BDD-cost: 26 c ---[1531]---> BDD-cost: 19 c ---[1530]---> BDD-cost: 23 c ---[1528]---> BDD-cost: 22 c ---[1525]---> BDD-cost: 21 c ---[1524]---> BDD-cost: 21 c ---[1522]---> BDD-cost: 23 c ---[1521]---> BDD-cost: 24 c ---[1520]---> BDD-cost: 18 c ---[1519]---> BDD-cost: 20 c ---[1517]---> BDD-cost: 21 c ---[1516]---> BDD-cost: 20 c ---[1515]---> BDD-cost: 26 c ---[1514]---> BDD-cost: 19 c ---[1513]---> BDD-cost: 23 c ---[1511]---> BDD-cost: 22 c ---[1508]---> BDD-cost: 21 c ---[1507]---> BDD-cost: 21 c ---[1505]---> BDD-cost: 23 c ---[1504]---> BDD-cost: 24 c ---[1503]---> BDD-cost: 18 c ---[1502]---> BDD-cost: 20 c ---[1500]---> BDD-cost: 21 c ---[1499]---> BDD-cost: 20 c ---[1498]---> BDD-cost: 26 c ---[1497]---> BDD-cost: 19 c ---[1496]---> BDD-cost: 23 c ---[1494]---> BDD-cost: 22 c ---[1491]---> BDD-cost: 21 c ---[1490]---> BDD-cost: 21 c ---[1488]---> BDD-cost: 23 c ---[1487]---> BDD-cost: 24 c ---[1486]---> BDD-cost: 18 c ---[1485]---> BDD-cost: 20 c ---[1483]---> BDD-cost: 21 c ---[1482]---> BDD-cost: 20 c ---[1481]---> BDD-cost: 26 c ---[1480]---> BDD-cost: 19 c ---[1479]---> BDD-cost: 23 c ---[1477]---> BDD-cost: 22 c ---[1474]---> BDD-cost: 21 c ---[1473]---> BDD-cost: 21 c ---[1471]---> BDD-cost: 23 c ---[1470]---> BDD-cost: 24 c ---[1469]---> BDD-cost: 18 c ---[1468]---> BDD-cost: 20 c ---[1466]---> BDD-cost: 21 c ---[1465]---> BDD-cost: 20 c ---[1464]---> BDD-cost: 26 c ---[1463]---> BDD-cost: 19 c ---[1462]---> BDD-cost: 23 c ---[1460]---> BDD-cost: 22 c ---[1457]---> BDD-cost: 21 c ---[1456]---> BDD-cost: 21 c ---[1454]---> BDD-cost: 23 c ---[1453]---> BDD-cost: 24 c ---[1452]---> BDD-cost: 18 c ---[1451]---> BDD-cost: 20 c ---[1449]---> BDD-cost: 21 c ---[1448]---> BDD-cost: 20 c ---[1447]---> BDD-cost: 26 c ---[1446]---> BDD-cost: 19 c ---[1445]---> BDD-cost: 23 c ---[1443]---> BDD-cost: 22 c ---[1440]---> BDD-cost: 21 c ---[1439]---> BDD-cost: 21 c ---[1437]---> BDD-cost: 23 c ---[1436]---> BDD-cost: 24 c ---[1435]---> BDD-cost: 18 c ---[1434]---> BDD-cost: 20 c ---[1432]---> BDD-cost: 21 c ---[1431]---> BDD-cost: 20 c ---[1430]---> BDD-cost: 26 c ---[1429]---> BDD-cost: 19 c ---[1428]---> BDD-cost: 23 c ---[1426]---> BDD-cost: 22 c ---[1423]---> BDD-cost: 21 c ---[1422]---> BDD-cost: 21 c ---[1420]---> BDD-cost: 23 c ---[1419]---> BDD-cost: 24 c ---[1418]---> BDD-cost: 18 c ---[1417]---> BDD-cost: 20 c ---[1415]---> BDD-cost: 21 c ---[1414]---> BDD-cost: 20 c ---[1413]---> BDD-cost: 26 c ---[1412]---> BDD-cost: 19 c ---[1411]---> BDD-cost: 23 c ---[1409]---> BDD-cost: 22 c ---[1406]---> BDD-cost: 21 c ---[1405]---> BDD-cost: 21 c ---[1403]---> BDD-cost: 23 c ---[1402]---> BDD-cost: 24 c ---[1401]---> BDD-cost: 18 c ---[1400]---> BDD-cost: 20 c ---[1398]---> BDD-cost: 21 c ---[1397]---> BDD-cost: 20 c ---[1396]---> BDD-cost: 26 c ---[1395]---> BDD-cost: 19 c ---[1394]---> BDD-cost: 23 c ---[1392]---> BDD-cost: 22 c ---[1389]---> BDD-cost: 21 c ---[1388]---> BDD-cost: 21 c ---[1386]---> BDD-cost: 23 c ---[1385]---> BDD-cost: 24 c ---[1384]---> BDD-cost: 18 c ---[1383]---> BDD-cost: 20 c ---[1381]---> BDD-cost: 21 c ---[1380]---> BDD-cost: 20 c ---[1379]---> BDD-cost: 26 c ---[1378]---> BDD-cost: 19 c ---[1377]---> BDD-cost: 23 c ---[1375]---> BDD-cost: 22 c ---[1372]---> BDD-cost: 21 c ---[1371]---> BDD-cost: 21 c ---[1369]---> BDD-cost: 23 c ---[1368]---> BDD-cost: 24 c ---[1367]---> BDD-cost: 18 c ---[1366]---> BDD-cost: 20 c ---[1364]---> BDD-cost: 21 c ---[1363]---> BDD-cost: 20 c ---[1362]---> BDD-cost: 26 c ---[1361]---> BDD-cost: 19 c ---[1360]---> BDD-cost: 23 c ---[1358]---> BDD-cost: 22 c ---[1355]---> BDD-cost: 21 c ---[1354]---> BDD-cost: 21 c ---[1352]---> BDD-cost: 23 c ---[1351]---> BDD-cost: 24 c ---[1350]---> BDD-cost: 18 c ---[1349]---> BDD-cost: 20 c ---[1347]---> BDD-cost: 21 c ---[1346]---> BDD-cost: 20 c ---[1345]---> BDD-cost: 26 c ---[1344]---> BDD-cost: 19 c ---[1343]---> BDD-cost: 23 c ---[1341]---> BDD-cost: 22 c ---[1338]---> BDD-cost: 21 c ---[1337]---> BDD-cost: 21 c ---[1335]---> BDD-cost: 23 c ---[1334]---> BDD-cost: 24 c ---[1333]---> BDD-cost: 18 c ---[1332]---> BDD-cost: 20 c ---[1330]---> BDD-cost: 21 c ---[1329]---> BDD-cost: 20 c ---[1328]---> BDD-cost: 26 c ---[1327]---> BDD-cost: 19 c ---[1326]---> BDD-cost: 23 c ---[1324]---> BDD-cost: 22 c ---[1321]---> BDD-cost: 21 c ---[1320]---> BDD-cost: 21 c ---[1318]---> BDD-cost: 23 c ---[1317]---> BDD-cost: 24 c ---[1316]---> BDD-cost: 18 c ---[1315]---> BDD-cost: 20 c ---[1313]---> BDD-cost: 21 c ---[1312]---> BDD-cost: 20 c ---[1311]---> BDD-cost: 26 c ---[1310]---> BDD-cost: 19 c ---[1309]---> BDD-cost: 23 c ---[1307]---> BDD-cost: 22 c ---[1304]---> BDD-cost: 21 c ---[1303]---> BDD-cost: 21 c ---[1301]---> BDD-cost: 23 c ---[1300]---> BDD-cost: 24 c ---[1299]---> BDD-cost: 18 c ---[1298]---> BDD-cost: 20 c ---[1296]---> BDD-cost: 21 c ---[1295]---> BDD-cost: 20 c ---[1294]---> BDD-cost: 26 c ---[1293]---> BDD-cost: 19 c ---[1292]---> BDD-cost: 23 c ---[1290]---> BDD-cost: 22 c ---[1287]---> BDD-cost: 21 c ---[1286]---> BDD-cost: 21 c ---[128
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/20211/stat): 20211 (minisat+_script) R 20210 20211 20115 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855064480 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/20211/statm): 174 3 169 147 0 27 0 [pid=20211] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=20212 New process pid=20213 New process pid=20214 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload One traced child (pid=20213) exited with status: 0 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=20214) exited with status: 0 One traced child (pid=20212) exited with status: 0 New process pid=20215 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-grow22.opb One traced child (pid=20215) exited with status: 5 open syscall for file /oldhome/oroussel/solvers/ New process pid=20216 execve syscall for /oldhome/oroussel/solvers/minisat+_bignum_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-grow22.opb [startup+10.0029 s] Raw data (loadavg): 0.21 0.05 0.01 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 3322 0 3 0 914 18 0 0 25 0 1 0 1855064511 14409728 3259 4294967295 134512640 135167914 3221224448 3221223184 134522751 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20216/statm): 3518 3259 162 162 0 3356 0 [pid=20216] vsize: 14072 Current children cumulated CPU time (s) 9.56 Current children cumulated vsize (Kb) 16200 [startup+20.0045 s] Raw data (loadavg): 0.33 0.08 0.02 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 6465 0 3 0 1880 34 0 0 25 0 1 0 1855064511 26214400 6149 4294967295 134512640 135167914 3221224448 3221183264 134516644 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/20216/statm): 6400 6149 162 162 0 6238 0 [pid=20216] vsize: 25600 Current children cumulated CPU time (s) 19.38 Current children cumulated vsize (Kb) 27728 [startup+30.0052 s] Raw data (loadavg): 0.44 0.11 0.03 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 2874 37 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221218208 134844725 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 29.35 Current children cumulated vsize (Kb) 28036 [startup+40.0058 s] Raw data (loadavg): 0.52 0.14 0.04 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 3874 37 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221218976 134843036 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 39.35 Current children cumulated vsize (Kb) 28036 [startup+50.0065 s] Raw data (loadavg): 0.60 0.16 0.05 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 4874 38 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221218928 134696256 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 49.36 Current children cumulated vsize (Kb) 28036 [startup+60.0062 s] Raw data (loadavg): 0.66 0.19 0.06 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 5874 38 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221218372 134843117 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 59.36 Current children cumulated vsize (Kb) 28036 [startup+70.0068 s] Raw data (loadavg): 0.71 0.22 0.07 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 6874 38 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221218652 134849088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 69.36 Current children cumulated vsize (Kb) 28036 [startup+80.0075 s] Raw data (loadavg): 0.75 0.24 0.08 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 7874 38 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221218652 134849088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 79.36 Current children cumulated vsize (Kb) 28036 [startup+90.0072 s] Raw data (loadavg): 0.79 0.27 0.09 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 8874 39 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221218828 134849056 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 89.37 Current children cumulated vsize (Kb) 28036 [startup+100.008 s] Raw data (loadavg): 0.82 0.29 0.10 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 9874 39 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221218824 134842997 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 99.37 Current children cumulated vsize (Kb) 28036 [startup+110.008 s] Raw data (loadavg): 0.85 0.31 0.11 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 10874 39 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219356 134849056 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 109.37 Current children cumulated vsize (Kb) 28036 [startup+120.009 s] Raw data (loadavg): 0.87 0.34 0.12 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 11875 39 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219152 134849110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 119.38 Current children cumulated vsize (Kb) 28036 [startup+130.01 s] Raw data (loadavg): 0.89 0.36 0.13 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 12875 39 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219012 134630852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 129.38 Current children cumulated vsize (Kb) 28036 [startup+140.01 s] Raw data (loadavg): 0.91 0.38 0.14 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 13875 39 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219440 134696316 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 139.38 Current children cumulated vsize (Kb) 28036 [startup+150.01 s] Raw data (loadavg): 0.92 0.40 0.15 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 14875 39 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221218960 134849153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 149.38 Current children cumulated vsize (Kb) 28036 [startup+160.011 s] Raw data (loadavg): 0.93 0.42 0.15 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 15875 39 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221218476 134694320 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 159.38 Current children cumulated vsize (Kb) 28036 [startup+170.011 s] Raw data (loadavg): 0.94 0.44 0.16 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 16875 39 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219516 134696182 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 169.38 Current children cumulated vsize (Kb) 28036 [startup+180.012 s] Raw data (loadavg): 0.95 0.45 0.17 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 17875 39 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219280 134843030 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 179.38 Current children cumulated vsize (Kb) 28036 [startup+190.013 s] Raw data (loadavg): 0.96 0.47 0.18 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 18876 39 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219136 134522492 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 189.39 Current children cumulated vsize (Kb) 28036 [startup+200.013 s] Raw data (loadavg): 0.96 0.49 0.19 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 19876 39 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221218720 134845901 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 199.39 Current children cumulated vsize (Kb) 28036 [startup+210.013 s] Raw data (loadavg): 0.97 0.51 0.20 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 20876 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219264 134845927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 209.4 Current children cumulated vsize (Kb) 28036 [startup+220.015 s] Raw data (loadavg): 0.98 0.53 0.21 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 21876 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219424 134845913 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 219.4 Current children cumulated vsize (Kb) 28036 [startup+230.015 s] Raw data (loadavg): 0.98 0.54 0.22 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 22876 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219628 134843002 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 229.4 Current children cumulated vsize (Kb) 28036 [startup+240.015 s] Raw data (loadavg): 0.98 0.56 0.22 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 23876 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220060 134694480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 239.4 Current children cumulated vsize (Kb) 28036 [startup+250.016 s] Raw data (loadavg): 0.98 0.57 0.23 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 24877 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221218924 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 249.41 Current children cumulated vsize (Kb) 28036 [startup+260.016 s] Raw data (loadavg): 0.99 0.59 0.24 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 25877 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219440 134696321 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 259.41 Current children cumulated vsize (Kb) 28036 [startup+270.017 s] Raw data (loadavg): 0.99 0.60 0.25 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 26877 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219872 134693570 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 269.41 Current children cumulated vsize (Kb) 28036 [startup+280.018 s] Raw data (loadavg): 0.99 0.61 0.26 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 27877 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219100 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 279.41 Current children cumulated vsize (Kb) 28036 [startup+290.018 s] Raw data (loadavg): 0.99 0.62 0.26 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 28877 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219716 134630852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 289.41 Current children cumulated vsize (Kb) 28036 [startup+300.019 s] Raw data (loadavg): 0.99 0.64 0.27 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 29878 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219104 134843001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 299.42 Current children cumulated vsize (Kb) 28036 [startup+310.02 s] Raw data (loadavg): 0.99 0.65 0.28 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 30878 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219584 134844672 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 309.42 Current children cumulated vsize (Kb) 28036 [startup+320.02 s] Raw data (loadavg): 0.99 0.66 0.29 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 31878 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219820 134844638 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 319.42 Current children cumulated vsize (Kb) 28036 [startup+330.021 s] Raw data (loadavg): 0.99 0.67 0.29 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 32878 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219696 134693570 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 329.42 Current children cumulated vsize (Kb) 28036 [startup+340.021 s] Raw data (loadavg): 0.99 0.68 0.30 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 33878 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219888 134629275 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 339.42 Current children cumulated vsize (Kb) 28036 [startup+350.021 s] Raw data (loadavg): 0.99 0.69 0.31 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 34878 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219968 134696658 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 349.42 Current children cumulated vsize (Kb) 28036 [startup+360.022 s] Raw data (loadavg): 0.99 0.70 0.31 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 35879 40 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220000 134720484 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 359.43 Current children cumulated vsize (Kb) 28036 [startup+370.022 s] Raw data (loadavg): 0.99 0.71 0.32 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 36879 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219652 134845938 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 369.44 Current children cumulated vsize (Kb) 28036 [startup+380.023 s] Raw data (loadavg): 0.99 0.72 0.33 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 37879 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219680 134843010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 379.44 Current children cumulated vsize (Kb) 28036 [startup+390.023 s] Raw data (loadavg): 0.99 0.73 0.33 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 38879 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220188 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 389.44 Current children cumulated vsize (Kb) 28036 [startup+400.023 s] Raw data (loadavg): 0.99 0.74 0.34 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 39879 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220080 134629448 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 399.44 Current children cumulated vsize (Kb) 28036 [startup+410.024 s] Raw data (loadavg): 0.99 0.74 0.35 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 40879 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219604 134843117 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 409.44 Current children cumulated vsize (Kb) 28036 [startup+420.025 s] Raw data (loadavg): 0.99 0.75 0.35 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 41880 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219792 134844691 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 419.45 Current children cumulated vsize (Kb) 28036 [startup+430.025 s] Raw data (loadavg): 0.99 0.76 0.36 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 42880 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219980 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 429.45 Current children cumulated vsize (Kb) 28036 [startup+440.025 s] Raw data (loadavg): 0.99 0.77 0.37 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 43880 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220144 134844703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 439.45 Current children cumulated vsize (Kb) 28036 [startup+450.026 s] Raw data (loadavg): 0.99 0.77 0.37 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 44880 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220208 134843139 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 449.45 Current children cumulated vsize (Kb) 28036 [startup+460.026 s] Raw data (loadavg): 0.99 0.78 0.38 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 45880 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219856 134843406 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 459.45 Current children cumulated vsize (Kb) 28036 [startup+470.028 s] Raw data (loadavg): 0.99 0.79 0.38 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 46881 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220384 134694539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 469.46 Current children cumulated vsize (Kb) 28036 [startup+480.029 s] Raw data (loadavg): 0.99 0.79 0.39 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 47881 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220688 134696613 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 479.46 Current children cumulated vsize (Kb) 28036 [startup+490.028 s] Raw data (loadavg): 0.99 0.80 0.40 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 48881 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219792 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 489.46 Current children cumulated vsize (Kb) 28036 [startup+500.029 s] Raw data (loadavg): 0.99 0.81 0.40 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 49881 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220012 134845940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 499.46 Current children cumulated vsize (Kb) 28036 [startup+510.029 s] Raw data (loadavg): 0.99 0.81 0.41 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 50881 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220172 134722225 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 509.46 Current children cumulated vsize (Kb) 28036 [startup+520.029 s] Raw data (loadavg): 0.99 0.82 0.41 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 51882 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220128 134845930 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 519.47 Current children cumulated vsize (Kb) 28036 [startup+530.03 s] Raw data (loadavg): 0.99 0.82 0.42 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 52882 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219264 134696328 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 529.47 Current children cumulated vsize (Kb) 28036 [startup+540.031 s] Raw data (loadavg): 0.99 0.83 0.43 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 53882 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220056 134693740 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 539.47 Current children cumulated vsize (Kb) 28036 [startup+550.031 s] Raw data (loadavg): 0.99 0.83 0.43 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 54882 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220048 134849108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 549.47 Current children cumulated vsize (Kb) 28036 [startup+560.031 s] Raw data (loadavg): 0.99 0.84 0.44 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 55882 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219792 134844725 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 559.47 Current children cumulated vsize (Kb) 28036 [startup+570.032 s] Raw data (loadavg): 0.99 0.84 0.44 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 56883 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220320 134696759 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 569.48 Current children cumulated vsize (Kb) 28036 [startup+580.032 s] Raw data (loadavg): 0.99 0.85 0.45 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 57883 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220400 134849110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 579.48 Current children cumulated vsize (Kb) 28036 [startup+590.033 s] Raw data (loadavg): 0.99 0.85 0.45 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 58883 41 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219968 134844644 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 589.48 Current children cumulated vsize (Kb) 28036 [startup+600.034 s] Raw data (loadavg): 0.99 0.86 0.46 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 59883 42 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220592 134629236 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 599.49 Current children cumulated vsize (Kb) 28036 [startup+610.034 s] Raw data (loadavg): 0.99 0.86 0.46 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 60883 42 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220336 134849187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 609.49 Current children cumulated vsize (Kb) 28036 [startup+620.035 s] Raw data (loadavg): 0.99 0.86 0.47 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 61883 42 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220848 134843036 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 619.49 Current children cumulated vsize (Kb) 28036 [startup+630.036 s] Raw data (loadavg): 0.99 0.87 0.47 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 62883 43 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219648 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 629.5 Current children cumulated vsize (Kb) 28036 [startup+640.036 s] Raw data (loadavg): 0.99 0.87 0.48 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 63882 43 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220000 134849187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 639.49 Current children cumulated vsize (Kb) 28036 [startup+650.037 s] Raw data (loadavg): 0.99 0.88 0.48 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 64882 44 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219820 134842996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 649.5 Current children cumulated vsize (Kb) 28036 [startup+660.037 s] Raw data (loadavg): 0.99 0.88 0.49 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 65882 44 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220208 134843404 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 659.5 Current children cumulated vsize (Kb) 28036 [startup+670.037 s] Raw data (loadavg): 0.99 0.88 0.49 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 66882 44 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220544 134722527 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 669.5 Current children cumulated vsize (Kb) 28036 [startup+680.038 s] Raw data (loadavg): 0.99 0.89 0.50 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 67882 44 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220432 134629445 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 679.5 Current children cumulated vsize (Kb) 28036 [startup+690.038 s] Raw data (loadavg): 0.99 0.89 0.50 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 68882 44 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220172 134693600 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 689.5 Current children cumulated vsize (Kb) 28036 [startup+700.038 s] Raw data (loadavg): 0.99 0.89 0.51 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 69883 44 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220672 134843010 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 699.51 Current children cumulated vsize (Kb) 28036 [startup+710.039 s] Raw data (loadavg): 0.99 0.90 0.51 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 70882 45 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220416 134629091 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 709.51 Current children cumulated vsize (Kb) 28036 [startup+720.04 s] Raw data (loadavg): 0.99 0.90 0.52 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 71883 45 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220672 134844725 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 719.52 Current children cumulated vsize (Kb) 28036 [startup+730.04 s] Raw data (loadavg): 0.99 0.90 0.52 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 72883 45 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220304 134845888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 729.52 Current children cumulated vsize (Kb) 28036 [startup+740.041 s] Raw data (loadavg): 0.99 0.90 0.53 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 73883 45 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220168 134842997 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 739.52 Current children cumulated vsize (Kb) 28036 [startup+750.042 s] Raw data (loadavg): 0.99 0.91 0.53 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 74883 45 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220220 134722656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 749.52 Current children cumulated vsize (Kb) 28036 [startup+760.042 s] Raw data (loadavg): 0.99 0.91 0.54 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 75883 45 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219840 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 759.52 Current children cumulated vsize (Kb) 28036 [startup+770.044 s] Raw data (loadavg): 0.99 0.91 0.54 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 76884 45 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220524 134722227 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 769.53 Current children cumulated vsize (Kb) 28036 [startup+780.045 s] Raw data (loadavg): 0.99 0.91 0.55 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 77884 45 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220536 134844674 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 779.53 Current children cumulated vsize (Kb) 28036 [startup+790.044 s] Raw data (loadavg): 0.99 0.92 0.55 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 78884 45 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220704 134695298 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 789.53 Current children cumulated vsize (Kb) 28036 [startup+800.045 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 79884 45 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220752 134522201 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 799.53 Current children cumulated vsize (Kb) 28036 [startup+810.045 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 80884 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220576 134694338 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 809.54 Current children cumulated vsize (Kb) 28036 [startup+820.046 s] Raw data (loadavg): 0.99 0.92 0.56 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 81884 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220924 134696566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 819.54 Current children cumulated vsize (Kb) 28036 [startup+830.047 s] Raw data (loadavg): 0.99 0.92 0.57 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 82884 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220320 134843118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 829.54 Current children cumulated vsize (Kb) 28036 [startup+840.047 s] Raw data (loadavg): 0.99 0.93 0.57 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 83885 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220928 134693561 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 839.55 Current children cumulated vsize (Kb) 28036 [startup+850.047 s] Raw data (loadavg): 0.99 0.93 0.57 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 84885 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220912 134694545 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 849.55 Current children cumulated vsize (Kb) 28036 [startup+860.048 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 85885 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221219792 134844706 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 859.55 Current children cumulated vsize (Kb) 28036 [startup+870.049 s] Raw data (loadavg): 0.99 0.93 0.58 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 86885 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220588 134842996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 869.55 Current children cumulated vsize (Kb) 28036 [startup+880.049 s] Raw data (loadavg): 0.99 0.93 0.59 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 87885 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220924 134849088 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 879.55 Current children cumulated vsize (Kb) 28036 [startup+890.05 s] Raw data (loadavg): 0.99 0.94 0.59 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 88886 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220672 134844694 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 889.56 Current children cumulated vsize (Kb) 28036 [startup+900.051 s] Raw data (loadavg): 0.99 0.94 0.59 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 89886 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220844 134844632 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 899.56 Current children cumulated vsize (Kb) 28036 [startup+910.05 s] Raw data (loadavg): 0.99 0.94 0.60 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 90886 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220752 134849068 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 909.56 Current children cumulated vsize (Kb) 28036 [startup+920.052 s] Raw data (loadavg): 0.99 0.94 0.60 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 91886 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220896 134722532 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 919.56 Current children cumulated vsize (Kb) 28036 [startup+930.053 s] Raw data (loadavg): 0.99 0.94 0.61 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 92886 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220524 134843033 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 929.56 Current children cumulated vsize (Kb) 28036 [startup+940.052 s] Raw data (loadavg): 0.99 0.94 0.61 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 93887 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220720 134522338 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 939.57 Current children cumulated vsize (Kb) 28036 [startup+950.054 s] Raw data (loadavg): 0.99 0.94 0.61 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 94887 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220848 134844725 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 949.57 Current children cumulated vsize (Kb) 28036 [startup+960.054 s] Raw data (loadavg): 0.99 0.95 0.62 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 95887 46 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220848 134844700 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 959.57 Current children cumulated vsize (Kb) 28036 [startup+970.054 s] Raw data (loadavg): 0.99 0.95 0.62 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 96887 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220508 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 969.58 Current children cumulated vsize (Kb) 28036 [startup+980.055 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 97887 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221200 134844641 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 979.58 Current children cumulated vsize (Kb) 28036 [startup+990.055 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 98887 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220320 134843153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 989.58 Current children cumulated vsize (Kb) 28036 [startup+1000.06 s] Raw data (loadavg): 0.99 0.95 0.63 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 99888 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220800 134844689 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 999.59 Current children cumulated vsize (Kb) 28036 [startup+1010.06 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 100888 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220052 134696408 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1009.59 Current children cumulated vsize (Kb) 28036 [startup+1020.06 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 101888 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221536 134844637 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1019.59 Current children cumulated vsize (Kb) 28036 [startup+1030.06 s] Raw data (loadavg): 0.99 0.95 0.64 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 102888 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220848 134844718 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1029.59 Current children cumulated vsize (Kb) 28036 [startup+1040.06 s] Raw data (loadavg): 0.99 0.95 0.65 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 103888 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220912 134694403 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1039.59 Current children cumulated vsize (Kb) 28036 [startup+1050.06 s] Raw data (loadavg): 0.99 0.95 0.65 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 104888 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221040 134843400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1049.59 Current children cumulated vsize (Kb) 28036 [startup+1060.06 s] Raw data (loadavg): 0.99 0.96 0.65 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 105889 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220752 134849092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1059.6 Current children cumulated vsize (Kb) 28036 [startup+1070.06 s] Raw data (loadavg): 0.99 0.96 0.65 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 106889 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221312 134629126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1069.6 Current children cumulated vsize (Kb) 28036 [startup+1080.06 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 107889 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220900 134843117 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1079.6 Current children cumulated vsize (Kb) 28036 [startup+1090.06 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 108889 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221284 134522188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1089.6 Current children cumulated vsize (Kb) 28036 [startup+1100.06 s] Raw data (loadavg): 0.99 0.96 0.66 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 109889 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221084 134845876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1099.6 Current children cumulated vsize (Kb) 28036 [startup+1110.06 s] Raw data (loadavg): 0.99 0.96 0.67 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 110889 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221568 134849187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1109.6 Current children cumulated vsize (Kb) 28036 [startup+1120.06 s] Raw data (loadavg): 0.99 0.96 0.67 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 111890 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220624 134844689 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1119.61 Current children cumulated vsize (Kb) 28036 [startup+1130.06 s] Raw data (loadavg): 0.99 0.96 0.67 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 112890 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220320 134844728 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1129.61 Current children cumulated vsize (Kb) 28036 [startup+1140.06 s] Raw data (loadavg): 0.99 0.96 0.68 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 113890 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220860 134723262 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1139.61 Current children cumulated vsize (Kb) 28036 [startup+1150.06 s] Raw data (loadavg): 0.99 0.96 0.68 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 114890 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221060 134844636 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1149.61 Current children cumulated vsize (Kb) 28036 [startup+1160.06 s] Raw data (loadavg): 0.99 0.97 0.68 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 115890 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220672 134844691 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1159.61 Current children cumulated vsize (Kb) 28036 [startup+1170.06 s] Raw data (loadavg): 0.99 0.97 0.68 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 116891 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221112 134842997 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1169.62 Current children cumulated vsize (Kb) 28036 [startup+1180.06 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 117891 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221448 134849057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1179.62 Current children cumulated vsize (Kb) 28036 [startup+1190.06 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 118891 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221904 134844713 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1189.62 Current children cumulated vsize (Kb) 28036 [startup+1200.06 s] Raw data (loadavg): 0.99 0.97 0.69 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 119891 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221220320 134844694 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1199.62 Current children cumulated vsize (Kb) 28036 [startup+1210.06 s] Raw data (loadavg): 0.99 0.97 0.70 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 120891 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221392 134843107 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1209.62 Current children cumulated vsize (Kb) 28036 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.07 s] Raw data (loadavg): 0.99 0.97 0.70 2/57 20216 Raw data (/proc/20211/stat): 20211 (minisat+_script) S 20210 20211 20115 0 -1 0 314 1227 0 0 0 0 18 6 17 0 1 0 1855064480 2179072 234 4294967295 134512640 135087896 3221224496 3221223384 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/20211/statm): 532 234 485 147 0 385 0 [pid=20211] vsize: 2128 Raw data (/proc/20216/stat): 20216 (minisat+_bignum) R 20211 20211 20115 0 -1 0 7038 0 3 0 120892 47 0 0 25 0 1 0 1855064511 26529792 6227 4294967295 134512640 135167914 3221224448 3221221200 134843123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/20216/statm): 6477 6227 162 162 0 6315 0 [pid=20216] vsize: 25908 Current children cumulated CPU time (s) 1209.63 Current children cumulated vsize (Kb) 28036 Sending SIGTERM to -20211 Sleeping 2 seconds One traced child (pid=20211) ended because it received signal 15 (SIGTERM) One traced child (pid=20216) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.08 CPU time (s): 1209.42 CPU user time (s): 1208.92 CPU system time (s): 0.494924 CPU usage (%): 99.9449 Max. virtual memory (cumulated for all children) (Kb): 28036
ERROR: no interpretation found !