Name | mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-UMTS.opb |
MD5SUM | ea791006d6c51b520e558c3246209299 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 34345742 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 4170 |
Biggest coefficient in the objective function | 23582998528 |
Number of bits for the biggest coefficient in the objective function | 35 |
Sum of the numbers in the objective function | 2904924551250 |
Number of bits of the sum of numbers in the objective function | 42 |
Biggest number in a constraint | 1024000000000 |
Number of bits of the biggest number in a constraint | 40 |
Biggest sum of numbers in a constraint | 2904924551250 |
Number of bits of the biggest sum of numbers | 42 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1267.05 |
Number of variables | 6402 |
Total number of constraints | 7267 |
Number of constraints which are clauses | 2785 |
Number of constraints which are cardinality constraints (but not clauses) | 4230 |
Number of constraints which are nor clauses,nor cardinality constraints | 252 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 511 |
LAUNCH ON wulflinc20 THE 2005-09-20 02:16:54 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3120 boxname=wulflinc20 idbench=776 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: ea791006d6c51b520e558c3246209299 /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-UMTS.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-UMTS.opb IDLAUNCH: 3120 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 927212 kB Buffers: 140 kB Cached: 77852 kB SwapCached: 820 kB Active: 19640 kB Inactive: 60912 kB HighTotal: 131008 kB HighFree: 49084 kB LowTotal: 903652 kB LowFree: 878128 kB SwapTotal: 2097892 kB SwapFree: 2096508 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5640 kB Slab: 21096 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 02:37:05 (client local time) WITH STATUS 0 IN 1206.2 SECONDS stats: 3120 7 1206.2 0
c Parsing PB file... c Converting 2057 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ############################################################################################################################################################################# c -- Clauses(.)/Splits(s): ssssssssssss..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ssssssssssss. c ---[2079]---> BDD-cost: 21 c ---[2077]---> BDD-cost: 21 c ---[2075]---> BDD-cost: 21 c ---[2073]---> BDD-cost: 21 c ---[2071]---> BDD-cost: 21 c ---[2069]---> BDD-cost: 21 c ---[2067]---> BDD-cost: 21 c ---[2065]---> BDD-cost: 21 c ---[2063]---> BDD-cost: 21 c ---[2061]---> BDD-cost: 21 c ---[2059]---> BDD-cost: 21 c ---[2057]---> BDD-cost: 21 c ---[2055]---> BDD-cost: 21 c ---[2053]---> BDD-cost: 21 c ---[2051]---> BDD-cost: 21 c ---[2049]---> BDD-cost: 21 c ---[2047]---> BDD-cost: 21 c ---[2045]---> BDD-cost: 21 c ---[2043]---> BDD-cost: 21 c ---[2041]---> BDD-cost: 19 c ---[2039]---> BDD-cost: 21 c ---[2037]---> BDD-cost: 21 c ---[2035]---> BDD-cost: 21 c ---[2033]---> BDD-cost: 21 c ---[2031]---> BDD-cost: 21 c ---[2029]---> BDD-cost: 21 c ---[2027]---> BDD-cost: 21 c ---[2025]---> BDD-cost: 21 c ---[2023]---> BDD-cost: 21 c ---[2021]---> BDD-cost: 21 c ---[2019]---> BDD-cost: 19 c ---[2017]---> BDD-cost: 19 c ---[2015]---> BDD-cost: 21 c ---[2013]---> BDD-cost: 21 c ---[2011]---> BDD-cost: 21 c ---[2009]---> BDD-cost: 21 c ---[2007]---> BDD-cost: 21 c ---[2005]---> BDD-cost: 21 c ---[2003]---> BDD-cost: 21 c ---[2001]---> BDD-cost: 21 c ---[1999]---> BDD-cost: 21 c ---[1997]---> BDD-cost: 21 c ---[1995]---> BDD-cost: 21 c ---[1993]---> BDD-cost: 21 c ---[1991]---> BDD-cost: 21 c ---[1989]---> BDD-cost: 21 c ---[1987]---> BDD-cost: 21 c ---[1985]---> BDD-cost: 21 c ---[1983]---> BDD-cost: 21 c ---[1981]---> BDD-cost: 19 c ---[1979]---> BDD-cost: 21 c ---[1977]---> BDD-cost: 21 c ---[1975]---> BDD-cost: 21 c ---[1973]---> BDD-cost: 19 c ---[1971]---> BDD-cost: 21 c ---[1969]---> BDD-cost: 19 c ---[1967]---> BDD-cost: 21 c ---[1965]---> BDD-cost: 21 c ---[1963]---> BDD-cost: 21 c ---[1961]---> BDD-cost: 21 c ---[1959]---> BDD-cost: 19 c ---[1957]---> BDD-cost: 15 c ---[1955]---> BDD-cost: 21 c ---[1953]---> BDD-cost: 15 c ---[1951]---> BDD-cost: 19 c ---[1949]---> BDD-cost: 17 c ---[1947]---> BDD-cost: 17 c ---[1945]---> BDD-cost: 15 c ---[1943]---> BDD-cost: 19 c ---[1941]---> BDD-cost: 15 c ---[1939]---> BDD-cost: 17 c ---[1937]---> BDD-cost: 17 c ---[1935]---> BDD-cost: 15 c ---[1933]---> BDD-cost: 21 c ---[1931]---> BDD-cost: 15 c ---[1929]---> BDD-cost: 17 c ---[1927]---> BDD-cost: 15 c ---[1925]---> BDD-cost: 21 c ---[1923]---> BDD-cost: 19 c ---[1921]---> BDD-cost: 21 c ---[1919]---> BDD-cost: 15 c ---[1917]---> BDD-cost: 19 c ---[1915]---> BDD-cost: 19 c ---[1913]---> BDD-cost: 19 c ---[1911]---> BDD-cost: 15 c ---[1909]---> BDD-cost: 13 c ---[1907]---> BDD-cost: 17 c ---[1905]---> BDD-cost: 15 c ---[1903]---> BDD-cost: 17 c ---[1901]---> BDD-cost: 17 c ---[1899]---> BDD-cost: 19 c ---[1897]---> BDD-cost: 19 c ---[1895]---> BDD-cost: 15 c ---[1893]---> BDD-cost: 19 c ---[1891]---> BDD-cost: 15 c ---[1889]---> BDD-cost: 19 c ---[1887]---> BDD-cost: 19 c ---[1885]---> BDD-cost: 17 c ---[1883]---> BDD-cost: 21 c ---[1881]---> BDD-cost: 15 c ---[1879]---> BDD-cost: 13 c ---[1877]---> BDD-cost: 19 c ---[1875]---> BDD-cost: 17 c ---[1873]---> BDD-cost: 19 c ---[1871]---> BDD-cost: 19 c ---[1869]---> BDD-cost: 11 c ---[1867]---> BDD-cost: 15 c ---[1865]---> BDD-cost: 15 c ---[1863]---> BDD-cost: 17 c ---[1861]---> BDD-cost: 11 c ---[1859]---> BDD-cost: 5 c ---[1857]---> BDD-cost: 13 c ---[1855]---> BDD-cost: 13 c ---[1853]---> BDD-cost: 11 c ---[1851]---> BDD-cost: 7 c ---[1849]---> BDD-cost: 1 c ---[1847]---> BDD-cost: 1 c ---[1845]---> BDD-cost: 11 c ---[1843]---> BDD-cost: 9 c ---[1841]---> BDD-cost: 1 c ---[1839]---> BDD-cost: 15 c ---[1837]---> BDD-cost: 3 c ---[1835]---> BDD-cost: 15 c ---[1833]---> BDD-cost: 9 c ---[1831]---> BDD-cost: 9 c ---[1829]---> BDD-cost: 7 c ---[1827]---> BDD-cost: 5 c ---[1825]---> BDD-cost: 11 c ---[1823]---> BDD-cost: 3 c ---[1821]---> BDD-cost: 5 c ---[1819]---> BDD-cost: 9 c ---[1817]---> BDD-cost: 11 c ---[1815]---> BDD-cost: 7 c ---[1813]---> BDD-cost: 7 c ---[1811]---> BDD-cost: 7 c ---[1809]---> BDD-cost: 3 c ---[1807]---> BDD-cost: 1 c ---[1805]---> BDD-cost: 9 c ---[1803]---> BDD-cost: 13 c ---[1801]---> BDD-cost: 7 c ---[1799]---> BDD-cost: 1 c ---[1797]---> BDD-cost: 15 c ---[1795]---> BDD-cost: 9 c ---[1793]---> BDD-cost: 13 c ---[1791]---> BDD-cost: 5 c ---[1789]---> BDD-cost: 9 c ---[1787]---> BDD-cost: 13 c ---[1785]---> BDD-cost: 1 c ---[1783]---> BDD-cost: 15 c ---[1782]---> Adder-cost: 704 maxlim: 3660 bits: 13/12 c ---[1781]---> Adder-cost: 704 maxlim: 3632 bits: 13/12 c ---[1780]---> Adder-cost: 596 maxlim: 2992 bits: 12/12 c ---[1779]---> Adder-cost: 726 maxlim: 3659 bits: 13/12 c ---[1778]---> Adder-cost: 704 maxlim: 3660 bits: 13/12 c ---[1777]---> Adder-cost: 596 maxlim: 2992 bits: 12/12 c ---[1776]---> Adder-cost: 640 maxlim: 3233 bits: 13/12 c ---[1775]---> Adder-cost: 586 maxlim: 2867 bits: 12/12 c ---[1774]---> Adder-cost: 532 maxlim: 2604 bits: 12/12 c ---[1773]---> Adder-cost: 640 maxlim: 3236 bits: 13/12 c ---[1772]---> Adder-cost: 662 maxlim: 3208 bits: 13/12 c ---[1771]---> Adder-cost: 610 maxlim: 2927 bits: 12/12 c ---[1770]---> Adder-cost: 266 maxlim: 132 bits: 8/8 c ---[1769]---> Adder-cost: 266 maxlim: 131 bits: 8/8 c ---[1768]---> Adder-cost: 228 maxlim: 110 bits: 8/7 c ---[1767]---> Adder-cost: 266 maxlim: 132 bits: 8/8 c ---[1766]---> Adder-cost: 266 maxlim: 132 bits: 8/8 c ---[1765]---> Adder-cost: 228 maxlim: 110 bits: 8/7 c ---[1764]---> Adder-cost: 244 maxlim: 120 bits: 8/7 c ---[1763]---> Adder-cost: 228 maxlim: 110 bits: 8/7 c ---[1762]---> Adder-cost: 204 maxlim: 99 bits: 8/7 c ---[1761]---> Adder-cost: 242 maxlim: 117 bits: 8/7 c ---[1760]---> Adder-cost: 234 maxlim: 115 bits: 8/7 c ---[1759]---> Adder-cost: 218 maxlim: 108 bits: 8/7 c ---[1758]---> Adder-cost: 136 maxlim: 132 bits: 8/8 c ---[1757]---> Adder-cost: 136 maxlim: 131 bits: 8/8 c ---[1756]---> Adder-cost: 114 maxlim: 110 bits: 8/7 c ---[1755]---> Adder-cost: 136 maxlim: 132 bits: 8/8 c ---[1754]---> Adder-cost: 136 maxlim: 132 bits: 8/8 c ---[1753]---> Adder-cost: 114 maxlim: 110 bits: 8/7 c ---[1752]---> Adder-cost: 122 maxlim: 120 bits: 8/7 c ---[1751]---> Adder-cost: 114 maxlim: 110 bits: 8/7 c ---[1750]---> Adder-cost: 106 maxlim: 99 bits: 8/7 c ---[1749]---> Adder-cost: 120 maxlim: 117 bits: 8/7 c ---[1748]---> Adder-cost: 116 maxlim: 115 bits: 8/7 c ---[1747]---> Adder-cost: 114 maxlim: 108 bits: 8/7 c ---[1734]---> BDD-cost: 9 c ---[1733]---> BDD-cost: 9 c ---[1732]---> BDD-cost: 9 c ---[1731]---> BDD-cost: 9 c ---[1730]---> BDD-cost: 9 c ---[1729]---> BDD-cost: 9 c ---[1728]---> BDD-cost: 9 c ---[1727]---> BDD-cost: 9 c ---[1726]---> BDD-cost: 9 c ---[1725]---> BDD-cost: 9 c ---[1724]---> BDD-cost: 9 c ---[1723]---> BDD-cost: 9 c ---[1722]---> BDD-cost: 9 c ---[1721]---> BDD-cost: 9 c ---[1720]---> BDD-cost: 9 c ---[1719]---> BDD-cost: 9 c ---[1718]---> BDD-cost: 9 c ---[1717]---> BDD-cost: 9 c ---[1716]---> BDD-cost: 9 c ---[1715]---> BDD-cost: 9 c ---[1714]---> BDD-cost: 9 c ---[1713]---> BDD-cost: 9 c ---[1712]---> BDD-cost: 9 c ---[1711]---> BDD-cost: 9 c ---[1710]---> BDD-cost: 9 c ---[1709]---> BDD-cost: 9 c ---[1708]---> BDD-cost: 9 c ---[1707]---> BDD-cost: 9 c ---[1706]---> BDD-cost: 9 c ---[1705]---> BDD-cost: 9 c ---[1704]---> BDD-cost: 9 c ---[1703]---> BDD-cost: 9 c ---[1702]---> BDD-cost: 9 c ---[1701]---> BDD-cost: 9 c ---[1700]---> BDD-cost: 9 c ---[1699]---> BDD-cost: 9 c ---[1698]---> BDD-cost: 9 c ---[1697]---> BDD-cost: 9 c ---[1696]---> BDD-cost: 9 c ---[1695]---> BDD-cost: 9 c ---[1694]---> BDD-cost: 9 c ---[1693]---> BDD-cost: 9 c ---[1692]---> BDD-cost: 9 c ---[1691]---> BDD-cost: 9 c ---[1690]---> BDD-cost: 9 c ---[1689]---> BDD-cost: 9 c ---[1688]---> BDD-cost: 9 c ---[1687]---> BDD-cost: 9 c ---[1686]---> BDD-cost: 9 c ---[1685]---> BDD-cost: 9 c ---[1684]---> BDD-cost: 9 c ---[1683]---> BDD-cost: 9 c ---[1682]---> BDD-cost: 9 c ---[1681]---> BDD-cost: 9 c ---[1680]---> BDD-cost: 9 c ---[1679]---> BDD-cost: 9 c ---[1678]---> BDD-cost: 9 c ---[1677]---> BDD-cost: 9 c ---[1676]---> BDD-cost: 9 c ---[1675]---> BDD-cost: 9 c ---[1674]---> BDD-cost: 9 c ---[1673]---> BDD-cost: 9 c ---[1672]---> BDD-cost: 9 c ---[1671]---> BDD-cost: 9 c ---[1670]---> BDD-cost: 9 c ---[1669]---> BDD-cost: 9 c ---[1668]---> Adder-cost: 506 maxlim: 50331635 bits: 26/26 c ---[1667]---> Adder-cost: 416 maxlim: 41943029 bits: 26/26 c ---[1666]---> Adder-cost: 458 maxlim: 46137332 bits: 26/26 c ---[1665]---> Adder-cost: 506 maxlim: 50331635 bits: 26/26 c ---[1664]---> Adder-cost: 506 maxlim: 50331635 bits: 26/26 c ---[1663]---> Sorter-cost: 3998 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1661]---> Adder-cost: 679 maxlim: 3748864 bits: 23/22 c ---[1659]---> Adder-cost: 687 maxlim: 3720192 bits: 23/22 c ---[1657]---> Adder-cost: 613 maxlim: 3064832 bits: 23/22 c ---[1655]---> Adder-cost: 677 maxlim: 3747840 bits: 23/22 c ---[1653]---> Adder-cost: 679 maxlim: 3748864 bits: 23/22 c ---[1651]---> Adder-cost: 613 maxlim: 3064832 bits: 23/22 c ---[1649]---> Adder-cost: 637 maxlim: 3311616 bits: 23/22 c ---[1647]---> Adder-cost: 603 maxlim: 2936832 bits: 23/22 c ---[1645]---> Adder-cost: 617 maxlim: 2667520 bits: 23/22 c ---[1643]---> Adder-cost: 748 maxlim: 3314688 bits: 23/22 c ---[1641]---> Adder-cost: 704 maxlim: 3286016 bits: 23/22 c ---[1639]---> Adder-cost: 627 maxlim: 2998272 bits: 23/22 c ---[1638]---> BDD-cost: 22 c ---[1637]---> BDD-cost: 22 c ---[1636]---> BDD-cost: 22 c ---[1635]---> BDD-cost: 22 c ---[1634]---> BDD-cost: 22 c ---[1633]---> BDD-cost: 22 c ---[1632]---> BDD-cost: 22 c ---[1631]---> BDD-cost: 22 c ---[1630]---> BDD-cost: 22 c ---[1629]---> BDD-cost: 22 c ---[1628]---> BDD-cost: 22 c ---[1627]---> BDD-cost: 22 c ---[1626]---> BDD-cost: 22 c ---[1625]---> BDD-cost: 22 c ---[1624]---> BDD-cost: 22 c ---[1623]---> BDD-cost: 22 c ---[1622]---> BDD-cost: 22 c ---[1621]---> BDD-cost: 22 c ---[1620]---> BDD-cost: 22 c ---[1619]---> BDD-cost: 22 c ---[1618]---> BDD-cost: 22 c ---[1617]---> BDD-cost: 22 c ---[1616]---> BDD-cost: 22 c ---[1615]---> BDD-cost: 22 c ---[1614]---> BDD-cost: 22 c ---[1613]---> BDD-cost: 22 c ---[1612]---> BDD-cost: 22 c ---[1611]---> BDD-cost: 22 c ---[1610]---> BDD-cost: 22 c ---[1609]---> BDD-cost: 22 c ---[1608]---> BDD-cost: 22 c ---[1607]---> BDD-cost: 22 c ---[1606]---> BDD-cost: 22 c ---[1605]---> BDD-cost: 22 c ---[1604]---> BDD-cost: 22 c ---[1603]---> BDD-cost: 22 c ---[1602]---> BDD-cost: 22 c ---[1601]---> BDD-cost: 22 c ---[1600]---> BDD-cost: 22 c ---[1599]---> BDD-cost: 22 c ---[1598]---> BDD-cost: 22 c ---[1597]---> BDD-cost: 22 c ---[1596]---> BDD-cost: 22 c ---[1595]---> BDD-cost: 22 c ---[1594]---> BDD-cost: 22 c ---[1593]---> BDD-cost: 22 c ---[1592]---> BDD-cost: 22 c ---[1591]---> BDD-cost: 22 c ---[1590]---> BDD-cost: 22 c ---[1589]---> BDD-cost: 22 c ---[1588]---> BDD-cost: 22 c ---[1587]---> BDD-cost: 22 c ---[1586]---> BDD-cost: 22 c ---[1585]---> BDD-cost: 22 c ---[1584]---> BDD-cost: 22 c ---[1583]---> BDD-cost: 22 c ---[1582]---> BDD-cost: 22 c ---[1581]---> BDD-cost: 22 c ---[1580]---> BDD-cost: 22 c ---[1579]---> BDD-cost: 22 c ---[1578]---> BDD-cost: 22 c ---[1577]---> BDD-cost: 22 c ---[1576]---> BDD-cost: 22 c ---[1575]---> BDD-cost: 22 c ---[1574]---> BDD-cost: 22 c ---[1573]---> BDD-cost: 22 c ---[1572]---> Adder-cost: 216 maxlim: 6131 bits: 13/13 c ---[1571]---> Sorter-cost: 1778 Base: 2 2 2 2 2 2 2 2 c ---[1570]---> Sorter-cost: 2027 Base: 2 2 2 2 2 2 2 2 c ---[1569]---> Adder-cost: 216 maxlim: 6131 bits: 13/13 c ---[1568]---> Adder-cost: 216 maxlim: 6131 bits: 13/13 c ---[1567]---> Sorter-cost: 1520 Base: 2 2 2 2 2 2 2 2 c ---[1553]---> BDD-cost: 18 c ---[1551]---> BDD-cost: 18 c ---[1549]---> BDD-cost: 18 c ---[1547]---> BDD-cost: 18 c ---[1545]---> BDD-cost: 18 c ---[1543]---> BDD-cost: 18 c ---[1541]---> BDD-cost: 18 c ---[1539]---> BDD-cost: 18 c ---[1537]---> BDD-cost: 12 c ---[1535]---> BDD-cost: 15 c ---[1533]---> BDD-cost: 15 c ---[1531]---> BDD-cost: 12 c ---[ 23]---> Adder-cost: 741 maxlim: 1264 bits: 12/11 c ---[ 22]---> Adder-cost: 737 maxlim: 1255 bits: 12/11 c ---[ 21]---> Adder-cost: 631 maxlim: 1036 bits: 12/11 c ---[ 20]---> Adder-cost: 791 maxlim: 1264 bits: 12/11 c ---[ 19]---> Adder-cost: 741 maxlim: 1264 bits: 12/11 c ---[ 18]---> Adder-cost: 631 maxlim: 1036 bits: 12/11 c ---[ 17]---> Adder-cost: 711 maxlim: 1124 bits: 12/11 c ---[ 16]---> Adder-cost: 688 maxlim: 1005 bits: 11/10 c ---[ 15]---> Adder-cost: 542 maxlim: 908 bits: 11/10 c ---[ 14]---> Adder-cost: 696 maxlim: 1118 bits: 12/11 c ---[ 13]---> Adder-cost: 656 maxlim: 1107 bits: 12/11 c ---[ 12]---> Adder-cost: 606 maxlim: 1016 bits: 11/10 c ---[ 11]---> BDD-cost: 12 c ---[ 10]---> BDD-cost: 12 c ---[ 9]---> BDD-cost: 12 c ---[ 8]---> BDD-cost: 12 c ---[ 7]---> BDD-cost: 12 c ---[ 6]---> BDD-cost: 12 c ---[ 5]---> BDD-cost: 12 c ---[ 4]---> BDD-cost: 12 c ---[ 3]---> BDD-cost: 8 c ---[ 2]---> BDD-cost: 10 c ---[ 1]---> BDD-cost: 10 c ---[ 0]---> BDD-cost: 8 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 246857 842111 | 82285 0 0 nan | 0.000 % | c | 100 | 246855 842107 | 90513 98 312 3.2 | 8.420 % | c | 250 | 246763 841883 | 99564 243 810 3.3 | 8.465 % | c | 475 | 246319 840818 | 109521 446 1941 4.4 | 8.718 % | c | 815 | 246294 840762 | 120473 784 4442 5.7 | 8.735 % | c | 1321 | 246233 840592 | 132520 1264 8215 6.5 | 8.763 % | c | 2080 | 246224 840561 | 145772 2017 12583 6.2 | 8.765 % | c | 3220 | 246166 840402 | 160350 3152 24892 7.9 | 8.787 % | c | 4928 | 246160 840385 | 176385 4858 43117 8.9 | 8.789 % | c | 7491 | 246150 840347 | 194023 7416 113094 15.2 | 8.791 % | c | 11337 | 246063 840104 | 213426 11249 182667 16.2 | 8.824 % | c | 17106 | 246054 840073 | 234768 17014 365946 21.5 | 8.826 % | c | 25756 | 245829 839330 | 258245 25629 701783 27.4 | 8.891 % | c | 38732 | 245662 838873 | 284070 38580 1372824 35.6 | 8.958 % | c | 58193 | 245485 838414 | 312477 58026 2419527 41.7 | 9.049 % | c | 87385 | 245261 837670 | 343724 87164 3581363 41.1 | 9.114 % | c | 131174 | 244769 836340 | 378097 130895 5489212 41.9 | 9.336 % | c | 196859 | 244328 834887 | 415907 196547 10809419 55.0 | 9.458 % | c | 295387 | 243758 833389 | 457497 295007 17141711 58.1 | 9.730 % | c | 443178 | 241268 826486 | 503247 442632 26545252 60.0 | 10.923 % |
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/27627/stat): 27627 (minisat+_script) R 27626 27627 2660 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854868701 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/27627/statm): 174 3 169 147 0 27 0 [pid=27627] 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=27628 New process pid=27629 New process pid=27630 execve syscall for /bin/sed executable One traced child (pid=27629) exited with status: 0 open syscall for file /etc/ld.so.preload 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=27630) exited with status: 0 One traced child (pid=27628) exited with status: 0 New process pid=27631 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-UMTS.opb [startup+10.0039 s] Raw data (loadavg): 0.96 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 5439 0 0 0 946 26 0 0 25 0 1 0 1854868706 22822912 5204 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 5572 5204 145 145 0 5427 0 [pid=27631] vsize: 22288 Current children cumulated CPU time (s) 9.73 Current children cumulated vsize (Kb) 24412 [startup+20.0047 s] Raw data (loadavg): 0.97 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 5976 0 0 0 1937 30 0 0 25 0 1 0 1854868706 25042944 5741 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27631/statm): 6114 5741 145 145 0 5969 0 [pid=27631] vsize: 24456 Current children cumulated CPU time (s) 19.68 Current children cumulated vsize (Kb) 26580 [startup+30.0054 s] Raw data (loadavg): 0.97 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 6609 0 0 0 2927 36 0 0 25 0 1 0 1854868706 27582464 6374 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 6734 6374 145 145 0 6589 0 [pid=27631] vsize: 26936 Current children cumulated CPU time (s) 29.64 Current children cumulated vsize (Kb) 29060 [startup+40.0061 s] Raw data (loadavg): 0.98 0.98 0.93 1/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) T 27627 27627 2660 0 -1 0 7355 0 0 0 3913 42 0 0 25 0 1 0 1854868706 30728192 7120 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27631/statm): 7502 7120 145 145 0 7357 0 [pid=27631] vsize: 30008 Current children cumulated CPU time (s) 39.56 Current children cumulated vsize (Kb) 32132 [startup+50.0068 s] Raw data (loadavg): 0.98 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 7938 0 0 0 4902 47 0 0 25 0 1 0 1854868706 33083392 7703 4294967295 134512640 135094434 3221224432 3221223096 134556566 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 8077 7703 145 145 0 7932 0 [pid=27631] vsize: 32308 Current children cumulated CPU time (s) 49.5 Current children cumulated vsize (Kb) 34432 [startup+60.0075 s] Raw data (loadavg): 0.98 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 8465 0 0 0 5893 51 0 0 25 0 1 0 1854868706 35209216 8230 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 8596 8230 145 145 0 8451 0 [pid=27631] vsize: 34384 Current children cumulated CPU time (s) 59.45 Current children cumulated vsize (Kb) 36508 [startup+70.0083 s] Raw data (loadavg): 0.98 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 8947 0 0 0 6887 54 0 0 25 0 1 0 1854868706 37404672 8712 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 9132 8712 145 145 0 8987 0 [pid=27631] vsize: 36528 Current children cumulated CPU time (s) 69.42 Current children cumulated vsize (Kb) 38652 [startup+80.009 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 9544 0 0 0 7877 57 0 0 25 0 1 0 1854868706 39817216 9309 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 9721 9309 145 145 0 9576 0 [pid=27631] vsize: 38884 Current children cumulated CPU time (s) 79.35 Current children cumulated vsize (Kb) 41008 [startup+90.0097 s] Raw data (loadavg): 0.99 0.98 0.93 1/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) T 27627 27627 2660 0 -1 0 9981 0 0 0 8869 60 0 0 25 0 1 0 1854868706 41627648 9746 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27631/statm): 10163 9746 145 145 0 10018 0 [pid=27631] vsize: 40652 Current children cumulated CPU time (s) 89.3 Current children cumulated vsize (Kb) 42776 [startup+100.01 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 10365 0 0 0 9863 64 0 0 25 0 1 0 1854868706 43175936 10130 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 10541 10130 145 145 0 10396 0 [pid=27631] vsize: 42164 Current children cumulated CPU time (s) 99.28 Current children cumulated vsize (Kb) 44288 [startup+110.012 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 10868 0 0 0 10854 67 0 0 25 0 1 0 1854868706 45199360 10633 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 11035 10633 145 145 0 10890 0 [pid=27631] vsize: 44140 Current children cumulated CPU time (s) 109.22 Current children cumulated vsize (Kb) 46264 [startup+120.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 11292 0 0 0 11847 69 0 0 25 0 1 0 1854868706 46891008 11057 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 11448 11057 145 145 0 11303 0 [pid=27631] vsize: 45792 Current children cumulated CPU time (s) 119.17 Current children cumulated vsize (Kb) 47916 [startup+130.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 11734 0 0 0 12840 72 0 0 25 0 1 0 1854868706 48672768 11499 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 11883 11499 145 145 0 11738 0 [pid=27631] vsize: 47532 Current children cumulated CPU time (s) 129.13 Current children cumulated vsize (Kb) 49656 [startup+140.013 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 12252 0 0 0 13833 76 0 0 25 0 1 0 1854868706 50757632 12017 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 12392 12017 145 145 0 12247 0 [pid=27631] vsize: 49568 Current children cumulated CPU time (s) 139.1 Current children cumulated vsize (Kb) 51692 [startup+150.014 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 12667 0 0 0 14825 79 0 0 25 0 1 0 1854868706 52957184 12432 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 12929 12432 145 145 0 12784 0 [pid=27631] vsize: 51716 Current children cumulated CPU time (s) 149.05 Current children cumulated vsize (Kb) 53840 [startup+160.015 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 13089 0 0 0 15817 82 0 0 25 0 1 0 1854868706 54665216 12854 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 13346 12854 145 145 0 13201 0 [pid=27631] vsize: 53384 Current children cumulated CPU time (s) 159 Current children cumulated vsize (Kb) 55508 [startup+170.016 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 13466 0 0 0 16810 86 0 0 25 0 1 0 1854868706 56201216 13231 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 13721 13231 145 145 0 13576 0 [pid=27631] vsize: 54884 Current children cumulated CPU time (s) 168.97 Current children cumulated vsize (Kb) 57008 [startup+180.016 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 13825 0 0 0 17803 89 0 0 25 0 1 0 1854868706 57647104 13590 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 14074 13590 145 145 0 13929 0 [pid=27631] vsize: 56296 Current children cumulated CPU time (s) 178.93 Current children cumulated vsize (Kb) 58420 [startup+190.017 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 14316 0 0 0 18793 93 0 0 25 0 1 0 1854868706 59641856 14081 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 14561 14081 145 145 0 14416 0 [pid=27631] vsize: 58244 Current children cumulated CPU time (s) 188.87 Current children cumulated vsize (Kb) 60368 [startup+200.018 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 14687 0 0 0 19786 96 0 0 25 0 1 0 1854868706 61145088 14452 4294967295 134512640 135094434 3221224432 3221223024 134556851 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 14928 14452 145 145 0 14783 0 [pid=27631] vsize: 59712 Current children cumulated CPU time (s) 198.83 Current children cumulated vsize (Kb) 61836 [startup+210.019 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 15014 0 0 0 20779 100 0 0 25 0 1 0 1854868706 62472192 14779 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 15252 14779 145 145 0 15107 0 [pid=27631] vsize: 61008 Current children cumulated CPU time (s) 208.8 Current children cumulated vsize (Kb) 63132 [startup+220.02 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 15342 0 0 0 21772 102 0 0 25 0 1 0 1854868706 63807488 15107 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 15578 15107 145 145 0 15433 0 [pid=27631] vsize: 62312 Current children cumulated CPU time (s) 218.75 Current children cumulated vsize (Kb) 64436 [startup+230.021 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 15639 0 0 0 22767 105 0 0 25 0 1 0 1854868706 65036288 15404 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 15878 15404 145 145 0 15733 0 [pid=27631] vsize: 63512 Current children cumulated CPU time (s) 228.73 Current children cumulated vsize (Kb) 65636 [startup+240.022 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 15900 0 0 0 23762 107 0 0 25 0 1 0 1854868706 66093056 15665 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 16136 15665 145 145 0 15991 0 [pid=27631] vsize: 64544 Current children cumulated CPU time (s) 238.7 Current children cumulated vsize (Kb) 66668 [startup+250.022 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 16166 0 0 0 24758 109 0 0 25 0 1 0 1854868706 67170304 15931 4294967295 134512640 135094434 3221224432 3221223092 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 16399 15931 145 145 0 16254 0 [pid=27631] vsize: 65596 Current children cumulated CPU time (s) 248.68 Current children cumulated vsize (Kb) 67720 [startup+260.022 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 16347 0 0 0 25753 112 0 0 25 0 1 0 1854868706 67903488 16112 4294967295 134512640 135094434 3221224432 3221223024 134557407 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 16578 16112 145 145 0 16433 0 [pid=27631] vsize: 66312 Current children cumulated CPU time (s) 258.66 Current children cumulated vsize (Kb) 68436 [startup+270.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 17225 0 0 0 26740 117 0 0 25 0 1 0 1854868706 71467008 16990 4294967295 134512640 135094434 3221224432 3221223088 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 17448 16990 145 145 0 17303 0 [pid=27631] vsize: 69792 Current children cumulated CPU time (s) 268.58 Current children cumulated vsize (Kb) 71916 [startup+280.022 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 17824 0 0 0 27731 120 0 0 25 0 1 0 1854868706 73916416 17589 4294967295 134512640 135094434 3221224432 3221223088 134558135 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 18046 17589 145 145 0 17901 0 [pid=27631] vsize: 72184 Current children cumulated CPU time (s) 278.52 Current children cumulated vsize (Kb) 74308 [startup+290.023 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 18316 0 0 0 28723 123 0 0 25 0 1 0 1854868706 75898880 18081 4294967295 134512640 135094434 3221224432 3221223136 134559013 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27631/statm): 18530 18081 145 145 0 18385 0 [pid=27631] vsize: 74120 Current children cumulated CPU time (s) 288.47 Current children cumulated vsize (Kb) 76244 [startup+300.024 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 18733 0 0 0 29716 126 0 0 25 0 1 0 1854868706 77574144 18498 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 18939 18498 145 145 0 18794 0 [pid=27631] vsize: 75756 Current children cumulated CPU time (s) 298.43 Current children cumulated vsize (Kb) 77880 [startup+310.024 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 18946 0 0 0 30712 128 0 0 25 0 1 0 1854868706 78422016 18711 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 19146 18711 145 145 0 19001 0 [pid=27631] vsize: 76584 Current children cumulated CPU time (s) 308.41 Current children cumulated vsize (Kb) 78708 [startup+320.024 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 19769 0 0 0 31701 132 0 0 25 0 1 0 1854868706 81743872 19534 4294967295 134512640 135094434 3221224432 3221223072 134562110 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 19957 19534 145 145 0 19812 0 [pid=27631] vsize: 79828 Current children cumulated CPU time (s) 318.34 Current children cumulated vsize (Kb) 81952 [startup+330.025 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 20160 0 0 0 32695 135 0 0 25 0 1 0 1854868706 83320832 19925 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 20342 19925 145 145 0 20197 0 [pid=27631] vsize: 81368 Current children cumulated CPU time (s) 328.31 Current children cumulated vsize (Kb) 83492 [startup+340.027 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 20535 0 0 0 33688 137 0 0 25 0 1 0 1854868706 84840448 20300 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 20713 20300 145 145 0 20568 0 [pid=27631] vsize: 82852 Current children cumulated CPU time (s) 338.26 Current children cumulated vsize (Kb) 84976 [startup+350.028 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 20872 0 0 0 34683 139 0 0 25 0 1 0 1854868706 86200320 20637 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 21045 20637 145 145 0 20900 0 [pid=27631] vsize: 84180 Current children cumulated CPU time (s) 348.23 Current children cumulated vsize (Kb) 86304 [startup+360.027 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 21398 0 0 0 35673 143 0 0 25 0 1 0 1854868706 88326144 21163 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 21564 21163 145 145 0 21419 0 [pid=27631] vsize: 86256 Current children cumulated CPU time (s) 358.17 Current children cumulated vsize (Kb) 88380 [startup+370.028 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 21827 0 0 0 36665 146 0 0 25 0 1 0 1854868706 90054656 21592 4294967295 134512640 135094434 3221224432 3221223072 134558264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 21986 21592 145 145 0 21841 0 [pid=27631] vsize: 87944 Current children cumulated CPU time (s) 368.12 Current children cumulated vsize (Kb) 90068 [startup+380.028 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 22651 0 0 0 37651 152 0 0 25 0 1 0 1854868706 93405184 22416 4294967295 134512640 135094434 3221224432 3221223024 134551908 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 22804 22416 145 145 0 22659 0 [pid=27631] vsize: 91216 Current children cumulated CPU time (s) 378.04 Current children cumulated vsize (Kb) 93340 [startup+390.028 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 23371 0 0 0 38638 158 0 0 25 0 1 0 1854868706 97382400 23136 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 23775 23136 145 145 0 23630 0 [pid=27631] vsize: 95100 Current children cumulated CPU time (s) 387.97 Current children cumulated vsize (Kb) 97224 [startup+400.029 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 23930 0 0 0 39628 162 0 0 25 0 1 0 1854868706 99655680 23695 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 24330 23695 145 145 0 24185 0 [pid=27631] vsize: 97320 Current children cumulated CPU time (s) 397.91 Current children cumulated vsize (Kb) 99444 [startup+410.029 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 24606 0 0 0 40617 167 0 0 25 0 1 0 1854868706 102400000 24371 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 25000 24371 145 145 0 24855 0 [pid=27631] vsize: 100000 Current children cumulated CPU time (s) 407.85 Current children cumulated vsize (Kb) 102124 [startup+420.03 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 25062 0 0 0 41610 170 0 0 25 0 1 0 1854868706 104235008 24827 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 25448 24827 145 145 0 25303 0 [pid=27631] vsize: 101792 Current children cumulated CPU time (s) 417.81 Current children cumulated vsize (Kb) 103916 [startup+430.03 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 25368 0 0 0 42604 172 0 0 25 0 1 0 1854868706 105467904 25133 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 25749 25133 145 145 0 25604 0 [pid=27631] vsize: 102996 Current children cumulated CPU time (s) 427.77 Current children cumulated vsize (Kb) 105120 [startup+440.031 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 25767 0 0 0 43596 176 0 0 25 0 1 0 1854868706 107081728 25532 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27631/statm): 26143 25532 145 145 0 25998 0 [pid=27631] vsize: 104572 Current children cumulated CPU time (s) 437.73 Current children cumulated vsize (Kb) 106696 [startup+450.032 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 25942 0 0 0 44591 178 0 0 25 0 1 0 1854868706 107786240 25707 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 26315 25707 145 145 0 26170 0 [pid=27631] vsize: 105260 Current children cumulated CPU time (s) 447.7 Current children cumulated vsize (Kb) 107384 [startup+460.033 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 25953 0 0 0 45592 178 0 0 25 0 1 0 1854868706 107827200 25718 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 26325 25718 145 145 0 26180 0 [pid=27631] vsize: 105300 Current children cumulated CPU time (s) 457.71 Current children cumulated vsize (Kb) 107424 [startup+470.033 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 26071 0 0 0 46590 179 0 0 25 0 1 0 1854868706 108302336 25836 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 26441 25836 145 145 0 26296 0 [pid=27631] vsize: 105764 Current children cumulated CPU time (s) 467.7 Current children cumulated vsize (Kb) 107888 [startup+480.034 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 26333 0 0 0 47585 181 0 0 25 0 1 0 1854868706 109355008 26098 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 26698 26098 145 145 0 26553 0 [pid=27631] vsize: 106792 Current children cumulated CPU time (s) 477.67 Current children cumulated vsize (Kb) 108916 [startup+490.035 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 26515 0 0 0 48582 183 0 0 25 0 1 0 1854868706 110092288 26280 4294967295 134512640 135094434 3221224432 3221223092 134553450 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 26878 26280 145 145 0 26733 0 [pid=27631] vsize: 107512 Current children cumulated CPU time (s) 487.66 Current children cumulated vsize (Kb) 109636 [startup+500.035 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 26677 0 0 0 49578 184 0 0 25 0 1 0 1854868706 110739456 26442 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 27036 26442 145 145 0 26891 0 [pid=27631] vsize: 108144 Current children cumulated CPU time (s) 497.63 Current children cumulated vsize (Kb) 110268 [startup+510.035 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 26951 0 0 0 50573 185 0 0 25 0 1 0 1854868706 111845376 26716 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 27306 26716 145 145 0 27161 0 [pid=27631] vsize: 109224 Current children cumulated CPU time (s) 507.59 Current children cumulated vsize (Kb) 111348 [startup+520.036 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 27180 0 0 0 51570 186 0 0 25 0 1 0 1854868706 112771072 26945 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 27532 26945 145 145 0 27387 0 [pid=27631] vsize: 110128 Current children cumulated CPU time (s) 517.57 Current children cumulated vsize (Kb) 112252 [startup+530.037 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 27619 0 0 0 52561 190 0 0 25 0 1 0 1854868706 114548736 27384 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 27966 27384 145 145 0 27821 0 [pid=27631] vsize: 111864 Current children cumulated CPU time (s) 527.52 Current children cumulated vsize (Kb) 113988 [startup+540.038 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 28092 0 0 0 53551 194 0 0 25 0 1 0 1854868706 116477952 27857 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 28437 27857 145 145 0 28292 0 [pid=27631] vsize: 113748 Current children cumulated CPU time (s) 537.46 Current children cumulated vsize (Kb) 115872 [startup+550.039 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 28336 0 0 0 54549 195 0 0 25 0 1 0 1854868706 117460992 28101 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 28677 28101 145 145 0 28532 0 [pid=27631] vsize: 114708 Current children cumulated CPU time (s) 547.45 Current children cumulated vsize (Kb) 116832 [startup+560.039 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 28574 0 0 0 55545 197 0 0 25 0 1 0 1854868706 118427648 28339 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 28913 28339 145 145 0 28768 0 [pid=27631] vsize: 115652 Current children cumulated CPU time (s) 557.43 Current children cumulated vsize (Kb) 117776 [startup+570.039 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 28793 0 0 0 56541 198 0 0 25 0 1 0 1854868706 119324672 28558 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 29132 28558 145 145 0 28987 0 [pid=27631] vsize: 116528 Current children cumulated CPU time (s) 567.4 Current children cumulated vsize (Kb) 118652 [startup+580.039 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 29005 0 0 0 57537 200 0 0 25 0 1 0 1854868706 120193024 28770 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 29344 28770 145 145 0 29199 0 [pid=27631] vsize: 117376 Current children cumulated CPU time (s) 577.38 Current children cumulated vsize (Kb) 119500 [startup+590.04 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 29215 0 0 0 58534 202 0 0 25 0 1 0 1854868706 121065472 28980 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 29557 28980 145 145 0 29412 0 [pid=27631] vsize: 118228 Current children cumulated CPU time (s) 587.37 Current children cumulated vsize (Kb) 120352 [startup+600.041 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 29429 0 0 0 59531 203 0 0 25 0 1 0 1854868706 121950208 29194 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 29773 29194 145 145 0 29628 0 [pid=27631] vsize: 119092 Current children cumulated CPU time (s) 597.35 Current children cumulated vsize (Kb) 121216 [startup+610.041 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 29622 0 0 0 60527 205 0 0 25 0 1 0 1854868706 122736640 29387 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 29965 29387 145 145 0 29820 0 [pid=27631] vsize: 119860 Current children cumulated CPU time (s) 607.33 Current children cumulated vsize (Kb) 121984 [startup+620.042 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 29799 0 0 0 61525 206 0 0 25 0 1 0 1854868706 123461632 29564 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 30142 29564 145 145 0 29997 0 [pid=27631] vsize: 120568 Current children cumulated CPU time (s) 617.32 Current children cumulated vsize (Kb) 122692 [startup+630.043 s] Raw data (loadavg): 0.99 0.98 0.93 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 29974 0 0 0 62523 207 0 0 25 0 1 0 1854868706 124190720 29739 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 30320 29739 145 145 0 30175 0 [pid=27631] vsize: 121280 Current children cumulated CPU time (s) 627.31 Current children cumulated vsize (Kb) 123404 [startup+640.045 s] Raw data (loadavg): 1.07 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 30079 0 0 0 63522 208 0 0 25 0 1 0 1854868706 124620800 29844 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 30425 29844 145 145 0 30280 0 [pid=27631] vsize: 121700 Current children cumulated CPU time (s) 637.31 Current children cumulated vsize (Kb) 123824 [startup+650.045 s] Raw data (loadavg): 1.06 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 30199 0 0 0 64519 209 0 0 25 0 1 0 1854868706 125104128 29964 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 30543 29964 145 145 0 30398 0 [pid=27631] vsize: 122172 Current children cumulated CPU time (s) 647.29 Current children cumulated vsize (Kb) 124296 [startup+660.045 s] Raw data (loadavg): 1.05 1.00 0.94 1/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) T 27627 27627 2660 0 -1 0 30250 0 0 0 65518 209 0 0 25 0 1 0 1854868706 125304832 30015 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/27631/statm): 30592 30015 145 145 0 30447 0 [pid=27631] vsize: 122368 Current children cumulated CPU time (s) 657.28 Current children cumulated vsize (Kb) 124492 [startup+670.046 s] Raw data (loadavg): 1.04 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 30479 0 0 0 66515 210 0 0 25 0 1 0 1854868706 126246912 30244 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 30822 30244 145 145 0 30677 0 [pid=27631] vsize: 123288 Current children cumulated CPU time (s) 667.26 Current children cumulated vsize (Kb) 125412 [startup+680.045 s] Raw data (loadavg): 1.03 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 30623 0 0 0 67514 211 0 0 25 0 1 0 1854868706 126844928 30388 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 30968 30388 145 145 0 30823 0 [pid=27631] vsize: 123872 Current children cumulated CPU time (s) 677.26 Current children cumulated vsize (Kb) 125996 [startup+690.046 s] Raw data (loadavg): 1.03 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 30782 0 0 0 68511 212 0 0 25 0 1 0 1854868706 127520768 30547 4294967295 134512640 135094434 3221224432 3221223092 134553508 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 31133 30547 145 145 0 30988 0 [pid=27631] vsize: 124532 Current children cumulated CPU time (s) 687.24 Current children cumulated vsize (Kb) 126656 [startup+700.047 s] Raw data (loadavg): 1.02 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 30790 0 0 0 69511 212 0 0 25 0 1 0 1854868706 127553536 30555 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 31141 30555 145 145 0 30996 0 [pid=27631] vsize: 124564 Current children cumulated CPU time (s) 697.24 Current children cumulated vsize (Kb) 126688 [startup+710.048 s] Raw data (loadavg): 1.02 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 30876 0 0 0 70510 213 0 0 25 0 1 0 1854868706 127905792 30641 4294967295 134512640 135094434 3221224432 3221223092 134553515 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 31227 30641 145 145 0 31082 0 [pid=27631] vsize: 124908 Current children cumulated CPU time (s) 707.24 Current children cumulated vsize (Kb) 127032 [startup+720.048 s] Raw data (loadavg): 1.02 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 30943 0 0 0 71508 214 0 0 25 0 1 0 1854868706 128184320 30708 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 31295 30708 145 145 0 31150 0 [pid=27631] vsize: 125180 Current children cumulated CPU time (s) 717.23 Current children cumulated vsize (Kb) 127304 [startup+730.049 s] Raw data (loadavg): 1.01 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 31049 0 0 0 72507 214 0 0 25 0 1 0 1854868706 128622592 30814 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 31402 30814 145 145 0 31257 0 [pid=27631] vsize: 125608 Current children cumulated CPU time (s) 727.22 Current children cumulated vsize (Kb) 127732 [startup+740.05 s] Raw data (loadavg): 1.01 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 31470 0 0 0 73500 217 0 0 25 0 1 0 1854868706 130322432 31235 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 31817 31235 145 145 0 31672 0 [pid=27631] vsize: 127268 Current children cumulated CPU time (s) 737.18 Current children cumulated vsize (Kb) 129392 [startup+750.051 s] Raw data (loadavg): 1.01 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 32024 0 0 0 74490 221 0 0 25 0 1 0 1854868706 132567040 31789 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 32365 31789 145 145 0 32220 0 [pid=27631] vsize: 129460 Current children cumulated CPU time (s) 747.12 Current children cumulated vsize (Kb) 131584 [startup+760.051 s] Raw data (loadavg): 1.01 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 32705 0 0 0 75478 225 0 0 25 0 1 0 1854868706 135340032 32470 4294967295 134512640 135094434 3221224432 3221223088 134558129 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 33042 32470 145 145 0 32897 0 [pid=27631] vsize: 132168 Current children cumulated CPU time (s) 757.04 Current children cumulated vsize (Kb) 134292 [startup+770.052 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 33469 0 0 0 76465 231 0 0 25 0 1 0 1854868706 138444800 33234 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 33800 33234 145 145 0 33655 0 [pid=27631] vsize: 135200 Current children cumulated CPU time (s) 766.97 Current children cumulated vsize (Kb) 137324 [startup+780.052 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 34213 0 0 0 77453 236 0 0 25 0 1 0 1854868706 141459456 33978 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 34536 33978 145 145 0 34391 0 [pid=27631] vsize: 138144 Current children cumulated CPU time (s) 776.9 Current children cumulated vsize (Kb) 140268 [startup+790.053 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 34698 0 0 0 78444 239 0 0 25 0 1 0 1854868706 143437824 34463 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 35019 34463 145 145 0 34874 0 [pid=27631] vsize: 140076 Current children cumulated CPU time (s) 786.84 Current children cumulated vsize (Kb) 142200 [startup+800.053 s] Raw data (loadavg): 1.08 1.02 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 35157 0 0 0 79436 243 0 0 25 0 1 0 1854868706 145305600 34922 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 35475 34922 145 145 0 35330 0 [pid=27631] vsize: 141900 Current children cumulated CPU time (s) 796.8 Current children cumulated vsize (Kb) 144024 [startup+810.054 s] Raw data (loadavg): 1.06 1.02 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 35574 0 0 0 80428 247 0 0 25 0 1 0 1854868706 147009536 35339 4294967295 134512640 135094434 3221224432 3221223024 134557175 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 35891 35339 145 145 0 35746 0 [pid=27631] vsize: 143564 Current children cumulated CPU time (s) 806.76 Current children cumulated vsize (Kb) 145688 [startup+820.055 s] Raw data (loadavg): 1.05 1.01 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 36012 0 0 0 81420 251 0 0 25 0 1 0 1854868706 148815872 35777 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 36332 35777 145 145 0 36187 0 [pid=27631] vsize: 145328 Current children cumulated CPU time (s) 816.72 Current children cumulated vsize (Kb) 147452 [startup+830.055 s] Raw data (loadavg): 1.04 1.01 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 36463 0 0 0 82410 256 0 0 25 0 1 0 1854868706 150659072 36228 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 36782 36228 145 145 0 36637 0 [pid=27631] vsize: 147128 Current children cumulated CPU time (s) 826.67 Current children cumulated vsize (Kb) 149252 [startup+840.057 s] Raw data (loadavg): 1.04 1.01 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 36925 0 0 0 83401 259 0 0 25 0 1 0 1854868706 152555520 36690 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 37245 36690 145 145 0 37100 0 [pid=27631] vsize: 148980 Current children cumulated CPU time (s) 836.61 Current children cumulated vsize (Kb) 151104 [startup+850.058 s] Raw data (loadavg): 1.03 1.01 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 37349 0 0 0 84393 262 0 0 25 0 1 0 1854868706 154271744 37114 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 37664 37114 145 145 0 37519 0 [pid=27631] vsize: 150656 Current children cumulated CPU time (s) 846.56 Current children cumulated vsize (Kb) 152780 [startup+860.058 s] Raw data (loadavg): 1.03 1.01 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 37749 0 0 0 85385 265 0 0 25 0 1 0 1854868706 155897856 37514 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 38061 37514 145 145 0 37916 0 [pid=27631] vsize: 152244 Current children cumulated CPU time (s) 856.51 Current children cumulated vsize (Kb) 154368 [startup+870.058 s] Raw data (loadavg): 1.02 1.01 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 38110 0 0 0 86380 267 0 0 25 0 1 0 1854868706 157360128 37875 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 38418 37875 145 145 0 38273 0 [pid=27631] vsize: 153672 Current children cumulated CPU time (s) 866.48 Current children cumulated vsize (Kb) 155796 [startup+880.059 s] Raw data (loadavg): 1.02 1.01 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 38457 0 0 0 87374 269 0 0 25 0 1 0 1854868706 158769152 38222 4294967295 134512640 135094434 3221224432 3221223088 134557917 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 38762 38222 145 145 0 38617 0 [pid=27631] vsize: 155048 Current children cumulated CPU time (s) 876.44 Current children cumulated vsize (Kb) 157172 [startup+890.06 s] Raw data (loadavg): 1.01 1.01 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 38821 0 0 0 88367 272 0 0 25 0 1 0 1854868706 160251904 38586 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 39124 38586 145 145 0 38979 0 [pid=27631] vsize: 156496 Current children cumulated CPU time (s) 886.4 Current children cumulated vsize (Kb) 158620 [startup+900.061 s] Raw data (loadavg): 1.01 1.01 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 39124 0 0 0 89362 274 0 0 25 0 1 0 1854868706 161484800 38889 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 39425 38889 145 145 0 39280 0 [pid=27631] vsize: 157700 Current children cumulated CPU time (s) 896.37 Current children cumulated vsize (Kb) 159824 [startup+910.061 s] Raw data (loadavg): 1.01 1.01 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 39293 0 0 0 90359 275 0 0 25 0 1 0 1854868706 162172928 39058 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 39593 39058 145 145 0 39448 0 [pid=27631] vsize: 158372 Current children cumulated CPU time (s) 906.35 Current children cumulated vsize (Kb) 160496 [startup+920.062 s] Raw data (loadavg): 1.01 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 39835 0 0 0 91351 279 0 0 25 0 1 0 1854868706 164364288 39600 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 40128 39600 145 145 0 39983 0 [pid=27631] vsize: 160512 Current children cumulated CPU time (s) 916.31 Current children cumulated vsize (Kb) 162636 [startup+930.063 s] Raw data (loadavg): 1.01 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 40285 0 0 0 92342 283 0 0 25 0 1 0 1854868706 166187008 40050 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/27631/statm): 40573 40050 145 145 0 40428 0 [pid=27631] vsize: 162292 Current children cumulated CPU time (s) 926.26 Current children cumulated vsize (Kb) 164416 [startup+940.064 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 40699 0 0 0 93334 286 0 0 25 0 1 0 1854868706 167866368 40464 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 40983 40464 145 145 0 40838 0 [pid=27631] vsize: 163932 Current children cumulated CPU time (s) 936.21 Current children cumulated vsize (Kb) 166056 [startup+950.065 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 41106 0 0 0 94329 288 0 0 25 0 1 0 1854868706 169512960 40871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 41385 40871 145 145 0 41240 0 [pid=27631] vsize: 165540 Current children cumulated CPU time (s) 946.18 Current children cumulated vsize (Kb) 167664 [startup+960.066 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 41426 0 0 0 95324 291 0 0 25 0 1 0 1854868706 170815488 41191 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 41703 41191 145 145 0 41558 0 [pid=27631] vsize: 166812 Current children cumulated CPU time (s) 956.16 Current children cumulated vsize (Kb) 168936 [startup+970.067 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 41734 0 0 0 96319 293 0 0 25 0 1 0 1854868706 172052480 41499 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42005 41499 145 145 0 41860 0 [pid=27631] vsize: 168020 Current children cumulated CPU time (s) 966.13 Current children cumulated vsize (Kb) 170144 [startup+980.067 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42026 0 0 0 97316 294 0 0 25 0 1 0 1854868706 173240320 41791 4294967295 134512640 135094434 3221224432 3221223072 134562230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42295 41791 145 145 0 42150 0 [pid=27631] vsize: 169180 Current children cumulated CPU time (s) 976.11 Current children cumulated vsize (Kb) 171304 [startup+990.068 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42319 0 0 0 98310 297 0 0 25 0 1 0 1854868706 174436352 42084 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42587 42084 145 145 0 42442 0 [pid=27631] vsize: 170348 Current children cumulated CPU time (s) 986.08 Current children cumulated vsize (Kb) 172472 [startup+1000.07 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 99307 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223024 134551428 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 996.07 Current children cumulated vsize (Kb) 173380 [startup+1010.07 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 100307 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1006.07 Current children cumulated vsize (Kb) 173380 [startup+1020.07 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 101307 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1016.07 Current children cumulated vsize (Kb) 173380 [startup+1030.07 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 102307 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1026.07 Current children cumulated vsize (Kb) 173380 [startup+1040.07 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 103307 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1036.07 Current children cumulated vsize (Kb) 173380 [startup+1050.07 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 104308 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1046.08 Current children cumulated vsize (Kb) 173380 [startup+1060.07 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 105308 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1056.08 Current children cumulated vsize (Kb) 173380 [startup+1070.07 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 106308 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1066.08 Current children cumulated vsize (Kb) 173380 [startup+1080.07 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 107308 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1076.08 Current children cumulated vsize (Kb) 173380 [startup+1090.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 108308 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1086.08 Current children cumulated vsize (Kb) 173380 [startup+1100.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 109308 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223092 134553533 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1096.08 Current children cumulated vsize (Kb) 173380 [startup+1110.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 110309 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1106.09 Current children cumulated vsize (Kb) 173380 [startup+1120.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 111309 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1116.09 Current children cumulated vsize (Kb) 173380 [startup+1130.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 112309 299 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223024 134557310 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1126.09 Current children cumulated vsize (Kb) 173380 [startup+1140.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 113309 300 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1136.1 Current children cumulated vsize (Kb) 173380 [startup+1150.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 114309 300 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1146.1 Current children cumulated vsize (Kb) 173380 [startup+1160.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 115309 300 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1156.1 Current children cumulated vsize (Kb) 173380 [startup+1170.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 116310 300 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1166.11 Current children cumulated vsize (Kb) 173380 [startup+1180.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 117310 300 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1176.11 Current children cumulated vsize (Kb) 173380 [startup+1190.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 118310 300 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1186.11 Current children cumulated vsize (Kb) 173380 [startup+1200.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 119311 300 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1196.12 Current children cumulated vsize (Kb) 173380 [startup+1210.08 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 120310 300 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223104 134556364 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1206.11 Current children cumulated vsize (Kb) 173380 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 1.00 1.00 0.94 2/57 27631 Raw data (/proc/27627/stat): 27627 (minisat+_script) S 27626 27627 2660 0 -1 0 289 239 0 0 0 1 0 0 21 0 1 0 1854868701 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/27627/statm): 531 226 485 147 0 384 0 [pid=27627] vsize: 2124 Raw data (/proc/27631/stat): 27631 (minisat+_64-bit) R 27627 27627 2660 0 -1 0 42548 0 0 0 120311 300 0 0 25 0 1 0 1854868706 175366144 42313 4294967295 134512640 135094434 3221224432 3221223104 134556377 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/27631/statm): 42814 42313 145 145 0 42669 0 [pid=27631] vsize: 171256 Current children cumulated CPU time (s) 1206.12 Current children cumulated vsize (Kb) 173380 Sending SIGTERM to -27627 Sleeping 2 seconds One traced child (pid=27627) ended because it received signal 15 (SIGTERM) One traced child (pid=27631) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1210.17 CPU time (s): 1206.2 CPU user time (s): 1203.11 CPU system time (s): 3.08553 CPU usage (%): 99.6719 Max. virtual memory (cumulated for all children) (Kb): 173380
ERROR: no interpretation found !