Name | mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-gesa3.opb |
MD5SUM | 2066c600bb1ef997326ad814b69b94ca |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 1040365708092 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 7992 |
Biggest coefficient in the objective function | 409031671808 |
Number of bits for the biggest coefficient in the objective function | 39 |
Sum of the numbers in the objective function | 143986524985584 |
Number of bits of the sum of numbers in the objective function | 48 |
Biggest number in a constraint | 524288000000 |
Number of bits of the biggest number in a constraint | 39 |
Biggest sum of numbers in a constraint | 143986524985584 |
Number of bits of the biggest sum of numbers | 48 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1227.99 |
Number of variables | 12720 |
Total number of constraints | 1824 |
Number of constraints which are clauses | 48 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 1776 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 211 |
LAUNCH ON wulflinc12 THE 2005-09-20 04:20:58 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3360 boxname=wulflinc12 idbench=1016 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 2066c600bb1ef997326ad814b69b94ca /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-gesa3.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-gesa3.opb IDLAUNCH: 3360 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 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 : 2 cpu MHz : 451.091 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 901960 kB Buffers: 33352 kB Cached: 68700 kB SwapCached: 492 kB Active: 51304 kB Inactive: 53304 kB HighTotal: 131008 kB HighFree: 60172 kB LowTotal: 903652 kB LowFree: 841788 kB SwapTotal: 2097136 kB SwapFree: 2096072 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5892 kB Slab: 22312 kB Committed_AS: 64164 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-20 04:40:58 (client local time) WITH STATUS 0 IN 1200.14 SECONDS stats: 3360 7 1200.14 0
c Parsing PB file... c Converting 1800 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################################ c -- Clauses(.)/Splits(s): ................................................................................................sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss c ---[1929]---> BDD-cost: 2 c ---[1928]---> BDD-cost: 2 c ---[1925]---> BDD-cost: 2 c ---[1924]---> BDD-cost: 2 c ---[1921]---> BDD-cost: 2 c ---[1920]---> BDD-cost: 2 c ---[1917]---> BDD-cost: 2 c ---[1916]---> BDD-cost: 2 c ---[1913]---> BDD-cost: 2 c ---[1912]---> BDD-cost: 2 c ---[1909]---> BDD-cost: 2 c ---[1908]---> BDD-cost: 2 c ---[1905]---> BDD-cost: 2 c ---[1904]---> BDD-cost: 2 c ---[1901]---> BDD-cost: 2 c ---[1900]---> BDD-cost: 2 c ---[1897]---> BDD-cost: 2 c ---[1896]---> BDD-cost: 2 c ---[1893]---> BDD-cost: 2 c ---[1892]---> BDD-cost: 2 c ---[1889]---> BDD-cost: 2 c ---[1888]---> BDD-cost: 2 c ---[1885]---> BDD-cost: 2 c ---[1884]---> BDD-cost: 2 c ---[1881]---> BDD-cost: 2 c ---[1880]---> BDD-cost: 2 c ---[1877]---> BDD-cost: 2 c ---[1876]---> BDD-cost: 2 c ---[1873]---> BDD-cost: 2 c ---[1872]---> BDD-cost: 2 c ---[1869]---> BDD-cost: 2 c ---[1868]---> BDD-cost: 2 c ---[1865]---> BDD-cost: 2 c ---[1864]---> BDD-cost: 2 c ---[1861]---> BDD-cost: 2 c ---[1860]---> BDD-cost: 2 c ---[1857]---> BDD-cost: 2 c ---[1856]---> BDD-cost: 2 c ---[1853]---> BDD-cost: 2 c ---[1852]---> BDD-cost: 2 c ---[1849]---> BDD-cost: 2 c ---[1848]---> BDD-cost: 2 c ---[1845]---> BDD-cost: 2 c ---[1844]---> BDD-cost: 2 c ---[1841]---> BDD-cost: 2 c ---[1840]---> BDD-cost: 2 c ---[1837]---> BDD-cost: 2 c ---[1836]---> BDD-cost: 2 c ---[1833]---> BDD-cost: 7 c ---[1832]---> BDD-cost: 7 c ---[1831]---> BDD-cost: 7 c ---[1830]---> BDD-cost: 7 c ---[1829]---> BDD-cost: 8 c ---[1828]---> BDD-cost: 9 c ---[1827]---> BDD-cost: 8 c ---[1826]---> BDD-cost: 8 c ---[1825]---> BDD-cost: 9 c ---[1824]---> BDD-cost: 8 c ---[1823]---> BDD-cost: 7 c ---[1822]---> BDD-cost: 8 c ---[1821]---> BDD-cost: 7 c ---[1820]---> BDD-cost: 7 c ---[1819]---> BDD-cost: 7 c ---[1818]---> BDD-cost: 7 c ---[1817]---> BDD-cost: 8 c ---[1816]---> BDD-cost: 9 c ---[1815]---> BDD-cost: 8 c ---[1814]---> BDD-cost: 8 c ---[1813]---> BDD-cost: 9 c ---[1812]---> BDD-cost: 8 c ---[1811]---> BDD-cost: 7 c ---[1810]---> BDD-cost: 8 c ---[1809]---> BDD-cost: 7 c ---[1808]---> BDD-cost: 7 c ---[1807]---> BDD-cost: 7 c ---[1806]---> BDD-cost: 7 c ---[1805]---> BDD-cost: 8 c ---[1804]---> BDD-cost: 9 c ---[1803]---> BDD-cost: 8 c ---[1802]---> BDD-cost: 8 c ---[1801]---> BDD-cost: 9 c ---[1800]---> BDD-cost: 8 c ---[1799]---> BDD-cost: 7 c ---[1798]---> BDD-cost: 8 c ---[1797]---> BDD-cost: 7 c ---[1796]---> BDD-cost: 7 c ---[1795]---> BDD-cost: 7 c ---[1794]---> BDD-cost: 7 c ---[1793]---> BDD-cost: 8 c ---[1792]---> BDD-cost: 9 c ---[1791]---> BDD-cost: 8 c ---[1790]---> BDD-cost: 8 c ---[1789]---> BDD-cost: 9 c ---[1788]---> BDD-cost: 8 c ---[1787]---> BDD-cost: 7 c ---[1786]---> BDD-cost: 8 c ---[1785]---> BDD-cost: 7 c ---[1784]---> BDD-cost: 7 c ---[1783]---> BDD-cost: 7 c ---[1782]---> BDD-cost: 7 c ---[1781]---> BDD-cost: 8 c ---[1780]---> BDD-cost: 9 c ---[1779]---> BDD-cost: 8 c ---[1778]---> BDD-cost: 8 c ---[1777]---> BDD-cost: 9 c ---[1776]---> BDD-cost: 8 c ---[1775]---> BDD-cost: 7 c ---[1774]---> BDD-cost: 8 c ---[1773]---> BDD-cost: 7 c ---[1772]---> BDD-cost: 7 c ---[1771]---> BDD-cost: 7 c ---[1770]---> BDD-cost: 7 c ---[1769]---> BDD-cost: 8 c ---[1768]---> BDD-cost: 9 c ---[1767]---> BDD-cost: 8 c ---[1766]---> BDD-cost: 8 c ---[1765]---> BDD-cost: 9 c ---[1764]---> BDD-cost: 8 c ---[1763]---> BDD-cost: 7 c ---[1762]---> BDD-cost: 8 c ---[1761]---> BDD-cost: 7 c ---[1760]---> BDD-cost: 7 c ---[1759]---> BDD-cost: 7 c ---[1758]---> BDD-cost: 7 c ---[1757]---> BDD-cost: 8 c ---[1756]---> BDD-cost: 9 c ---[1755]---> BDD-cost: 8 c ---[1754]---> BDD-cost: 8 c ---[1753]---> BDD-cost: 9 c ---[1752]---> BDD-cost: 8 c ---[1751]---> BDD-cost: 7 c ---[1750]---> BDD-cost: 8 c ---[1749]---> BDD-cost: 7 c ---[1748]---> BDD-cost: 7 c ---[1747]---> BDD-cost: 7 c ---[1746]---> BDD-cost: 7 c ---[1745]---> BDD-cost: 8 c ---[1744]---> BDD-cost: 9 c ---[1743]---> BDD-cost: 8 c ---[1742]---> BDD-cost: 8 c ---[1741]---> BDD-cost: 9 c ---[1740]---> BDD-cost: 8 c ---[1739]---> BDD-cost: 7 c ---[1738]---> BDD-cost: 8 c ---[1737]---> BDD-cost: 7 c ---[1736]---> BDD-cost: 7 c ---[1735]---> BDD-cost: 7 c ---[1734]---> BDD-cost: 7 c ---[1733]---> BDD-cost: 8 c ---[1732]---> BDD-cost: 9 c ---[1731]---> BDD-cost: 8 c ---[1730]---> BDD-cost: 8 c ---[1729]---> BDD-cost: 9 c ---[1728]---> BDD-cost: 8 c ---[1727]---> BDD-cost: 7 c ---[1726]---> BDD-cost: 8 c ---[1725]---> BDD-cost: 7 c ---[1724]---> BDD-cost: 7 c ---[1723]---> BDD-cost: 7 c ---[1722]---> BDD-cost: 7 c ---[1721]---> BDD-cost: 8 c ---[1720]---> BDD-cost: 9 c ---[1719]---> BDD-cost: 8 c ---[1718]---> BDD-cost: 8 c ---[1717]---> BDD-cost: 9 c ---[1716]---> BDD-cost: 8 c ---[1715]---> BDD-cost: 7 c ---[1714]---> BDD-cost: 8 c ---[1713]---> BDD-cost: 7 c ---[1712]---> BDD-cost: 7 c ---[1711]---> BDD-cost: 7 c ---[1710]---> BDD-cost: 7 c ---[1709]---> BDD-cost: 8 c ---[1708]---> BDD-cost: 9 c ---[1707]---> BDD-cost: 8 c ---[1706]---> BDD-cost: 8 c ---[1705]---> BDD-cost: 9 c ---[1704]---> BDD-cost: 8 c ---[1703]---> BDD-cost: 7 c ---[1702]---> BDD-cost: 8 c ---[1701]---> BDD-cost: 7 c ---[1700]---> BDD-cost: 7 c ---[1699]---> BDD-cost: 7 c ---[1698]---> BDD-cost: 7 c ---[1697]---> BDD-cost: 8 c ---[1696]---> BDD-cost: 9 c ---[1695]---> BDD-cost: 8 c ---[1694]---> BDD-cost: 8 c ---[1693]---> BDD-cost: 9 c ---[1692]---> BDD-cost: 8 c ---[1691]---> BDD-cost: 7 c ---[1690]---> BDD-cost: 8 c ---[1689]---> BDD-cost: 7 c ---[1688]---> BDD-cost: 7 c ---[1687]---> BDD-cost: 7 c ---[1686]---> BDD-cost: 7 c ---[1685]---> BDD-cost: 8 c ---[1684]---> BDD-cost: 9 c ---[1683]---> BDD-cost: 8 c ---[1682]---> BDD-cost: 8 c ---[1681]---> BDD-cost: 9 c ---[1680]---> BDD-cost: 8 c ---[1679]---> BDD-cost: 7 c ---[1678]---> BDD-cost: 8 c ---[1677]---> BDD-cost: 7 c ---[1676]---> BDD-cost: 7 c ---[1675]---> BDD-cost: 7 c ---[1674]---> BDD-cost: 7 c ---[1673]---> BDD-cost: 8 c ---[1672]---> BDD-cost: 9 c ---[1671]---> BDD-cost: 8 c ---[1670]---> BDD-cost: 8 c ---[1669]---> BDD-cost: 9 c ---[1668]---> BDD-cost: 8 c ---[1667]---> BDD-cost: 7 c ---[1666]---> BDD-cost: 8 c ---[1665]---> BDD-cost: 7 c ---[1664]---> BDD-cost: 7 c ---[1663]---> BDD-cost: 7 c ---[1662]---> BDD-cost: 7 c ---[1661]---> BDD-cost: 8 c ---[1660]---> BDD-cost: 9 c ---[1659]---> BDD-cost: 8 c ---[1658]---> BDD-cost: 8 c ---[1657]---> BDD-cost: 9 c ---[1656]---> BDD-cost: 8 c ---[1655]---> BDD-cost: 7 c ---[1654]---> BDD-cost: 8 c ---[1653]---> BDD-cost: 7 c ---[1652]---> BDD-cost: 7 c ---[1651]---> BDD-cost: 7 c ---[1650]---> BDD-cost: 7 c ---[1649]---> BDD-cost: 8 c ---[1648]---> BDD-cost: 9 c ---[1647]---> BDD-cost: 8 c ---[1646]---> BDD-cost: 8 c ---[1645]---> BDD-cost: 9 c ---[1644]---> BDD-cost: 8 c ---[1643]---> BDD-cost: 7 c ---[1642]---> BDD-cost: 8 c ---[1641]---> BDD-cost: 7 c ---[1640]---> BDD-cost: 7 c ---[1639]---> BDD-cost: 7 c ---[1638]---> BDD-cost: 7 c ---[1637]---> BDD-cost: 8 c ---[1636]--->
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/11857/stat): 11857 (minisat+_script) R 11856 11857 8263 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1797373659 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/11857/statm): 174 3 169 147 0 27 0 [pid=11857] 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=11858 New process pid=11859 New process pid=11860 execve syscall for /bin/sed executable One traced child (pid=11859) 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=11860) exited with status: 0 One traced child (pid=11858) exited with status: 0 New process pid=11861 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-gesa3.opb [startup+10.0043 s] Raw data (loadavg): 0.93 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 979 7 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221219520 134600301 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 9.87 Current children cumulated vsize (Kb) 7288 [startup+20.0052 s] Raw data (loadavg): 0.94 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 1978 8 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221219376 134783223 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 19.87 Current children cumulated vsize (Kb) 7288 [startup+30.007 s] Raw data (loadavg): 0.95 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 2978 8 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221219600 134677078 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 29.87 Current children cumulated vsize (Kb) 7288 [startup+40.0078 s] Raw data (loadavg): 0.96 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 3978 9 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221219400 134676609 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 39.88 Current children cumulated vsize (Kb) 7288 [startup+50.0087 s] Raw data (loadavg): 0.96 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 4978 9 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221219520 134677307 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 49.88 Current children cumulated vsize (Kb) 7288 [startup+60.0095 s] Raw data (loadavg): 0.97 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 5978 9 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 59.88 Current children cumulated vsize (Kb) 7288 [startup+70.0104 s] Raw data (loadavg): 0.97 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 6977 9 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220224 134677248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 69.87 Current children cumulated vsize (Kb) 7288 [startup+80.0122 s] Raw data (loadavg): 0.98 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 7977 10 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221219872 134676601 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 79.88 Current children cumulated vsize (Kb) 7288 [startup+90.013 s] Raw data (loadavg): 0.98 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 8977 10 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220024 134600694 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 89.88 Current children cumulated vsize (Kb) 7288 [startup+100.013 s] Raw data (loadavg): 0.98 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 9977 10 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221219168 134676539 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 99.88 Current children cumulated vsize (Kb) 7288 [startup+110.014 s] Raw data (loadavg): 0.98 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 10977 10 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220296 134677084 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 109.88 Current children cumulated vsize (Kb) 7288 [startup+120.015 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 11977 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221219792 134677021 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 119.89 Current children cumulated vsize (Kb) 7288 [startup+130.015 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 12977 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220376 134676989 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 129.89 Current children cumulated vsize (Kb) 7288 [startup+140.016 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 13977 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220296 134677084 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 139.89 Current children cumulated vsize (Kb) 7288 [startup+150.017 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 14977 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 149.89 Current children cumulated vsize (Kb) 7288 [startup+160.018 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 15977 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220144 134676376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 159.89 Current children cumulated vsize (Kb) 7288 [startup+170.019 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 16978 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220048 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 169.9 Current children cumulated vsize (Kb) 7288 [startup+180.021 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 17977 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220144 134676280 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 179.89 Current children cumulated vsize (Kb) 7288 [startup+190.021 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 18978 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 189.9 Current children cumulated vsize (Kb) 7288 [startup+200.022 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 19978 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220576 134676552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 199.9 Current children cumulated vsize (Kb) 7288 [startup+210.023 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 20978 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221221280 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 209.9 Current children cumulated vsize (Kb) 7288 [startup+220.024 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 21979 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220284 134676460 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 219.91 Current children cumulated vsize (Kb) 7288 [startup+230.026 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 22979 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 229.91 Current children cumulated vsize (Kb) 7288 [startup+240.027 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 23979 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 239.91 Current children cumulated vsize (Kb) 7288 [startup+250.028 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 24979 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221221608 134676241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 249.91 Current children cumulated vsize (Kb) 7288 [startup+260.028 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 25980 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221221632 134600314 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 259.92 Current children cumulated vsize (Kb) 7288 [startup+270.029 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 26980 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220480 134676328 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 269.92 Current children cumulated vsize (Kb) 7288 [startup+280.03 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 27980 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220284 134676610 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 279.92 Current children cumulated vsize (Kb) 7288 [startup+290.031 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 28979 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221221344 134677086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 289.91 Current children cumulated vsize (Kb) 7288 [startup+300.032 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 29979 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221219520 134676589 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 299.91 Current children cumulated vsize (Kb) 7288 [startup+310.033 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 30980 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221222128 134518669 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 309.92 Current children cumulated vsize (Kb) 7288 [startup+320.033 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 31980 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221221376 134676251 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 319.92 Current children cumulated vsize (Kb) 7288 [startup+330.034 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 32980 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220288 134677091 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 329.92 Current children cumulated vsize (Kb) 7288 [startup+340.035 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 33981 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220372 134676244 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 339.93 Current children cumulated vsize (Kb) 7288 [startup+350.036 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 34981 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220928 134676503 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 349.93 Current children cumulated vsize (Kb) 7288 [startup+360.038 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1255 0 0 0 35981 11 0 0 25 0 1 0 1797373663 5287936 1167 4294967295 134512640 135094434 3221224432 3221220848 134784993 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1291 1167 145 145 0 1146 0 [pid=11861] vsize: 5164 Current children cumulated CPU time (s) 359.93 Current children cumulated vsize (Kb) 7288 [startup+370.039 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 36981 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221219344 134600310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 369.93 Current children cumulated vsize (Kb) 7736 [startup+380.039 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 37982 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221219440 134676280 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 379.94 Current children cumulated vsize (Kb) 7736 [startup+390.04 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 38982 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220036 134600238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 389.94 Current children cumulated vsize (Kb) 7736 [startup+400.04 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 39982 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221219856 134600167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 399.94 Current children cumulated vsize (Kb) 7736 [startup+410.041 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 40982 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220400 134600267 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 409.94 Current children cumulated vsize (Kb) 7736 [startup+420.042 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 41982 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221219344 134600228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 419.94 Current children cumulated vsize (Kb) 7736 [startup+430.043 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 42983 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 429.95 Current children cumulated vsize (Kb) 7736 [startup+440.043 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 43983 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220400 134600344 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 439.95 Current children cumulated vsize (Kb) 7736 [startup+450.044 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 44983 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220216 134600155 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 449.95 Current children cumulated vsize (Kb) 7736 [startup+460.045 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 45983 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220204 134677150 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 459.95 Current children cumulated vsize (Kb) 7736 [startup+470.046 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 46984 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220048 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 469.96 Current children cumulated vsize (Kb) 7736 [startup+480.048 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 47984 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220640 134677086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 479.96 Current children cumulated vsize (Kb) 7736 [startup+490.049 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 48984 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 489.96 Current children cumulated vsize (Kb) 7736 [startup+500.05 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 49985 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220752 134600301 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 499.97 Current children cumulated vsize (Kb) 7736 [startup+510.05 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 50985 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220032 134600246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 509.97 Current children cumulated vsize (Kb) 7736 [startup+520.051 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 51985 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220732 134677150 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 519.97 Current children cumulated vsize (Kb) 7736 [startup+530.053 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 52985 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 529.97 Current children cumulated vsize (Kb) 7736 [startup+540.054 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 53985 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221219968 134677138 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 539.97 Current children cumulated vsize (Kb) 7736 [startup+550.054 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 54986 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220472 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 549.98 Current children cumulated vsize (Kb) 7736 [startup+560.056 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 55986 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221219344 134600277 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 559.98 Current children cumulated vsize (Kb) 7736 [startup+570.056 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 56986 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 569.98 Current children cumulated vsize (Kb) 7736 [startup+580.057 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 57987 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 579.99 Current children cumulated vsize (Kb) 7736 [startup+590.058 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 58987 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220048 134676601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 589.99 Current children cumulated vsize (Kb) 7736 [startup+600.059 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 59987 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220048 134600228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 599.99 Current children cumulated vsize (Kb) 7736 [startup+610.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 60987 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221221696 134677091 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 609.99 Current children cumulated vsize (Kb) 7736 [startup+620.061 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 61987 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220224 134599992 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 619.99 Current children cumulated vsize (Kb) 7736 [startup+630.06 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 62988 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 630 Current children cumulated vsize (Kb) 7736 [startup+640.061 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 63988 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221219696 134677346 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 640 Current children cumulated vsize (Kb) 7736 [startup+650.062 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 64988 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220400 134601168 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 650 Current children cumulated vsize (Kb) 7736 [startup+660.063 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 65988 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220724 134676992 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 660 Current children cumulated vsize (Kb) 7736 [startup+670.064 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 66989 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221219872 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 670.01 Current children cumulated vsize (Kb) 7736 [startup+680.065 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 67989 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221221280 134600274 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 680.01 Current children cumulated vsize (Kb) 7736 [startup+690.066 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 68989 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221221200 134676321 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 690.01 Current children cumulated vsize (Kb) 7736 [startup+700.065 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 69989 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221219668 134676992 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 700.01 Current children cumulated vsize (Kb) 7736 [startup+710.067 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 70990 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220400 134677248 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 710.02 Current children cumulated vsize (Kb) 7736 [startup+720.068 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 71990 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220812 134676460 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 720.02 Current children cumulated vsize (Kb) 7736 [startup+730.068 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1360 0 0 0 72990 11 0 0 25 0 1 0 1797373663 5746688 1272 4294967295 134512640 135094434 3221224432 3221220752 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1403 1272 145 145 0 1258 0 [pid=11861] vsize: 5612 Current children cumulated CPU time (s) 730.02 Current children cumulated vsize (Kb) 7736 [startup+740.069 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 73990 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 740.02 Current children cumulated vsize (Kb) 7740 [startup+750.068 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 74990 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221218816 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 750.02 Current children cumulated vsize (Kb) 7740 [startup+760.069 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 75991 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221218992 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 760.03 Current children cumulated vsize (Kb) 7740 [startup+770.07 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 76991 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220048 134676552 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 770.03 Current children cumulated vsize (Kb) 7740 [startup+780.07 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 77991 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221219872 134600301 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 780.03 Current children cumulated vsize (Kb) 7740 [startup+790.071 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 78991 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221219772 134676331 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 790.03 Current children cumulated vsize (Kb) 7740 [startup+800.072 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 79992 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221219696 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 800.04 Current children cumulated vsize (Kb) 7740 [startup+810.073 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 80992 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220480 134676328 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 810.04 Current children cumulated vsize (Kb) 7740 [startup+820.073 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 81992 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 820.04 Current children cumulated vsize (Kb) 7740 [startup+830.073 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 82992 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221219696 134677290 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 830.04 Current children cumulated vsize (Kb) 7740 [startup+840.074 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 83992 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220816 134676336 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 840.04 Current children cumulated vsize (Kb) 7740 [startup+850.074 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 84993 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 850.05 Current children cumulated vsize (Kb) 7740 [startup+860.075 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 85993 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220224 134676601 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 860.05 Current children cumulated vsize (Kb) 7740 [startup+870.076 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 86993 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 870.05 Current children cumulated vsize (Kb) 7740 [startup+880.075 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 87993 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221219968 134677099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 880.05 Current children cumulated vsize (Kb) 7740 [startup+890.076 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 88993 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220896 134518664 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 890.05 Current children cumulated vsize (Kb) 7740 [startup+900.077 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 89994 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221221280 134600310 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 900.06 Current children cumulated vsize (Kb) 7740 [startup+910.078 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 90994 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220672 134677035 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 910.06 Current children cumulated vsize (Kb) 7740 [startup+920.079 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 91994 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220224 134600175 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 920.06 Current children cumulated vsize (Kb) 7740 [startup+930.079 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 92994 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220320 134677065 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 930.06 Current children cumulated vsize (Kb) 7740 [startup+940.079 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 93995 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221221156 134676464 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 940.07 Current children cumulated vsize (Kb) 7740 [startup+950.08 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 94995 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221221104 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 950.07 Current children cumulated vsize (Kb) 7740 [startup+960.081 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 95995 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220400 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 960.07 Current children cumulated vsize (Kb) 7740 [startup+970.082 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 96995 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220224 134677284 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 970.07 Current children cumulated vsize (Kb) 7740 [startup+980.083 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 97996 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220028 134677150 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 980.08 Current children cumulated vsize (Kb) 7740 [startup+990.084 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 98996 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221221200 134677059 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 990.08 Current children cumulated vsize (Kb) 7740 [startup+1000.08 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 99996 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220256 134783376 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 1000.08 Current children cumulated vsize (Kb) 7740 [startup+1010.08 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 100996 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220824 134676334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 1010.08 Current children cumulated vsize (Kb) 7740 [startup+1020.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 101996 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220576 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 1020.08 Current children cumulated vsize (Kb) 7740 [startup+1030.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 102997 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221219756 134676460 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 1030.09 Current children cumulated vsize (Kb) 7740 [startup+1040.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 103997 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220752 134599924 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 1040.09 Current children cumulated vsize (Kb) 7740 [startup+1050.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 104997 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221221456 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 1050.09 Current children cumulated vsize (Kb) 7740 [startup+1060.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 105997 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220752 134677313 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 1060.09 Current children cumulated vsize (Kb) 7740 [startup+1070.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 106998 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221221200 134677099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 1070.1 Current children cumulated vsize (Kb) 7740 [startup+1080.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 107998 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220576 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 1080.1 Current children cumulated vsize (Kb) 7740 [startup+1090.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1365 0 0 0 108998 11 0 0 25 0 1 0 1797373663 5750784 1277 4294967295 134512640 135094434 3221224432 3221220452 134677232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1404 1277 145 145 0 1259 0 [pid=11861] vsize: 5616 Current children cumulated CPU time (s) 1090.1 Current children cumulated vsize (Kb) 7740 [startup+1100.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1376 0 0 0 109998 11 0 0 25 0 1 0 1797373663 5648384 1256 4294967295 134512640 135094434 3221224432 3221218816 134600311 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1379 1256 145 145 0 1234 0 [pid=11861] vsize: 5516 Current children cumulated CPU time (s) 1100.1 Current children cumulated vsize (Kb) 7640 [startup+1110.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1376 0 0 0 110998 11 0 0 25 0 1 0 1797373663 5648384 1256 4294967295 134512640 135094434 3221224432 3221218640 134677366 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1379 1256 145 145 0 1234 0 [pid=11861] vsize: 5516 Current children cumulated CPU time (s) 1110.1 Current children cumulated vsize (Kb) 7640 [startup+1120.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1376 0 0 0 111999 11 0 0 25 0 1 0 1797373663 5648384 1256 4294967295 134512640 135094434 3221224432 3221220048 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1379 1256 145 145 0 1234 0 [pid=11861] vsize: 5516 Current children cumulated CPU time (s) 1120.11 Current children cumulated vsize (Kb) 7640 [startup+1130.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1376 0 0 0 112999 11 0 0 25 0 1 0 1797373663 5648384 1256 4294967295 134512640 135094434 3221224432 3221219344 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1379 1256 145 145 0 1234 0 [pid=11861] vsize: 5516 Current children cumulated CPU time (s) 1130.11 Current children cumulated vsize (Kb) 7640 [startup+1140.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1376 0 0 0 113999 11 0 0 25 0 1 0 1797373663 5648384 1256 4294967295 134512640 135094434 3221224432 3221219756 134677378 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1379 1256 145 145 0 1234 0 [pid=11861] vsize: 5516 Current children cumulated CPU time (s) 1140.11 Current children cumulated vsize (Kb) 7640 [startup+1150.09 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1376 0 0 0 114999 11 0 0 25 0 1 0 1797373663 5648384 1256 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1379 1256 145 145 0 1234 0 [pid=11861] vsize: 5516 Current children cumulated CPU time (s) 1150.11 Current children cumulated vsize (Kb) 7640 [startup+1160.1 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1376 0 0 0 116000 11 0 0 25 0 1 0 1797373663 5648384 1256 4294967295 134512640 135094434 3221224432 3221219584 134676336 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1379 1256 145 145 0 1234 0 [pid=11861] vsize: 5516 Current children cumulated CPU time (s) 1160.12 Current children cumulated vsize (Kb) 7640 [startup+1170.1 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1376 0 0 0 117000 11 0 0 25 0 1 0 1797373663 5648384 1256 4294967295 134512640 135094434 3221224432 3221219872 134677307 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1379 1256 145 145 0 1234 0 [pid=11861] vsize: 5516 Current children cumulated CPU time (s) 1170.12 Current children cumulated vsize (Kb) 7640 [startup+1180.1 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1376 0 0 0 118000 11 0 0 25 0 1 0 1797373663 5648384 1256 4294967295 134512640 135094434 3221224432 3221220320 134677056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1379 1256 145 145 0 1234 0 [pid=11861] vsize: 5516 Current children cumulated CPU time (s) 1180.12 Current children cumulated vsize (Kb) 7640 [startup+1190.1 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1376 0 0 0 119000 11 0 0 25 0 1 0 1797373663 5648384 1256 4294967295 134512640 135094434 3221224432 3221220048 134600228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1379 1256 145 145 0 1234 0 [pid=11861] vsize: 5516 Current children cumulated CPU time (s) 1190.12 Current children cumulated vsize (Kb) 7640 [startup+1200.1 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1376 0 0 0 120001 11 0 0 25 0 1 0 1797373663 5648384 1256 4294967295 134512640 135094434 3221224432 3221219856 134600246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1379 1256 145 145 0 1234 0 [pid=11861] vsize: 5516 Current children cumulated CPU time (s) 1200.13 Current children cumulated vsize (Kb) 7640 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1200.1 s] Raw data (loadavg): 0.99 0.98 0.95 2/57 11861 Raw data (/proc/11857/stat): 11857 (minisat+_script) S 11856 11857 8263 0 -1 0 289 239 0 0 0 0 0 1 18 0 1 0 1797373659 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/11857/statm): 531 226 485 147 0 384 0 [pid=11857] vsize: 2124 Raw data (/proc/11861/stat): 11861 (minisat+_64-bit) R 11857 11857 8263 0 -1 0 1376 0 0 0 120001 11 0 0 25 0 1 0 1797373663 5648384 1256 4294967295 134512640 135094434 3221224432 3221219952 134677078 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/11861/statm): 1379 1256 145 145 0 1234 0 [pid=11861] vsize: 5516 Current children cumulated CPU time (s) 1200.13 Current children cumulated vsize (Kb) 7640 Sending SIGTERM to -11857 Sleeping 2 seconds One traced child (pid=11857) ended because it received signal 15 (SIGTERM) One traced child (pid=11861) exited with status: 0 All traced children have exited ! Game is over. Child status: 0 Real time (s): 1200.11 CPU time (s): 1200.14 CPU user time (s): 1200.01 CPU system time (s): 0.122981 CPU usage (%): 100.002 Max. virtual memory (cumulated for all children) (Kb): 7740
ERROR: no interpretation found !